# 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: "A dummy implementation of Tactician"
description: """
This package acts as a stand-in for the Tactician plugin (`coq-tactician`).
It provides short files that replicate Tactician's tactics without actually
doing much. This is useful when you have a development that uses Tactician
that you want to package up. In most situations, it is not a good idea to
have your package directly depend on `coq-tactician`. Instead you should load
Tactician through your `coqrc` file. In order for your package to be compilable
by others, your package can depend on this package. Just add
`From Tactician Require Import Ltac1Dummy` in your development and you are good
to go."""
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-dummy/issues"
depends: [
"coq-core"
"dune" {>= "3.5" & < "3.8~"}
"odoc" {with-doc}
]
build: [
["dune" "subst"] {dev}
[
"dune"
"build"
"-p"
name
"-j"
jobs
"@install"
"@runtest" {with-test}
"@doc" {with-doc}
]
]
dev-repo: "git+https://github.com/coq-tactician/coq-tactician-dummy.git"
tags: [
"keyword:tactic-learning"
"keyword:machine-learning"
"keyword:automation"
"keyword:proof-synthesis"
"category:Miscellaneous/Coq Extensions"
"logpath:Tactician"
]
url {
src: "https://github.com/coq-tactician/coq-tactician-dummy/archive/1.0-beta2-8.17.tar.gz"
checksum: "sha512=301266149d28b93bb8a747e170b6bdf5bca47ae5b21e9f31d652916c35d749f651ea2b472079db40e02d90a1b1e8137c3e956f9922f9d421a4751f20f0f5e364"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-tactician-dummy.1.0~beta2+8.17 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-dummy.1.0~beta2+8.17 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
- recompile coq-core dev [uses dune]
- recompile coqide-server dev [uses dune]
- recompile coq-stdlib dev [uses dune]
===== 3 to recompile | 1 to downgrade =====
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
-> retrieved coq-core.dev (no changes)
-> retrieved coqide-server.dev (no changes)
-> retrieved coq-stdlib.dev (no changes)
-> retrieved dune.3.7.1 (https://opam.ocaml.org/cache)
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-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/Compat/Coq818.vos
- lib/coq/user-contrib/Ltac2/Compat/Coq818.vo
- lib/coq/user-contrib/Ltac2/Compat/Coq818.v
- lib/coq/user-contrib/Ltac2/Compat/Coq818.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/theories/ssr/ssrsetoid.glob
- lib/coq/theories/ssr/ssrfun.vos
- lib/coq/theories/ssr/ssrfun.vo
- lib/coq/theories/ssr/ssrfun.v
- lib/coq/theories/ssr/ssrfun.glob
- lib/coq/theories/ssr/ssreflect.vos
- lib/coq/theories/ssr/ssreflect.vo
- lib/coq/theories/ssr/ssreflect.v
- lib/coq/theories/ssr/ssreflect.glob
- lib/coq/theories/ssr/ssrclasses.vos
- lib/coq/theories/ssr/ssrclasses.vo
- lib/coq/theories/ssr/ssrclasses.v
- lib/coq/theories/ssr/ssrclasses.glob
- lib/coq/theories/ssr/ssrbool.vos
- lib/coq/theories/ssr/ssrbool.vo
- lib/coq/theories/ssr/ssrbool.v
- lib/coq/theories/ssr/ssrbool.glob
- lib/coq/theories/setoid_ring/ZArithRing.vos
- lib/coq/theories/setoid_ring/ZArithRing.vo
- lib/coq/theories/setoid_ring/ZArithRing.v
- lib/coq/theories/setoid_ring/ZArithRing.glob
- lib/coq/theories/setoid_ring/Rings_Z.vos
- lib/coq/theories/setoid_ring/Rings_Z.vo
- lib/coq/theories/setoid_ring/Rings_Z.v
- lib/coq/theories/setoid_ring/Rings_Z.glob
- lib/coq/theories/setoid_ring/Rings_R.vos
- lib/coq/theories/setoid_ring/Rings_R.vo
- lib/coq/theories/setoid_ring/Rings_R.v
- lib/coq/theories/setoid_ring/Rings_R.glob
- lib/coq/theories/setoid_ring/Rings_Q.vos
- lib/coq/theories/setoid_ring/Rings_Q.vo
- lib/coq/theories/setoid_ring/Rings_Q.v
- lib/coq/theories/setoid_ring/Rings_Q.glob
- lib/coq/theories/setoid_ring/Ring_theory.vos
- lib/coq/theories/setoid_ring/Ring_theory.vo
- lib/coq/theories/setoid_ring/Ring_theory.v
- lib/coq/theories/setoid_ring/Ring_theory.glob
- lib/coq/theories/setoid_ring/Ring_tac.vos
- lib/coq/theories/setoid_ring/Ring_tac.vo
- lib/coq/theories/setoid_ring/Ring_tac.v
- lib/coq/theories/setoid_ring/Ring_tac.glob
- l
[...] truncated
mpat/Coq818.glob
- lib/coq/theories/Compat/Coq817.vos
- lib/coq/theories/Compat/Coq817.vo
- lib/coq/theories/Compat/Coq817.v
- lib/coq/theories/Compat/Coq817.glob
- lib/coq/theories/Compat/AdmitAxiom.vos
- lib/coq/theories/Compat/AdmitAxiom.vo
- lib/coq/theories/Compat/AdmitAxiom.v
- lib/coq/theories/Compat/AdmitAxiom.glob
- lib/coq/theories/Classes/SetoidTactics.vos
- lib/coq/theories/Classes/SetoidTactics.vo
- lib/coq/theories/Classes/SetoidTactics.v
- lib/coq/theories/Classes/SetoidTactics.glob
- lib/coq/theories/Classes/SetoidDec.vos
- lib/coq/theories/Classes/SetoidDec.vo
- lib/coq/theories/Classes/SetoidDec.v
- lib/coq/theories/Classes/SetoidDec.glob
- lib/coq/theories/Classes/SetoidClass.vos
- lib/coq/theories/Classes/SetoidClass.vo
- lib/coq/theories/Classes/SetoidClass.v
- lib/coq/theories/Classes/SetoidClass.glob
- lib/coq/theories/Classes/RelationPairs.vos
- lib/coq/theories/Classes/RelationPairs.vo
- lib/coq/theories/Classes/RelationPairs.v
- lib/coq/theories/Classes/RelationPairs.glob
- lib/coq/theories/Classes/RelationClasses.vos
- lib/coq/theories/Classes/RelationClasses.vo
- lib/coq/theories/Classes/RelationClasses.v
- lib/coq/theories/Classes/RelationClasses.glob
- lib/coq/theories/Classes/Morphisms_Relations.vos
- lib/coq/theories/Classes/Morphisms_Relations.vo
- lib/coq/theories/Classes/Morphisms_Relations.v
- lib/coq/theories/Classes/Morphisms_Relations.glob
- lib/coq/theories/Classes/Morphisms_Prop.vos
- lib/coq/theories/Classes/Morphisms_Prop.vo
- lib/coq/theories/Classes/Morphisms_Prop.v
- lib/coq/theories/Classes/Morphisms_Prop.glob
- lib/coq/theories/Classes/Morphisms.vos
- lib/coq/theories/Classes/Morphisms.vo
- lib/coq/theories/Classes/Morphisms.v
- lib/coq/theories/Classes/Morphisms.glob
- lib/coq/theories/Classes/Init.vos
- lib/coq/theories/Classes/Init.vo
- lib/coq/theories/Classes/Init.v
- lib/coq/theories/Classes/Init.glob
- lib/coq/theories/Classes/Equivalence.vos
- lib/coq/theories/Classes/Equivalence.vo
- lib/coq/theories/Classes/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 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-3351-7a0d88.env
# output-file ~/.opam/log/coq-stdlib-3351-7a0d88.out
### output ###
# [...]
# 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
# File "theories/dune", line 3481, characters 1-1671:
# 3481 | (rule
# 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
<><> 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
+-
# 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-20240114042614.export"
The middle of the output is truncated (maximum 20000 characters)
trueNo files were installed.
true