presumably ocaml-related:
>>> Building on i386-2 under math/coq
BDEPENDS = [math/ocaml-zarith;lang/ocaml;sysutils/findlib;shells/bash;devel/gmake;x11/lablgtk3]
DIST = [math/coq:coq-8.13.2.tar.gz]
FULLPKGNAME = coq-8.13.2
RDEPENDS = [lang/ocaml;x11/lablgtk3]
(Junk lock obtained for i386-2 at 1638878332.14)
>>> Running depends in math/coq at 1638878332.15
last junk was in textproc/apertium-dicts/pt-gl
/usr/sbin/pkg_add -aI -Drepair bash-5.1.12 findlib-1.8.1p3 lablgtk3-3.1.1p2 ocaml-4.11.2p0 ocaml-zarith-1.11p0
was: /usr/sbin/pkg_add -aI -Drepair bash-5.1.12 findlib-1.8.1p3 gmake-4.3 lablgtk3-3.1.1p2 ocaml-4.11.2p0 ocaml-zarith-1.11p0
/usr/sbin/pkg_add -aI -Drepair bash-5.1.12 findlib-1.8.1p3 lablgtk3-3.1.1p2 ocaml-4.11.2p0 ocaml-zarith-1.11p0
>>> Running show-prepare-results in math/coq at 1638878336.42
===> math/coq
===> coq-8.13.2 depends on: lablgtk3-* -> lablgtk3-3.1.1p2
===> coq-8.13.2 depends on: ocaml-zarith-* -> ocaml-zarith-1.11p0
===> coq-8.13.2 depends on: bash-* -> bash-5.1.12
===> coq-8.13.2 depends on: findlib-* -> findlib-1.8.1p3
===> coq-8.13.2 depends on: ocaml-=4.11.2 -> ocaml-4.11.2p0
===> coq-8.13.2 depends on: gmake-* -> gmake-4.3
===> Verifying specs: atk-1.0 c cairo cairo-gobject fontconfig freetype gdk-3 gdk_pixbuf-2.0 gio-2.0 glib-2.0 gobject-2.0 gtk-3 gtksourceview-3.0 harfbuzz intl m pango-1.0 pangocairo-1.0 pthread z
===> found atk-1.0.21809.4 c.96.1 cairo.13.1 cairo-gobject.2.1 fontconfig.13.1 freetype.30.1 gdk-3.2201.1 gdk_pixbuf-2.0.3200.3 gio-2.0.4200.14 glib-2.0.4201.7 gobject-2.0.4200.14 gtk-3.2201.0 gtksourceview-3.0.3.5 harfbuzz.16.1 intl.7.0 m.10.1 pango-1.0.3801.3 pangocairo-1.0.3801.3 pthread.26.1 z.6.0
bash-5.1.12
findlib-1.8.1p3
gmake-4.3
lablgtk3-3.1.1p2
ocaml-4.11.2p0
ocaml-zarith-1.11p0
(Junk lock released for i386-2 at 1638878337.28)
distfiles size=6952855
>>> Running patch in math/coq at 1638878337.29
===> math/coq
===> Checking files for coq-8.13.2
`/mnt/distfiles/coq-8.13.2.tar.gz' is up to date.
>> (SHA256) coq-8.13.2.tar.gz: OK
===> Extracting for coq-8.13.2
===> Patching for coq-8.13.2
===> Applying OpenBSD patch patch-Makefile_ide
Hmm... Looks like a unified diff to me...
The text leading up to this was:
--------------------------
|$OpenBSD: patch-Makefile_ide,v 1.3 2020/07/16 02:50:08 daniel Exp $
|
|Index: Makefile.ide
|--- Makefile.ide.orig
|+++ Makefile.ide
--------------------------
Patching file Makefile.ide using Plan A...
Hunk #1 succeeded at 187.
done
===> Compiler link: clang -> /usr/bin/clang
===> Compiler link: clang++ -> /usr/bin/clang++
===> Compiler link: cc -> /usr/bin/cc
===> Compiler link: c++ -> /usr/bin/c++
>>> Running configure in math/coq at 1638878338.01
===> math/coq
===> Generating configure for coq-8.13.2
===> Configuring for coq-8.13.2
You have OCaml 4.11.2. Good!
You have OCamlfind 1.8.1. Good!
You have native-code compilation. Good!
You have the Zarith library 1.11 installed. Good!
LablGtk3 and LablGtkSourceView3 found (3.1.1), with native threads:
=> native CoqIde will be built.
Architecture : OpenBSD
Sys.os_type : Unix
Coq VM bytecode link flags : -dllib -lcoqrun -dllpath /usr/local/lib/ocaml/coq/kernel/byterun
Other bytecode link flags :
OCaml version : 4.11.2
OCaml binaries in : /usr/local/bin/
OCaml library in : /usr/local/lib/ocaml
OCaml flambda flags :
Native dynamic link support : true
Lablgtk3 library in : +lablgtk3-sourceview3
CoqIde : opt
Documentation : None
Web browser : firefox -remote "OpenURL(%s,new-tab)" || firefox %s &
Coq web site : http://coq.inria.fr/
Bytecode VM enabled : true
Native Compiler enabled : ondemand
Paths for true installation:
- the Coq binaries will be copied in /usr/local/bin
- the Coq library will be copied in /usr/local/lib/ocaml/coq
- the Coqide configuration files will be copied in /etc/xdg/coq
- the Coqide data files will be copied in /usr/local/share/coq
- the Coq man pages will be copied in /usr/local/man
- the Coq documentation will be copied in /usr/local/share/doc/coq
- the Coqdoc LaTeX files will be copied in /usr/local/share/texmf/tex/latex/misc
If anything is wrong above, please restart './configure'.
*Warning* To compile the system for a new architecture
don't forget to do a 'make clean' before './configure'.
>>> Running build in math/coq at 1638878338.96
===> math/coq
===> Building for coq-8.13.2
ulimit -Ss 8192 && cd /pobj/coq-8.13.2/coq-8.13.2 && env -i OCAMLFIND_DESTDIR=/pobj/coq-8.13.2/fake-i386/usr/local/lib/ocaml OCAMLFIND_COMMANDS="ocamldoc=ocamldoc.opt" PORTSDIR="/usr/ports" LIBTOOL="/usr/bin/libtool" PATH='/pobj/coq-8.13.2/bin:/usr/bin:/bin:/usr/sbin:/sbin:/usr/local/bin:/usr/X11R6/bin' PREFIX='/usr/local' LOCALBASE='/usr/local' X11BASE='/usr/X11R6' CFLAGS='-O2 -pipe' TRUEPREFIX='/usr/local' COQINSTALLPREFIX='' HOME='/coq-8.13.2_writes_to_HOME' PICFLAG="-fpic" BINGRP=bin BINOWN=root BINMODE=755 NONBINMODE=644 DIRMODE=755 INSTALL_STRIP=-s MANGRP=bin MANOWN=root MANMODE=644 BSD_INSTALL_PROGRAM="/pobj/coq-8.13.2/bin/install -s -m 755" BSD_INSTALL_SCRIPT="/pobj/coq-8.13.2/bin/install -m 755" BSD_INSTALL_DATA="/pobj/coq-8.13.2/bin/install -m 644" BSD_INSTALL_MAN="/pobj/coq-8.13.2/bin/install -m 644" BSD_INSTALL_PROGRAM_DIR="/pobj/coq-8.13.2/bin/install -d -m 755" BSD_INSTALL_SCRIPT_DIR="/pobj/coq-8.13.2/bin/install -d -m 755" BSD_INSTALL_DATA_DIR="/pobj/coq-8.13.2/bin/install -d -m 755" BSD_INSTALL_MAN_DIR="/pobj/coq-8.13.2/bin/install -d -m 755" gmake LIBTOOL="/usr/bin/libtool" SHARED_LIBS_LOG=/pobj/coq-8.13.2/coq-8.13.2/shared_libs.log -f Makefile world
rm -f
cp -a ".merlin.in" ".merlin"
cp -a "ide/.merlin.in" "ide/.merlin"
cp -a "kernel/.merlin.in" "kernel/.merlin"
cp -a "plugins/.merlin.in" "plugins/.merlin"
cp -a "test-suite/unit-tests/.merlin.in" "test-suite/unit-tests/.merlin"
cp -a "META.coq.in" "META.coq"
mkdir bin
gmake --warn-undefined-variable --no-builtin-rules -f Makefile.build world
gmake[1]: Entering directory '/pobj/coq-8.13.2/coq-8.13.2'
OCAMLC clib/segmenttree.mli
OCAMLOPT clib/segmenttree.ml
OCAMLC clib/segmenttree.ml
OCAMLC clib/unicodetable.ml
OCAMLOPT clib/unicodetable.ml
OCAMLC clib/unicode.mli
OCAMLOPT clib/unicode.ml
OCAMLC clib/unicode.ml
OCAMLC clib/minisys.ml
OCAMLOPT clib/minisys.ml
OCAMLC tools/coqdep_lexer.mli
OCAMLLEX tools/coqdep_lexer.mll
217 states, 2223 transitions, table size 10194 bytes
OCAMLOPT tools/coqdep_lexer.ml
OCAMLC tools/coqdep_common.mli
OCAMLOPT tools/coqdep_common.ml
OCAMLC tools/coqdep_boot.ml
OCAMLOPT tools/coqdep_boot.ml
OCAMLBEST -o bin/coqdep_boot
COQDEP VFILES
OCAMLC kernel/genOpcodeFiles.ml
WRITE kernel/byterun/coq_instruct.h
WRITE kernel/byterun/coq_jumptbl.h
CCDEP kernel/byterun/coq_values.c
CCDEP kernel/byterun/coq_memory.c
CCDEP kernel/byterun/coq_interp.c
CCDEP kernel/byterun/coq_float64.c
CCDEP kernel/byterun/coq_fix_code.c
OCAMLLEX tools/ocamllibdep.mll
14 states, 417 transitions, table size 1752 bytes
OCAMLC tools/ocamllibdep.ml
OCAMLOPT tools/ocamllibdep.ml
OCAMLBEST -o bin/ocamllibdep
OCAMLC coqpp/coqpp_ast.mli
OCAMLYACC coqpp/coqpp_parse.mly
gmake[1]: Circular coqpp/coqpp_parse.cmi <- coqpp/coqpp_parse.cmo dependency dropped.
OCAMLC coqpp/coqpp_parse.mli
OCAMLC coqpp/coqpp_parse.ml
OCAMLLEX coqpp/coqpp_lex.mll
240 states, 15992 transitions, table size 65408 bytes
OCAMLC coqpp/coqpp_lex.ml
OCAMLC -a bin/coqpp
mkdir -p gramlib/.pack
OCAMLLEX ide/coqide/config_lexer.mll
30 states, 1657 transitions, table size 6808 bytes
6052 additional bytes used for bindings
OCAMLLEX ide/coqide/coq_lex.mll
124 states, 1808 transitions, table size 7976 bytes
OCAMLLEX ide/coqide/protocol/xml_lexer.mll
80 states, 774 transitions, table size 3576 bytes
OCAMLLEX ide/coqide/utf8_convert.mll
15 states, 827 transitions, table size 3398 bytes
OCAMLLEX tools/coqdoc/cpretty.mll
2719 states, 8742 transitions, table size 51282 bytes
17643 additional bytes used for bindings
OCAMLLEX tools/coqwc.mll
244 states, 858 transitions, table size 4896 bytes
COQPP parsing/g_constr.mlg
COQPP parsing/g_prim.mlg
COQPP plugins/btauto/g_btauto.mlg
COQPP plugins/cc/g_congruence.mlg
COQPP plugins/derive/g_derive.mlg
COQPP plugins/extraction/g_extraction.mlg
COQPP plugins/firstorder/g_ground.mlg
COQPP plugins/funind/g_indfun.mlg
COQPP plugins/ltac/coretactics.mlg
COQPP plugins/ltac/extraargs.mlg
COQPP plugins/ltac/extratactics.mlg
COQPP plugins/ltac/g_auto.mlg
COQPP plugins/ltac/g_class.mlg
COQPP plugins/ltac/g_eqdecide.mlg
COQPP plugins/ltac/g_ltac.mlg
COQPP plugins/ltac/g_obligations.mlg
COQPP plugins/ltac/g_rewrite.mlg
COQPP plugins/ltac/g_tactic.mlg
COQPP plugins/ltac/profile_ltac_tactics.mlg
COQPP plugins/micromega/g_micromega.mlg
COQPP plugins/micromega/g_zify.mlg
COQPP plugins/nsatz/g_nsatz.mlg
COQPP plugins/omega/g_omega.mlg
COQPP plugins/ring/g_ring.mlg
COQPP plugins/rtauto/g_rtauto.mlg
COQPP plugins/ssr/ssrparser.mlg
COQPP plugins/ssr/ssrvernac.mlg
COQPP plugins/ssrmatching/g_ssrmatching.mlg
COQPP plugins/ssrsearch/g_search.mlg
COQPP plugins/syntax/g_number_string.mlg
COQPP toplevel/g_toplevel.mlg
COQPP vernac/g_proofs.mlg
COQPP vernac/g_vernac.mlg
COQPP user-contrib/Ltac2/g_ltac2.mlg
printf '# 1 "%s"\n' gramlib/ploc.ml > gramlib/.pack/gramlib__Ploc.ml
cat gramlib/ploc.ml >> gramlib/.pack/gramlib__Ploc.ml
printf '# 1 "%s"\n' gramlib/plexing.ml > gramlib/.pack/gramlib__Plexing.ml
cat gramlib/plexing.ml >> gramlib/.pack/gramlib__Plexing.ml
printf '# 1 "%s"\n' gramlib/gramext.ml > gramlib/.pack/gramlib__Gramext.ml
cat gramlib/gramext.ml >> gramlib/.pack/gramlib__Gramext.ml
printf '# 1 "%s"\n' gramlib/grammar.ml > gramlib/.pack/gramlib__Grammar.ml
cat gramlib/grammar.ml >> gramlib/.pack/gramlib__Grammar.ml
echo " \
module Ploc = Gramlib__Ploc \
module Plexing = Gramlib__Plexing \
module Gramext = Gramlib__Gramext \
module Grammar = Gramlib__Grammar" > gramlib/.pack/gramlib.ml
rm -f ide/coqide/coqide_os_specific.ml && cp ide/coqide/coqide_X11.ml.in ide/coqide/coqide_os_specific.ml && chmod a-w ide/coqide/coqide_os_specific.ml
WRITE kernel/vmopcodes.ml
rm -f kernel/uint63.ml && cp kernel/uint63_31.ml kernel/uint63.ml && chmod a-w kernel/uint63.ml
rm -f kernel/float64.ml && cp kernel/float64_31.ml kernel/float64.ml && chmod a-w kernel/float64.ml
printf '# 1 "%s"\n' gramlib/ploc.mli > gramlib/.pack/gramlib__Ploc.mli
cat gramlib/ploc.mli >> gramlib/.pack/gramlib__Ploc.mli
printf '# 1 "%s"\n' gramlib/plexing.mli > gramlib/.pack/gramlib__Plexing.mli
cat gramlib/plexing.mli >> gramlib/.pack/gramlib__Plexing.mli
printf '# 1 "%s"\n' gramlib/gramext.mli > gramlib/.pack/gramlib__Gramext.mli
cat gramlib/gramext.mli >> gramlib/.pack/gramlib__Gramext.mli
printf '# 1 "%s"\n' gramlib/grammar.mli > gramlib/.pack/gramlib__Grammar.mli
cat gramlib/grammar.mli >> gramlib/.pack/gramlib__Grammar.mli
OCAMLLIBDEP user-contrib/MLLIBFILES user-contrib/MLPACKFILES
OCAMLDEP user-contrib/MLFILES user-contrib/MLIFILES
OCAMLLIBDEP plugins/MLLIBFILES plugins/MLPACKFILES
OCAMLDEP plugins/MLFILES plugins/MLIFILES
OCAMLLIBDEP MLLIBFILES MLPACKFILES
OCAMLDEP MLFILES MLIFILES
OCAMLLIBDEP checker/MLLIBFILES checker/MLPACKFILES
OCAMLDEP checker/MLFILES checker/MLIFILES
gmake[1]: Circular coqpp/coqpp_parse.cmi <- coqpp/coqpp_parse.cmo dependency dropped.
OCAMLC config/coq_config.mli
OCAMLOPT config/coq_config.ml
OCAMLOPT -a -o config/config.cmxa
OCAMLC clib/cObj.mli
OCAMLOPT clib/cObj.ml
OCAMLC clib/cEphemeron.mli
OCAMLOPT clib/cEphemeron.ml
OCAMLC clib/cSig.mli
OCAMLC clib/cMap.mli
OCAMLOPT clib/cMap.ml
OCAMLC clib/int.mli
OCAMLOPT clib/int.ml
OCAMLC clib/hashset.mli
OCAMLOPT clib/hashset.ml
OCAMLC clib/hashcons.mli
OCAMLOPT clib/hashcons.ml
OCAMLC clib/orderedType.mli
OCAMLOPT clib/orderedType.ml
OCAMLC clib/cSet.mli
OCAMLOPT clib/cSet.ml
OCAMLC clib/cList.mli
OCAMLOPT clib/cList.ml
OCAMLC clib/cString.mli
OCAMLOPT clib/cString.ml
OCAMLC clib/range.mli
OCAMLOPT clib/range.ml
OCAMLC clib/hMap.mli
OCAMLOPT clib/hMap.ml
OCAMLC clib/cArray.mli
OCAMLOPT clib/cArray.ml
OCAMLC clib/option.mli
OCAMLOPT clib/option.ml
OCAMLC clib/cUnix.mli
OCAMLOPT clib/cUnix.ml
OCAMLC clib/cThread.mli
OCAMLOPT clib/cThread.ml
OCAMLC clib/trie.mli
OCAMLOPT clib/trie.ml
OCAMLC clib/predicate.mli
OCAMLOPT clib/predicate.ml
OCAMLC clib/heap.mli
OCAMLOPT clib/heap.ml
OCAMLC clib/unionfind.mli
OCAMLOPT clib/unionfind.ml
OCAMLC clib/dyn.mli
OCAMLOPT clib/dyn.ml
OCAMLC clib/store.mli
OCAMLOPT clib/store.ml
OCAMLC clib/exninfo.mli
OCAMLOPT clib/exninfo.ml
OCAMLC clib/iStream.mli
OCAMLOPT clib/iStream.ml
OCAMLC clib/terminal.mli
OCAMLOPT clib/terminal.ml
OCAMLC clib/monad.mli
OCAMLOPT clib/monad.ml
OCAMLC clib/diff2.mli
OCAMLOPT clib/diff2.ml
OCAMLOPT -a -o clib/clib.cmxa
OCAMLC lib/hook.mli
OCAMLOPT lib/hook.ml
OCAMLC lib/flags.mli
OCAMLOPT lib/flags.ml
OCAMLC lib/control.mli
OCAMLOPT lib/control.ml
OCAMLC lib/util.mli
OCAMLOPT lib/util.ml
OCAMLC lib/pp.mli
OCAMLOPT lib/pp.ml
OCAMLC lib/pp_diff.mli
OCAMLOPT lib/pp_diff.ml
OCAMLC lib/loc.mli
OCAMLOPT lib/loc.ml
OCAMLC lib/stateid.mli
OCAMLOPT lib/stateid.ml
OCAMLC lib/xml_datatype.mli
OCAMLC lib/feedback.mli
OCAMLOPT lib/feedback.ml
OCAMLC lib/cErrors.mli
OCAMLOPT lib/cErrors.ml
OCAMLC lib/cWarnings.mli
OCAMLOPT lib/cWarnings.ml
OCAMLC lib/acyclicGraph.mli
OCAMLOPT lib/acyclicGraph.ml
OCAMLC lib/rtree.mli
OCAMLOPT lib/rtree.ml
OCAMLC lib/system.mli
OCAMLOPT lib/system.ml
OCAMLC lib/objFile.mli
OCAMLOPT lib/objFile.ml
OCAMLC lib/explore.mli
OCAMLOPT lib/explore.ml
OCAMLC lib/cProfile.mli
OCAMLOPT lib/cProfile.ml
OCAMLC lib/future.mli
OCAMLOPT lib/future.ml
OCAMLC lib/spawn.mli
OCAMLOPT lib/spawn.ml
OCAMLC lib/cAst.mli
OCAMLOPT lib/cAst.ml
OCAMLC lib/dAst.mli
OCAMLOPT lib/dAst.ml
OCAMLC lib/genarg.mli
OCAMLOPT lib/genarg.ml
OCAMLC lib/remoteCounter.mli
OCAMLOPT lib/remoteCounter.ml
OCAMLC lib/aux_file.mli
OCAMLOPT lib/aux_file.ml
OCAMLC lib/envars.mli
OCAMLOPT lib/envars.ml
OCAMLC lib/coqProject_file.mli
OCAMLOPT lib/coqProject_file.ml
OCAMLOPT -a -o lib/lib.cmxa
OCAMLC kernel/names.mli
OCAMLOPT kernel/names.ml
OCAMLC kernel/transparentState.mli
OCAMLOPT kernel/transparentState.ml
OCAMLC kernel/uint63.mli
OCAMLOPT kernel/uint63.ml
OCAMLC kernel/parray.mli
OCAMLOPT kernel/parray.ml
OCAMLC kernel/float64_common.mli
OCAMLOPT kernel/float64_common.ml
OCAMLC kernel/float64.mli
OCAMLOPT kernel/float64.ml
OCAMLC kernel/univ.mli
OCAMLOPT kernel/univ.ml
OCAMLC kernel/uGraph.mli
OCAMLOPT kernel/uGraph.ml
OCAMLC kernel/esubst.mli
OCAMLOPT kernel/esubst.ml
OCAMLC kernel/sorts.mli
OCAMLOPT kernel/sorts.ml
OCAMLC kernel/evar.mli
OCAMLOPT kernel/evar.ml
OCAMLC kernel/context.mli
OCAMLOPT kernel/context.ml
OCAMLC kernel/constr.mli
OCAMLOPT kernel/constr.ml
OCAMLC kernel/vars.mli
OCAMLOPT kernel/vars.ml
OCAMLC kernel/term.mli
OCAMLOPT kernel/term.ml
OCAMLC kernel/cPrimitives.mli
OCAMLOPT kernel/cPrimitives.ml
OCAMLC kernel/retroknowledge.mli
OCAMLOPT kernel/retroknowledge.ml
OCAMLC kernel/mod_subst.mli
OCAMLOPT kernel/mod_subst.ml
OCAMLC kernel/vmvalues.mli
OCAMLOPT kernel/vmvalues.ml
OCAMLC kernel/vmbytecodes.mli
OCAMLOPT kernel/vmbytecodes.ml
OCAMLC kernel/vmopcodes.ml
OCAMLOPT kernel/vmopcodes.ml
OCAMLC kernel/vmemitcodes.mli
OCAMLOPT kernel/vmemitcodes.ml
OCAMLC kernel/opaqueproof.mli
OCAMLOPT kernel/opaqueproof.ml
OCAMLC kernel/conv_oracle.mli
OCAMLOPT kernel/conv_oracle.ml
OCAMLC kernel/declarations.ml
OCAMLOPT kernel/declarations.ml
OCAMLC kernel/entries.ml
OCAMLOPT kernel/entries.ml
OCAMLC kernel/nativevalues.mli
OCAMLOPT kernel/nativevalues.ml
OCAMLC kernel/declareops.mli
OCAMLOPT kernel/declareops.ml
OCAMLC kernel/environ.mli
OCAMLOPT kernel/environ.ml
OCAMLC kernel/primred.mli
OCAMLOPT kernel/primred.ml
OCAMLC kernel/cClosure.mli
OCAMLOPT kernel/cClosure.ml
OCAMLC kernel/relevanceops.mli
OCAMLOPT kernel/relevanceops.ml
OCAMLC kernel/reduction.mli
OCAMLOPT kernel/reduction.ml
OCAMLC kernel/vmlambda.mli
OCAMLOPT kernel/vmlambda.ml
OCAMLC kernel/nativelambda.mli
OCAMLOPT kernel/nativelambda.ml
OCAMLC kernel/vmbytegen.mli
OCAMLOPT kernel/vmbytegen.ml
OCAMLC kernel/nativecode.mli
OCAMLOPT kernel/nativecode.ml
OCAMLC kernel/nativelib.mli
OCAMLOPT kernel/nativelib.ml
OCAMLC kernel/vmsymtable.mli
OCAMLOPT kernel/vmsymtable.ml
OCAMLC kernel/vm.mli
OCAMLOPT kernel/vm.ml
OCAMLC kernel/vconv.mli
OCAMLOPT kernel/vconv.ml
OCAMLC kernel/nativeconv.mli
OCAMLOPT kernel/nativeconv.ml
OCAMLC kernel/type_errors.mli
OCAMLOPT kernel/type_errors.ml
OCAMLC kernel/modops.mli
OCAMLOPT kernel/modops.ml
OCAMLC kernel/inductive.mli
OCAMLOPT kernel/inductive.ml
OCAMLC kernel/typeops.mli
OCAMLOPT kernel/typeops.ml
OCAMLC kernel/inferCumulativity.mli
OCAMLOPT kernel/inferCumulativity.ml
OCAMLC kernel/indTyping.mli
OCAMLOPT kernel/indTyping.ml
OCAMLC kernel/indtypes.mli
OCAMLOPT kernel/indtypes.ml
OCAMLC kernel/cooking.mli
OCAMLOPT kernel/cooking.ml
OCAMLC kernel/term_typing.mli
OCAMLOPT kernel/term_typing.ml
OCAMLC kernel/subtyping.mli
OCAMLOPT kernel/subtyping.ml
OCAMLC kernel/mod_typing.mli
OCAMLOPT kernel/mod_typing.ml
OCAMLC kernel/nativelibrary.mli
OCAMLOPT kernel/nativelibrary.ml
OCAMLC kernel/section.mli
OCAMLOPT kernel/section.ml
OCAMLC kernel/safe_typing.mli
OCAMLOPT kernel/safe_typing.ml
OCAMLOPT -a -o kernel/kernel.cmxa
OCAMLC library/libnames.mli
OCAMLOPT library/libnames.ml
OCAMLC library/globnames.mli
OCAMLOPT library/globnames.ml
OCAMLC library/libobject.mli
OCAMLOPT library/libobject.ml
OCAMLC library/summary.mli
OCAMLOPT library/summary.ml
OCAMLC library/nametab.mli
OCAMLOPT library/nametab.ml
OCAMLC library/global.mli
OCAMLOPT library/global.ml
OCAMLC library/lib.mli
OCAMLOPT library/lib.ml
OCAMLC library/goptions.mli
OCAMLOPT library/goptions.ml
OCAMLC library/coqlib.mli
OCAMLOPT library/coqlib.ml
OCAMLOPT -a -o library/library.cmxa
OCAMLC engine/univNames.mli
OCAMLOPT engine/univNames.ml
OCAMLC engine/univGen.mli
OCAMLOPT engine/univGen.ml
OCAMLC engine/univSubst.mli
OCAMLOPT engine/univSubst.ml
OCAMLC engine/univProblem.mli
OCAMLOPT engine/univProblem.ml
OCAMLC engine/univMinim.mli
OCAMLOPT engine/univMinim.ml
OCAMLC engine/uState.mli
OCAMLOPT engine/uState.ml
OCAMLC engine/univops.mli
OCAMLOPT engine/univops.ml
OCAMLC engine/nameops.mli
OCAMLOPT engine/nameops.ml
OCAMLC engine/evar_kinds.mli
OCAMLOPT engine/evar_kinds.ml
OCAMLC engine/evd.mli
OCAMLOPT engine/evd.ml
OCAMLC engine/eConstr.mli
OCAMLOPT engine/eConstr.ml
OCAMLC engine/namegen.mli
OCAMLOPT engine/namegen.ml
OCAMLC engine/termops.mli
OCAMLOPT engine/termops.ml
OCAMLC engine/evarutil.mli
OCAMLOPT engine/evarutil.ml
OCAMLC engine/logic_monad.mli
OCAMLOPT engine/logic_monad.ml
OCAMLC engine/proofview_monad.mli
OCAMLOPT engine/proofview_monad.ml
OCAMLC engine/proofview.mli
OCAMLOPT engine/proofview.ml
OCAMLC engine/ftactic.mli
OCAMLOPT engine/ftactic.ml
OCAMLOPT -a -o engine/engine.cmxa
OCAMLC pretyping/geninterp.mli
OCAMLOPT pretyping/geninterp.ml
OCAMLC pretyping/locus.ml
OCAMLOPT pretyping/locus.ml
OCAMLC pretyping/locusops.mli
OCAMLOPT pretyping/locusops.ml
OCAMLC pretyping/reductionops.mli
OCAMLOPT pretyping/reductionops.ml
OCAMLC pretyping/pretype_errors.mli
OCAMLOPT pretyping/pretype_errors.ml
OCAMLC pretyping/inductiveops.mli
OCAMLOPT pretyping/inductiveops.ml
OCAMLC pretyping/arguments_renaming.mli
OCAMLOPT pretyping/arguments_renaming.ml
OCAMLC pretyping/retyping.mli
OCAMLOPT pretyping/retyping.ml
OCAMLC pretyping/vnorm.mli
OCAMLOPT pretyping/vnorm.ml
OCAMLC pretyping/nativenorm.mli
OCAMLOPT pretyping/nativenorm.ml
OCAMLC pretyping/cbv.mli
OCAMLOPT pretyping/cbv.ml
OCAMLC pretyping/find_subterm.mli
OCAMLOPT pretyping/find_subterm.ml
OCAMLC pretyping/evardefine.mli
OCAMLOPT pretyping/evardefine.ml
OCAMLC pretyping/evarsolve.mli
OCAMLOPT pretyping/evarsolve.ml
OCAMLC pretyping/recordops.mli
OCAMLOPT pretyping/recordops.ml
OCAMLC pretyping/heads.mli
OCAMLOPT pretyping/heads.ml
OCAMLC pretyping/evarconv.mli
OCAMLOPT pretyping/evarconv.ml
OCAMLC pretyping/typing.mli
OCAMLOPT pretyping/typing.ml
OCAMLC pretyping/glob_term.ml
OCAMLOPT pretyping/glob_term.ml
OCAMLC pretyping/ltac_pretype.ml
OCAMLOPT pretyping/ltac_pretype.ml
OCAMLC pretyping/glob_ops.mli
OCAMLOPT pretyping/glob_ops.ml
OCAMLC pretyping/pattern.ml
OCAMLOPT pretyping/pattern.ml
OCAMLC pretyping/patternops.mli
OCAMLOPT pretyping/patternops.ml
OCAMLC pretyping/constr_matching.mli
OCAMLOPT pretyping/constr_matching.ml
OCAMLC pretyping/tacred.mli
OCAMLOPT pretyping/tacred.ml
OCAMLC pretyping/typeclasses_errors.mli
OCAMLOPT pretyping/typeclasses_errors.ml
OCAMLC pretyping/typeclasses.mli
OCAMLOPT pretyping/typeclasses.ml
OCAMLC pretyping/coercionops.mli
OCAMLOPT pretyping/coercionops.ml
OCAMLC pretyping/program.mli
OCAMLOPT pretyping/program.ml
OCAMLC pretyping/coercion.mli
OCAMLOPT pretyping/coercion.ml
OCAMLC pretyping/detyping.mli
OCAMLOPT pretyping/detyping.ml
OCAMLC pretyping/indrec.mli
OCAMLOPT pretyping/indrec.ml
OCAMLC pretyping/globEnv.mli
OCAMLOPT pretyping/globEnv.ml
OCAMLC pretyping/cases.mli
OCAMLOPT pretyping/cases.ml
OCAMLC pretyping/pretyping.mli
OCAMLOPT pretyping/pretyping.ml
OCAMLC pretyping/keys.mli
OCAMLOPT pretyping/keys.ml
OCAMLC pretyping/unification.mli
OCAMLOPT pretyping/unification.ml
OCAMLOPT -a -o pretyping/pretyping.cmxa
OCAMLC interp/deprecation.mli
OCAMLOPT interp/deprecation.ml
OCAMLC interp/numTok.mli
OCAMLOPT interp/numTok.ml
OCAMLC interp/constrexpr.ml
OCAMLOPT interp/constrexpr.ml
OCAMLC proofs/tactypes.ml
OCAMLOPT proofs/tactypes.ml
OCAMLC interp/notation_term.ml
OCAMLC interp/genintern.mli
OCAMLC interp/stdarg.mli
OCAMLOPT interp/stdarg.ml
OCAMLOPT interp/notation_term.ml
OCAMLOPT interp/genintern.ml
OCAMLC interp/notation_ops.mli
OCAMLOPT interp/notation_ops.ml
OCAMLC interp/notation.mli
OCAMLOPT interp/notation.ml
OCAMLC interp/syntax_def.mli
OCAMLOPT interp/syntax_def.ml
OCAMLC interp/smartlocate.mli
OCAMLOPT interp/smartlocate.ml
OCAMLC interp/constrexpr_ops.mli
OCAMLOPT interp/constrexpr_ops.ml
OCAMLC interp/decls.mli
OCAMLOPT interp/decls.ml
OCAMLC interp/dumpglob.mli
OCAMLOPT interp/dumpglob.ml
OCAMLC interp/reserve.mli
OCAMLOPT interp/reserve.ml
OCAMLC interp/impargs.mli
OCAMLOPT interp/impargs.ml
OCAMLC interp/implicit_quantifiers.mli
OCAMLOPT interp/implicit_quantifiers.ml
OCAMLC interp/constrintern.mli
OCAMLOPT interp/constrintern.ml
OCAMLC interp/modintern.mli
OCAMLOPT interp/modintern.ml
OCAMLC interp/constrextern.mli
OCAMLOPT interp/constrextern.ml
OCAMLOPT -a -o interp/interp.cmxa
OCAMLC proofs/miscprint.mli
OCAMLOPT proofs/miscprint.ml
OCAMLC proofs/goal.mli
OCAMLOPT proofs/goal.ml
OCAMLC proofs/evar_refiner.mli
OCAMLOPT proofs/evar_refiner.ml
OCAMLC proofs/refine.mli
OCAMLOPT proofs/refine.ml
OCAMLC proofs/goal_select.mli
OCAMLOPT proofs/goal_select.ml
OCAMLC proofs/proof.mli
OCAMLOPT proofs/proof.ml
OCAMLC proofs/logic.mli
OCAMLOPT proofs/logic.ml
OCAMLC proofs/proof_bullet.mli
OCAMLOPT proofs/proof_bullet.ml
OCAMLC proofs/tacmach.mli
OCAMLOPT proofs/tacmach.ml
OCAMLC proofs/clenv.mli
OCAMLOPT proofs/clenv.ml
OCAMLOPT -a -o proofs/proofs.cmxa
OCAMLC gramlib/.pack/gramlib.ml
OCAMLOPT gramlib/.pack/gramlib.ml
OCAMLC gramlib/.pack/gramlib__Ploc.mli
OCAMLOPT gramlib/.pack/gramlib__Ploc.ml
OCAMLC gramlib/.pack/gramlib__Plexing.mli
OCAMLOPT gramlib/.pack/gramlib__Plexing.ml
OCAMLC gramlib/.pack/gramlib__Gramext.mli
OCAMLOPT gramlib/.pack/gramlib__Gramext.ml
OCAMLC gramlib/.pack/gramlib__Grammar.mli
OCAMLOPT gramlib/.pack/gramlib__Grammar.ml
OCAMLOPT -a -o gramlib/.pack/gramlib.cmxa
OCAMLC parsing/tok.mli
OCAMLOPT parsing/tok.ml
OCAMLC parsing/cLexer.mli
OCAMLOPT parsing/cLexer.ml
OCAMLC parsing/extend.mli
OCAMLOPT parsing/extend.ml
OCAMLC parsing/notation_gram.ml
OCAMLOPT parsing/notation_gram.ml
OCAMLC parsing/notgram_ops.mli
OCAMLOPT parsing/notgram_ops.ml
OCAMLC parsing/ppextend.mli
OCAMLOPT parsing/ppextend.ml
OCAMLC parsing/pcoq.mli
OCAMLOPT parsing/pcoq.ml
OCAMLC parsing/g_constr.ml
OCAMLOPT parsing/g_constr.ml
OCAMLC parsing/g_prim.ml
OCAMLOPT parsing/g_prim.ml
OCAMLOPT -a -o parsing/parsing.cmxa
OCAMLC printing/genprint.mli
OCAMLOPT printing/genprint.ml
OCAMLC printing/pputils.mli
OCAMLOPT printing/pputils.ml
OCAMLC printing/ppconstr.mli
OCAMLOPT printing/ppconstr.ml
OCAMLC printing/proof_diffs.mli
OCAMLOPT printing/proof_diffs.ml
OCAMLC printing/printer.mli
OCAMLOPT printing/printer.ml
OCAMLOPT -a -o printing/printing.cmxa
OCAMLC tactics/declareScheme.mli
OCAMLOPT tactics/declareScheme.ml
OCAMLC tactics/dnet.mli
OCAMLOPT tactics/dnet.ml
OCAMLC tactics/dn.mli
OCAMLOPT tactics/dn.ml
OCAMLC tactics/btermdn.mli
OCAMLOPT tactics/btermdn.ml
OCAMLC tactics/tacticals.mli
OCAMLOPT tactics/tacticals.ml
OCAMLC tactics/hipattern.mli
OCAMLOPT tactics/hipattern.ml
OCAMLC tactics/ind_tables.mli
OCAMLOPT tactics/ind_tables.ml
OCAMLC tactics/eqschemes.mli
OCAMLOPT tactics/eqschemes.ml
OCAMLC tactics/elimschemes.mli
OCAMLOPT tactics/elimschemes.ml
OCAMLC tactics/genredexpr.ml
OCAMLOPT tactics/genredexpr.ml
OCAMLC tactics/redops.mli
OCAMLOPT tactics/redops.ml
OCAMLC tactics/cbn.mli
OCAMLOPT tactics/cbn.ml
OCAMLC tactics/redexpr.mli
OCAMLOPT tactics/redexpr.ml
OCAMLC tactics/ppred.mli
OCAMLOPT tactics/ppred.ml
OCAMLC tactics/tactics.mli
OCAMLOPT tactics/tactics.ml
OCAMLC tactics/abstract.mli
OCAMLOPT tactics/abstract.ml
OCAMLC tactics/elim.mli
OCAMLOPT tactics/elim.ml
OCAMLC tactics/equality.mli
OCAMLOPT tactics/equality.ml
OCAMLC tactics/contradiction.mli
OCAMLOPT tactics/contradiction.ml
OCAMLC tactics/inv.mli
OCAMLOPT tactics/inv.ml
OCAMLC tactics/declareUctx.mli
OCAMLOPT tactics/declareUctx.ml
OCAMLC tactics/hints.mli
OCAMLOPT tactics/hints.ml
OCAMLC tactics/auto.mli
OCAMLOPT tactics/auto.ml
OCAMLC tactics/eauto.mli
OCAMLOPT tactics/eauto.ml
OCAMLC tactics/class_tactics.mli
OCAMLOPT tactics/class_tactics.ml
OCAMLC tactics/term_dnet.mli
OCAMLOPT tactics/term_dnet.ml
OCAMLC tactics/eqdecide.mli
OCAMLOPT tactics/eqdecide.ml
OCAMLC tactics/autorewrite.mli
OCAMLOPT tactics/autorewrite.ml
OCAMLOPT -a -o tactics/tactics.cmxa
OCAMLC vernac/declaremods.mli
OCAMLOPT vernac/declaremods.ml
OCAMLC vernac/attributes.mli
OCAMLOPT vernac/attributes.ml
OCAMLC vernac/vernacexpr.ml
OCAMLOPT vernac/vernacexpr.ml
OCAMLC vernac/pvernac.mli
OCAMLOPT vernac/pvernac.ml
OCAMLC vernac/g_vernac.ml
OCAMLOPT vernac/g_vernac.ml
OCAMLC vernac/g_proofs.ml
OCAMLOPT vernac/g_proofs.ml
OCAMLC vernac/vernacprop.mli
OCAMLOPT vernac/vernacprop.ml
OCAMLC vernac/himsg.mli
OCAMLOPT vernac/himsg.ml
OCAMLC vernac/locality.mli
OCAMLOPT vernac/locality.ml
OCAMLC vernac/egramml.mli
OCAMLOPT vernac/egramml.ml
OCAMLC vernac/retrieveObl.mli
OCAMLOPT vernac/retrieveObl.ml
OCAMLC vernac/ppvernac.mli
OCAMLOPT vernac/ppvernac.ml
OCAMLC vernac/proof_using.mli
OCAMLOPT vernac/proof_using.ml
OCAMLC vernac/egramcoq.mli
OCAMLOPT vernac/egramcoq.ml
OCAMLC vernac/metasyntax.mli
OCAMLOPT vernac/metasyntax.ml
OCAMLC vernac/declareUniv.mli
OCAMLOPT vernac/declareUniv.ml
OCAMLC vernac/declare.mli
OCAMLOPT vernac/declare.ml
OCAMLC vernac/vernacextend.mli
OCAMLOPT vernac/vernacextend.ml
OCAMLC vernac/comHints.mli
OCAMLOPT vernac/comHints.ml
OCAMLC vernac/canonical.mli
OCAMLOPT vernac/canonical.ml
OCAMLC vernac/recLemmas.mli
OCAMLOPT vernac/recLemmas.ml
OCAMLC vernac/library.mli
OCAMLOPT vernac/library.ml
OCAMLC vernac/comCoercion.mli
OCAMLOPT vernac/comCoercion.ml
OCAMLC vernac/auto_ind_decl.mli
OCAMLOPT vernac/auto_ind_decl.ml
OCAMLC vernac/indschemes.mli
OCAMLOPT vernac/indschemes.ml
OCAMLC vernac/comDefinition.mli
OCAMLOPT vernac/comDefinition.ml
OCAMLC vernac/classes.mli
OCAMLOPT vernac/classes.ml
OCAMLC vernac/comPrimitive.mli
OCAMLOPT vernac/comPrimitive.ml
OCAMLC vernac/comAssumption.mli
OCAMLOPT vernac/comAssumption.ml
OCAMLC vernac/declareInd.mli
OCAMLOPT vernac/declareInd.ml
OCAMLC vernac/search.mli
OCAMLOPT vernac/search.ml
OCAMLC vernac/comSearch.mli
OCAMLOPT vernac/comSearch.ml
OCAMLC vernac/comInductive.mli
OCAMLOPT vernac/comInductive.ml
OCAMLC vernac/comFixpoint.mli
OCAMLOPT vernac/comFixpoint.ml
OCAMLC vernac/comProgramFixpoint.mli
OCAMLOPT vernac/comProgramFixpoint.ml
OCAMLC vernac/vernacstate.mli
OCAMLOPT vernac/vernacstate.ml
OCAMLC vernac/printmod.mli
OCAMLOPT vernac/printmod.ml
OCAMLC vernac/prettyp.mli
OCAMLOPT vernac/prettyp.ml
OCAMLC vernac/record.mli
OCAMLOPT vernac/record.ml
OCAMLC vernac/assumptions.mli
OCAMLOPT vernac/assumptions.ml
OCAMLC vernac/mltop.mli
OCAMLOPT vernac/mltop.ml
OCAMLC vernac/topfmt.mli
OCAMLOPT vernac/topfmt.ml
OCAMLC vernac/loadpath.mli
OCAMLOPT vernac/loadpath.ml
OCAMLC vernac/comArguments.mli
OCAMLOPT vernac/comArguments.ml
OCAMLC vernac/vernacentries.mli
OCAMLOPT vernac/vernacentries.ml
OCAMLC vernac/comTactic.mli
OCAMLOPT vernac/comTactic.ml
OCAMLC vernac/vernacinterp.mli
OCAMLOPT vernac/vernacinterp.ml
OCAMLOPT -a -o vernac/vernac.cmxa
OCAMLC stm/spawned.mli
OCAMLOPT stm/spawned.ml
OCAMLC stm/dag.mli
OCAMLOPT stm/dag.ml
OCAMLC stm/vcs.mli
OCAMLOPT stm/vcs.ml
OCAMLC stm/tQueue.mli
OCAMLOPT stm/tQueue.ml
OCAMLC stm/coqworkmgrApi.mli
OCAMLOPT stm/coqworkmgrApi.ml
OCAMLC stm/workerPool.mli
OCAMLOPT stm/workerPool.ml
OCAMLC stm/vernac_classifier.mli
OCAMLOPT stm/vernac_classifier.ml
OCAMLC stm/asyncTaskQueue.mli
OCAMLOPT stm/asyncTaskQueue.ml
OCAMLC stm/partac.mli
OCAMLOPT stm/partac.ml
OCAMLC stm/stm.mli
OCAMLOPT stm/stm.ml
OCAMLC stm/proofBlockDelimiter.mli
OCAMLOPT stm/proofBlockDelimiter.ml
OCAMLC stm/vio_checking.mli
OCAMLOPT stm/vio_checking.ml
OCAMLOPT -a -o stm/stm.cmxa
OCAMLC toplevel/vernac.mli
OCAMLOPT toplevel/vernac.ml
OCAMLC toplevel/usage.mli
OCAMLOPT toplevel/usage.ml
OCAMLC toplevel/coqinit.mli
OCAMLOPT toplevel/coqinit.ml
OCAMLC toplevel/coqargs.mli
OCAMLOPT toplevel/coqargs.ml
OCAMLC toplevel/coqcargs.mli
OCAMLOPT toplevel/coqcargs.ml
OCAMLC toplevel/g_toplevel.ml
OCAMLOPT toplevel/g_toplevel.ml
OCAMLC toplevel/coqloop.mli
OCAMLOPT toplevel/coqloop.ml
OCAMLC toplevel/ccompile.mli
OCAMLOPT toplevel/ccompile.ml
OCAMLC toplevel/coqtop.mli
OCAMLOPT toplevel/coqtop.ml
OCAMLC toplevel/workerLoop.mli
OCAMLOPT toplevel/workerLoop.ml
OCAMLC toplevel/coqc.mli
OCAMLOPT toplevel/coqc.ml
OCAMLOPT -a -o toplevel/toplevel.cmxa
OCAMLC kernel/byterun/coq_fix_code.c
OCAMLC kernel/byterun/coq_float64.c
OCAMLC kernel/byterun/coq_memory.c
OCAMLC kernel/byterun/coq_values.c
OCAMLC kernel/byterun/coq_interp.c
cd kernel/byterun/ && \
"/usr/local/bin/ocamlfind" ocamlmklib -oc coqrun coq_fix_code.o coq_float64.o coq_memory.o coq_values.o coq_interp.o
COQMKTOP -o bin/coqc.opt
ld: error: undefined symbol: ml_as_z_neg
>>> referenced by numTok.o:(camlNumTok__of_bigint_234) in archive interp/interp.a
>>> referenced by numTok.o:(camlNumTok__to_bigint_and_exponent_519) in archive interp/interp.a
>>> referenced by notation.o:(camlNotation__z_of_bigint_5265) in archive interp/interp.a
>>> referenced 13 more times
>>> did you mean: _ml_as_z_neg
>>> defined in: /usr/local/lib/ocaml/zarith/libzarith.a
ld: error: undefined symbol: ml_as_z_sub
>>> referenced by numTok.o:(camlNumTok__to_bigint_and_exponent_519) in archive interp/interp.a
>>> referenced by z.o:(camlZ__ediv_rem_242) in archive /usr/local/lib/ocaml/zarith/zarith.a
>>> referenced by z.o:(camlZ__gcdext_257) in archive /usr/local/lib/ocaml/zarith/zarith.a
>>> referenced 5 more times
ld: error: undefined symbol: ml_as_z_mul
>>> referenced by notation.o:(camlNotation__bigint_of_pos_5257) in archive interp/interp.a
>>> referenced by notation.o:(camlNotation__bigint_of_pos_5257) in archive interp/interp.a
>>> referenced by z.o:(camlZ__gcdext_257) in archive /usr/local/lib/ocaml/zarith/zarith.a
>>> referenced 19 more times
ld: error: undefined symbol: ml_as_z_add
>>> referenced by notation.o:(camlNotation__bigint_of_pos_5257) in archive interp/interp.a
>>> referenced by z.o:(camlZ__ediv_rem_242) in archive /usr/local/lib/ocaml/zarith/zarith.a
>>> referenced by z.o:(camlZ__erem_252) in archive /usr/local/lib/ocaml/zarith/zarith.a
>>> referenced 6 more times
ld: error: undefined symbol: ml_as_z_pred
>>> referenced by z.o:(camlZ__ediv_rem_242) in archive /usr/local/lib/ocaml/zarith/zarith.a
>>> referenced by z.o:(camlZ__log2up_288) in archive /usr/local/lib/ocaml/zarith/zarith.a
>>> referenced by z.o:(.data+0x494) in archive /usr/local/lib/ocaml/zarith/zarith.a
>>> referenced 1 more times
ld: error: undefined symbol: ml_as_z_succ
>>> referenced by z.o:(camlZ__ediv_rem_242) in archive /usr/local/lib/ocaml/zarith/zarith.a
>>> referenced by z.o:(.data+0x498) in archive /usr/local/lib/ocaml/zarith/zarith.a
>>> referenced by big_int_Z.o:(camlBig_int_Z__succ_big_int_89) in archive /usr/local/lib/ocaml/zarith/zarith.a
ld: error: undefined symbol: ml_as_z_rem
>>> referenced by z.o:(camlZ__erem_252) in archive /usr/local/lib/ocaml/zarith/zarith.a
>>> referenced by z.o:(.data+0x370) in archive /usr/local/lib/ocaml/zarith/zarith.a
>>> referenced by z.o:(.data+0x4A0) in archive /usr/local/lib/ocaml/zarith/zarith.a
ld: error: undefined symbol: ml_as_z_abs
>>> referenced by z.o:(camlZ__erem_252) in archive /usr/local/lib/ocaml/zarith/zarith.a
>>> referenced by z.o:(camlZ__lcm_264) in archive /usr/local/lib/ocaml/zarith/zarith.a
>>> referenced by z.o:(.data+0x490) in archive /usr/local/lib/ocaml/zarith/zarith.a
>>> referenced 3 more times
ld: error: undefined symbol: ml_as_z_div
>>> referenced by z.o:(camlZ__gcdext_257) in archive /usr/local/lib/ocaml/zarith/zarith.a
>>> referenced by z.o:(camlZ__gcdext_257) in archive /usr/local/lib/ocaml/zarith/zarith.a
>>> referenced by z.o:(.data+0x380) in archive /usr/local/lib/ocaml/zarith/zarith.a
>>> referenced 2 more times
ld: error: undefined symbol: ml_as_z_divexact
>>> referenced by z.o:(camlZ__lcm_264) in archive /usr/local/lib/ocaml/zarith/zarith.a
>>> referenced by z.o:(.data+0x374) in archive /usr/local/lib/ocaml/zarith/zarith.a
>>> referenced by z.o:(.data+0x3F4) in archive /usr/local/lib/ocaml/zarith/zarith.a
>>> referenced 2 more times
ld: error: undefined symbol: ml_as_z_lognot
>>> referenced by z.o:(camlZ__signed_extract_280) in archive /usr/local/lib/ocaml/zarith/zarith.a
>>> referenced by z.o:(camlZ__signed_extract_280) in archive /usr/local/lib/ocaml/zarith/zarith.a
>>> referenced by z.o:(.data+0x360) in archive /usr/local/lib/ocaml/zarith/zarith.a
>>> referenced 1 more times
ld: error: undefined symbol: ml_as_z_shift_right
>>> referenced by z.o:(camlZ__to_float_340) in archive /usr/local/lib/ocaml/zarith/zarith.a
>>> referenced by z.o:(.data+0x358) in archive /usr/local/lib/ocaml/zarith/zarith.a
>>> referenced by z.o:(.data+0x478) in archive /usr/local/lib/ocaml/zarith/zarith.a
>>> referenced 1 more times
ld: error: undefined symbol: ml_as_z_shift_left
>>> referenced by z.o:(camlZ__to_float_340) in archive /usr/local/lib/ocaml/zarith/zarith.a
>>> referenced by z.o:(.data+0x35C) in archive /usr/local/lib/ocaml/zarith/zarith.a
>>> referenced by z.o:(.data+0x47C) in archive /usr/local/lib/ocaml/zarith/zarith.a
>>> referenced 10 more times
ld: error: undefined symbol: ml_as_z_logxor
>>> referenced by z.o:(.data+0x364) in archive /usr/local/lib/ocaml/zarith/zarith.a
>>> referenced by z.o:(.data+0x484) in archive /usr/local/lib/ocaml/zarith/zarith.a
>>> referenced by big_int_Z.o:(camlBig_int_Z__xor_big_int_174) in archive /usr/local/lib/ocaml/zarith/zarith.a
ld: error: undefined symbol: ml_as_z_logor
>>> referenced by z.o:(.data+0x368) in archive /usr/local/lib/ocaml/zarith/zarith.a
>>> referenced by z.o:(.data+0x488) in archive /usr/local/lib/ocaml/zarith/zarith.a
>>> referenced by q.o:(camlQ__to_float_200) in archive /usr/local/lib/ocaml/zarith/zarith.a
>>> referenced 1 more times
ld: error: undefined symbol: ml_as_z_logand
>>> referenced by z.o:(.data+0x36C) in archive /usr/local/lib/ocaml/zarith/zarith.a
>>> referenced by z.o:(.data+0x48C) in archive /usr/local/lib/ocaml/zarith/zarith.a
>>> referenced by big_int_Z.o:(camlBig_int_Z__and_big_int_172) in archive /usr/local/lib/ocaml/zarith/zarith.a
cc: error: linker command failed with exit code 1 (use -v to see invocation)
File "caml_startup", line 1:
Error: Error during linking (exit code 1)
gmake[1]: Leaving directory '/pobj/coq-8.13.2/coq-8.13.2'
gmake[1]: *** [Makefile.build:428: bin/coqc.opt] Error 2
gmake: *** [Makefile.make:178: submake] Error 2
*** Error 2 in math/coq (Makefile:61 'do-build')
*** Error 2 in math/coq (/usr/ports/infrastructure/mk/bsd.port.mk:2944 '/pobj/coq-8.13.2/.build_done': @cd /usr/ports/math/coq && PKGPATH=ma...)
*** Error 2 in math/coq (/usr/ports/infrastructure/mk/bsd.port.mk:2594 'build': @lock=coq-8.13.2; export _LOCKS_HELD=" coq-8.13.2"; /usr/...)
===> Exiting math/coq with an error
*** Error 1 in /usr/ports (infrastructure/mk/bsd.port.subdir.mk:137 'build': @: ${echo_msg:=echo}; : ${target:=build}; for i in ; do eval...)
>>> Ended at 1638878453.65
max_stuck=3.77/depends=4.27/show-prepare-results=0.86/patch=0.72/configure=0.95/build=114.70
Error: job failed with 512 on i386-2 at 1638878453
No comments:
Post a Comment