# Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-domains base base-nnp base Naked pointers prohibited in the OCaml heap base-threads base base-unix base conf-gmp 4 Virtual package relying on a GMP lib system installation coq 8.17.1 The Coq Proof Assistant coq-core 8.17.1 The Coq Proof Assistant -- Core Binaries and Tools coq-stdlib 8.17.1 The Coq Proof Assistant -- Standard Library coqide-server 8.17.1 The Coq Proof Assistant, XML protocol server dune 3.12.1 Fast, portable, and opinionated build system ocaml 5.1.1 The OCaml compiler (virtual package) ocaml-base-compiler 5.1.1 Official release 5.1.1 ocaml-config 3 OCaml Switch Configuration ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled ocamlfind 1.9.6 A library manager for OCaml zarith 1.13 Implements arithmetic and logical operations over arbitrary-precision integers # opam file: opam-version: "2.0" synopsis: "Tactician: A Seamless, Interactive Tactic Learner and Prover for Coq" description: """ Tactician is a tactic learner and prover for the Coq Proof Assistant. The system will help users make tactical proof decisions while they retain control over the general proof strategy. To this end, Tactician will learn from previously written tactic scripts, and either gives the user suggestions about the next tactic to be executed or altogether takes over the burden of proof synthesis. Tactician's goal is to provide the user with a seamless, interactive, and intuitive experience together with strong, adaptive proof automation.""" maintainer: ["Lasse Blaauwbroek <lasse@blaauwbroek.eu>"] authors: ["Lasse Blaauwbroek <lasse@blaauwbroek.eu>"] license: "MIT" homepage: "https://coq-tactician.github.io" bug-reports: "https://github.com/coq-tactician/coq-tactician/issues" depends: [ "ocaml" {>= "4.08"} "dune" {>= "3.5" & < "3.8~"} "dune-site" {>= "2.9.1"} "opam-client" {>= "2.1.0"} "cmdliner" {>= "1.1.0"} "coq-core" {>= "8.17" & < "8.18~"} "coq-stdlib" {with-test} "conf-git" "bos" {>= "0.2.1"} "coq-tactician-dummy" {= "1.0~beta2+8.17" & with-test} "odoc" {with-doc} ] build: [ ["dune" "subst"] {dev} [ "dune" "build" "-p" name "-j" jobs "--promote-install-files=false" "@install" "@runtest" {with-test} "@doc" {with-doc} ] ["dune" "install" "-p" name "--create-install-files" name] ] dev-repo: "git+https://github.com/coq-tactician/coq-tactician.git" post-messages: [" --- Tactician was successfully installed --- In order to enable Tactician, you should run tactician enable " {success}] tags: [ "keyword:tactic-learning" "keyword:machine-learning" "keyword:automation" "keyword:proof-synthesis" "category:Miscellaneous/Coq Extensions" "logpath:Tactician" ] substs: [ "coq-shim/tactician-patch" "coq-shim/tactician.ml" ] url { src: "https://github.com/coq-tactician/coq-tactician/archive/1.0-beta2.1-8.17.tar.gz" checksum: "sha512=9f0dc305e0ad61acce0fa00ade66f3da7ac82d4ff8a1f455b79e588e62618b766133d7f4e2f67e6d1857b0c2ba68449425b2642b49199e8e8269cdbf8e8446c5" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-tactician.1.0~beta2.1+8.17 coq.8.17.1
Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
true
opam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-tactician.1.0~beta2.1+8.17 coq.8.17.1
# Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-domains base base-nnp base Naked pointers prohibited in the OCaml heap base-threads base base-unix base conf-gmp 4 Virtual package relying on a GMP lib system installation coq 8.17.1 The Coq Proof Assistant coq-core 8.17.1 The Coq Proof Assistant -- Core Binaries and Tools coq-stdlib 8.17.1 The Coq Proof Assistant -- Standard Library coqide-server 8.17.1 The Coq Proof Assistant, XML protocol server dune 3.12.1 Fast, portable, and opinionated build system ocaml 5.1.1 The OCaml compiler (virtual package) ocaml-base-compiler 5.1.1 Official release 5.1.1 ocaml-config 3 OCaml Switch Configuration ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled ocamlfind 1.9.6 A library manager for OCaml zarith 1.13 Implements arithmetic and logical operations over arbitrary-precision integers The following actions will be performed: - install ocamlbuild 0.14.3 - install cmdliner 1.2.0 - downgrade dune 3.12.1 to 3.7.1 - install seq base - install conf-git 1.1 - install topkg 1.0.7 - install stdlib-shims 0.3.0 - install pp 1.2.0 - install ordering 3.12.1 - install opam-file-format 2.1.6 - install csexp 1.5.2 - install cppo 1.6.9 - install base64 3.5.1 - recompile coq-core 8.17.1 [uses dune] - install re 1.11.0 - install rresult 0.7.0 - install fmt 0.9.0 - install astring 0.8.5 - install ocamlgraph 2.1.0 - install dyn 3.12.1 - install extlib 1.7.9 - recompile coqide-server 8.17.1 [uses dune] - recompile coq-stdlib 8.17.1 [uses dune] - install logs 0.7.0 - install fpath 0.7.3 - install opam-core 2.1.5 - install stdune 3.12.1 - install cudf 0.10 - install bos 0.2.1 - install opam-format 2.1.5 - install dune-private-libs 3.12.1 - install mccs 1.1+17 - install dose3 7.0.0 - install opam-repository 2.1.5 - install dune-site 3.12.1 - install opam-solver 2.1.5 - install opam-state 2.1.5 - install opam-client 2.1.5 ===== 34 to install | 3 to recompile | 1 to downgrade ===== <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> -> retrieved astring.0.8.5 (https://opam.ocaml.org/cache) -> retrieved base64.3.5.1 (https://opam.ocaml.org/cache) -> retrieved bos.0.2.1 (https://opam.ocaml.org/cache) -> retrieved coq-core.8.17.1 (cached) -> installed conf-git.1.1 -> retrieved coq-stdlib.8.17.1 (cached) -> retrieved cmdliner.1.2.0 (https://opam.ocaml.org/cache) -> retrieved coqide-server.8.17.1 (cached) -> retrieved cppo.1.6.9 (https://opam.ocaml.org/cache) -> retrieved csexp.1.5.2 (https://opam.ocaml.org/cache) -> retrieved cudf.0.10 (https://opam.ocaml.org/cache) -> retrieved dose3.7.0.0 (https://opam.ocaml.org/cache) -> retrieved dune-private-libs.3.12.1 (cached) -> retrieved dune.3.7.1 (https://opam.ocaml.org/cache) -> retrieved dune-site.3.12.1 (cached) -> retrieved dyn.3.12.1 (cached) -> retrieved extlib.1.7.9 (https://opam.ocaml.org/cache) -> retrieved fmt.0.9.0 (https://opam.ocaml.org/cache) -> retrieved fpath.0.7.3 (https://opam.ocaml.org/cache) -> retrieved logs.0.7.0 (https://opam.ocaml.org/cache) -> retrieved mccs.1.1+17 (https://opam.ocaml.org/cache) -> retrieved ocamlbuild.0.14.3 (https://opam.ocaml.org/cache) -> retrieved opam-client.2.1.5 (https://opam.ocaml.org/cache) -> retrieved ocamlgraph.2.1.0 (https://opam.ocaml.org/cache) -> retrieved opam-format.2.1.5 (cached) -> retrieved opam-repository.2.1.5 (cached) -> retrieved opam-file-format.2.1.6 (https://opam.ocaml.org/cache) -> retrieved opam-solver.2.1.5 (cached) -> retrieved opam-state.2.1.5 (cached) -> retrieved pp.1.2.0 (https://opam.ocaml.org/cache) -> retrieved ordering.3.12.1 (cached) -> retrieved opam-core.2.1.5 (https://opam.ocaml.org/cache) -> installed seq.base -> retrieved re.1.11.0 (https://opam.ocaml.org/cache) -> retrieved rresult.0.7.0 (https://opam.ocaml.org/cache) -> retrieved stdlib-shims.0.3.0 (https://opam.ocaml.org/cache) -> retrieved topkg.1.0.7 (https://opam.ocaml.org/cache) -> retrieved stdune.3.12.1 (cached) -> installed cmdliner.1.2.0 While removing coq-stdlib.8.17.1: these files have been modified since installation: - lib/coq/user-contrib/Ltac2/Uint63.vos - lib/coq/user-contrib/Ltac2/Uint63.vo - lib/coq/user-contrib/Ltac2/Uint63.v - lib/coq/user-contrib/Ltac2/Uint63.glob - lib/coq/user-contrib/Ltac2/String.vos - lib/coq/user-contrib/Ltac2/String.vo - lib/coq/user-contrib/Ltac2/String.v - lib/coq/user-contrib/Ltac2/String.glob - lib/coq/user-contrib/Ltac2/Std.vos - lib/coq/user-contrib/Ltac2/Std.vo - lib/coq/user-contrib/Ltac2/Std.v - lib/coq/user-contrib/Ltac2/Std.glob - lib/coq/user-contrib/Ltac2/Proj.vos - lib/coq/user-contrib/Ltac2/Proj.vo - lib/coq/user-contrib/Ltac2/Proj.v - lib/coq/user-contrib/Ltac2/Proj.glob - lib/coq/user-contrib/Ltac2/Printf.vos - lib/coq/user-contrib/Ltac2/Printf.vo - lib/coq/user-contrib/Ltac2/Printf.v - lib/coq/user-contrib/Ltac2/Printf.glob - lib/coq/user-contrib/Ltac2/Pattern.vos - lib/coq/user-contrib/Ltac2/Pattern.vo - lib/coq/user-contrib/Ltac2/Pattern.v - lib/coq/user-contrib/Ltac2/Pattern.glob - lib/coq/user-contrib/Ltac2/Option.vos - lib/coq/user-contrib/Ltac2/Option.vo - lib/coq/user-contrib/Ltac2/Option.v - lib/coq/user-contrib/Ltac2/Option.glob - lib/coq/user-contrib/Ltac2/Notations.vos - lib/coq/user-contrib/Ltac2/Notations.vo - lib/coq/user-contrib/Ltac2/Notations.v - lib/coq/user-contrib/Ltac2/Notations.glob - lib/coq/user-contrib/Ltac2/Meta.vos - lib/coq/user-contrib/Ltac2/Meta.vo - lib/coq/user-contrib/Ltac2/Meta.v - lib/coq/user-contrib/Ltac2/Meta.glob - lib/coq/user-contrib/Ltac2/Message.vos - lib/coq/user-contrib/Ltac2/Message.vo - lib/coq/user-contrib/Ltac2/Message.v - lib/coq/user-contrib/Ltac2/Message.glob - lib/coq/user-contrib/Ltac2/Ltac2.vos - lib/coq/user-contrib/Ltac2/Ltac2.vo - lib/coq/user-contrib/Ltac2/Ltac2.v - lib/coq/user-contrib/Ltac2/Ltac2.glob - lib/coq/user-contrib/Ltac2/Ltac1.vos - lib/coq/user-contrib/Ltac2/Ltac1.vo - lib/coq/user-contrib/Ltac2/Ltac1.v - lib/coq/user-contrib/Ltac2/Ltac1.glob - lib/coq/user-contrib/Ltac2/List.vos - lib/coq/user-contrib/Ltac2/List.vo - lib/coq/user-contrib/Ltac2/List.v - lib/coq/user-contrib/Ltac2/List.glob - lib/coq/user-contrib/Ltac2/Int.vos - lib/coq/user-contrib/Ltac2/Int.vo - lib/coq/user-contrib/Ltac2/Int.v - lib/coq/user-contrib/Ltac2/Int.glob - lib/coq/user-contrib/Ltac2/Init.vos - lib/coq/user-contrib/Ltac2/Init.vo - lib/coq/user-contrib/Ltac2/Init.v - lib/coq/user-contrib/Ltac2/Init.glob - lib/coq/user-contrib/Ltac2/Ind.vos - lib/coq/user-contrib/Ltac2/Ind.vo - lib/coq/user-contrib/Ltac2/Ind.v - lib/coq/user-contrib/Ltac2/Ind.glob - lib/coq/user-contrib/Ltac2/Ident.vos - lib/coq/user-contrib/Ltac2/Ident.vo - lib/coq/user-contrib/Ltac2/Ident.v - lib/coq/user-contrib/Ltac2/Ident.glob - lib/coq/user-contrib/Ltac2/Fresh.vos - lib/coq/user-contrib/Ltac2/Fresh.vo - lib/coq/user-contrib/Ltac2/Fresh.v - lib/coq/user-contrib/Ltac2/Fresh.glob - lib/coq/user-contrib/Ltac2/Float.vos - lib/coq/user-contrib/Ltac2/Float.vo - lib/coq/user-contrib/Ltac2/Float.v - lib/coq/user-contrib/Ltac2/Float.glob - lib/coq/user-contrib/Ltac2/Evar.vos - lib/coq/user-contrib/Ltac2/Evar.vo - lib/coq/user-contrib/Ltac2/Evar.v - lib/coq/user-contrib/Ltac2/Evar.glob - lib/coq/user-contrib/Ltac2/Env.vos - lib/coq/user-contrib/Ltac2/Env.vo - lib/coq/user-contrib/Ltac2/Env.v - lib/coq/user-contrib/Ltac2/Env.glob - lib/coq/user-contrib/Ltac2/Control.vos - lib/coq/user-contrib/Ltac2/Control.vo - lib/coq/user-contrib/Ltac2/Control.v - lib/coq/user-contrib/Ltac2/Control.glob - lib/coq/user-contrib/Ltac2/Constructor.vos - lib/coq/user-contrib/Ltac2/Constructor.vo - lib/coq/user-contrib/Ltac2/Constructor.v - lib/coq/user-contrib/Ltac2/Constructor.glob - lib/coq/user-contrib/Ltac2/Constr.vos - lib/coq/user-contrib/Ltac2/Constr.vo - lib/coq/user-contrib/Ltac2/Constr.v - lib/coq/user-contrib/Ltac2/Constr.glob - lib/coq/user-contrib/Ltac2/Constant.vos - lib/coq/user-contrib/Ltac2/Constant.vo - lib/coq/user-contrib/Ltac2/Constant.v - lib/coq/user-contrib/Ltac2/Constant.glob - lib/coq/user-contrib/Ltac2/Char.vos - lib/coq/user-contrib/Ltac2/Char.vo - lib/coq/user-contrib/Ltac2/Char.v - lib/coq/user-contrib/Ltac2/Char.glob - lib/coq/user-contrib/Ltac2/Bool.vos - lib/coq/user-contrib/Ltac2/Bool.vo - lib/coq/user-contrib/Ltac2/Bool.v - lib/coq/user-contrib/Ltac2/Bool.glob - lib/coq/user-contrib/Ltac2/Array.vos - lib/coq/user-contrib/Ltac2/Array.vo - lib/coq/user-contrib/Ltac2/Array.v - lib/coq/user-contrib/Ltac2/Array.glob - lib/coq/theories/ssrmatching/ssrmatching.vos - lib/coq/theories/ssrmatching/ssrmatching.vo - lib/coq/theories/ssrmatching/ssrmatching.v - lib/coq/theories/ssrmatching/ssrmatching.glob - lib/coq/theories/ssr/ssrunder.vos - lib/coq/theories/ssr/ssrunder.vo - lib/coq/theories/ssr/ssrunder.v - lib/coq/theories/ssr/ssrunder.glob - lib/coq/theories/ssr/ssrsetoid.vos - lib/coq/theories/ssr/ssrsetoid.vo - lib/coq/theories/ssr/ssrsetoid.v - lib/coq/theori [...] truncated ies/Bool/Bvector.vos - lib/coq/theories/Bool/Bvector.vo - lib/coq/theories/Bool/Bvector.v - lib/coq/theories/Bool/Bvector.glob - lib/coq/theories/Bool/BoolOrder.vos - lib/coq/theories/Bool/BoolOrder.vo - lib/coq/theories/Bool/BoolOrder.v - lib/coq/theories/Bool/BoolOrder.glob - lib/coq/theories/Bool/BoolEq.vos - lib/coq/theories/Bool/BoolEq.vo - lib/coq/theories/Bool/BoolEq.v - lib/coq/theories/Bool/BoolEq.glob - lib/coq/theories/Bool/Bool.vos - lib/coq/theories/Bool/Bool.vo - lib/coq/theories/Bool/Bool.v - lib/coq/theories/Bool/Bool.glob - lib/coq/theories/Array/PArray.vos - lib/coq/theories/Array/PArray.vo - lib/coq/theories/Array/PArray.v - lib/coq/theories/Array/PArray.glob - lib/coq/theories/Arith/Wf_nat.vos - lib/coq/theories/Arith/Wf_nat.vo - lib/coq/theories/Arith/Wf_nat.v - lib/coq/theories/Arith/Wf_nat.glob - lib/coq/theories/Arith/Plus.vos - lib/coq/theories/Arith/Plus.vo - lib/coq/theories/Arith/Plus.v - lib/coq/theories/Arith/Plus.glob - lib/coq/theories/Arith/Peano_dec.vos - lib/coq/theories/Arith/Peano_dec.vo - lib/coq/theories/Arith/Peano_dec.v - lib/coq/theories/Arith/Peano_dec.glob - lib/coq/theories/Arith/PeanoNat.vos - lib/coq/theories/Arith/PeanoNat.vo - lib/coq/theories/Arith/PeanoNat.v - lib/coq/theories/Arith/PeanoNat.glob - lib/coq/theories/Arith/Mult.vos - lib/coq/theories/Arith/Mult.vo - lib/coq/theories/Arith/Mult.v - lib/coq/theories/Arith/Mult.glob - lib/coq/theories/Arith/Minus.vos - lib/coq/theories/Arith/Minus.vo - lib/coq/theories/Arith/Minus.v - lib/coq/theories/Arith/Minus.glob - lib/coq/theories/Arith/Min.vos - lib/coq/theories/Arith/Min.vo - lib/coq/theories/Arith/Min.v - lib/coq/theories/Arith/Min.glob - lib/coq/theories/Arith/Max.vos - lib/coq/theories/Arith/Max.vo - lib/coq/theories/Arith/Max.v - lib/coq/theories/Arith/Max.glob - lib/coq/theories/Arith/Lt.vos - lib/coq/theories/Arith/Lt.vo - lib/coq/theories/Arith/Lt.v - lib/coq/theories/Arith/Lt.glob - lib/coq/theories/Arith/Le.vos - lib/coq/theories/Arith/Le.vo - lib/coq/theories/Arith/Le.v - lib/coq/theories/Arith/Le.glob - lib/coq/theories/Arith/Gt.vos - lib/coq/theories/Arith/Gt.vo - lib/coq/theories/Arith/Gt.v - lib/coq/theories/Arith/Gt.glob - lib/coq/theories/Arith/Factorial.vos - lib/coq/theories/Arith/Factorial.vo - lib/coq/theories/Arith/Factorial.v - lib/coq/theories/Arith/Factorial.glob - lib/coq/theories/Arith/Even.vos - lib/coq/theories/Arith/Even.vo - lib/coq/theories/Arith/Even.v - lib/coq/theories/Arith/Even.glob - lib/coq/theories/Arith/Euclid.vos - lib/coq/theories/Arith/Euclid.vo - lib/coq/theories/Arith/Euclid.v - lib/coq/theories/Arith/Euclid.glob - lib/coq/theories/Arith/EqNat.vos - lib/coq/theories/Arith/EqNat.vo - lib/coq/theories/Arith/EqNat.v - lib/coq/theories/Arith/EqNat.glob - lib/coq/theories/Arith/Div2.vos - lib/coq/theories/Arith/Div2.vo - lib/coq/theories/Arith/Div2.v - lib/coq/theories/Arith/Div2.glob - lib/coq/theories/Arith/Compare_dec.vos - lib/coq/theories/Arith/Compare_dec.vo - lib/coq/theories/Arith/Compare_dec.v - lib/coq/theories/Arith/Compare_dec.glob - lib/coq/theories/Arith/Compare.vos - lib/coq/theories/Arith/Compare.vo - lib/coq/theories/Arith/Compare.v - lib/coq/theories/Arith/Compare.glob - lib/coq/theories/Arith/Cantor.vos - lib/coq/theories/Arith/Cantor.vo - lib/coq/theories/Arith/Cantor.v - lib/coq/theories/Arith/Cantor.glob - lib/coq/theories/Arith/Bool_nat.vos - lib/coq/theories/Arith/Bool_nat.vo - lib/coq/theories/Arith/Bool_nat.v - lib/coq/theories/Arith/Bool_nat.glob - lib/coq/theories/Arith/Between.vos - lib/coq/theories/Arith/Between.vo - lib/coq/theories/Arith/Between.v - lib/coq/theories/Arith/Between.glob - lib/coq/theories/Arith/Arith_prebase.vos - lib/coq/theories/Arith/Arith_prebase.vo - lib/coq/theories/Arith/Arith_prebase.v - lib/coq/theories/Arith/Arith_prebase.glob - lib/coq/theories/Arith/Arith_base.vos - lib/coq/theories/Arith/Arith_base.vo - lib/coq/theories/Arith/Arith_base.v - lib/coq/theories/Arith/Arith_base.glob - lib/coq/theories/Arith/Arith.vos - lib/coq/theories/Arith/Arith.vo - lib/coq/theories/Arith/Arith.v - lib/coq/theories/Arith/Arith.glob Remove them anyway? [y/N] y -> removed coq-stdlib.8.17.1 -> removed coqide-server.8.17.1 -> removed coq-core.8.17.1 -> removed dune.3.12.1 -> installed dune.3.7.1 -> installed ocamlbuild.0.14.3 -> installed base64.3.5.1 -> installed cppo.1.6.9 -> installed csexp.1.5.2 -> installed opam-file-format.2.1.6 -> installed extlib.1.7.9 -> installed pp.1.2.0 -> installed re.1.11.0 -> installed cudf.0.10 -> installed ordering.3.12.1 -> installed stdlib-shims.0.3.0 -> installed topkg.1.0.7 -> installed dyn.3.12.1 -> installed astring.0.8.5 -> installed mccs.1.1+17 -> installed ocamlgraph.2.1.0 -> installed fpath.0.7.3 -> installed fmt.0.9.0 -> installed rresult.0.7.0 -> installed dose3.7.0.0 -> installed logs.0.7.0 -> installed bos.0.2.1 -> installed opam-core.2.1.5 -> installed stdune.3.12.1 -> installed dune-private-libs.3.12.1 -> installed opam-format.2.1.5 -> installed dune-site.3.12.1 -> installed opam-repository.2.1.5 -> installed opam-solver.2.1.5 -> installed coq-core.8.17.1 -> installed opam-state.2.1.5 -> installed coqide-server.8.17.1 [ERROR] The compilation of coq-stdlib.8.17.1 failed at "dune build -p coq-stdlib -j 4 @install". -> installed opam-client.2.1.5 #=== ERROR while compiling coq-stdlib.8.17.1 ==================================# # context 2.1.5 | linux/x86_64 | ocaml-base-compiler.5.1.1 | https://opam.ocaml.org#09658dd9 # path ~/.opam/ocaml-base-compiler.5.1.1/.opam-switch/build/coq-stdlib.8.17.1 # command ~/.opam/opam-init/hooks/sandbox.sh build dune build -p coq-stdlib -j 4 @install # exit-code 1 # env-file ~/.opam/log/coq-stdlib-29031-4295fb.env # output-file ~/.opam/log/coq-stdlib-29031-4295fb.out ### output ### # [...] # 3015 | (targets Notations.glob Notations.vos Notations.vo) # 3016 | (deps ) # 3017 | (action (run coqc -noinit -boot -R ../. Coq -I /home/bench/.opam/ocaml-base-compiler.5.1.1/lib/coq-core/plugins/number_string_notation -I /home/bench/.opam/ocaml-base-compiler.5.1.1/lib/coq-core/plugins/zify -I /home/bench/.opam/ocaml-base-compiler.5.1.1/lib/coq-core/plugins/tauto -I /home/bench/.opam/ocaml-base-compiler.5.1.1/lib/coq-core/plugins/ssreflect -I /home/bench/.opam/ocaml[...] # (cd _build/default/theories/Init && /home/bench/.opam/ocaml-base-compiler.5.1.1/bin/coqc -noinit -boot -R ../. Coq -I /home/bench/.opam/ocaml-base-compiler.5.1.1/lib/coq-core/plugins/number_string_notation -I /home/bench/.opam/ocaml-base-compiler.5.1.1/lib/coq-core/plugins/zify -I /home/bench/.opam/ocaml-base-compiler.5.1.1/lib/coq-core/plugins/tauto -I /home/bench/.opam/ocaml-base-compiler.5[...] # Fatal error: Not enough heap memory to reserve minor heaps # File "theories/dune", line 2999, characters 1-1575: # 2999 | (rule # 3000 | (targets Ltac.glob Ltac.vos Ltac.vo) # 3001 | (deps /home/bench/.opam/ocaml-base-compiler.5.1.1/lib/coq-core/plugins/ltac/ltac_plugin.cmxs) # 3002 | (action (run coqc -noinit -boot -R ../. Coq -I /home/bench/.opam/ocaml-base-compiler.5.1.1/lib/coq-core/plugins/number_string_notation -I /home/bench/.opam/ocaml-base-compiler.5.1.1/lib/coq-core/plugins/zify -I /home/bench/.opam/ocaml-base-compiler.5.1.1/lib/coq-core/plugins/tauto -I /home/bench/.opam/ocaml-base-compiler.5.1.1/lib/coq-core/plugins/ssreflect -I /home/bench/.opam/ocaml[...] # (cd _build/default/theories/Init && /home/bench/.opam/ocaml-base-compiler.5.1.1/bin/coqc -noinit -boot -R ../. Coq -I /home/bench/.opam/ocaml-base-compiler.5.1.1/lib/coq-core/plugins/number_string_notation -I /home/bench/.opam/ocaml-base-compiler.5.1.1/lib/coq-core/plugins/zify -I /home/bench/.opam/ocaml-base-compiler.5.1.1/lib/coq-core/plugins/tauto -I /home/bench/.opam/ocaml-base-compiler.5[...] # Fatal error: Not enough heap memory to reserve minor heaps <><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><> +- The following actions failed | - build coq-stdlib 8.17.1 +- +- The following changes have been performed | - remove coq-stdlib 8.17.1 | - downgrade dune 3.12.1 to 3.7.1 | - recompile coq-core 8.17.1 | - recompile coqide-server 8.17.1 | - install astring 0.8.5 | - install base64 3.5.1 | - install bos 0.2.1 | - install cmdliner 1.2.0 | - install conf-git 1.1 | - install cppo 1.6.9 | - install csexp 1.5.2 | - install cudf 0.10 | - install dose3 7.0.0 | - install dune-private-libs 3.12.1 | - install dune-site 3.12.1 | - install dyn 3.12.1 | - install extlib 1.7.9 | - install fmt 0.9.0 | - install fpath 0.7.3 | - install logs 0.7.0 | - install mccs 1.1+17 | - install ocamlbuild 0.14.3 | - install ocamlgraph 2.1.0 | - install opam-client 2.1.5 | - install opam-core 2.1.5 | - install opam-file-format 2.1.6 | - install opam-format 2.1.5 | - install opam-repository 2.1.5 | - install opam-solver 2.1.5 | - install opam-state 2.1.5 | - install ordering 3.12.1 | - install pp 1.2.0 | - install re 1.11.0 | - install rresult 0.7.0 | - install seq base | - install stdlib-shims 0.3.0 | - install stdune 3.12.1 | - install topkg 1.0.7 +- # Run eval $(opam env) to update the current shell environment The former state can be restored with: /usr/local/bin/opam switch import "/home/bench/.opam/ocaml-base-compiler.5.1.1/.opam-switch/backup/state-20231228224609.export" The middle of the output is truncated (maximum 20000 characters)
true
No files were installed.
true