Bug 505472 – sci-mathematics/ssreflect-1.5 - The Ssreflect extension for the Coq Proof Assistant

• Status: UNCONFIRMED
• Product: Gentoo Linux

[Description Christian D. 2014-03-23 17:30:56 UTC]

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.

[Comment 1 Christian D. 2014-03-23 17:34:05 UTC]

Created attachment 373324 [details]
Emacs site file

[Comment 2 OGINO Masanori 2014-06-21 12:56:35 UTC]

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.)

[Comment 3 OGINO Masanori 2014-06-21 12:59:40 UTC]

(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.

[Comment 4 OGINO Masanori 2014-06-21 13:00:33 UTC]

(In reply to OGINO Masanori from comment #3)
> Ssreflect, sorry.) However, Ssreflect should also be updated when you
s/updated/rebuilt/, I'm sorry.