# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-threads base
base-unix base
conf-findutils 1 Virtual package relying on findutils
num 1.4 The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.09.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.09.1 Official release 4.09.1
ocaml-config 1 OCaml Switch Configuration
ocamlfind 1.9.5 A library manager for OCaml
# opam file:
opam-version: "2.0"
maintainer: "Li-yao Xia <lysxia@gmail.com>"
synopsis: "A Library for Representing Recursive and Impure Programs in Coq"
homepage: "https://github.com/DeepSpec/InteractionTrees"
dev-repo: "git+https://github.com/DeepSpec/InteractionTrees"
bug-reports: "https://github.com/DeepSpec/InteractionTrees/issues"
license: "MIT"
build: [
["dune" "subst"] {pinned}
["dune" "build" "-p" name "-j" jobs]
["dune" "build" "--root=." "-j" jobs] {with-test}
["dune" "runtest" "--root=." "-j" jobs] {with-test}
]
depends: [
"coq" {>= "8.10"}
"coq-ext-lib" {>= "0.11.1" & < "0.12"}
"coq-paco" {>= "4.0.1"}
"dune" {>= "2.6"}
]
authors: [
"Li-yao Xia <lysxia@gmail.com>"
"Yannick Zakowski <zakowski@seas.upenn.edu>"
"Paul He <paulhe@seas.upenn.edu>"
"Chung-Kil Hur <gil.hur@gmail.com>"
"Gregory Malecha <gmalecha@gmail.com>"
"Steve Zdancewic <stevez@cis.upenn.edu>"
"Benjamin C. Pierce <bcpierce@cis.upenn.edu>"
]
tags: [
"org:deepspec"
"logpath: ITree"
"date: 2021-03-15"
]
url {
http: "https://github.com/DeepSpec/InteractionTrees/archive/4.0.0.tar.gz"
checksum: "sha512=5474977a355de77a7775f70cc885164058f5b7ffa122c914fc53b43db08b238c354e0ef99cbcb53b1e9a24640357cd1902c0afe3ed512c24da3d1c8ce006e5b3"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-itree.4.0.0 coq.8.16.0Dry 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-itree.4.0.0 coq.8.16.0opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-itree.4.0.0 coq.8.16.0# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-threads base
base-unix base
conf-findutils 1 Virtual package relying on findutils
conf-gmp 4 Virtual package relying on a GMP lib system installation
dune 3.4.1 Fast, portable, and opinionated build system
num 1.4 The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.09.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.09.1 Official release 4.09.1
ocaml-config 1 OCaml Switch Configuration
ocamlfind 1.9.5 A library manager for OCaml
zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integers
The following actions will be performed:
- install coq 8.16.0
- install coq-paco 4.1.2 [required by coq-itree]
- install coq-ext-lib 0.11.7 [required by coq-itree]
- install coq-itree 4.0.0
===== 4 to install =====
<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing 1/4: [coq.8.16.0: dl]
Processing 2/4: [coq.8.16.0: dl] [coq-ext-lib.0.11.7: http]
Processing 3/4: [coq.8.16.0: dl] [coq-ext-lib.0.11.7: http] [coq-itree.4.0.0: http]
[coq-ext-lib.0.11.7] downloaded from https://github.com/coq-community/coq-ext-lib/archive/v0.11.7.tar.gz
Processing 3/4: [coq.8.16.0: dl] [coq-itree.4.0.0: http]
[coq-itree.4.0.0] downloaded from https://github.com/DeepSpec/InteractionTrees/archive/4.0.0.tar.gz
Processing 3/4: [coq.8.16.0: dl]
Processing 4/4: [coq.8.16.0: dl] [coq-paco.4.1.2: http]
[coq.8.16.0] downloaded from cache at https://opam.ocaml.org/cache
Processing 4/4: [coq-paco.4.1.2: http]
[coq-paco.4.1.2] downloaded from https://github.com/snu-sf/paco/archive/v4.1.2.tar.gz
Processing 4/4:
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing 1/8: [coq: ./configure no]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "./configure" "-configdir" "/home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/config" "-prefix" "/home/bench/.opam/ocaml-base-compiler.4.09.1" "-mandir" "/home/bench/.opam/ocaml-base-compiler.4.09.1/man" "-docdir" "/home/bench/.opam/ocaml-base-compiler.4.09.1/doc/coq" "-libdir" "/home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq" "-datadir" "/home/bench/.opam/ocaml-base-compiler.4.09.1/share/coq" "-coqide" "no" "-native-compiler" "no" (CWD=/home/bench/.opam/ocaml-base-compiler.4.09.1/.opam-switch/build/coq.8.16.0)
- You have OCaml 4.09.1. Good!
- You have OCamlfind 1.9.5. Good!
- You have native-code compilation. Good!
- You have the Zarith library 1.12 installed. Good!
- CoqIde manually disabled:
- => no CoqIDE will be built.
-
- Architecture : Linux
- Sys.os_type : Unix
- OCaml version : 4.09.1
- OCaml binaries in : /home/bench/.opam/ocaml-base-compiler.4.09.1/bin/
- OCaml library in : /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/ocaml
- Native dynamic link support : true
- CoqIDE : no
- Documentation : None
- Web browser : firefox -remote "OpenURL(%s,new-tab)" || firefox %s &
- Coq web site : http://coq.inria.fr/
- Bytecode VM enabled : true
- Native Compiler enabled : no
-
- Paths for true installation:
- - Coq will be copied in /home/bench/.opam/ocaml-base-compiler.4.09.1
- - the Coq library will be copied in /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq
- - the Coqide configuration files will be copied in /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/config
- - the Coqide data files will be copied in /home/bench/.opam/ocaml-base-compiler.4.09.1/share/coq
- - the Coq man pages will be copied in /home/bench/.opam/ocaml-base-compiler.4.09.1/man
- - documentation prefix path for all Coq packages will be copied in /home/bench/.opam/ocaml-base-compiler.4.09.1/doc/coq
-
- If anything is wrong above, please restart './configure'.
-
- *Warning* To compile the system for a new architecture
- don't forget to do a 'make clean' before './configure'.
Processing 1/8: [coq: make]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "make" "COQ_USE_DUNE=" "-j4" (CWD=/home/bench/.opam/ocaml-base-compiler.4.09.1/.opam-switch/build/coq.8.16.0)
- make --warn-undefined-variable --no-builtin-rules -f Makefile.build
- make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.09.1/.opam-switch/build/coq.8.16.0'
- MKDIR BUILD_OUT
- DUNE _build/install/default/bin/coqdep
- DUNE sources
- COQDEP VFILES
- DUNE sources
- DUNE _build/install/default/bin/coqc
- DUNE _build/default/plugins/ltac/ltac_plugin.cmxs
- DUNE _build/default/plugins/syntax/number_string_notation_plugin.cmxs
- DUNE _build/default/plugins/ltac/tauto_plugin.cmxs
- DUNE _build/default/plugins/cc/cc_plugin.cmxs
- DUNE _build/default/plugins/firstorder/firstorder_plugin.cmxs
- DUNE _build/default/plugins/rtauto/rtauto_plugin.cmxs
- DUNE _build/default/plugins/ssrmatching/ssrmatching_plugin.cmxs
- DUNE _build/default/plugins/ring/ring_plugin.cmxs
- DUNE _build/default/plugins/micromega/zify_plugin.cmxs
- DUNE _build/default/plugins/micromega/micromega_plugin.cmxs
- DUNE _build/default/plugins/btauto/btauto_plugin.cmxs
- DUNE _build/default/plugins/extraction/extraction_plugin.cmxs
- DUNE _build/default/plugins/ssr/ssreflect_plugin.cmxs
- DUNE _build/default/plugins/nsatz/nsatz_plugin.cmxs
- DUNE _build/default/plugins/derive/derive_plugin.cmxs
- DUNE _build/default/plugins/funind/funind_plugin.cmxs
- DUNE _build/default/plugins/ltac2/ltac2_plugin.cmxs
- DUNE _build/install/default/bin/coqproofworker.opt
- DUNE _build/install/default/bin/coqtacticworker.opt
- DUNE _build/install/default/bin/coqqueryworker.opt
- DUNE _build/install/default/bin/coqtop
- DUNE _build/install/default/bin/coqchk
- DUNE _build/install/default/bin/csdpcert
- DUNE _build/install/default/bin/coqnative
- DUNE _build/install/default/bin/votour
- DUNE _build/install/default/bin/coqdoc
- DUNE _build/install/default/lib/coq-core/tools/coqdoc/coqdoc.sty
- DUNE _build/install/default/lib/coq-core/tools/coqdoc/coqdoc.css
- DUNE _build/install/default/bin/coqwc
- DUNE _build/install/default/bin/coq_makefile
- DUNE _build/default/tools/CoqMakefile.in
- DUNE _build/install/default/bin/ocamllibdep
- DUNE _build/default/doc/tools/docgram/doc_grammar.exe
- DUNE _build/default/coq-core.install
- DUNE _build/default/coqide-server.install
- DUNE revision
- COQCBOOT theories/Init/Notations.v
- COQCBOOT theories/Init/Ltac.v
- COQCBOOT theories/Init/Logic.v
- COQCBOOT theories/Init/Datatypes.v
- COQCBOOT theories/Init/Specif.v
- COQCBOOT theories/Init/Wf.v
- COQCBOOT theories/Init/Tactics.v
- COQCBOOT theories/Init/Tauto.v
- COQCBOOT theories/Init/Decimal.v
- COQCBOOT theories/Init/Hexadecimal.v
- COQCBOOT theories/Init/Number.v
- COQCBOOT theories/Init/Nat.v
- COQCBOOT theories/Init/Byte.v
- COQCBOOT theories/Init/Peano.v
- COQCBOOT theories/Init/Prelude.v
- COQC theories/Numbers/BinNums.v
- COQC theories/Logic/EqdepFacts.v
- COQC theories/Program/Basics.v
- COQC theories/Program/Tactics.v
- COQC theories/Relations/Relation_Definitions.v
- COQC theories/ssr/ssrclasses.v
- COQC theories/Bool/Bool.v
- COQC theories/Relations/Relation_Operators.v
- COQC theories/Logic/Decidable.v
- COQC theories/PArith/BinPosDef.v
- COQC theories/Sets/Relations_1.v
- COQC theories/Lists/Streams.v
- COQC theories/ssrmatching/ssrmatching.v
- COQC theories/Bool/Sumbool.v
- COQC theories/micromega/ZifyClasses.v
- COQC theories/Sets/Permut.v
- COQC theories/Logic/FunctionalExtensionality.v
- COQC theories/Logic/PropExtensionalityFacts.v
- COQC theories/Logic/Hurkens.v
- COQC theories/extraction/Extraction.v
- COQC theories/Unicode/Utf8_core.v
- COQC theories/Numbers/Cyclic/Abstract/CarryType.v
- COQC theories/extraction/ExtrHaskellBasic.v
- COQC theories/Floats/FloatClass.v
- COQC theories/Numbers/AltBinNotations.v
- COQC theories/Sets/Ensembles.v
- COQC theories/Sets/Relations_1_facts.v
- COQC theories/Sets/Uniset.v
- COQC theories/Sets/Relations_2.v
- COQC theories/setoid_ring/Algebra_syntax.v
- COQC theories/Wellfounded/Transitive_Closure.v
- COQC theories/Wellfounded/Inverse_Image.v
- COQC theories/Wellfounded/Well_Ordering.v
- COQC theories/Wellfounded/Disjoint_Union.v
- COQC theories/Wellfounded/Inclusion.v
- COQC theories/derive/Derive.v
- COQC theories/Program/Utils.v
- COQC theories/Logic/Eqdep.v
- COQC theories/Logic/ProofIrrelevanceFacts.v
- COQC theories/Program/Combinators.v
- COQC theories/funind/FunInd.v
- COQC theories/Bool/BoolEq.v
- COQC theories/Bool/IfProp.v
- COQC theories/Bool/DecBool.v
- COQC theories/Compat/AdmitAxiom.v
- COQC theories/Compat/Coq816.v
- COQC theories/Logic/Adjointification.v
- COQC theories/Logic/RelationalChoice.v
- COQC theories/Logic/PropFacts.v
- COQC theories/Logic/SetIsType.v
- COQC theories/Logic/ExtensionalFunctionRepresentative.v
- COQC theories/Logic/Berardi.v
- COQC theories/Logic/StrictProp.v
- COQC theories/Logic/ExtensionalityFacts.v
- COQC user-contrib/Ltac2/Init.v
- COQC theories/Logic/Eqdep_dec.v
- COQC theories/Classes/Init.v
- COQC theories/ssr/ssrunder.v
- COQC theories/Relations/Operators_Properties.v
- COQC theories/Logic/HLevels.v
- COQC theories/extraction/ExtrOcamlBasic.v
- COQC
[...] truncated
mpiler.4.09.1/lib/coq/plugins/ltac
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/..
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Ltac2
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib
-
-
- Error:
- Dynlink error: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"/home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/ltac/ltac_plugin.cmxs: undefined symbol: camlNumTok__2\")")
- Findlib paths:
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/rtauto
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/ssrmatching
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/btauto
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/cc
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/extraction
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/ssr
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/nsatz
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/micromega
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/syntax
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/derive
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/omega
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/firstorder
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/setoid_ring
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/funind
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/ltac
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/..
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Ltac2
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib
-
-
- make[2]: *** [Makefile.coq:659: theories/Core/RelDec.vo] Error 1
- make[2]: *** [Makefile.coq:659: theories/Tactics/Injection.vo] Error 1
- make[2]: *** [Makefile.coq:659: theories/Tactics/Forward.vo] Error 1
- make[1]: *** [Makefile.coq:321: all] Error 2
- make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.09.1/.opam-switch/build/coq-ext-lib.0.11.7'
- make: *** [Makefile:7: theories] Error 2
[ERROR] The compilation of coq-ext-lib failed at "/home/bench/.opam/opam-init/hooks/sandbox.sh build make -j4 theories".
Processing 4/8: [coq-paco: make src]
Processing 5/8: [coq-paco: make src]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "make" "-C" "src" "all" "-j4" (CWD=/home/bench/.opam/ocaml-base-compiler.4.09.1/.opam-switch/build/coq-paco.4.1.2)
- make: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.09.1/.opam-switch/build/coq-paco.4.1.2/src'
- (echo "-Q . Paco"; \
- \
- echo paco.v examples.v gpaco8.v paco10.v gpaco13.v paco_internal.v gpaco12.v paco9.v paco3.v tutorial.v gpaco7.v paco4.v paco0.v gpaco11.v pacoall.v paconotation.v gpaco9.v paco13.v pacotac.v gpaco3.v paco1.v paco5.v paco6.v gpaco4.v gpaco0.v gpaco14.v paconotation_internal.v paco8.v gpaco10.v gpacotac.v gpaco1.v hpattern.v paco11.v paco7.v paco2.v paco14.v gpacoall.v pacotac_internal.v gpaco5.v gpaco6.v gpaco2.v paco12.v) > _CoqProject
- coq_makefile -f _CoqProject -o Makefile.coq
- make -f Makefile.coq all
- make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.09.1/.opam-switch/build/coq-paco.4.1.2/src'
- COQDEP VFILES
- COQC paconotation.v
- COQC hpattern.v
- Error:
- Dynlink error: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"/home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/ltac/ltac_plugin.cmxs: undefined symbol: camlNumTok__2\")")
- Findlib paths:
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/rtauto
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/ssrmatching
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/btauto
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/cc
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/extraction
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/ssr
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/nsatz
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/micromega
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/syntax
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/derive
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/omega
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/firstorder
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/setoid_ring
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/funind
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/ltac
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/..
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Ltac2
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib
-
-
- make[2]: *** [Makefile.coq:659: paconotation.vo] Error 1
- make[2]: *** Waiting for unfinished jobs....
- Error:
- Dynlink error: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"/home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/ltac/ltac_plugin.cmxs: undefined symbol: camlNumTok__2\")")
- Findlib paths:
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/rtauto
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/ssrmatching
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/btauto
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/cc
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/extraction
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/ssr
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/nsatz
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/micromega
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/syntax
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/derive
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/omega
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/firstorder
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/setoid_ring
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/funind
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/ltac
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/..
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Ltac2
- /home/bench/.opam/ocaml-base-compiler.4.09.1/lib
-
-
- make[2]: *** [Makefile.coq:659: hpattern.vo] Error 1
- make[1]: *** [Makefile.coq:321: all] Error 2
- make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.09.1/.opam-switch/build/coq-paco.4.1.2/src'
- make: *** [Makefile:8: all] Error 2
- make: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.09.1/.opam-switch/build/coq-paco.4.1.2/src'
[ERROR] The compilation of coq-paco failed at "/home/bench/.opam/opam-init/hooks/sandbox.sh build make -C src all -j4".
#=== ERROR while compiling coq-paco.4.1.2 =====================================#
# context 2.0.6 | linux/x86_64 | ocaml-base-compiler.4.09.1 | file:///home/bench/run/opam-coq-archive/released
# path ~/.opam/ocaml-base-compiler.4.09.1/.opam-switch/build/coq-paco.4.1.2
# command ~/.opam/opam-init/hooks/sandbox.sh build make -C src all -j4
# exit-code 2
# env-file ~/.opam/log/coq-paco-9858-126656.env
# output-file ~/.opam/log/coq-paco-9858-126656.out
### output ###
# [...]
# /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/funind
# /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/ltac
# /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/..
# /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Ltac2
# /home/bench/.opam/ocaml-base-compiler.4.09.1/lib
#
#
# make[2]: *** [Makefile.coq:659: hpattern.vo] Error 1
# make[1]: *** [Makefile.coq:321: all] Error 2
# make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.09.1/.opam-switch/build/coq-paco.4.1.2/src'
# make: *** [Makefile:8: all] Error 2
# make: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.09.1/.opam-switch/build/coq-paco.4.1.2/src'
#=== ERROR while compiling coq-ext-lib.0.11.7 =================================#
# context 2.0.6 | linux/x86_64 | ocaml-base-compiler.4.09.1 | file:///home/bench/run/opam-coq-archive/released
# path ~/.opam/ocaml-base-compiler.4.09.1/.opam-switch/build/coq-ext-lib.0.11.7
# command ~/.opam/opam-init/hooks/sandbox.sh build make -j4 theories
# exit-code 2
# env-file ~/.opam/log/coq-ext-lib-9858-51aaa5.env
# output-file ~/.opam/log/coq-ext-lib-9858-51aaa5.out
### output ###
# [...]
# /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/plugins/ltac
# /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/..
# /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Ltac2
# /home/bench/.opam/ocaml-base-compiler.4.09.1/lib
#
#
# make[2]: *** [Makefile.coq:659: theories/Core/RelDec.vo] Error 1
# make[2]: *** [Makefile.coq:659: theories/Tactics/Injection.vo] Error 1
# make[2]: *** [Makefile.coq:659: theories/Tactics/Forward.vo] Error 1
# make[1]: *** [Makefile.coq:321: all] Error 2
# make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.09.1/.opam-switch/build/coq-ext-lib.0.11.7'
# make: *** [Makefile:7: theories] Error 2
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions were aborted
| - install coq-itree 4.0.0
+-
+- The following actions failed
| - build coq-ext-lib 0.11.7
| - build coq-paco 4.1.2
+-
+- The following changes have been performed (the rest was aborted)
| - install coq 8.16.0
+-
# Run eval $(opam env) to update the current shell environment
The former state can be restored with:
opam switch import "/home/bench/.opam/ocaml-base-compiler.4.09.1/.opam-switch/backup/state-20220920043036.export"
'opam install -y -v coq-itree.4.0.0 coq.8.16.0' failed.
The middle of the output is truncated (maximum 20000 characters)
No files were installed.
true