"This version comes with many improvements of existing features, especially regarding the tactics, the module system, extraction, the type classes, the program command, libraries, coqdoc. It also includes a new tactic ("nsatz", standing for Hilbert's NullStellensatz, that solves systems of polynomial equations in Z or R) and a few new libraries (a certification of mergesort, a new library of finite sets with computational and logical contents separated)." For a full log of changes, see URL
Created attachment 254245 [details] Proposed ebuild Mostly just a copy from the previous version. coq 8.3 doesn't have build options corresponding to not building the realanalysis package (previously USE flag norealanalysis). I have gotten this to work without having it build coqide (USE flags -gtk).
(In reply to comment #1) > Created an attachment (id=254245) [details] > Proposed ebuild Hi, I'm looking into this. Why do you depend on >=ocaml-3.12 ?
Have you seen anything like this: ---snip---- make[1]: Leaving directory `/var/tmp/portage/sci-mathematics/coq-8.3/work/coq-8.3' make[1]: Entering directory `/var/tmp/portage/sci-mathematics/coq-8.3/work/coq-8.3' Makefile.doc:188: warning: undefined variable `QUICK' OCAMLC config/coq_config.ml File "config/coq_config.ml", line 22, characters 17-22: Error: This expression has type string but an expression was expected of type int TOUCH lib/compat.ml CHECK revision OCAMLOPT config/coq_config.ml File "config/coq_config.ml", line 22, characters 17-22: Error: This expression has type string but an expression was expected of type int make[1]: *** [config/coq_config.cmx] Error 2 rm lib/compat.ml make[1]: Leaving directory `/var/tmp/portage/sci-mathematics/coq-8.3/work/coq-8.3' make: *** [world] Error 2 emake failed * ERROR: sci-mathematics/coq-8.3 failed: ----snap----
Created attachment 254367 [details] Don't depend on ocaml-3.12
I think that I did see this, but only when compiling coqide (USE flag gtk). I haven't gotten a chance to figure out what the problem is yet though. (In reply to comment #3) > Have you seen anything like this: > > ---snip---- > make[1]: Leaving directory > `/var/tmp/portage/sci-mathematics/coq-8.3/work/coq-8.3' > make[1]: Entering directory > `/var/tmp/portage/sci-mathematics/coq-8.3/work/coq-8.3' > Makefile.doc:188: warning: undefined variable `QUICK' > OCAMLC config/coq_config.ml > File "config/coq_config.ml", line 22, characters 17-22: > Error: This expression has type string but an expression was expected of type > int > TOUCH lib/compat.ml > CHECK revision > OCAMLOPT config/coq_config.ml > File "config/coq_config.ml", line 22, characters 17-22: > Error: This expression has type string but an expression was expected of type > int > make[1]: *** [config/coq_config.cmx] Error 2 > rm lib/compat.ml > make[1]: Leaving directory > `/var/tmp/portage/sci-mathematics/coq-8.3/work/coq-8.3' > make: *** [world] Error 2 > emake failed > * ERROR: sci-mathematics/coq-8.3 failed: > ----snap---- >
Done. Thanks everybody. Please test. @gmalachea: I appreciate your effort, however, I don't understand most of the changes you have done to the ebuild. Especially why you dropped RDEPEND and removed some DEPEND. Also your RESTRICT is not correct. Why should the binaries not be stripped? The mechanism in the last ebuild was to use STRIP="true" which replaces the strip program used by the program 'true' which does no\ thing (see 'man true'). Then all these ${P/_/} can just be ${P}. The build failed with coqide because they replaced ${libdir} by "${libdir}" somewhere in the configure script which would then lead to an assignment includeline="-I "${libdir}"" leading to failure. I've sent that upstream and they fixed it. Unfortunately I see runtime text relocations with plugins now, I have no idea how to fix this.
Ah, it seems that I used an outdated version of the ebuild as my template.
