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)

patch-coq-8.0pl2-ocaml-3.09 (818 bytes) - added by reilles@… 18 years ago.
patch for ocaml 3.09

Download all attachments as: .zip

Change History (5)

Changed 18 years ago by reilles@…

Attachment: patch-coq-8.0pl2-ocaml-3.09 added

patch for ocaml 3.09

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: newclosed

commited - thanks.

Note: See TracTickets for help on using tickets.