ports/121879: math/coq doesn't build

Anatoly Borodin anatoly.borodin at gmail.com
Wed Mar 19 20:30:02 UTC 2008

>Number:         121879
>Category:       ports
>Synopsis:       math/coq doesn't build
>Confidential:   no
>Severity:       serious
>Priority:       medium
>Responsible:    freebsd-ports-bugs
>State:          open
>Class:          sw-bug
>Submitter-Id:   current-users
>Arrival-Date:   Wed Mar 19 20:30:01 UTC 2008
>Originator:     Anatoly Borodin
>Release:        FreeBSD 7.0-STABLE
FreeBSD fractal.home 7.0-STABLE FreeBSD 7.0-STABLE #0: Mon Mar 17 15:09:39 EET 2008     anatoly.borodin at gmail.com:/usr/obj/usr/src/sys/GENERIC  i386

# 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 > \
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; \
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.




More information about the freebsd-ports-bugs mailing list