Opened 18 years ago
Closed 18 years ago
#6130 closed defect (fixed)
BUG: coq-8.0pl2
Reported by: | wss@… | Owned by: | reilles@… |
---|---|---|---|
Priority: | Normal | Milestone: | |
Component: | ports | Version: | 1.0 |
Keywords: | Cc: | pguyot (Paul Guyot), olegb@… | |
Port: |
Description
I cannot build coq 8.0pl2 using darwinports. I am currently using MacOS 10.4.3 and darwinports version 1.200. Attempting to build gives the following output:
---> Building coq with target world Error: Target com.apple.build returned: shell command "cd "/opt/local/var/db/dpo rts/build/_opt_local_var_db_dports_sources_rsync.rsync.darwinports.org_dpupdate_ dports_lang_coq/work/coq-8.0pl2" && make world" returned error 2 Command output: OCAMLOPT4 parsing/pcoq.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. File "parsing/pcoq.ml4", line 620, characters 4-18: Warning Y: unused variable l'. The implementation parsing/pcoq.ml4 does not match the interface parsing/pcoq.cmi: Values do not match:
val main_entry : ((Coqast.t -> Util.loc) * '_a) option Gram.Entry.e
is not included in
val main_entry : (Util.loc * Vernacexpr.vernac_expr) option Gram.Entry.e
make: * [parsing/pcoq.cmx] Error 2
Error: /opt/local/bin/port: Status 1 encountered during processing.
Attachments (1)
Change History (5)
Changed 18 years ago by reilles@…
Attachment: | patch-coq-8.0pl2-ocaml-3.09 added |
---|
comment:1 Changed 18 years ago by olegb@…
Cc: | olegb@… pguyot@… added |
---|
is this fixed ? seems ocaml has been bumped.
comment:2 Changed 18 years ago by reilles@…
(In reply to comment #2)
is this fixed ? seems ocaml has been bumped.
I don't think this make the patch obsolete. Anyway, coq has also been updated to 8.0pl3 (which probably is just pl2 with the patch for ocaml 3.09). I will try to package the latter soon
comment:3 Changed 18 years ago by reilles@…
(In reply to comment #3) I just checked coq-8.0pl3, and it compiles happyly with ocaml 3.09.1
There are also little changes, as for the installation path of the coqdoc.sty file, with is now in the same directory as coq.el
So,
-version 8.0pl2 +version 8.0pl3
and -master_sites ftp://ftp.inria.fr/INRIA/coq/V8.0pl2/ +master_sites ftp://ftp.inria.fr/INRIA/coq/V8.0pl3/
should fix the issue
comment:4 Changed 18 years ago by olegb@…
Resolution: | → fixed |
---|---|
Status: | new → closed |
commited - thanks.
patch for ocaml 3.09