Bug 24616 – coq-7.4.ebuild (New Package)

• Status: RESOLVED DUPLICATE of bug 30388
• Product: Gentoo Linux

[Description Peter Lietz 2003-07-16 14:57:25 UTC]

Hello!

Please find attached coq-7.4.tgz containing coq-7.4.ebuild.

Coq is a widely used proof assistent developed at INRIA and written in
ocaml. Information can be found at http://coq.inria.fr/.

I suggest app-sci/coq.

Please have a closer look, as this is the first ebuild that I have submitted.
However, I assure that I have tested it and it works well for me.

Peter



Reproducible: Always
Steps to Reproduce:
1.
2.
3.

[Comment 1 Peter Lietz 2003-07-16 15:01:12 UTC]

Created attachment 14563 [details]
coq-7.4.ebuild

[Comment 2 Peter Lietz 2003-07-17 06:28:28 UTC]

There seems to be a bug in einfo: the output of einfo "\\\\" is not \\ but \. I have adapted the ebuild using keycodes. The adapted version of the original package is coq-7.4-r1.ebuild. In coq-7.4-r2.ebuild, a local USE variable controls the inclusion of an extensive mathematical library. The default is to include the library, which is why I called the variable 'norealanalysis'.

Both ebuilds have been used to install, use and deinstall the package several times without problems.

[Comment 3 Peter Lietz 2003-07-17 06:29:51 UTC]

Created attachment 14618 [details]
coq-7.4-r1.ebuild

[Comment 4 Peter Lietz 2003-07-17 06:30:53 UTC]

Created attachment 14619 [details]
coq-7.4-r2.ebuild

[Comment 5 Peter Lietz 2003-07-19 04:03:15 UTC]

Please do ignore my ignorant comment on einfo in comment #2 or else read bug report #24673.

[Comment 6 Matthieu Sozeau (RETIRED) 2004-01-21 15:44:45 UTC]

I just commited an ebuild for Coq in CVS.

*** This bug has been marked as a duplicate of 30388 ***