Coq is a theorem prover using the calculus of inductive constructions written in O'Caml. See attached ebuild for the latest version of Coq. Should go in dev-ml/ or app-sci/ maybe.
Created attachment 18781 [details] ebuild source
Just add EBUILD keyword
Hi Matthieu. Sorry for the delay - previous week was quite loaded on me. But I'll start going through your stuff. Could you please email me the list of the bugs you submitted? After last bauzilla change I ended up with ~100 open bugs, and not all the names in your submissions may be apparent.. So, getting back to the ebuild. I think it fits nicely into app-sci, but it may be herded under both sci and ml. Alternatively you can add yourself to the sci herd (when you get cvs access), with the remark that you are maintaining only certain applications (then ebuild only resides in the sci herd).. I haven't seen yet multiple-herd option being executed, but this was one of the points in the herd idea, so you may set the precendent ;). More stuff as I go.. 1. Naming: It is the policy to try to avoid upper-case in the names of ebuild if this doesn't cause terrible inconvenience. Besides in your case looks like you have to do some name-mangling, which would be unnecessary, should you just have called ebuild coq-... You might want refresh your stance on developer's policy ;), here: http://www.gentoo.org/doc/en/index.xml#doc_chap6 BTW, this should also help you with the quiz. 2. lintool complaints: Just had some white space on an empty line and more importantly - missing IUSE="". IUSE should list all the use flags ebuild makes use of. After screwing with the ideas on how to parse ebuilds for use flags employed no reliable way of parsing was found, so we have to help portage with a bit of manual work. Another point here is that it is usefull to run your ebuilds trough lintool (which is a separate emerge now). It isn't maintained anymore (and thus not required), but it is still usefull, as it catches eraly few trivial things. You might want to give it a try, just ignore warnings about missing RDEPEND (not the DEPEND!) and year in the header (it doesn't know about 2003 :)). 3. Since you do not have any conditionals to the ./configure parameters it is not necessary to define local myconf - you could have just passed these lines directly to configure. Also, econf might save a few lines, as you do not need to supplt "standsrt" definitions. Ok, the ebuild is still compiling, but I'll submit this part now, as I might need to run off shortly george
Hi Matthieu. Thanks for the list. but I'll go back here for the rest, as there seem to be problems with the package. >I found it more clean to have a $myconf and a simple ./configure $myconf >| die, but it's a matter of taste i think. Yea, this really is more a stilistic thing, although your taste seems to be a bit unusual, as this is pretty muchthe first time I see such wrapping ;). But the future need more than warrants it anywy, so don't worry too much. >I can't, the Coq configure is not a GNU one, its hand written and pretty >messy with its arguments. Yea, noticed that now, - yesterday I ran off even before ebuild started compiling.. However it does not finish on me, here are the last lines: ocamlc -I config -I tools -I scripts -I lib -I kernel -I library -I proofs -I tactics -I pretyping -I interp -I toplevel -I parsing -I contrib/omega -I contrib/romega -I contrib/ring -I contrib/xml -I contrib/extraction -I contrib/correctness -I contrib/interface -I contrib/fourier -I contrib/jprover -I contrib/cc -I /usr/lib/ocaml/camlp4 -c toplevel/metasyntax.ml The implementation parsing/pcoq.ml4 does not match the interface parsing/pcoq.cmi: Modules do not match: sig type te = Token.t and parsable = G.parsable val parsable : char Stream.t -> G.parsable val tokens : string -> (string * int) list module Entry : sig type 'a e = 'a Grammar.Make(L).Entry.e val create : string -> 'a e val parse : 'a e -> G.parsable -> 'a val parse_token : 'a e -> G.te Stream.t -> 'a val name : 'a e -> string val of_parser : string -> (G.te Stream.t -> 'a) -> 'a e val print : 'a e -> unit external obj : 'a e -> G.te Gramext.g_entry = "%identity" end module Unsafe : sig val gram_reinit : G.te Token.glexer -> unit val clear_entry : 'a G.Entry.e -> unit val reinit_gram : Token.lexer -> unit end val extend : 'a G.Entry.e -> Gramext.position option -> (string option * Gramext.g_assoc option * (G.te Gramext.g_symbol list * Gramext.g_action) list) list -> unit val delete_rule : 'a -> 'b -> 'c end is not included in sig type te = Token.t and parsable val parsable : char Stream.t -> parsable val tokens : string -> (string * int) list val glexer : te Token.glexer module Entry : sig type 'a e val create : string -> 'a e val parse : 'a e -> parsable -> 'a val parse_token : 'a e -> te Stream.t -> 'a val name : 'a e -> string val of_parser : string -> (te Stream.t -> 'a) -> 'a e val print : 'a e -> unit external obj : 'a e -> te Gramext.g_entry = "%identity" end module Unsafe : sig val gram_reinit : te Token.glexer -> unit val clear_entry : 'a Entry.e -> unit val reinit_gram : Token.lexer -> unit end val extend : 'a Entry.e -> Gramext.position option -> (string option * Gramext.g_assoc option * (te Gramext.g_symbol list * Gramext.g_action) list) list -> unit val delete_rule : 'a Entry.e -> te Gramext.g_symbol list -> unit end The field `glexer' is required but not provided make: *** [parsing/pcoq.cmo] Error 2 Relevant parts of emerge info on my side: Portage 2.0.49-r13 (default-x86-1.4, gcc-3.2.3, glibc-2.3.2-r1, 2.4.20-ck6) ================================================================= System uname: 2.4.20-ck6 i686 Pentium III (Coppermine) Gentoo Base System version 1.4.3.10p1 ccache version 2.3 [enabled] CFLAGS="-march=pentium3 -O2 -pipe -fforce-addr -fomit-frame-pointer -falign-functions=4 -mfpmath=sse" CHOST="i686-pc-linux-gnu" COMPILER="gcc3" George
Bug #24616 has Coq ebuilds too ! They look the same, except for the Real analysis USE flag. Could you attach your modified version george, or should i submit one ? The make error comes from the new version of the camlp4 Grammar module in ocaml-3.07. Correcting it just requires adding one line in parsing/pcoq.ml4, i attach the patch.
Created attachment 19307 [details, diff] ocaml-3.07 patch
Created attachment 19647 [details] the updated coq-7.4.ebuild Hi Matthieu Sorry for the delay, looks like bugzilla still likes to skip on intermittent notifications :( (or I just lost it in the pile of others). Anyway, here it goes. I would rather let you add the pacth yourself and try to move on to more of your submissions. One additional thing I just spotted - the string[s you put in LICENSE should precisely match one of the files under /usr/portage/licenses. We do not make much use of that right now, but eventually licenses are going to be enforced (that is this field is going to act as another way of "masking" according to what licenses user decided to accept). As such this field is already being checked.. George
*** Bug 24616 has been marked as a duplicate of this bug. ***
I commited app-sci/coq-7.4 ebuild commited, with ml and sci herds, and the patch for ocaml-3.07 applied if needed. It uses also the norealanalysis USE flag bug#24616 had.
