# 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.18.0 The Coq Proof Assistant
coq-core 8.18.0 The Coq Proof Assistant -- Core Binaries and Tools
coq-stdlib 8.18.0 The Coq Proof Assistant -- Standard Library
coqide-server 8.18.0 The Coq Proof Assistant, XML protocol server
dune 3.13.0 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 library of Coq definitions, theorems, and tactics"
description:
"A collection of theories and plugins that may be useful in other Coq developments."
maintainer: "gmalecha@gmail.com"
authors: "Gregory Malecha"
license: "BSD-2-Clause"
tags: "logpath:ExtLib"
homepage: "https://github.com/coq-community/coq-ext-lib"
bug-reports: "https://github.com/coq-community/coq-ext-lib/issues"
depends: [
"ocaml"
"coq" {>= "8.8"}
]
build: [make "-j%{jobs}%" "theories"]
run-test: [make "-j%{jobs}%" "examples"]
install: [make "install"]
dev-repo: "git+https://github.com/coq-community/coq-ext-lib.git"
url {
src: "https://github.com/coq-community/coq-ext-lib/archive/v0.11.5.tar.gz"
checksum: [
"md5=054577e702e9cf596f37aa28b0b0394c"
"sha512=84b79097c9ad6823024a0af875c07389accb597337527f905f067c7fa39a7c170239edb68d2a45b102714b6f6860cc7a7f937340824a688df19b4c35aa2e075c"
]
}
trueDry install with the current Coq version:
opam install -y --show-action coq-ext-lib.0.11.5 coq.8.18.0Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
trueopam list; echo; timeout 4h opam install -y --deps-only coq-ext-lib.0.11.5 coq.8.18.0opam list; echo; timeout 4h opam install -y -v coq-ext-lib.0.11.5 coq.8.18.0# 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.18.0 The Coq Proof Assistant
coq-core 8.18.0 The Coq Proof Assistant -- Core Binaries and Tools
coq-stdlib 8.18.0 The Coq Proof Assistant -- Standard Library
coqide-server 8.18.0 The Coq Proof Assistant, XML protocol server
dune 3.13.0 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
[NOTE] Package coq is already installed (current version is 8.18.0).
The following actions will be performed:
- install coq-ext-lib 0.11.5
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing 1/3: [coq-ext-lib.0.11.5: http]
Processing 1/3:
-> retrieved coq-ext-lib.0.11.5 (https://github.com/coq-community/coq-ext-lib/archive/v0.11.5.tar.gz)
Processing 2/3: [coq-ext-lib: make theories]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "make" "-j4" "theories" (CWD=/home/bench/.opam/ocaml-base-compiler.5.0.0/.opam-switch/build/coq-ext-lib.0.11.5)
- coq_makefile -f _CoqProject -o Makefile.coq
- make -f Makefile.coq
- make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.5.0.0/.opam-switch/build/coq-ext-lib.0.11.5'
- COQDEP VFILES
- COQC theories/Core/RelDec.v
- COQC theories/Tactics/Injection.v
- COQC theories/Tactics/Forward.v
- COQC theories/Core/Any.v
- COQC theories/Core/EquivDec.v
- COQC theories/Core/Decision.v
- COQC theories/Structures/BinOps.v
- COQC theories/Structures/CoFunctor.v
- COQC theories/Structures/CoMonad.v
- COQC theories/Data/PreFun.v
- COQC theories/Data/Unit.v
- COQC theories/Data/Bool.v
- COQC theories/Data/Checked.v
- COQC theories/Data/Eq/UIP_trans.v
- COQC theories/Data/ListNth.v
- COQC theories/Data/LazyList.v
- COQC theories/Data/ListFirstnSkipn.v
- COQC theories/Data/N.v
- COQC theories/Data/Positive.v
- File "./theories/Data/ListNth.v", line 17, characters 24-33:
- Warning: Notation lt_S_n is deprecated since 8.16.
- The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
- [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
- File "./theories/Data/ListNth.v", line 17, characters 24-33:
- Warning: Notation lt_S_n is deprecated since 8.16.
- The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
- [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
- File "./theories/Data/ListNth.v", line 26, characters 23-32:
- Warning: Notation Le.le_S_n is deprecated since 8.16.
- The Arith.Le file is obsolete. Use Nat.succ_le_mono instead.
- [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
- File "./theories/Data/ListNth.v", line 26, characters 23-32:
- Warning: Notation Le.le_S_n is deprecated since 8.16.
- The Arith.Le file is obsolete. Use Nat.succ_le_mono instead.
- [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
- File "./theories/Data/ListNth.v", line 48, characters 24-33:
- Warning: Notation Le.le_S_n is deprecated since 8.16.
- The Arith.Le file is obsolete. Use Nat.succ_le_mono instead.
- [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
- File "./theories/Data/ListNth.v", line 48, characters 24-33:
- Warning: Notation Le.le_S_n is deprecated since 8.16.
- The Arith.Le file is obsolete. Use Nat.succ_le_mono instead.
- [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
- File "./theories/Data/ListNth.v", line 55, characters 12-25:
- Warning: Notation plus_0_r is deprecated since 8.16.
- The Arith.Plus file is obsolete. Use Nat.add_0_r instead.
- [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
- File "./theories/Data/ListNth.v", line 55, characters 12-25:
- Warning: Notation plus_0_r is deprecated since 8.16.
- The Arith.Plus file is obsolete. Use Nat.add_0_r instead.
- [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
- File "./theories/Data/ListNth.v", line 55, characters 12-25:
- Warning: Notation plus_0_r is deprecated since 8.16.
- The Arith.Plus file is obsolete. Use Nat.add_0_r instead.
- [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
- File "./theories/Data/ListNth.v", line 56, characters 15-32:
- Warning: Notation plus_Snm_nSm is deprecated since 8.16.
- The Arith.Plus file is obsolete. Use Nat.add_succ_comm instead.
- [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
- File "./theories/Data/ListNth.v", line 56, characters 15-32:
- Warning: Notation plus_Snm_nSm is deprecated since 8.16.
- The Arith.Plus file is obsolete. Use Nat.add_succ_comm instead.
- [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
- File "./theories/Data/ListNth.v", line 56, characters 15-32:
- Warning: Notation plus_Snm_nSm is deprecated since 8.16.
- The Arith.Plus file is obsolete. Use Nat.add_succ_comm instead.
- [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
- File "./theories/Data/ListNth.v", line 64, characters 19-28:
- Warning: Notation Le.le_0_n is deprecated since 8.16.
- The Arith.Le file is obsolete. Use Nat.le_0_l instead.
- [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
- File "./theories/Data/ListNth.v", line 64, characters 19-28:
- Warning: Notation Le.le_0_n is deprecated since 8.16.
- The Arith.Le file is obsolete. Use Nat.le_0_l instead.
- [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
- File "./theories/Data/ListNth.v", line 66, characters 21-30:
- Warning: Notation Le.le_n_S is deprecated since 8.16.
- The Arith.Le file is obsolete. Use Nat.succ_le_mono instead.
- [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
- File "./theories/Data/ListNth.v", line 66, characters 21-30:
- Warning: Notation Le.le_n_S is deprecated since 8.16.
- The Arith.Le file is obsolete. Use Nat.succ_le_mono instead.
- [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
- File "./theories/Data/ListNth.v", line 75, characters 12-22:
- Warning: Notation lt_0_Sn is deprecated since 8.16.
- The Arith.Lt file is obsolete. Use Nat.lt_0_succ instead.
- [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
- File "./theories/Data/ListNth.v", line 75, characters 12-22:
- Warning: Notation lt_0_Sn is deprecated since 8.16.
- The Arith.Lt file is obsolete. Use Nat.lt_0_succ instead.
- [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
- File "./theories/Data/ListNth.v", line 76, characters 12-21:
- Warning: Notation lt_n_S is deprecated since 8.16.
- The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
- [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
- File "./theories/Data/ListNth.v", line 76, characters 12-21:
- Warning: Notation lt_n_S is deprecated since 8.16.
- The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
- [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
- COQC theories/Data/Prop.v
- COQC theories/Data/Stream.v
- COQC theories/Data/Z.v
- COQC theories/Data/PPair.v
- COQC theories/Programming/Injection.v
- COQC theories/Programming/Eqv.v
- COQC theories/Programming/Le.v
- COQC theories/Programming/With.v
- File "./theories/Programming/Eqv.v", line 8, characters 0-77:
- Warning: A coercion will be introduced instead of an instance in future
- versions when using ':>' in 'Class' declarations. Replace ':>' with '::' (or
- use '#[global] Existing Instance field.' for compatibility with Coq < 8.18).
- Beware that the default locality for '::' is #[export], as opposed to
- #[global] for ':>' currently. Add an explicit #[global] attribute to the
- field if you need to keep the current behavior. For example: "Class foo := {
- #[global] field :: bar }."
- [future-coercion-class-field,deprecated-since-8.17,deprecated,default]
- COQC theories/Recur/Facts.v
- File "./theories/Programming/Le.v", line 27, characters 0-71:
- Warning: A coercion will be introduced instead of an instance in future
- versions when using ':>' in 'Class' declarations. Replace ':>' with '::' (or
- use '#[global] Existing Instance field.' for compatibility with Coq < 8.18).
- Beware that the default locality for '::' is #[export], as opposed to
-
[...] truncated
v
- COQC theories/Structures/Functor.v
- COQC theories/Structures/CoMonadLaws.v
- COQC theories/Structures/Monoid.v
- File "./theories/Structures/Monoid.v", line 16, characters 2-229:
- Warning: A coercion will be introduced instead of an instance in future
- versions when using ':>' in 'Class' declarations. Replace ':>' with '::' (or
- use '#[global] Existing Instance field.' for compatibility with Coq < 8.18).
- Beware that the default locality for '::' is #[export], as opposed to
- #[global] for ':>' currently. Add an explicit #[global] attribute to the
- field if you need to keep the current behavior. For example: "Class foo := {
- #[global] field :: bar }."
- [future-coercion-class-field,deprecated-since-8.17,deprecated,default]
- COQC theories/Data/Eq.v
- COQC theories/Recur/Relation.v
- COQC theories/Tactics/Cases.v
- COQC theories/Structures/EqDep.v
- COQC theories/Core/CmpDec.v
- COQC theories/Structures/Applicative.v
- COQC theories/Structures/Foldable.v
- COQC theories/Structures/Sets.v
- COQC theories/Data/Char.v
- COQC theories/Data/Nat.v
- COQC theories/Data/Pair.v
- COQC theories/Data/Sum.v
- COQC theories/Data/POption.v
- File "./theories/Data/Nat.v", line 12, characters 13-26:
- Warning: Notation EqNat.beq_nat is deprecated since 8.16.
- Use Nat.eqb instead.
- [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
- COQC theories/Tactics/Equality.v
- File "./theories/Data/Nat.v", line 30, characters 28-50:
- Warning: Notation EqNat.beq_nat_true_iff is deprecated since 8.16.
- Use Nat.eqb_eq instead.
- [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
- File "./theories/Data/Nat.v", line 30, characters 28-50:
- Warning: Notation EqNat.beq_nat_true_iff is deprecated since 8.16.
- Use Nat.eqb_eq instead.
- [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
- COQC theories/Tactics/EqDep.v
- COQC theories/Data/Fun.v
- COQC theories/Structures/Monad.v
- COQC theories/Structures/Traversable.v
- COQC theories/Data/PList.v
- COQC theories/Structures/FunctorLaws.v
- File "./theories/Structures/Monad.v", line 56, characters 2-39:
- Warning: Declaring a scope implicitly is deprecated; use in advance an
- explicit "Declare Scope monad_scope.".
- [undeclared-scope,deprecated-since-8.10,deprecated,default]
- COQC theories/Structures/Reducible.v
- COQC theories/Structures/MonadExc.v
- COQC theories/Structures/MonadCont.v
- COQC theories/Structures/MonadFix.v
- COQC theories/Structures/MonadZero.v
- COQC theories/Structures/MonadPlus.v
- COQC theories/Structures/MonadReader.v
- COQC theories/Structures/MonadWriter.v
- COQC theories/Structures/MonadState.v
- COQC theories/Structures/MonadTrans.v
- COQC theories/Data/Fin.v
- COQC theories/Data/SigT.v
- COQC theories/Data/Option.v
- COQC theories/Data/Lazy.v
- COQC theories/Data/List.v
- File "./theories/Data/Fin.v", line 103, characters 2-29:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./theories/Data/Fin.v", line 106, characters 2-29:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- COQC theories/Data/String.v
- COQC theories/Data/Monads/IdentityMonad.v
- COQC theories/Data/Monads/ContMonad.v
- COQC theories/Tactics.v
- COQC theories/Structures/Maps.v
- COQC theories/Structures/Monads.v
- File "./theories/Data/String.v", line 57, characters 2-122:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./theories/Data/String.v", line 57, characters 2-122:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./theories/Data/String.v", line 97, characters 11-19:
- Warning: Notation neq_0_lt is deprecated since 8.16.
- The Arith.Lt file is obsolete. Use the bidirectional version Nat.neq_0_lt_0 (together with Nat.neq_sym) instead.
- [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
- File "./theories/Data/String.v", line 97, characters 11-19:
- Warning: Notation neq_0_lt is deprecated since 8.16.
- The Arith.Lt file is obsolete. Use the bidirectional version Nat.neq_0_lt_0 (together with Nat.neq_sym) instead.
- [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
- COQC theories/Data/Member.v
- COQC theories/Data/Tuple.v
- COQC theories/Data/Vector.v
- COQC theories/Programming/Extras.v
- COQC theories/Data/Monads/StateMonad.v
- COQC theories/Data/Monads/WriterMonad.v
- COQC theories/Data/Monads/FuelMonad.v
- COQC theories/Data/Monads/OptionMonad.v
- COQC theories/Data/Map/FMapTwoThreeK.v
- COQC theories/Data/Monads/EitherMonad.v
- COQC theories/Data/Monads/ListMonad.v
- COQC theories/Data/Monads/ReaderMonad.v
- COQC theories/Data/Set/ListSet.v
- COQC theories/Data/Set/SetMap.v
- COQC theories/Data/Set/TwoThreeTrees.v
- COQC theories/Structures/MonadLaws.v
- COQC theories/Data/HList.v
- COQC theories/Data/Map/FMapPositive.v
- COQC theories/Generic/Func.v
- COQC theories/Programming/Show.v
- File "./theories/Data/HList.v", line 462, characters 26-43:
- Warning: Notation app_assoc_reverse is deprecated since 8.18.
- Use app_assoc instead.
- [deprecated-syntactic-definition-since-8.18,deprecated-since-8.18,deprecated-syntactic-definition,deprecated,default]
- File "./theories/Data/HList.v", line 462, characters 26-43:
- Warning: Notation app_assoc_reverse is deprecated since 8.18.
- Use app_assoc instead.
- [deprecated-syntactic-definition-since-8.18,deprecated-since-8.18,deprecated-syntactic-definition,deprecated,default]
- COQC theories/Tactics/MonadTac.v
- File "./theories/Data/HList.v", line 661, characters 14-23:
- Warning: Notation Lt.lt_S_n is deprecated since 8.16.
- The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
- [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
- File "./theories/Data/HList.v", line 661, characters 14-23:
- Warning: Notation Lt.lt_S_n is deprecated since 8.16.
- The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
- [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
- File "./theories/Data/HList.v", line 681, characters 17-32:
- Error: The reference Minus.minus_n_O was not found in the current
- environment.
-
- make[2]: *** [Makefile.coq:838: theories/Data/HList.vo] Error 1
- make[2]: *** [theories/Data/HList.vo] Deleting file 'theories/Data/HList.glob'
- make[2]: *** Waiting for unfinished jobs....
- File "./theories/Programming/Show.v", line 64, characters 2-37:
- Warning: Declaring a scope implicitly is deprecated; use in advance an
- explicit "Declare Scope show_scope.".
- [undeclared-scope,deprecated-since-8.10,deprecated,default]
- File "./theories/Programming/Show.v", line 180, characters 23-33:
- Warning: Notation lt_O_Sn is deprecated since 8.16.
- The Arith.Lt file is obsolete. Use Nat.lt_0_succ instead.
- [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
- File "./theories/Programming/Show.v", line 180, characters 4-15:
- Error: No such hypothesis: H
-
- make[2]: *** [Makefile.coq:838: theories/Programming/Show.vo] Error 1
- make[2]: *** [theories/Programming/Show.vo] Deleting file 'theories/Programming/Show.glob'
- make[1]: *** [Makefile.coq:409: all] Error 2
- make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.5.0.0/.opam-switch/build/coq-ext-lib.0.11.5'
- make: *** [Makefile:7: theories] Error 2
[ERROR] The compilation of coq-ext-lib.0.11.5 failed at "make -j4 theories".
#=== ERROR while compiling coq-ext-lib.0.11.5 =================================#
# context 2.1.5 | linux/x86_64 | ocaml-base-compiler.5.0.0 | file:///home/bench/run/opam-coq-archive/released
# path ~/.opam/ocaml-base-compiler.5.0.0/.opam-switch/build/coq-ext-lib.0.11.5
# command ~/.opam/opam-init/hooks/sandbox.sh build make -j4 theories
# exit-code 2
# env-file ~/.opam/log/coq-ext-lib-10199-7969a5.env
# output-file ~/.opam/log/coq-ext-lib-10199-7969a5.out
### output ###
# [...]
# File "./theories/Programming/Show.v", line 180, characters 23-33:
# Warning: Notation lt_O_Sn is deprecated since 8.16.
# The Arith.Lt file is obsolete. Use Nat.lt_0_succ instead.
# [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
# File "./theories/Programming/Show.v", line 180, characters 4-15:
# Error: No such hypothesis: H
#
# make[2]: *** [Makefile.coq:838: theories/Programming/Show.vo] Error 1
# make[2]: *** [theories/Programming/Show.vo] Deleting file 'theories/Programming/Show.glob'
# make[1]: *** [Makefile.coq:409: all] Error 2
# make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.5.0.0/.opam-switch/build/coq-ext-lib.0.11.5'
# make: *** [Makefile:7: theories] Error 2
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build coq-ext-lib 0.11.5
+-
- No changes have been performed
# Run eval $(opam env) to update the current shell environment
'opam install -y -v coq-ext-lib.0.11.5 coq.8.18.0' failed.
The middle of the output is truncated (maximum 20000 characters)
No files were installed.
true