Summary: | sci-mathematics/ssreflect-1.5 - The Ssreflect extension for the Coq Proof Assistant | ||
---|---|---|---|
Product: | Gentoo Linux | Reporter: | Christian D. <ThyrusG> |
Component: | New packages | Assignee: | Default Assignee for New Packages <maintainer-wanted> |
Status: | UNCONFIRMED --- | ||
Severity: | enhancement | CC: | jauhien, sci-mathematics |
Priority: | Normal | Keywords: | EBUILD |
Version: | unspecified | ||
Hardware: | All | ||
OS: | Linux | ||
URL: | http://www.msr-inria.fr/projects/mathematical-components-2/ | ||
Whiteboard: | |||
Package list: | Runtime testing required: | --- | |
Bug Depends on: | |||
Bug Blocks: | 505496 | ||
Attachments: |
Proposed Ebuild
Emacs site file |
Description
Christian D.
2014-03-23 17:30:56 UTC
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. |