# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-num base Num library distributed with the OCaml compiler
base-threads base
base-unix base
camlp5 7.14 Preprocessor-pretty-printer of OCaml
conf-findutils 1 Virtual package relying on findutils
conf-perl 2 Virtual package relying on perl
coq 8.7.1+2 Formal proof management system
num 0 The Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.05.0 The OCaml compiler (virtual package)
ocaml-base-compiler 4.05.0 Official 4.05.0 release
ocaml-config 1 OCaml Switch Configuration
ocamlfind 1.9.3 A library manager for OCaml
# opam file:
opam-version: "2.0"
maintainer: "beta.ziliani@gmail.com"
homepage: "https://github.com/Mtac2/Mtac2"
dev-repo: "git+https://github.com/Mtac2/Mtac2.git"
bug-reports: "https://github.com/Mtac2/Mtac2/issues"
authors: ["Beta Ziliani <beta.ziliani@gmail.com>" "Jan-Oliver Kaiser <janno@mpi-sws.org>" "Robbert Krebbers <mail@robbertkrebbers.nl>" "Yann Régis-Gianas <yrg@pps.univ-paris-diderot.fr>" "Derek Dreyer <dreyer@mpi-sws.org>"]
license: "MIT"
build: [
["./configure.sh"]
[make "-j%{jobs}%"]
]
install: [
[make "install"]
]
remove: ["rm" "-R" "%{lib}%/coq/user-contrib/Mtac2"]
depends: [
"ocaml"
"coq" {>= "8.7.0" & < "8.8~"}
"coq-unicoq" {>= "1.3~" & < "2~"}
]
synopsis: "Mtac2: Typed Tactics for Coq"
flags: light-uninstall
url {
src: "https://github.com/Mtac2/Mtac2/archive/v1.0.0-coq8.7.tar.gz"
checksum: "md5=10fdc9569e0105d40f4ed22b8f92c2a7"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-mtac2.1.0.0+8.7 coq.8.7.1+2Dry 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-mtac2.1.0.0+8.7 coq.8.7.1+2opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-mtac2.1.0.0+8.7 coq.8.7.1+2# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-num base Num library distributed with the OCaml compiler
base-threads base
base-unix base
camlp5 7.14 Preprocessor-pretty-printer of OCaml
conf-findutils 1 Virtual package relying on findutils
conf-perl 2 Virtual package relying on perl
coq 8.7.1+2 Formal proof management system
coq-unicoq 1.3+8.7 An enhanced unification algorithm for Coq
num 0 The Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.05.0 The OCaml compiler (virtual package)
ocaml-base-compiler 4.05.0 Official 4.05.0 release
ocaml-config 1 OCaml Switch Configuration
ocamlfind 1.9.3 A library manager for OCaml
[NOTE] Package coq is already installed (current version is 8.7.1+2).
The following actions will be performed:
- install coq-mtac2 1.0.0+8.7
<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing 1/1: [coq-mtac2.1.0.0+8.7: http]
[coq-mtac2.1.0.0+8.7] downloaded from https://github.com/Mtac2/Mtac2/archive/v1.0.0-coq8.7.tar.gz
Processing 1/1:
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing 1/2: [coq-mtac2: ./configure.sh]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "./configure.sh" (CWD=/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-mtac2.1.0.0+8.7)
- Warning: no common logical root
- Warning: in such case INSTALLDEFAULTROOT must be defined
- Warning: the install-doc target is going to install files
- Warning: in orphan_Mtac2Tests_Mtac2
- ./configure.sh: 7: cd: can't cd to .git/hooks
Processing 1/2: [coq-mtac2: make]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "make" "-j7" (CWD=/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-mtac2.1.0.0+8.7)
- CAMLDEP src/metaCoqInterp.mli
- CAMLDEP src/run.mli
- CAMLDEP src/machine.mli
- CAMLDEP src/mConstr.mli
- CAMLDEP src/mtacNames.mli
- CAMLDEP src/constrs.mli
- CAMLDEP src/metaCoqInstr.mli
- COQDEP src/MetaCoqPlugin.mlpack
- CAMLDEP src/metaCoqInterp.ml
- CAMLDEP src/run.ml
- CAMLDEP src/cClosure_copy.ml
- CAMLDEP src/machine.ml
- CAMLDEP src/mConstr.ml
- CAMLDEP src/mtacNames.ml
- CAMLDEP src/constrs.ml
- CAMLDEP -pp src/metaCoqTactic.ml4
- CAMLDEP -pp src/metaCoqInit.ml4
- COQDEP theories/ideas/Transport.v
- COQDEP theories/ideas/StaticApply.v
- COQDEP theories/ideas/SubgoalsStrict.v
- COQDEP theories/ideas/DepDestruct.v
- COQDEP theories/ideas/Abstract.v
- COQDEP theories/meta/Exhaustive.v
- COQDEP theories/intf/M.v
- COQDEP theories/intf/Tm_kind.v
- COQDEP theories/intf/Lift.v
- COQDEP theories/intf/Goals.v
- COQDEP theories/intf/Case.v
- COQDEP theories/intf/Unification.v
- COQDEP theories/intf/DeclarationDefs.v
- COQDEP theories/intf/Reduction.v
- COQDEP theories/intf/Exceptions.v
- COQDEP theories/intf/Name.v
- COQDEP theories/intf/Dyn.v
- COQDEP theories/Pattern.v
- COQDEP theories/ideas/SumRun.v
- COQDEP theories/meta/MFix.v
- COQDEP theories/meta/MFixDef.v
- COQDEP theories/meta/MTeleMatch.v
- COQDEP theories/meta/MTeleMatchDef.v
- COQDEP theories/intf/MTele.v
- COQDEP theories/tactics/Ttactics.v
- COQDEP theories/Mtac2.v
- COQDEP theories/tactics/ConstrSelector.v
- COQDEP theories/tactics/CompoundTactics.v
- COQDEP theories/tactics/IntroPatt.v
- COQDEP theories/tactics/ImportedTactics.v
- COQDEP theories/tactics/Tactics.v
- COQDEP theories/tactics/TacticsBase.v
- COQDEP theories/DecomposeApp.v
- COQDEP theories/Base.v
- COQDEP theories/intf/Sorts.v
- COQDEP theories/lib/Utils.v
- *** Warning: in file theories/Base.v, declared ML module unicoq has not been found!
- *** Warning: in file theories/Base.v, declared ML module unicoq has not been found!
- COQDEP theories/lib/List.v
- COQDEP theories/lib/Datatypes.v
- COQDEP theories/lib/Specif.v
- COQDEP theories/lib/Logic.v
- COQC theories/lib/Logic.v
- COQC theories/lib/Datatypes.v
- COQC theories/intf/Sorts.v
- COQC theories/intf/Unification.v
- COQC theories/intf/Dyn.v
- COQC theories/intf/DeclarationDefs.v
- COQC theories/intf/Name.v
- COQC theories/intf/Tm_kind.v
- CAMLOPT -c -for-pack MetaCoqPlugin src/cClosure_copy.ml
- CAMLC -c src/constrs.mli
- CAMLC -c src/cClosure_copy.ml
- CAMLC -c src/metaCoqInstr.mli
- COQC theories/lib/Specif.v
- COQC theories/lib/List.v
- COQC theories/intf/MTele.v
- COQC theories/intf/Reduction.v
- COQC theories/intf/Goals.v
- File "./theories/lib/Specif.v", line 199, characters 0-144:
- Warning: Notation { _ } + { _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- File "./theories/lib/Specif.v", line 199, characters 0-144:
- Warning: Notation { _ } + { _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- File "./theories/lib/Specif.v", line 212, characters 0-144:
- Warning: Notation _ + { _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- File "./theories/lib/Specif.v", line 212, characters 0-144:
- Warning: Notation _ + { _ } was already used in scope type_scope.
- [notation-overridden,parsing]
- CAMLOPT -c -for-pack MetaCoqPlugin src/constrs.ml
- CAMLC -c src/mtacNames.mli
- File "src/mtacNames.mli", line 1:
- Error: Corrupted compiled interface
- src/cClosure_copy.cmi
- CAMLC -c src/mConstr.mli
- File "src/mConstr.mli", line 1:
- Error: Corrupted compiled interface
- src/cClosure_copy.cmi
- make[1]: *** [Makefile:577: src/mConstr.cmi] Error 2
- make[1]: *** Waiting for unfinished jobs....
- make[1]: *** [Makefile:577: src/mtacNames.cmi] Error 2
- = MTele_In@{Mtac2.intf.MTele.495 Mtac2.intf.MTele.496
- Mtac2.intf.MTele.497 Mtac2.intf.MTele.498 Mtac2.intf.MTele.499}
- SType
- : (forall
- now_ty : forall s : Sort,
- MTele_Sort@{Mtac2.intf.MTele.495 Mtac2.intf.MTele.499
- Mtac2.intf.MTele.499 Mtac2.intf.MTele.495} s
- ?n -> s,
- (forall (s : Sort)
- (T : MTele_Sort@{Mtac2.intf.MTele.495 Mtac2.intf.MTele.499
- Mtac2.intf.MTele.499 Mtac2.intf.MTele.495} s
- ?n),
- MTele_val@{Mtac2.intf.MTele.499 Mtac2.intf.MTele.495
- Mtac2.intf.MTele.499} T -> now_ty s T) -> SType) ->
- MTele_Sort@{Mtac2.intf.MTele.495 Mtac2.intf.MTele.498
- Mtac2.intf.MTele.496 Mtac2.intf.MTele.497} SType
- ?n
- make: *** [Makefile:318: all] Error 2
[ERROR] The compilation of coq-mtac2 failed at "/home/bench/.opam/opam-init/hooks/sandbox.sh build make -j7".
#=== ERROR while compiling coq-mtac2.1.0.0+8.7 ================================#
# context 2.0.1 | linux/x86_64 | ocaml-base-compiler.4.05.0 | file:///home/bench/run/opam-coq-archive/released
# path ~/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-mtac2.1.0.0+8.7
# command ~/.opam/opam-init/hooks/sandbox.sh build make -j7
# exit-code 2
# env-file ~/.opam/log/coq-mtac2-16192-e4db2f.env
# output-file ~/.opam/log/coq-mtac2-16192-e4db2f.out
### output ###
# make[1]: *** [Makefile:577: src/mtacNames.cmi] Error 2
# [...]
# ?n -> s,
# (forall (s : Sort)
# (T : MTele_Sort@{Mtac2.intf.MTele.495 Mtac2.intf.MTele.499
# Mtac2.intf.MTele.499 Mtac2.intf.MTele.495} s
# ?n),
# MTele_val@{Mtac2.intf.MTele.499 Mtac2.intf.MTele.495
# Mtac2.intf.MTele.499} T -> now_ty s T) -> SType) ->
# MTele_Sort@{Mtac2.intf.MTele.495 Mtac2.intf.MTele.498
# Mtac2.intf.MTele.496 Mtac2.intf.MTele.497} SType
# ?n
# make: *** [Makefile:318: all] Error 2
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build coq-mtac2 1.0.0+8.7
+-
- No changes have been performed
# Run eval $(opam env) to update the current shell environment
'opam install -y -v coq-mtac2.1.0.0+8.7 coq.8.7.1+2' failed.
No files were installed.
true