# 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 dev The Coq Proof Assistant
coq-core dev The Coq Proof Assistant -- Core Binaries and Tools
coq-stdlib dev The Coq Proof Assistant -- Standard Library
coqide-server dev The Coq Proof Assistant, XML protocol server
dune 3.12.2 Fast, portable, and opinionated build system
ocaml 5.0.0 The OCaml compiler (virtual package)
ocaml-base-compiler 5.0.0 Official release 5.0.0
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>"]
homepage: "https://coq-tactician.github.io"
bug-reports: "https://github.com/coq-tactician/coq-tactician/issues"
license: "MIT"
depends: [
"dune" {>= "3.5" & < "3.8~"}
"ocaml" {>= "4.08"}
"dune-site" {>= "2.9.1"}
"opam-client" {>= "2.1.0"}
"cmdliner" {>= "1.1.0"}
"coq-core" {= "dev"}
"coq-stdlib" {= "dev" & with-test}
"conf-git"
"bos" {>= "0.2.1"}
"coq-tactician-dummy" {= "8.17.dev" & 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: "git+https://github.com/coq-tactician/coq-tactician.git#coqdev"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-tactician.dev coq.devDry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
trueopam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-tactician.dev coq.dev# 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 dev The Coq Proof Assistant
coq-core dev The Coq Proof Assistant -- Core Binaries and Tools
coq-stdlib dev The Coq Proof Assistant -- Standard Library
coqide-server dev The Coq Proof Assistant, XML protocol server
dune 3.12.2 Fast, portable, and opinionated build system
ocaml 5.0.0 The OCaml compiler (virtual package)
ocaml-base-compiler 5.0.0 Official release 5.0.0
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:
- downgrade dune 3.12.2 to 3.7.1
- install ocamlbuild 0.14.3
- install cmdliner 1.2.0
- install seq base
- install conf-git 1.1
- install stdlib-shims 0.3.0
- install pp 1.2.0
- install ordering 3.12.2
- 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 dev [uses dune]
- install topkg 1.0.7
- install re 1.11.0
- install ocamlgraph 2.1.0
- install dyn 3.12.2
- install extlib 1.7.9
- recompile coqide-server dev [uses dune]
- recompile coq-stdlib dev [uses dune]
- install rresult 0.7.0
- install fmt 0.9.0
- install astring 0.8.5
- install opam-core 2.1.5
- install stdune 3.12.2
- install cudf 0.10
- install logs 0.7.0
- install fpath 0.7.3
- install opam-format 2.1.5
- install dune-private-libs 3.12.2
- install mccs 1.1+17
- install dose3 7.0.0
- install bos 0.2.1
- install opam-repository 2.1.5
- install dune-site 3.12.2
- 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 base64.3.5.1 (https://opam.ocaml.org/cache)
-> retrieved bos.0.2.1 (https://opam.ocaml.org/cache)
-> retrieved astring.0.8.5 (https://opam.ocaml.org/cache)
-> retrieved cmdliner.1.2.0 (https://opam.ocaml.org/cache)
-> installed conf-git.1.1
-> retrieved coq-core.dev (git+https://github.com/coq/coq.git#master)
-> 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.3.7.1 (https://opam.ocaml.org/cache)
-> retrieved dune-private-libs.3.12.2 (cached)
-> retrieved coqide-server.dev (git+https://github.com/coq/coq.git#master)
-> retrieved coq-stdlib.dev (git+https://github.com/coq/coq.git#master)
-> 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 dune-site.3.12.2 (cached)
-> retrieved dyn.3.12.2 (cached)
-> retrieved logs.0.7.0 (https://opam.ocaml.org/cache)
-> retrieved mccs.1.1+17 (https://opam.ocaml.org/cache)
-> installed cmdliner.1.2.0
-> retrieved ocamlbuild.0.14.3 (https://opam.ocaml.org/cache)
-> retrieved ocamlgraph.2.1.0 (https://opam.ocaml.org/cache)
-> retrieved opam-client.2.1.5 (https://opam.ocaml.org/cache)
-> retrieved opam-format.2.1.5 (cached)
-> retrieved opam-file-format.2.1.6 (https://opam.ocaml.org/cache)
-> retrieved opam-repository.2.1.5 (cached)
-> retrieved opam-solver.2.1.5 (cached)
-> retrieved opam-state.2.1.5 (cached)
-> retrieved opam-core.2.1.5 (https://opam.ocaml.org/cache)
-> retrieved pp.1.2.0 (https://opam.ocaml.org/cache)
-> retrieved re.1.11.0 (https://opam.ocaml.org/cache)
-> installed seq.base
-> 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 ordering.3.12.2 (cached)
-> retrieved stdune.3.12.2 (cached)
-> installed ocamlbuild.0.14.3
-> installed topkg.1.0.7
-> installed rresult.0.7.0
While removing coq-stdlib.dev: these files have been modified since installation:
- lib/coq/user-contrib/Ltac2/Unification.vos
- lib/coq/user-contrib/Ltac2/Unification.vo
- lib/coq/user-contrib/Ltac2/Unification.v
- lib/coq/user-contrib/Ltac2/Unification.glob
- 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/TransparentState.vos
- lib/coq/user-contrib/Ltac2/TransparentState.vo
- lib/coq/user-contrib/Ltac2/TransparentState.v
- lib/coq/user-contrib/Ltac2/TransparentState.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/Ref.vos
- lib/coq/user-contrib/Ltac2/Ref.vo
- lib/coq/user-contrib/Ltac2/Ref.v
- lib/coq/user-contrib/Ltac2/Ref.glob
- lib/coq/user-contrib/Ltac2/RedFlags.vos
- lib/coq/user-contrib/Ltac2/RedFlags.vo
- lib/coq/user-contrib/Ltac2/RedFlags.v
- lib/coq/user-contrib/Ltac2/RedFlags.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/Lazy.vos
- lib/coq/user-contrib/Ltac2/Lazy.vo
- lib/coq/user-contrib/Ltac2/Lazy.v
- lib/coq/user-contrib/Ltac2/Lazy.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/FSet.vos
- lib/coq/user-contrib/Ltac2/FSet.vo
- lib/coq/user-contrib/Ltac2/FSet.v
- lib/coq/user-contrib/Ltac2/FSet.glob
- lib/coq/user-contrib/Ltac2/FMap.vos
- lib/coq/user-contrib/Ltac2/FMap.vo
- lib/coq/user-contrib/Ltac2/FMap.v
- lib/coq/user-contrib/Ltac2/FMap.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-
[...] truncated
sses/Equivalence.v
- lib/coq/theories/Classes/Equivalence.glob
- lib/coq/theories/Classes/EquivDec.vos
- lib/coq/theories/Classes/EquivDec.vo
- lib/coq/theories/Classes/EquivDec.v
- lib/coq/theories/Classes/EquivDec.glob
- lib/coq/theories/Classes/DecidableClass.vos
- lib/coq/theories/Classes/DecidableClass.vo
- lib/coq/theories/Classes/DecidableClass.v
- lib/coq/theories/Classes/DecidableClass.glob
- lib/coq/theories/Classes/CRelationClasses.vos
- lib/coq/theories/Classes/CRelationClasses.vo
- lib/coq/theories/Classes/CRelationClasses.v
- lib/coq/theories/Classes/CRelationClasses.glob
- lib/coq/theories/Classes/CMorphisms.vos
- lib/coq/theories/Classes/CMorphisms.vo
- lib/coq/theories/Classes/CMorphisms.v
- lib/coq/theories/Classes/CMorphisms.glob
- lib/coq/theories/Classes/CEquivalence.vos
- lib/coq/theories/Classes/CEquivalence.vo
- lib/coq/theories/Classes/CEquivalence.v
- lib/coq/theories/Classes/CEquivalence.glob
- lib/coq/theories/Bool/Zerob.vos
- lib/coq/theories/Bool/Zerob.vo
- lib/coq/theories/Bool/Zerob.v
- lib/coq/theories/Bool/Zerob.glob
- lib/coq/theories/Bool/Sumbool.vos
- lib/coq/theories/Bool/Sumbool.vo
- lib/coq/theories/Bool/Sumbool.v
- lib/coq/theories/Bool/Sumbool.glob
- lib/coq/theories/Bool/IfProp.vos
- lib/coq/theories/Bool/IfProp.vo
- lib/coq/theories/Bool/IfProp.v
- lib/coq/theories/Bool/IfProp.glob
- lib/coq/theories/Bool/DecBool.vos
- lib/coq/theories/Bool/DecBool.vo
- lib/coq/theories/Bool/DecBool.v
- lib/coq/theories/Bool/DecBool.glob
- lib/coq/theories/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/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/Factorial.vos
- lib/coq/theories/Arith/Factorial.vo
- lib/coq/theories/Arith/Factorial.v
- lib/coq/theories/Arith/Factorial.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/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_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.dev
-> removed coqide-server.dev
-> removed coq-core.dev
-> removed dune.3.12.2
-> installed dune.3.7.1
-> installed astring.0.8.5
-> installed fmt.0.9.0
-> installed base64.3.5.1
-> installed csexp.1.5.2
-> installed cppo.1.6.9
-> installed fpath.0.7.3
-> installed logs.0.7.0
-> installed opam-file-format.2.1.6
-> installed extlib.1.7.9
-> installed pp.1.2.0
-> installed cudf.0.10
-> installed bos.0.2.1
-> installed ordering.3.12.2
-> installed stdlib-shims.0.3.0
-> installed re.1.11.0
-> installed dyn.3.12.2
-> installed ocamlgraph.2.1.0
-> installed dose3.7.0.0
-> installed mccs.1.1+17
-> installed stdune.3.12.2
-> installed dune-private-libs.3.12.2
-> installed dune-site.3.12.2
-> installed opam-core.2.1.5
-> installed opam-format.2.1.5
-> installed opam-repository.2.1.5
-> installed opam-solver.2.1.5
-> installed opam-state.2.1.5
-> installed opam-client.2.1.5
-> installed coq-core.dev
[ERROR] The compilation of coq-stdlib.dev failed at "dune build -p coq-stdlib -j 4 --promote-install-files=false @install".
-> installed coqide-server.dev
#=== ERROR while compiling coq-stdlib.dev =====================================#
# context 2.1.5 | linux/x86_64 | ocaml-base-compiler.5.0.0 | file:///home/bench/run/opam-coq-archive/core-dev
# path ~/.opam/ocaml-base-compiler.5.0.0/.opam-switch/build/coq-stdlib.dev
# command ~/.opam/opam-init/hooks/sandbox.sh build dune build -p coq-stdlib -j 4 --promote-install-files=false @install
# exit-code 1
# env-file ~/.opam/log/coq-stdlib-23476-24e13a.env
# output-file ~/.opam/log/coq-stdlib-23476-24e13a.out
### output ###
# [...]
# 3482 | (targets Notations.timing Notations.glob Notations.vos Notations.vo)
# 3483 | (deps )
# 3484 | (action (chdir ../../. (run coqc -noinit -boot -R theories Coq -I /home/bench/.opam/ocaml-base-compiler.5.0.0/lib/coq-core/plugins/number_string_notation -I /home/bench/.opam/ocaml-base-compiler.5.0.0/lib/coq-core/plugins/zify -I /home/bench/.opam/ocaml-base-compiler.5.0.0/lib/coq-core/plugins/tauto -I /home/bench/.opam/ocaml-base-compiler.5.0.0/lib/coq-core/plugins/ssreflect -I /hom[...]
# (cd _build/default && /home/bench/.opam/ocaml-base-compiler.5.0.0/bin/coqc -noinit -boot -R theories Coq -I /home/bench/.opam/ocaml-base-compiler.5.0.0/lib/coq-core/plugins/number_string_notation -I /home/bench/.opam/ocaml-base-compiler.5.0.0/lib/coq-core/plugins/zify -I /home/bench/.opam/ocaml-base-compiler.5.0.0/lib/coq-core/plugins/tauto -I /home/bench/.opam/ocaml-base-compiler.5.0.0/lib/c[...]
# Fatal error: Not enough heap memory to reserve minor heaps
# File "theories/dune", line 3465, characters 1-1727:
# 3465 | (rule
# 3466 | (targets Ltac.timing Ltac.glob Ltac.vos Ltac.vo)
# 3467 | (deps /home/bench/.opam/ocaml-base-compiler.5.0.0/lib/coq-core/plugins/ltac/ltac_plugin.cmxs)
# 3468 | (action (chdir ../../. (run coqc -noinit -boot -R theories Coq -I /home/bench/.opam/ocaml-base-compiler.5.0.0/lib/coq-core/plugins/number_string_notation -I /home/bench/.opam/ocaml-base-compiler.5.0.0/lib/coq-core/plugins/zify -I /home/bench/.opam/ocaml-base-compiler.5.0.0/lib/coq-core/plugins/tauto -I /home/bench/.opam/ocaml-base-compiler.5.0.0/lib/coq-core/plugins/ssreflect -I /hom[...]
# (cd _build/default && /home/bench/.opam/ocaml-base-compiler.5.0.0/bin/coqc -noinit -boot -R theories Coq -I /home/bench/.opam/ocaml-base-compiler.5.0.0/lib/coq-core/plugins/number_string_notation -I /home/bench/.opam/ocaml-base-compiler.5.0.0/lib/coq-core/plugins/zify -I /home/bench/.opam/ocaml-base-compiler.5.0.0/lib/coq-core/plugins/tauto -I /home/bench/.opam/ocaml-base-compiler.5.0.0/lib/c[...]
# Fatal error: Not enough heap memory to reserve minor heaps
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build coq-stdlib dev
+-
+- The following changes have been performed
| - remove coq-stdlib dev
| - downgrade dune 3.12.2 to 3.7.1
| - recompile coq-core dev
| - recompile coqide-server dev
| - 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.2
| - install dune-site 3.12.2
| - install dyn 3.12.2
| - 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.2
| - 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.2
| - 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.0.0/.opam-switch/backup/state-20240115211201.export"
The middle of the output is truncated (maximum 20000 characters)
trueNo files were installed.
true