# 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.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>"]
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"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-tactician.1.0~beta2.1+8.17 coq.8.17.1Dry 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.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.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 8.17.1 [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 8.17.1 [uses dune]
- recompile coq-stdlib 8.17.1 [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 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.2 (cached)
-> retrieved dune.3.7.1 (https://opam.ocaml.org/cache)
-> retrieved dune-site.3.12.2 (cached)
-> retrieved dyn.3.12.2 (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 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)
-> retrieved rresult.0.7.0 (https://opam.ocaml.org/cache)
-> installed cmdliner.1.2.0
-> installed seq.base
-> 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
-> installed fmt.0.9.0
-> installed astring.0.8.5
-> installed fpath.0.7.3
-> installed logs.0.7.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/
[...] truncated
ol/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/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.2
-> installed dune.3.7.1
-> installed bos.0.2.1
-> installed csexp.1.5.2
-> installed base64.3.5.1
-> installed cppo.1.6.9
-> installed opam-file-format.2.1.6
-> installed pp.1.2.0
-> installed ordering.3.12.2
-> installed stdlib-shims.0.3.0
-> installed extlib.1.7.9
-> installed re.1.11.0
-> installed cudf.0.10
-> installed dyn.3.12.2
-> installed ocamlgraph.2.1.0
-> installed dose3.7.0.0
-> installed stdune.3.12.2
-> installed mccs.1.1+17
-> installed dune-private-libs.3.12.2
-> installed opam-core.2.1.5
-> installed dune-site.3.12.2
-> 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.8.17.1
-> 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".
#=== ERROR while compiling coq-stdlib.8.17.1 ==================================#
# context 2.1.5 | linux/x86_64 | ocaml-base-compiler.5.0.0 | https://opam.ocaml.org#e2c19b40
# path ~/.opam/ocaml-base-compiler.5.0.0/.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-23882-4e5b21.env
# output-file ~/.opam/log/coq-stdlib-23882-4e5b21.out
### output ###
# [...]
# 3000 | (targets Ltac.glob Ltac.vos Ltac.vo)
# 3001 | (deps /home/bench/.opam/ocaml-base-compiler.5.0.0/lib/coq-core/plugins/ltac/ltac_plugin.cmxs)
# 3002 | (action (run coqc -noinit -boot -R ../. 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 /home/bench/.opam/ocaml[...]
# (cd _build/default/theories/Init && /home/bench/.opam/ocaml-base-compiler.5.0.0/bin/coqc -noinit -boot -R ../. 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[...]
# Fatal error: Not enough heap memory to reserve minor heaps
# File "theories/dune", line 3014, characters 1-1509:
# 3014 | (rule
# 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.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 /home/bench/.opam/ocaml[...]
# (cd _build/default/theories/Init && /home/bench/.opam/ocaml-base-compiler.5.0.0/bin/coqc -noinit -boot -R ../. 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[...]
# 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.2 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.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-20240112010602.export"
The middle of the output is truncated (maximum 20000 characters)
trueNo files were installed.
true