Date: Wed, 19 Mar 2008 20:28:17 GMT From: Anatoly Borodin <anatoly.borodin@gmail.com> To: freebsd-gnats-submit@FreeBSD.org Subject: ports/121879: math/coq doesn't build Message-ID: <200803192028.m2JKSHi6097073@www.freebsd.org> Resent-Message-ID: <200803192030.m2JKU1gj038167@freefall.freebsd.org>
next in thread | raw e-mail | index | archive | help
>Number: 121879
>Category: ports
>Synopsis: math/coq doesn't build
>Confidential: no
>Severity: serious
>Priority: medium
>Responsible: freebsd-ports-bugs
>State: open
>Quarter:
>Keywords:
>Date-Required:
>Class: sw-bug
>Submitter-Id: current-users
>Arrival-Date: Wed Mar 19 20:30:01 UTC 2008
>Closed-Date:
>Last-Modified:
>Originator: Anatoly Borodin
>Release: FreeBSD 7.0-STABLE
>Organization:
>Environment:
FreeBSD fractal.home 7.0-STABLE FreeBSD 7.0-STABLE #0: Mon Mar 17 15:09:39 EET 2008 anatoly.borodin@gmail.com:/usr/obj/usr/src/sys/GENERIC i386
>Description:
# cd /usr/ports/math/coq; make install
===> Extracting for coq-8.1.1
=> MD5 Checksum OK for coq-8.1pl1.tar.gz.
=> SHA256 Checksum OK for coq-8.1pl1.tar.gz.
===> Patching for coq-8.1.1
===> coq-8.1.1 depends on executable: ocamlc - found
===> coq-8.1.1 depends on executable: lablgtk2 - found
===> coq-8.1.1 depends on executable: gmake - found
===> Configuring for coq-8.1.1
You have Objective-Caml 3.09.3. Good!
You have native-code compilation. Good!
LablGtk2 found, native threads: native CoqIde will be available
Coq top directory : /usr/obj/usr/ports/math/coq/work/coq-8.1pl1
Architecture : FreeBSD
OS dependent libraries : -cclib -lunix
Objective-Caml/Camlp4 version : 3.09.3
Objective-Caml/Camlp4 binaries in : /usr/local/bin
Objective-Caml library in : /usr/local/lib/ocaml
Camlp4 library in : +camlp4
FSets theory : All
Reals theory : All
CoqIde : opt
Paths for true installation:
binaries will be copied in /usr/local/bin
library will be copied in /usr/local/lib/coq
man pages will be copied in /usr/local/man
emacs mode will be copied in /usr/local/share/emacs/site-lisp
If anything in the above is wrong, please restart './configure'
*Warning* To compile the system for a new architecture
don't forget to do a 'make archclean' before './configure'.
===> Building for coq-8.1.1
sed -n -e '/^ /s/ \([A-Z]\)/ \&\&coq_lbl_\1/gp' \
-e '/^}/q' kernel/byterun/coq_instruct.h > \
kernel/byterun/coq_jumptbl.h
sed -n -e '/^enum/p' -e 's/,//g' -e '/^ /p' \
kernel/byterun/coq_instruct.h | \
awk -f kernel/make-opcodes > kernel/copcodes.ml
ECHO... > scripts/tolink.ml
OCAMLLEX ide/config_lexer.mll
13 states, 332 transitions, table size 1406 bytes
OCAMLLEX ide/find_phrase.mll
15 states, 265 transitions, table size 1150 bytes
OCAMLLEX ide/highlight.mll
31 states, 3790 transitions, table size 15346 bytes
OCAMLYACC ide/config_parser.mly
OCAMLLEX ide/utf8_convert.mll
15 states, 827 transitions, table size 3398 bytes
OCAMLLEX tools/coqdep_lexer.mll
181 states, 5332 transitions, table size 22414 bytes
OCAMLC config/coq_config.mli
OCAMLC config/coq_config.ml
OCAMLC tools/coqdep_lexer.ml
OCAMLC tools/coqdep.ml
OCAMLC -o bin/coqdep
OCAMLLEX tools/gallina_lexer.mll
151 states, 498 transitions, table size 2898 bytes
OCAMLLEX tools/coqwc.mll
183 states, 833 transitions, table size 4430 bytes
OCAMLLEX tools/coqdoc/pretty.mll
1110 states, 11338 transitions, table size 52012 bytes
OCAMLLEX tools/coqdoc/index.mll
178 states, 5225 transitions, table size 21968 bytes
rm -f .depend.camlp4
for f in tactics/tauto.ml4 tactics/eqdecide.ml4 tactics/extraargs.ml4 tactics/extratactics.ml4 tactics/eauto.ml4 toplevel/whelp.ml4 tactics/hipattern.ml4 contrib/omega/g_omega.ml4 contrib/romega/g_romega.ml4 contrib/ring/g_quote.ml4 contrib/ring/g_ring.ml4 contrib/dp/g_dp.ml4 contrib/setoid_ring/newring.ml4 contrib/field/field.ml4 contrib/fourier/g_fourier.ml4 contrib/extraction/g_extraction.ml4 contrib/xml/xmlentries.ml4 contrib/jprover/jprover.ml4 contrib/cc/g_congruence.ml4 contrib/funind/tacinv.ml4 contrib/first-order/g_ground.ml4 contrib/subtac/g_subtac.ml4 contrib/subtac/g_eterm.ml4 contrib/rtauto/g_rtauto.ml4 contrib/recdef/recdef.ml4 contrib/funind/indfun_main.ml4 contrib/interface/debug_tac.ml4 contrib/interface/centaur.ml4 parsing/lexer.ml4 parsing/pcoq.ml4 parsing/q_util.ml4 parsing/q_coqast.ml4 parsing/g_prim.ml4 parsing/g_minicoq.ml4 parsing/g_vernac.ml4 parsing/g_proofs.ml4 parsing/g_xml.ml4 parsing/g_constr.ml4 parsing/g_tactic.ml4 parsing/g_ltac.ml4 parsing/
argextend.ml4 parsing/tacextend.ml4 parsing/vernacextend.ml4 parsing/q_constr.ml4 parsing/g_decl_mode.ml4 toplevel/mltop.ml4 lib/pp.ml4 lib/compat.ml4 contrib/xml/xml.ml4 contrib/xml/acic2Xml.ml4 contrib/xml/proofTree2Xml.ml4 contrib/interface/line_parser.ml4 tools/coq_makefile.ml4 tools/coq-tex.ml4; do \
printf "%s" `dirname $f`/`basename $f .ml4`".ml: " >> .depend.camlp4; \
echo `sed -n -e 's|^(\*.*camlp4deps: "\(.*\)".*\*)|\1|p' $f` >> .depend.camlp4; \
done
OCAMLC lib/pp_control.mli
OCAMLC lib/pp_control.ml
camlp4o -I . pa_extend.cmo pa_extend_m.cmo q_MLast.cmo pa_ifdef.cmo pr_o.cmo `sed -n -e 's|^(\*.*camlp4deps: "\(.*\)".*\*)|\1|p' lib/pp.ml4` -loc loc -impl lib/pp.ml4 > lib/pp.ml || rm -f lib/pp.ml
Error while loading "pa_extend.cmo": native-code program cannot do a dynamic load.
OCAMLC lib/pp.mli
OCAMLC lib/pp.ml
I/O error: lib/pp.ml: No such file or directory
gmake: *** [lib/pp.cmo] Error 2
*** Error code 2
Stop in /usr/ports/math/coq.
>How-To-Repeat:
>Fix:
>Release-Note:
>Audit-Trail:
>Unformatted:
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?200803192028.m2JKSHi6097073>