Created attachment 373322 [details] Proposed Ebuild This is a proposed ebuild for the Ssreflect[1] extension to the Coq proof assistant (sci-mathematics/coq in Gentoo). It is licensed under the CeCILL-B license, the french equivalent of the BSD license [2]. [1] http://www.msr-inria.inria.fr/projects/mathematical-components-2/ [2] http://www.cecill.info/licences/Licence_CeCILL-B_V1-en.txt The ebuild works for me, but I'm not sure whether the way the syntax highlighting for ProofGeneral (the emacs mode for Coq) is installed is appropriate.
Created attachment 373324 [details] Emacs site file
I think ">=sci-mathematics/coq-8.4_p2:=[camlp5] <sci-mathematics/coq-8.5:=[camlp5]" is better. (I confirmed that Coq 8.4 and 8.4p1 fails to build Ssreflect 1.5. Also, blocking Coq 8.5 is probably correct.)
(In reply to OGINO Masanori from comment #2) > I think ">=sci-mathematics/coq-8.4_p2:=[camlp5] > <sci-mathematics/coq-8.5:=[camlp5]" is better. (I confirmed that Coq 8.4 and > 8.4p1 fails to build Ssreflect 1.5. Also, blocking Coq 8.5 is probably > correct.) Well, the ':=' is not necessary now. (I copied from my personal ebuild for Ssreflect, sorry.) However, Ssreflect should also be updated when you updated Coq, so adding a sub-slot to Coq is good IMHO.
(In reply to OGINO Masanori from comment #3) > Ssreflect, sorry.) However, Ssreflect should also be updated when you s/updated/rebuilt/, I'm sorry.