(2020-09-04 23:50:27 UTC)
This result is black-listed as it is considered as too hard to reproduce / to solve. If you find a way to fix this package, please make a pull-request to github.com/coq/opam-coq-archive. The list of black-listed packages is in black_list.rb.
# 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.12 Preprocessor-pretty-printer of OCaml
conf-findutils 1 Virtual package relying on findutils
conf-m4 1 Virtual package relying on m4
coq 8.8.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.8.1 A library manager for OCaml
# opam file:
opam-version: "2.0"
maintainer: "Jacques-Henri Jourdan <jacques-Henri.jourdan@normalesup.org>"
homepage: "http://compcert.inria.fr/"
dev-repo: "git+https://github.com/AbsInt/CompCert.git"
bug-reports: "https://github.com/AbsInt/CompCert/issues"
license: "INRIA Non-Commercial License Agreement"
build: [
[
"./configure"
"ia32-linux" {os = "linux"}
"ia32-macosx" {os = "macos"}
"ia32-cygwin" {os = "cygwin"}
"-bindir"
"%{bin}%"
"-libdir"
"%{lib}%/compcert"
"-install-coqdev"
"-clightgen"
"-coqdevdir"
"%{lib}%/coq/user-contrib/compcert"
"-ignore-coq-version"
]
[make "-j%{jobs}%"]
]
install: [
[make "install"]
["install" "-m" "0644" "VERSION" "%{lib}%/coq/user-contrib/compcert/"]
]
remove: [
["rm" "%{bin}%/ccomp"]
["rm" "%{bin}%/clightgen"]
["rm" "-R" "%{lib}%/compcert"]
["rm" "-R" "%{lib}%/coq/user-contrib/compcert"]
["rm" "%{share}%/compcert.ini"]
["rm" "%{share}%/man/man1/ccomp.1"]
["sh" "-c" "rmdir -p %{share}%/man/man1 || true"]
]
depends: [
"ocaml" {< "4.08"}
"coq" {>= "8.8.1" & <= "8.8.2"}
"menhir" {>= "20180530" & < "20181006"}
]
synopsis: "The CompCert C compiler"
authors: "Xavier Leroy <xavier.leroy@inria.fr>"
url {
src: "https://github.com/AbsInt/CompCert/archive/v3.4.tar.gz"
checksum: "md5=122b717e2c48c1a8fe36c89ec5a1050d"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-compcert.3.4 coq.8.8.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 2h opam install -y --deps-only coq-compcert.3.4 coq.8.8.2opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-compcert.3.4 coq.8.8.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.12 Preprocessor-pretty-printer of OCaml conf-findutils 1 Virtual package relying on findutils conf-m4 1 Virtual package relying on m4 coq 8.8.2 Formal proof management system. menhir 20180905 LR(1) parser generator 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 ocamlbuild 0.14.0 OCamlbuild is a build system with builtin rules to easily build most OCaml projects. ocamlfind 1.8.1 A library manager for OCaml [NOTE] Package coq is already installed (current version is 8.8.2). The following actions will be performed: - install coq-compcert 3.4 <><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><> Processing 1/1: [coq-compcert.3.4: http] [coq-compcert.3.4] downloaded from https://github.com/AbsInt/CompCert/archive/v3.4.tar.gz Processing 1/1: <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> Processing 1/2: [coq-compcert: ./configure ia32-linux] + /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "./configure" "ia32-linux" "-bindir" "/home/bench/.opam/ocaml-base-compiler.4.05.0/bin" "-libdir" "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/compcert" "-install-coqdev" "-clightgen" "-coqdevdir" "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/user-contrib/compcert" "-ignore-coq-version" (CWD=/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-compcert.3.4) - Testing assembler support for CFI directives... yes - Testing linker support for '-no-pie' / '-nopie' option... no - Testing Coq... version 8.8.2 -- good! - Testing OCaml... version 4.05.0 -- good! - Testing OCaml .opt compilers... yes - Testing Menhir... version 20180905 -- good! - Testing GNU make... version 4.2.1 (command 'make') -- good! - - CompCert configuration: - Target architecture........... x86 - Hardware model................ 32sse2 - Application binary interface.. standard - Endianness.................... little - OS and development env........ linux - C compiler.................... gcc -m32 - C preprocessor................ gcc - Assembler..................... gcc - Assembler supports CFI........ true - Assembler for runtime lib..... gcc -m32 -c - Linker........................ gcc - Linker needs '-no-pie'........ false - Math library.................. -lm - Build command to use.......... make - Binaries installed in......... /home/bench/.opam/ocaml-base-compiler.4.05.0/bin - Runtime library provided...... true - Library files installed in.... /home/bench/.opam/ocaml-base-compiler.4.05.0/lib/compcert - Standard headers provided..... true - Standard headers installed in. /home/bench/.opam/ocaml-base-compiler.4.05.0/lib/compcert/include - Coq development installed in.. /home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/user-contrib/compcert Processing 1/2: [coq-compcert: make] + /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "make" "-j4" (CWD=/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-compcert.3.4) - make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-compcert.3.4' - ocamlopt -o tools/ndfun str.cmxa tools/ndfun.ml - menhir --coq-lib-path compcert.cparser.MenhirLib --coq cparser/Parser.vy - Preprocessing x86/ConstpropOp.vp - Preprocessing x86/SelectOp.vp - Preprocessing x86/SelectLong.vp - Preprocessing backend/SelectDiv.vp - Preprocessing backend/SplitLong.vp - Analyzing Coq dependencies - make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-compcert.3.4' - make proof - make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-compcert.3.4' - COQC lib/Axioms.v - COQC lib/Coqlib.v - COQC flocq/Core/Fcore_Zaux.v - COQC driver/Compopts.v - COQC cparser/MenhirLib/Alphabet.v - COQC cparser/MenhirLib/Tuples.v - COQC cparser/Cabs.v - COQC lib/Wfsimpl.v - COQC cparser/MenhirLib/Grammar.v - COQC flocq/Core/Fcore_Raux.v - COQC flocq/Core/Fcore_digits.v - COQC lib/Intv.v - COQC lib/Maps.v - COQC lib/Iteration.v - COQC lib/Parmov.v - COQC lib/UnionFind.v - COQC lib/FSetAVLplus.v - COQC lib/IntvSets.v - COQC lib/Decidableplus.v - COQC lib/BoolEqual.v - COQC common/Errors.v - COQC cparser/MenhirLib/Automaton.v - COQC flocq/Core/Fcore_defs.v - COQC lib/Lattice.v - COQC lib/Postorder.v - COQC common/Unityping.v - COQC cparser/MenhirLib/Interpreter.v - COQC cparser/MenhirLib/Validator_complete.v - COQC cparser/MenhirLib/Validator_safe.v - COQC flocq/Core/Fcore_float_prop.v - COQC flocq/Core/Fcore_rnd.v - COQC flocq/Calc/Fcalc_digits.v - COQC flocq/Calc/Fcalc_bracket.v - COQC flocq/Calc/Fcalc_ops.v - COQC cparser/MenhirLib/Interpreter_complete.v - COQC cparser/MenhirLib/Interpreter_correct.v - COQC cparser/MenhirLib/Interpreter_safe.v - COQC flocq/Core/Fcore_generic_fmt.v - COQC flocq/Calc/Fcalc_div.v - COQC flocq/Calc/Fcalc_sqrt.v - COQC flocq/Core/Fcore_ulp.v - COQC flocq/Prop/Fprop_Sterbenz.v - COQC cparser/MenhirLib/Main.v - COQC flocq/Core/Fcore_rnd_ne.v - COQC cparser/Parser.v - COQC flocq/Core/Fcore_FIX.v - COQC flocq/Core/Fcore_FLX.v - COQC flocq/Core/Fcore_FLT.v - COQC flocq/Core/Fcore_FTZ.v - COQC flocq/Core/Fcore.v - COQC flocq/Prop/Fprop_plus_error.v - COQC flocq/Appli/Fappli_double_round.v - COQC flocq/Calc/Fcalc_round.v - COQC flocq/Prop/Fprop_relative.v - COQC flocq/Appli/Fappli_rnd_odd.v - COQC flocq/Prop/Fprop_div_sqrt_error.v - COQC flocq/Prop/Fprop_mult_error.v - COQC flocq/Appli/Fappli_IEEE.v - COQC flocq/Appli/Fappli_IEEE_bits.v - COQC lib/Fappli_IEEE_extra.v - COQC x86_32/Archi.v - COQC lib/Integers.v - COQC lib/Ordered.v - COQC lib/Floats.v - COQC lib/Heaps.v - COQC common/AST.v - COQC common/Linking.v - COQC common/Values.v - COQC cfrontend/Ctypes.v - COQC common/Memdata.v - COQC common/Switch.v - COQC backend/Registers.v - COQC common/Memtype.v - COQC common/Memory.v - COQC common/Globalenvs.v - COQC cfrontend/Cop.v - COQC common/Events.v - COQC cfrontend/Csyntax.v - COQC cfrontend/Initializers.v - COQC common/Smallstep.v - COQC common/Separation.v - COQC x86/Op.v - COQC common/Behaviors.v - COQC backend/Cminor.v - COQC cfrontend/Csem.v - COQC cfrontend/Clight.v - COQC cfrontend/Csharpminor.v - COQC common/Determinism.v - COQC cfrontend/Ctyping.v - COQC cfrontend/Cstrategy.v - COQC cfrontend/Initializersproof.v - COQC cfrontend/SimplExpr.v - COQC cfrontend/ClightBigstep.v - COQC cfrontend/SimplLocals.v - COQC cfrontend/Cshmgen.v - COQC cfrontend/Cminorgen.v - COQC backend/Kildall.v - COQC cfrontend/SimplExprspec.v - COQC cfrontend/SimplLocalsproof.v - COQC cfrontend/Cshmgenproof.v - COQC cfrontend/Cminorgenproof.v - COQC cfrontend/Cexec.v - COQC cfrontend/SimplExprproof.v - COQC backend/CminorSel.v - COQC x86/Machregs.v - COQC backend/RTL.v - COQC x86/SelectOp.v - COQC backend/Locations.v - COQC backend/Inlining.v - COQC backend/RTLgen.v - COQC backend/Renumber.v - COQC backend/Liveness.v - COQC backend/ValueDomain.v - COQC backend/CSEdomain.v - COQC backend/Unusedglob.v - COQC backend/RTLgenspec.v - COQC x86/Conventions1.v - COQC backend/Inliningspec.v - COQC backend/Renumberproof.v - COQC x86/CombineOp.v - COQC backend/Unusedglobproof.v - COQC backend/SplitLong.v - COQC x86/SelectOpproof.v - COQC backend/RTLgenproof.v - COQC backend/Conventions.v - COQC x86/CombineOpproof.v - COQC backend/LTL.v - COQC x86/SelectLong.v - COQC backend/SplitLongproof.v - COQC backend/Tailcall.v - COQC backend/Inliningproof.v - COQC backend/RTLtyping.v - COQC backend/Tunneling.v - COQC backend/Linear.v - COQC backend/SelectDiv.v - COQC backend/Tailcallproof.v - COQC x86/ValueAOp.v - COQC x86/ConstpropOp.v - COQC backend/NeedDomain.v - COQC backend/Allocation.v - COQC backend/Tunnelingproof.v - COQC backend/Lineartyping.v - COQC backend/Linearize.v - COQC backend/CleanupLabels.v - COQC backend/Debugvar.v - COQC backend/Bounds.v - COQC backend/Selection.v - COQC backend/ValueAnalysis.v - COQC x86/ConstpropOpproof.v - COQC x86/NeedOp.v - COQC backend/Allocproof.v - COQC backend/Linearizeproof.v - COQC backend/CleanupLabelsproof.v - COQC backend/Debugvarproof.v - COQC x86/Stacklayout.v - COQC x86/SelectLongproof.v - COQC backend/Constprop.v - COQC backend/CSE.v - COQC backend/Deadcode.v - COQC backend/Mach.v - COQC x86/Asm.v - COQC backend/Constpropproof.v - COQC backend/CSEproof.v - COQC backend/Deadcodeproof.v - COQC backend/Stacking.v - COQC x86/Asmgen.v - COQC backend/SelectDivproof.v - COQC backend/Stackingproof.v - COQC backend/Asmgenproof0.v - COQC x86/Asmgenproof1.v - COQC backend/Selectionproof.v - COQC x86/Asmgenproof.v - COQC driver/Compiler.v - COQC driver/Complements.v - make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-compcert.3.4' - make extraction - make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-compcert.3.4' - rm -f extraction/*.ml extraction/*.mli - "coqtop" -R lib compcert.lib -R common compcert.common -R x86_32 compcert.x86_32 -R x86 compcert.x86 -R backend compcert.backend -R cfrontend compcert.cfrontend -R driver compcert.driver -R flocq compcert.flocq -R exportclight compcert.exportclight -R cparser compcert.cparser -batch -load-vernac-source extraction/extraction.v - File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-compcert.3.4/extraction/extraction.v", line 169, characters 0-1043: - Warning: The [...] truncated extraction/String0.mli - OCAMLC extraction/Errors.mli - OCAMLC extraction/Equalities.mli - OCAMLC extraction/Specif.mli - OCAMLC extraction/Memtype.mli - OCAMLC extraction/PeanoNat.mli - OCAMLC cparser/Machine.mli - OCAMLC cparser/C.mli - OCAMLC lib/Responsefile.mli - OCAMLC driver/Commandline.mli - OCAMLC extraction/Ring.mli - OCAMLC lib/Printlines.mli - OCAMLC driver/Driveraux.mli - OCAMLC driver/Linker.mli - OCAMLC extraction/DecidableClass.mli - OCAMLC cparser/Unblock.mli - OCAMLC cparser/StructPassing.mli - OCAMLC cparser/Rename.mli - OCAMLC extraction/Tuples.mli - OCAMLC extraction/Streams.mli - OCAMLC extraction/Int31.mli - OCAMLC extraction/Cabs.mli - OCAMLC cparser/pre_parser_aux.mli - OCAMLOPT cparser/pre_parser_messages.ml - OCAMLC cparser/Cleanup.mli - OCAMLC cparser/Checks.mli - OCAMLC cparser/Elab.mli - OCAMLC cparser/Bitfields.mli - OCAMLC cparser/Parse.mli - OCAMLC lib/Tokenize.mli - OCAMLC extraction/UnionFind.mli - OCAMLC extraction/Compopts.mli - OCAMLC extraction/Compare_dec.mli - OCAMLC extraction/Mergesort.mli - OCAMLC driver/Clflags.ml - OCAMLC driver/Assembler.mli - OCAMLOPT lib/Readconfig.ml - OCAMLOPT extraction/Datatypes.ml - OCAMLC extraction/Nat.mli - OCAMLOPT extraction/BinNums.ml - OCAMLC extraction/BinPosDef.mli - OCAMLC extraction/List0.mli - OCAMLOPT extraction/Bool.ml - OCAMLOPT extraction/Orders.ml - OCAMLC extraction/OrdersTac.mli - OCAMLOPT extraction/EquivDec.ml - OCAMLOPT extraction/BoolEqual.ml - OCAMLOPT extraction/String0.ml - OCAMLOPT extraction/Errors.ml - OCAMLOPT extraction/Equalities.ml - OCAMLC extraction/DecidableType.mli - OCAMLOPT extraction/Specif.ml - OCAMLOPT extraction/Memtype.ml - OCAMLOPT extraction/PeanoNat.ml - OCAMLOPT cparser/Machine.ml - OCAMLC cparser/Env.mli - OCAMLOPT lib/Responsefile.ml - OCAMLC cparser/Diagnostics.mli - OCAMLC cparser/Cprint.mli - OCAMLC cparser/Cutil.mli - OCAMLC cparser/Ceval.mli - OCAMLC cparser/Builtins.mli - OCAMLOPT extraction/Ring.ml - OCAMLOPT lib/Printlines.ml - OCAMLOPT extraction/DecidableClass.ml - OCAMLC cparser/Transform.mli - OCAMLOPT extraction/Tuples.ml - OCAMLOPT extraction/Streams.ml - OCAMLOPT extraction/Cabs.ml - OCAMLOPT cparser/pre_parser_aux.ml - OCAMLC cparser/pre_parser.mli - OCAMLC cparser/Cflow.mli - OCAMLOPT cparser/Cabshelper.ml - OCAMLOPT lib/Tokenize.ml - OCAMLOPT extraction/UnionFind.ml - OCAMLOPT extraction/Compare_dec.ml - OCAMLOPT extraction/Mergesort.ml - OCAMLOPT driver/Configuration.ml - OCAMLOPT extraction/Nat.ml - OCAMLOPT extraction/BinPosDef.ml - OCAMLC extraction/BinPos.mli - OCAMLOPT extraction/List0.ml - OCAMLOPT extraction/OrdersTac.ml - OCAMLC extraction/OrderedType.mli - OCAMLC extraction/OrdersFacts.mli - OCAMLOPT extraction/DecidableType.ml - OCAMLC extraction/FSetInterface.mli - OCAMLOPT cparser/Env.ml - OCAMLOPT driver/Commandline.ml - OCAMLOPT cparser/Cprint.ml - OCAMLC extraction/Alphabet.mli - OCAMLC extraction/FMapList.mli - OCAMLOPT cparser/pre_parser.ml - OCAMLC cparser/ErrorReports.mli - OCAMLOPT driver/Clflags.ml - OCAMLOPT extraction/BinPos.ml - OCAMLC extraction/Zpower.mli - OCAMLC extraction/BinNat.mli - OCAMLC extraction/Fcore_digits.mli - OCAMLOPT extraction/OrderedType.ml - OCAMLC extraction/OrdersAlt.mli - OCAMLOPT extraction/OrdersFacts.ml - OCAMLC extraction/MSetInterface.mli - OCAMLOPT extraction/FSetInterface.ml - OCAMLOPT cparser/Diagnostics.ml - OCAMLOPT backend/Fileinfo.ml - OCAMLC extraction/Grammar.mli - OCAMLOPT extraction/FMapList.ml - OCAMLOPT extraction/Compopts.ml - OCAMLOPT driver/CommonOptions.ml - OCAMLOPT extraction/Zpower.ml - OCAMLOPT extraction/BinNat.ml - OCAMLC extraction/BinInt.mli - OCAMLOPT extraction/Fcore_digits.ml - OCAMLC extraction/Fcore_Zaux.mli - OCAMLC extraction/Fcore_FLT.mli - OCAMLC extraction/Zbool.mli - OCAMLC extraction/Int0.mli - OCAMLOPT extraction/OrdersAlt.ml - OCAMLOPT extraction/MSetInterface.ml - OCAMLC extraction/MSetAVL.mli - OCAMLOPT cparser/Cutil.ml - OCAMLC extraction/Decidableplus.mli - OCAMLC extraction/Automaton.mli - OCAMLC extraction/FMapAVL.mli - OCAMLC extraction/FSetAVLplus.mli - OCAMLOPT extraction/BinInt.ml - OCAMLC extraction/ZArith_dec.mli - OCAMLC extraction/Fcalc_bracket.mli - OCAMLOPT extraction/Int0.ml - OCAMLC extraction/FSetAVL.mli - OCAMLOPT extraction/Decidableplus.ml - OCAMLC extraction/Validator_safe.mli - OCAMLC extraction/Interpreter_correct.mli - OCAMLC extraction/Interpreter.mli - OCAMLOPT cparser/ErrorReports.ml - OCAMLOPT extraction/ZArith_dec.ml - OCAMLC extraction/Coqlib.mli - OCAMLOPT extraction/Fcore_Zaux.ml - OCAMLOPT extraction/Fcore_FLT.ml - OCAMLOPT extraction/Zbool.ml - OCAMLC extraction/Fcalc_round.mli - OCAMLC extraction/Maps.mli - OCAMLOPT extraction/MSetAVL.ml - OCAMLC extraction/Iteration.mli - OCAMLC extraction/Unityping.mli - OCAMLOPT cparser/Ceval.ml - OCAMLOPT cparser/Builtins.ml - OCAMLC extraction/Interpreter_safe.mli - OCAMLOPT extraction/FMapAVL.ml - OCAMLC extraction/Validator_complete.mli - OCAMLOPT cparser/Checks.ml - OCAMLOPT cparser/Cflow.ml - OCAMLC extraction/Postorder.mli - OCAMLC extraction/IntvSets.mli - OCAMLOPT extraction/FSetAVLplus.ml - OCAMLOPT extraction/Coqlib.ml - OCAMLOPT extraction/Fcalc_bracket.ml - OCAMLC extraction/Fappli_IEEE.mli - OCAMLOPT extraction/Maps.ml - OCAMLC extraction/Ordered.mli - OCAMLOPT extraction/FSetAVL.ml - OCAMLC extraction/Lattice.mli - OCAMLOPT extraction/Iteration.ml - OCAMLC extraction/Heaps.mli - OCAMLOPT cparser/Transform.ml - OCAMLOPT cparser/Rename.ml - OCAMLC extraction/Interpreter_complete.mli - OCAMLOPT extraction/Postorder.ml - OCAMLOPT extraction/IntvSets.ml - OCAMLOPT extraction/Fcalc_round.ml - OCAMLC extraction/Archi.mli - OCAMLC extraction/Fappli_IEEE_extra.mli - OCAMLC extraction/Fappli_IEEE_bits.mli - OCAMLOPT extraction/Ordered.ml - OCAMLC extraction/Registers.mli - OCAMLOPT extraction/Lattice.ml - OCAMLC extraction/Kildall.mli - OCAMLOPT extraction/Unityping.ml - OCAMLOPT cparser/StructPassing.ml - OCAMLC extraction/Main.mli - OCAMLOPT cparser/PackedStructs.ml - OCAMLC x86/CBuiltins.ml - OCAMLOPT extraction/Fappli_IEEE.ml - OCAMLC extraction/Integers.mli - OCAMLOPT extraction/Registers.ml - OCAMLOPT extraction/Heaps.ml - OCAMLOPT extraction/Archi.ml - OCAMLOPT extraction/Fappli_IEEE_extra.ml - OCAMLOPT extraction/Fappli_IEEE_bits.ml - OCAMLC extraction/Floats.mli - OCAMLOPT extraction/Kildall.ml - OCAMLOPT x86/CBuiltins.ml - OCAMLC extraction/Switch.mli - OCAMLOPT extraction/Integers.ml - OCAMLC extraction/AST.mli - OCAMLC lib/Camlcoq.ml - OCAMLC extraction/Parser.mli - OCAMLC extraction/Op.mli - OCAMLC extraction/Values.mli - OCAMLC extraction/Ctypes.mli - OCAMLC common/Sections.mli - OCAMLC backend/AisAnnot.mli - OCAMLC extraction/Cminor.mli - OCAMLC extraction/Events.mli - OCAMLC debug/DebugTypes.mli - OCAMLC extraction/CminorSel.mli - OCAMLC extraction/Csharpminor.mli - OCAMLC extraction/CSEdomain.mli - OCAMLOPT extraction/Floats.ml - OCAMLC extraction/Machregs.mli - OCAMLC extraction/RTL.mli - OCAMLC extraction/Memdata.mli - OCAMLC debug/DwarfTypes.mli - OCAMLC extraction/Asm.mli - OCAMLC extraction/Determinism.mli - OCAMLC extraction/Unusedglob.mli - OCAMLOPT extraction/Switch.ml - OCAMLC extraction/SelectOp.mli - OCAMLC extraction/Renumber.mli - OCAMLC extraction/RTLgen.mli - OCAMLC extraction/ValueDomain.mli - OCAMLC extraction/Liveness.mli - OCAMLC extraction/Cminorgen.mli - OCAMLC extraction/CombineOp.mli - OCAMLC backend/Asmexpandaux.mli - OCAMLC x86/AsmToJSON.mli - OCAMLOPT lib/Camlcoq.ml - OCAMLOPT extraction/AST.ml - OCAMLC extraction/Locations.mli - OCAMLC x86/Machregsaux.mli - OCAMLC extraction/Mach.mli - OCAMLC extraction/Memory.mli - OCAMLC debug/Debug.mli - File "debug/Debug.mli", line 1: - Error: Corrupted compiled interface - lib/Camlcoq.cmi - make[2]: *** [Makefile.extr:117: debug/Debug.cmi] Error 2 - make[2]: *** Waiting for unfinished jobs.... - OCAMLOPT debug/DwarfUtil.ml - make[2]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-compcert.3.4' - make[1]: *** [Makefile:164: ccomp] Error 2 - make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-compcert.3.4' - make: *** [Makefile:139: all] Error 2 [ERROR] The compilation of coq-compcert failed at "/home/bench/.opam/opam-init/hooks/sandbox.sh build make -j4". #=== ERROR while compiling coq-compcert.3.4 ===================================# # context 2.0.6 | 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-compcert.3.4 # command ~/.opam/opam-init/hooks/sandbox.sh build make -j4 # exit-code 2 # env-file ~/.opam/log/coq-compcert-9047-e4db2f.env # output-file ~/.opam/log/coq-compcert-9047-e4db2f.out ### output ### # [...] # OCAMLC extraction/Memory.mli # OCAMLC debug/Debug.mli # File "debug/Debug.mli", line 1: # Error: Corrupted compiled interface # lib/Camlcoq.cmi # make[2]: *** [Makefile.extr:117: debug/Debug.cmi] Error 2 # make[2]: *** Waiting for unfinished jobs.... # OCAMLOPT debug/DwarfUtil.ml # make[2]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-compcert.3.4' # make[1]: *** [Makefile:164: ccomp] Error 2 # make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-compcert.3.4' # make: *** [Makefile:139: all] Error 2 <><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><> +- The following actions failed | - build coq-compcert 3.4 +- - No changes have been performed # Run eval $(opam env) to update the current shell environment 'opam install -y -v coq-compcert.3.4 coq.8.8.2' failed. The middle of the output is truncated (maximum 20000 characters)
No files were installed.
true