>>> Building on octeon-2 under math/rocq BDEPENDS = [math/ocaml-zarith;devel/dune;x11/lablgtk3;lang/ocaml;devel/gmake;sysutils/findlib;devel/gmp;shells/bash] DIST = [math/rocq:coq-8.20.1.tar.gz] FULLPKGNAME = rocq-8.20.1p0 RDEPENDS = [devel/gmp;math/ocaml-zarith;x11/lablgtk3;lang/ocaml] (Junk lock obtained for octeon-2 at 1750758404.39) >>> Running depends in math/rocq at 1750758404.43 /usr/sbin/pkg_add -aI -Drepair bash-5.2.37 dune-3.6.2p2 findlib-1.9.6p2 gmp-6.3.0 lablgtk3-3.1.1p7 ocaml-4.14.2 ocaml-zarith-1.12p3 was: /usr/sbin/pkg_add -aI -Drepair bash-5.2.37 dune-3.6.2p2 findlib-1.9.6p2 gmake-4.4.1 gmp-6.3.0 lablgtk3-3.1.1p7 ocaml-4.14.2 ocaml-zarith-1.12p3 /usr/sbin/pkg_add -aI -Drepair bash-5.2.37 dune-3.6.2p2 findlib-1.9.6p2 gmp-6.3.0 lablgtk3-3.1.1p7 ocaml-4.14.2 ocaml-zarith-1.12p3 >>> Running show-prepare-results in math/rocq at 1750758466.51 ===> math/rocq ===> Building from scratch rocq-8.20.1p0 ===> rocq-8.20.1p0 depends on: lablgtk3-* -> lablgtk3-3.1.1p7 ===> rocq-8.20.1p0 depends on: ocaml-zarith-* -> ocaml-zarith-1.12p3 ===> rocq-8.20.1p0 depends on: bash-* -> bash-5.2.37 ===> rocq-8.20.1p0 depends on: findlib-* -> findlib-1.9.6p2 ===> rocq-8.20.1p0 depends on: dune-* -> dune-3.6.2p2 ===> rocq-8.20.1p0 depends on: ocaml-=4.14.2 -> ocaml-4.14.2 ===> rocq-8.20.1p0 depends on: gmake-* -> gmake-4.4.1 ===> rocq-8.20.1p0 depends on: gmp-* -> gmp-6.3.0 ===> Verifying specs: c gmp m pthread ===> found c.100.3 gmp.11.1 m.10.1 pthread.27.1 bash-5.2.37 dune-3.6.2p2 findlib-1.9.6p2 gmake-4.4.1 gmp-6.3.0 lablgtk3-3.1.1p7 ocaml-4.14.2 ocaml-zarith-1.12p3 Still tainted: host marked nojunk by devel/py-thrift >>> Running junk in math/rocq at 1750758481.92 Can't run junk because of lock on devel/py-thrift (Junk lock released for octeon-2 at 1750758492.13) distfiles size=7842928 >>> Running patch in math/rocq at 1750758492.22 ===> math/rocq ===> Checking files for rocq-8.20.1p0 `/ports/distfiles/coq-8.20.1.tar.gz' is up to date. >> (SHA256) all files: OK ===> Extracting for rocq-8.20.1p0 ===> Patching for rocq-8.20.1p0 ===> 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/rocq at 1750758502.25 ===> math/rocq ===> Generating configure for rocq-8.20.1p0 ===> Configuring for rocq-8.20.1p0 You have OCaml 4.14.2. Good! You have OCamlfind 1.9.6. Good! Warning: Cannot find the OCaml native-code compiler. Only the bytecode version of Coq will be available. You have the Zarith library 1.12 installed. Good! Architecture : OpenBSD Sys.os_type : Unix OCaml version : 4.14.2 OCaml binaries in : /usr/local/bin/ OCaml library in : /usr/local/lib/ocaml Web browser : firefox -remote "OpenURL(%s,new-tab)" || firefox %s & Coq web site : http://coq.inria.fr/ Bytecode VM enabled : true Native Compiler enabled : no Paths where installation is expected by Coq Makefile: - Coq is expected in /usr/local - the Coq library is expected in /usr/local/lib/coq - the Coqide configuration files is expected in /etc/xdg/coq - the Coqide data files is expected in /usr/local/share/coq - the Coq man pages is expected in /usr/local/share/man - documentation prefix path for all Coq packages is expected in /usr/local/share/doc 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'. cd /pobj/rocq-8.20.1/coq-8.20.1 && gmake dunestrap dune build --root . theories_dune ltac2_dune touch .dune-stamp cp -a _build/default/theories_dune theories/dune && chmod +w theories/dune cp -a _build/default/ltac2_dune user-contrib/Ltac2/dune && chmod +w user-contrib/Ltac2/dune >>> Running build in math/rocq at 1750758623.89 ===> math/rocq ===> Building for rocq-8.20.1p0 cd /pobj/rocq-8.20.1/coq-8.20.1 && dune build -j 1 -p coq-core,coq-stdlib,coqide-server,coq File "user-contrib/Ltac2/dune", line 69, characters 0-703: 69 | (rule 70 | (targets Init.timing Init.glob Init.vos Init.vo) 71 | (deps ../../theories/Init/Prelude.vo ../../plugins/ltac2/ltac2_plugin.cmxs 72 | ../../plugins/ltac2_ltac1/ltac2_ltac1_plugin.cmxs) 73 | (action (chdir ../../. (run coqc -boot -R theories Coq -Q user-contrib/Ltac2 Ltac2 -I plugins/firstorder -I plugins/funind -I plugins/ltac2 -I plugins/ltac2_ltac1 -I plugins/nsatz -I plugins/ring -I plugins/rtauto -I plugins/ssr -I plugins/ssrmatching -I plugins/syntax -I plugins/btauto -I plugins/cc -I plugins/derive -I plugins/extraction -I plugins/ltac -I plugins/micromega -w +default -q -w -deprecated-native-compiler-option -native-compiler off -time-file user-contrib/Ltac2/Init.timing %{dep:Init.v})))) Error: No rule found for plugins/ltac2/ltac2_plugin.cmxs File "user-contrib/Ltac2/dune", line 69, characters 0-703: 69 | (rule 70 | (targets Init.timing Init.glob Init.vos Init.vo) 71 | (deps ../../theories/Init/Prelude.vo ../../plugins/ltac2/ltac2_plugin.cmxs 72 | ../../plugins/ltac2_ltac1/ltac2_ltac1_plugin.cmxs) 73 | (action (chdir ../../. (run coqc -boot -R theories Coq -Q user-contrib/Ltac2 Ltac2 -I plugins/firstorder -I plugins/funind -I plugins/ltac2 -I plugins/ltac2_ltac1 -I plugins/nsatz -I plugins/ring -I plugins/rtauto -I plugins/ssr -I plugins/ssrmatching -I plugins/syntax -I plugins/btauto -I plugins/cc -I plugins/derive -I plugins/extraction -I plugins/ltac -I plugins/micromega -w +default -q -w -deprecated-native-compiler-option -native-compiler off -time-file user-contrib/Ltac2/Init.timing %{dep:Init.v})))) Error: No rule found for plugins/ltac2_ltac1/ltac2_ltac1_plugin.cmxs File "theories/dune", line 511, characters 1-1137: 511 | (rule 512 | (targets Prelude.timing Prelude.glob Prelude.vos Prelude.vo) 513 | (deps ../../theories/Init/Notations.vo ../../theories/Init/Logic.vo ..... 520 | ../../plugins/cc/cc_plugin.cmxs 521 | ../../plugins/firstorder/firstorder_plugin.cmxs) 522 | (action (chdir ../../. (run coqc -noinit -boot -R theories Coq -I plugins/firstorder -I plugins/funind -I plugins/ltac2 -I plugins/ltac2_ltac1 -I plugins/nsatz -I plugins/ring -I plugins/rtauto -I plugins/ssr -I plugins/ssrmatching -I plugins/syntax -I plugins/btauto -I plugins/cc -I plugins/derive -I plugins/extraction -I plugins/ltac -I plugins/micromega -w +default -q -w -deprecated-native-compiler-option -native-compiler off -time-file theories/Init/Prelude.timing %{dep:Prelude.v})))) Error: No rule found for plugins/cc/cc_plugin.cmxs File "theories/dune", line 511, characters 1-1137: 511 | (rule 512 | (targets Prelude.timing Prelude.glob Prelude.vos Prelude.vo) 513 | (deps ../../theories/Init/Notations.vo ../../theories/Init/Logic.vo ..... 520 | ../../plugins/cc/cc_plugin.cmxs 521 | ../../plugins/firstorder/firstorder_plugin.cmxs) 522 | (action (chdir ../../. (run coqc -noinit -boot -R theories Coq -I plugins/firstorder -I plugins/funind -I plugins/ltac2 -I plugins/ltac2_ltac1 -I plugins/nsatz -I plugins/ring -I plugins/rtauto -I plugins/ssr -I plugins/ssrmatching -I plugins/syntax -I plugins/btauto -I plugins/cc -I plugins/derive -I plugins/extraction -I plugins/ltac -I plugins/micromega -w +default -q -w -deprecated-native-compiler-option -native-compiler off -time-file theories/Init/Prelude.timing %{dep:Prelude.v})))) Error: No rule found for plugins/firstorder/firstorder_plugin.cmxs File "theories/dune", line 462, characters 1-783: 462 | (rule 463 | (targets Byte.timing Byte.glob Byte.vos Byte.vo) 464 | (deps ../../theories/Init/Ltac.vo ../../theories/Init/Datatypes.vo 465 | ../../theories/Init/Logic.vo ../../theories/Init/Specif.vo 466 | ../../theories/Init/Nat.vo 467 | ../../plugins/syntax/number_string_notation_plugin.cmxs) 468 | (action (chdir ../../. (run coqc -noinit -boot -R theories Coq -I plugins/firstorder -I plugins/funind -I plugins/ltac2 -I plugins/ltac2_ltac1 -I plugins/nsatz -I plugins/ring -I plugins/rtauto -I plugins/ssr -I plugins/ssrmatching -I plugins/syntax -I plugins/btauto -I plugins/cc -I plugins/derive -I plugins/extraction -I plugins/ltac -I plugins/micromega -w +default -q -w -deprecated-native-compiler-option -native-compiler off -time-file theories/Init/Byte.timing %{dep:Byte.v})))) Error: No rule found for plugins/syntax/number_string_notation_plugin.cmxs File "theories/dune", line 487, characters 1-592: 487 | (rule 488 | (targets Ltac.timing Ltac.glob Ltac.vos Ltac.vo) 489 | (deps ../../plugins/ltac/ltac_plugin.cmxs) 490 | (action (chdir ../../. (run coqc -noinit -boot -R theories Coq -I plugins/firstorder -I plugins/funind -I plugins/ltac2 -I plugins/ltac2_ltac1 -I plugins/nsatz -I plugins/ring -I plugins/rtauto -I plugins/ssr -I plugins/ssrmatching -I plugins/syntax -I plugins/btauto -I plugins/cc -I plugins/derive -I plugins/extraction -I plugins/ltac -I plugins/micromega -w +default -q -w -deprecated-native-compiler-option -native-compiler off -time-file theories/Init/Ltac.timing %{dep:Ltac.v})))) Error: No rule found for plugins/ltac/ltac_plugin.cmxs File "theories/dune", line 533, characters 1-738: 533 | (rule 534 | (targets Tauto.timing Tauto.glob Tauto.vos Tauto.vo) 535 | (deps ../../theories/Init/Notations.vo ../../theories/Init/Ltac.vo 536 | ../../theories/Init/Datatypes.vo ../../theories/Init/Logic.vo 537 | ../../plugins/ltac/tauto_plugin.cmxs) 538 | (action (chdir ../../. (run coqc -noinit -boot -R theories Coq -I plugins/firstorder -I plugins/funind -I plugins/ltac2 -I plugins/ltac2_ltac1 -I plugins/nsatz -I plugins/ring -I plugins/rtauto -I plugins/ssr -I plugins/ssrmatching -I plugins/syntax -I plugins/btauto -I plugins/cc -I plugins/derive -I plugins/extraction -I plugins/ltac -I plugins/micromega -w +default -q -w -deprecated-native-compiler-option -native-compiler off -time-file theories/Init/Tauto.timing %{dep:Tauto.v})))) Error: No rule found for plugins/ltac/tauto_plugin.cmxs File "theories/dune", line 3196, characters 1-641: 3196 | (rule 3197 | (targets Derive.timing Derive.glob Derive.vos Derive.vo) 3198 | (deps ../../theories/Init/Prelude.vo 3199 | ../../plugins/derive/derive_plugin.cmxs) 3200 | (action (chdir ../../. (run coqc -boot -R theories Coq -I plugins/firstorder -I plugins/funind -I plugins/ltac2 -I plugins/ltac2_ltac1 -I plugins/nsatz -I plugins/ring -I plugins/rtauto -I plugins/ssr -I plugins/ssrmatching -I plugins/syntax -I plugins/btauto -I plugins/cc -I plugins/derive -I plugins/extraction -I plugins/ltac -I plugins/micromega -w +default -q -w -deprecated-native-compiler-option -native-compiler off -time-file theories/derive/Derive.timing %{dep:Derive.v})))) Error: No rule found for plugins/derive/derive_plugin.cmxs File "theories/dune", line 3368, characters 1-689: 3368 | (rule 3369 | (targets FunInd.timing FunInd.glob FunInd.vos FunInd.vo) 3370 | (deps ../../theories/Init/Prelude.vo 3371 | ../../theories/extraction/Extraction.vo 3372 | ../../plugins/funind/funind_plugin.cmxs) 3373 | (action (chdir ../../. (run coqc -boot -R theories Coq -I plugins/firstorder -I plugins/funind -I plugins/ltac2 -I plugins/ltac2_ltac1 -I plugins/nsatz -I plugins/ring -I plugins/rtauto -I plugins/ssr -I plugins/ssrmatching -I plugins/syntax -I plugins/btauto -I plugins/cc -I plugins/derive -I plugins/extraction -I plugins/ltac -I plugins/micromega -w +default -q -w -deprecated-native-compiler-option -native-compiler off -time-file theories/funind/FunInd.timing %{dep:FunInd.v})))) Error: No rule found for plugins/funind/funind_plugin.cmxs File "theories/dune", line 3906, characters 1-686: 3906 | (rule 3907 | (targets ssrmatching.timing ssrmatching.glob ssrmatching.vos ssrmatching.vo) 3908 | (deps ../../theories/Init/Prelude.vo 3909 | ../../plugins/ssrmatching/ssrmatching_plugin.cmxs) 3910 | (action (chdir ../../. (run coqc -boot -R theories Coq -I plugins/firstorder -I plugins/funind -I plugins/ltac2 -I plugins/ltac2_ltac1 -I plugins/nsatz -I plugins/ring -I plugins/rtauto -I plugins/ssr -I plugins/ssrmatching -I plugins/syntax -I plugins/btauto -I plugins/cc -I plugins/derive -I plugins/extraction -I plugins/ltac -I plugins/micromega -w +default -q -w -deprecated-native-compiler-option -native-compiler off -time-file theories/ssrmatching/ssrmatching.timing %{dep:ssrmatching.v})))) Error: No rule found for plugins/ssrmatching/ssrmatching_plugin.cmxs File "theories/dune", line 3181, characters 1-715: 3181 | (rule 3182 | (targets Btauto.timing Btauto.glob Btauto.vos Btauto.vo) 3183 | (deps ../../theories/Init/Prelude.vo ../../theories/btauto/Algebra.vo 3184 | ../../theories/btauto/Reflect.vo 3185 | ../../plugins/btauto/btauto_plugin.cmxs) 3186 | (action (chdir ../../. (run coqc -boot -R theories Coq -I plugins/firstorder -I plugins/funind -I plugins/ltac2 -I plugins/ltac2_ltac1 -I plugins/nsatz -I plugins/ring -I plugins/rtauto -I plugins/ssr -I plugins/ssrmatching -I plugins/syntax -I plugins/btauto -I plugins/cc -I plugins/derive -I plugins/extraction -I plugins/ltac -I plugins/micromega -w +default -q -w -deprecated-native-compiler-option -native-compiler off -time-file theories/btauto/Btauto.timing %{dep:Btauto.v})))) Error: No rule found for plugins/btauto/btauto_plugin.cmxs File "theories/dune", line 3361, characters 1-677: 3361 | (rule 3362 | (targets Extraction.timing Extraction.glob Extraction.vos Extraction.vo) 3363 | (deps ../../theories/Init/Prelude.vo 3364 | ../../plugins/extraction/extraction_plugin.cmxs) 3365 | (action (chdir ../../. (run coqc -boot -R theories Coq -I plugins/firstorder -I plugins/funind -I plugins/ltac2 -I plugins/ltac2_ltac1 -I plugins/nsatz -I plugins/ring -I plugins/rtauto -I plugins/ssr -I plugins/ssrmatching -I plugins/syntax -I plugins/btauto -I plugins/cc -I plugins/derive -I plugins/extraction -I plugins/ltac -I plugins/micromega -w +default -q -w -deprecated-native-compiler-option -native-compiler off -time-file theories/extraction/Extraction.timing %{dep:Extraction.v})))) Error: No rule found for plugins/extraction/extraction_plugin.cmxs File "theories/dune", line 3412, characters 1-948: 3412 | (rule 3413 | (targets Lia.timing Lia.glob Lia.vos Lia.vo) 3414 | (deps ../../theories/Init/Prelude.vo ../../theories/micromega/ZMicromega.vo 3415 | ../../theories/micromega/RingMicromega.vo 3416 | ../../theories/micromega/VarMap.vo 3417 | ../../theories/micromega/DeclConstant.vo 3418 | ../../theories/Numbers/BinNums.vo ../../theories/micromega/Tauto.vo 3419 | ../../plugins/micromega/micromega_core_plugin.cmxs 3420 | ../../plugins/micromega/micromega_plugin.cmxs) 3421 | (action (chdir ../../. (run coqc -boot -R theories Coq -I plugins/firstorder -I plugins/funind -I plugins/ltac2 -I plugins/ltac2_ltac1 -I plugins/nsatz -I plugins/ring -I plugins/rtauto -I plugins/ssr -I plugins/ssrmatching -I plugins/syntax -I plugins/btauto -I plugins/cc -I plugins/derive -I plugins/extraction -I plugins/ltac -I plugins/micromega -w +default -q -w -deprecated-native-compiler-option -native-compiler off -time-file theories/micromega/Lia.timing %{dep:Lia.v})))) Error: No rule found for plugins/micromega/micromega_core_plugin.cmxs File "theories/dune", line 3412, characters 1-948: 3412 | (rule 3413 | (targets Lia.timing Lia.glob Lia.vos Lia.vo) 3414 | (deps ../../theories/Init/Prelude.vo ../../theories/micromega/ZMicromega.vo 3415 | ../../theories/micromega/RingMicromega.vo 3416 | ../../theories/micromega/VarMap.vo 3417 | ../../theories/micromega/DeclConstant.vo 3418 | ../../theories/Numbers/BinNums.vo ../../theories/micromega/Tauto.vo 3419 | ../../plugins/micromega/micromega_core_plugin.cmxs 3420 | ../../plugins/micromega/micromega_plugin.cmxs) 3421 | (action (chdir ../../. (run coqc -boot -R theories Coq -I plugins/firstorder -I plugins/funind -I plugins/ltac2 -I plugins/ltac2_ltac1 -I plugins/nsatz -I plugins/ring -I plugins/rtauto -I plugins/ssr -I plugins/ssrmatching -I plugins/syntax -I plugins/btauto -I plugins/cc -I plugins/derive -I plugins/extraction -I plugins/ltac -I plugins/micromega -w +default -q -w -deprecated-native-compiler-option -native-compiler off -time-file theories/micromega/Lia.timing %{dep:Lia.v})))) Error: No rule found for plugins/micromega/micromega_plugin.cmxs File "theories/dune", line 3555, characters 1-726: 3555 | (rule 3556 | (targets Zify.timing Zify.glob Zify.vos Zify.vo) 3557 | (deps ../../theories/Init/Prelude.vo 3558 | ../../theories/micromega/ZifyClasses.vo 3559 | ../../theories/micromega/ZifyInst.vo 3560 | ../../plugins/micromega/zify_plugin.cmxs) 3561 | (action (chdir ../../. (run coqc -boot -R theories Coq -I plugins/firstorder -I plugins/funind -I plugins/ltac2 -I plugins/ltac2_ltac1 -I plugins/nsatz -I plugins/ring -I plugins/rtauto -I plugins/ssr -I plugins/ssrmatching -I plugins/syntax -I plugins/btauto -I plugins/cc -I plugins/derive -I plugins/extraction -I plugins/ltac -I plugins/micromega -w +default -q -w -deprecated-native-compiler-option -native-compiler off -time-file theories/micromega/Zify.timing %{dep:Zify.v})))) Error: No rule found for plugins/micromega/zify_plugin.cmxs File "theories/dune", line 3644, characters 1-1290: 3644 | (rule 3645 | (targets NsatzTactic.timing NsatzTactic.glob NsatzTactic.vos NsatzTactic.vo) 3646 | (deps ../../theories/Init/Prelude.vo ../../theories/Lists/List.vo ...... 3656 | ../../theories/ZArith/ZArith.vo ../../theories/micromega/Lia.vo 3657 | ../../plugins/nsatz/nsatz_plugin.cmxs ../../theories/QArith/QArith.vo) 3658 | (action (chdir ../../. (run coqc -boot -R theories Coq -I plugins/firstorder -I plugins/funind -I plugins/ltac2 -I plugins/ltac2_ltac1 -I plugins/nsatz -I plugins/ring -I plugins/rtauto -I plugins/ssr -I plugins/ssrmatching -I plugins/syntax -I plugins/btauto -I plugins/cc -I plugins/derive -I plugins/extraction -I plugins/ltac -I plugins/micromega -w +default -q -w -deprecated-native-compiler-option -native-compiler off -time-file theories/nsatz/NsatzTactic.timing %{dep:NsatzTactic.v})))) Error: No rule found for plugins/nsatz/nsatz_plugin.cmxs File "theories/dune", line 3681, characters 1-779: 3681 | (rule 3682 | (targets Rtauto.timing Rtauto.glob Rtauto.vos Rtauto.vo) 3683 | (deps ../../theories/Init/Prelude.vo ../../theories/Lists/List.vo 3684 | ../../theories/rtauto/Bintree.vo ../../theories/Bool/Bool.vo 3685 | ../../theories/PArith/BinPos.vo 3686 | ../../plugins/rtauto/rtauto_plugin.cmxs) 3687 | (action (chdir ../../. (run coqc -boot -R theories Coq -I plugins/firstorder -I plugins/funind -I plugins/ltac2 -I plugins/ltac2_ltac1 -I plugins/nsatz -I plugins/ring -I plugins/rtauto -I plugins/ssr -I plugins/ssrmatching -I plugins/syntax -I plugins/btauto -I plugins/cc -I plugins/derive -I plugins/extraction -I plugins/ltac -I plugins/micromega -w +default -q -w -deprecated-native-compiler-option -native-compiler off -time-file theories/rtauto/Rtauto.timing %{dep:Rtauto.v})))) Error: No rule found for plugins/rtauto/rtauto_plugin.cmxs File "theories/dune", line 3815, characters 1-799: 3815 | (rule 3816 | (targets Ring_base.timing Ring_base.glob Ring_base.vos Ring_base.vo) 3817 | (deps ../../theories/Init/Prelude.vo ../../plugins/ring/ring_plugin.cmxs 3818 | ../../theories/setoid_ring/Ring_theory.vo 3819 | ../../theories/setoid_ring/Ring_tac.vo 3820 | ../../theories/setoid_ring/InitialRing.vo) 3821 | (action (chdir ../../. (run coqc -boot -R theories Coq -I plugins/firstorder -I plugins/funind -I plugins/ltac2 -I plugins/ltac2_ltac1 -I plugins/nsatz -I plugins/ring -I plugins/rtauto -I plugins/ssr -I plugins/ssrmatching -I plugins/syntax -I plugins/btauto -I plugins/cc -I plugins/derive -I plugins/extraction -I plugins/ltac -I plugins/micromega -w +default -q -w -deprecated-native-compiler-option -native-compiler off -time-file theories/setoid_ring/Ring_base.timing %{dep:Ring_base.v})))) Error: No rule found for plugins/ring/ring_plugin.cmxs File "theories/dune", line 3882, characters 1-773: 3882 | (rule 3883 | (targets ssreflect.timing ssreflect.glob ssreflect.vos ssreflect.vo) 3884 | (deps ../../theories/Init/Prelude.vo ../../theories/Bool/Bool.vo 3885 | ../../theories/ssrmatching/ssrmatching.vo 3886 | ../../plugins/ssr/ssreflect_plugin.cmxs 3887 | ../../theories/ssr/ssrunder.vo) 3888 | (action (chdir ../../. (run coqc -boot -R theories Coq -I plugins/firstorder -I plugins/funind -I plugins/ltac2 -I plugins/ltac2_ltac1 -I plugins/nsatz -I plugins/ring -I plugins/rtauto -I plugins/ssr -I plugins/ssrmatching -I plugins/syntax -I plugins/btauto -I plugins/cc -I plugins/derive -I plugins/extraction -I plugins/ltac -I plugins/micromega -w +default -q -w -deprecated-native-compiler-option -native-compiler off -time-file theories/ssr/ssreflect.timing %{dep:ssreflect.v})))) Error: No rule found for plugins/ssr/ssreflect_plugin.cmxs (cd _build/default && /usr/local/bin/bash -e -u -o pipefail -c dev/tools/make_git_revision.sh) > _build/default/revision skipping make_git_revision: git not found (cd _build/default && /usr/local/bin/ocamlc -w -40 -g -o dev/bench/timelog2html.exe -output-complete-exe /usr/local/lib/ocaml/unix.cma -I /usr/local/lib/ocaml /usr/local/lib/ocaml/str.cma -I /usr/local/lib/ocaml /usr/local/lib/ocaml/threads/threads.cma -I /usr/local/lib/ocaml clib/clib.cma /usr/local/lib/ocaml/zarith/zarith.cma -I /usr/local/lib/ocaml/zarith dev/bench/benchlib.cma dev/bench/.timelog2html.eobjs/byte/dune__exe__Timelog2html.cmo) /usr/local/lib/libgmp.so.11.1: warning: vsprintf() is often misused, please use vsnprintf() (cd _build/default && /usr/local/bin/ocamlc -w -40 -open Micromega_core_plugin -g -o plugins/micromega/csdpcert.exe -output-complete-exe /usr/local/lib/ocaml/zarith/zarith.cma -I /usr/local/lib/ocaml/zarith /usr/local/lib/ocaml/str.cma -I /usr/local/lib/ocaml /usr/local/lib/ocaml/unix.cma -I /usr/local/lib/ocaml /usr/local/lib/ocaml/threads/threads.cma -I /usr/local/lib/ocaml clib/clib.cma plugins/micromega/micromega_core_plugin.cma plugins/micromega/.csdpcert.eobjs/byte/dune__exe__Csdpcert.cmo) /usr/local/lib/libgmp.so.11.1: warning: vsprintf() is often misused, please use vsnprintf() (cd _build/default && /usr/local/bin/ocamlc -w -40 -g -o topbin/coqc_bin.exe -output-complete-exe -linkall config/config.cma boot/boot.cma /usr/local/lib/ocaml/str.cma -I /usr/local/lib/ocaml /usr/local/lib/ocaml/unix.cma -I /usr/local/lib/ocaml /usr/local/lib/ocaml/threads/threads.cma -I /usr/local/lib/ocaml clib/clib.cma lib/lib.cma gramlib/gramlib.cma /usr/local/lib/ocaml/zarith/zarith.cma -I /usr/local/lib/ocaml/zarith kernel/byterun/coqrun.cma -I kernel/byterun /usr/local/lib/ocaml/dynlink.cma -I /usr/local/lib/ocaml kernel/kernel.cma library/library.cma engine/engine.cma pretyping/pretyping.cma interp/interp.cma parsing/parsing.cma proofs/proofs.cma printing/printing.cma tactics/tactics.cma /usr/local/lib/ocaml/findlib/findlib.cma /usr/local/lib/ocaml/findlib/findlib_dynload.cma topbin/.coqc_bin.eobjs/byte/findlib_initl.cmo vernac/vernac.cma sysinit/sysinit.cma tools/coqworkmgr/coqworkmgrlib.cma stm/stm.cma toplevel/toplevel.cma topbin/.coqc_bin.eobjs/byte/dune__exe__Coqc_bin.cmo) /usr/local/lib/libgmp.so.11.1: warning: vsprintf() is often misused, please use vsnprintf() (cd _build/default && /usr/local/bin/ocamlc -w -40 -g -o ide/coqide/idetop.exe -output-complete-exe -linkall config/config.cma boot/boot.cma /usr/local/lib/ocaml/str.cma -I /usr/local/lib/ocaml /usr/local/lib/ocaml/unix.cma -I /usr/local/lib/ocaml /usr/local/lib/ocaml/threads/threads.cma -I /usr/local/lib/ocaml clib/clib.cma lib/lib.cma gramlib/gramlib.cma /usr/local/lib/ocaml/zarith/zarith.cma -I /usr/local/lib/ocaml/zarith kernel/byterun/coqrun.cma -I kernel/byterun /usr/local/lib/ocaml/dynlink.cma -I /usr/local/lib/ocaml kernel/kernel.cma library/library.cma engine/engine.cma pretyping/pretyping.cma interp/interp.cma parsing/parsing.cma proofs/proofs.cma printing/printing.cma tactics/tactics.cma /usr/local/lib/ocaml/findlib/findlib.cma /usr/local/lib/ocaml/findlib/findlib_dynload.cma ide/coqide/.idetop.eobjs/byte/findlib_initl.cmo vernac/vernac.cma sysinit/sysinit.cma tools/coqworkmgr/coqworkmgrlib.cma stm/stm.cma toplevel/toplevel.cma ide/coqide/protocol/protocol.cma ide/coqide/platform_specific.cma -I ide/coqide ide/coqide/.idetop.eobjs/byte/dune__exe__Idetop.cmo -linkall) /usr/local/lib/libgmp.so.11.1: warning: vsprintf() is often misused, please use vsnprintf() (cd _build/default && /usr/local/bin/ocamlc -w -40 -g -o topbin/coqtop_bin.exe -output-complete-exe -linkall config/config.cma boot/boot.cma /usr/local/lib/ocaml/str.cma -I /usr/local/lib/ocaml /usr/local/lib/ocaml/unix.cma -I /usr/local/lib/ocaml /usr/local/lib/ocaml/threads/threads.cma -I /usr/local/lib/ocaml clib/clib.cma lib/lib.cma gramlib/gramlib.cma /usr/local/lib/ocaml/zarith/zarith.cma -I /usr/local/lib/ocaml/zarith kernel/byterun/coqrun.cma -I kernel/byterun /usr/local/lib/ocaml/dynlink.cma -I /usr/local/lib/ocaml kernel/kernel.cma library/library.cma engine/engine.cma pretyping/pretyping.cma interp/interp.cma parsing/parsing.cma proofs/proofs.cma printing/printing.cma tactics/tactics.cma /usr/local/lib/ocaml/findlib/findlib.cma /usr/local/lib/ocaml/findlib/findlib_dynload.cma topbin/.coqtop_bin.eobjs/byte/findlib_initl.cmo vernac/vernac.cma sysinit/sysinit.cma tools/coqworkmgr/coqworkmgrlib.cma stm/stm.cma toplevel/toplevel.cma topbin/.coqtop_bin.eobjs/byte/dune__exe__Coqtop_bin.cmo) /usr/local/lib/libgmp.so.11.1: warning: vsprintf() is often misused, please use vsnprintf() (cd _build/default && /usr/local/bin/ocamlc -w -40 -g -o topbin/coqworker_bin.exe -output-complete-exe -linkall config/config.cma boot/boot.cma /usr/local/lib/ocaml/str.cma -I /usr/local/lib/ocaml /usr/local/lib/ocaml/unix.cma -I /usr/local/lib/ocaml /usr/local/lib/ocaml/threads/threads.cma -I /usr/local/lib/ocaml clib/clib.cma lib/lib.cma gramlib/gramlib.cma /usr/local/lib/ocaml/zarith/zarith.cma -I /usr/local/lib/ocaml/zarith kernel/byterun/coqrun.cma -I kernel/byterun /usr/local/lib/ocaml/dynlink.cma -I /usr/local/lib/ocaml kernel/kernel.cma library/library.cma engine/engine.cma pretyping/pretyping.cma interp/interp.cma parsing/parsing.cma proofs/proofs.cma printing/printing.cma tactics/tactics.cma /usr/local/lib/ocaml/findlib/findlib.cma /usr/local/lib/ocaml/findlib/findlib_dynload.cma topbin/.coqworker_bin.eobjs/byte/findlib_initl.cmo vernac/vernac.cma sysinit/sysinit.cma tools/coqworkmgr/coqworkmgrlib.cma stm/stm.cma toplevel/toplevel.cma topbin/.coqworker_bin.eobjs/byte/dune__exe__Coqworker_bin.cmo) /usr/local/lib/libgmp.so.11.1: warning: vsprintf() is often misused, please use vsnprintf() *** Error 1 in math/rocq (Makefile:51 'do-build') *** Error 2 in math/rocq (/ports/infrastructure/mk/bsd.port.mk:3065 '/pobj/rocq-8.20.1/.build_done': @cd /ports/math/rocq && PKGPATH=math/ro...) *** Error 2 in math/rocq (/ports/infrastructure/mk/bsd.port.mk:2712 'build': @lock=rocq-8.20.1p0; export _LOCKS_HELD=" rocq-8.20.1p0"; /u...) ===> Exiting math/rocq with an error *** Error 1 in /ports (infrastructure/mk/bsd.port.subdir.mk:144 'build': @: ${echo_msg:=echo}; : ${target:=build}; for i in ; do eval ${e...) >>> Ended at 1750761160.55 max_stuck=1671.51/depends=62.08/show-prepare-results=14.85/junk=10.25/patch=10.04/configure=121.64/build=2536.70 Error: job failed with 512 on octeon-2 at 1750761160