ยซ Up

compcert 3.3.0 Black list ๐Ÿดโ€โ˜ ๏ธ

Context

# Packages matching: installed
# Name              # Installed # Synopsis
base-bigarray       base
base-num            base        Num library distributed with the OCaml compiler
base-ocamlbuild     base        OCamlbuild binary and libraries 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.0       Formal proof management system
num                 0           The Num library for arbitrary-precision integer and rational arithmetic
ocaml               4.02.3      The OCaml compiler (virtual package)
ocaml-base-compiler 4.02.3      Official 4.02.3 release
ocaml-config        1           OCaml Switch Configuration
ocamlfind           1.9.6       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.07.0"}
  "coq" {> "8.6.0" & < "8.8.1"}
  "menhir" {>= "20161201" & < "20180530"}
]
synopsis: "The CompCert C compiler"
authors: "Xavier Leroy <xavier.leroy@inria.fr>"
url {
  src: "https://github.com/AbsInt/CompCert/archive/v3.3.tar.gz"
  checksum: "md5=89c62f13cea4c2be7917aa04590e8c7d"
}

Lint

Command
true
Return code
0

Dry install ๐Ÿœ๏ธ

Dry install with the current Coq version:

Command
opam install -y --show-action coq-compcert.3.3.0 coq.8.7.0
Return code
0

Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:

Command
true
Return code
0

Install dependencies

Command
opam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-compcert.3.3.0 coq.8.7.0
Return code
0
Duration
2 m 0 s

Install ๐Ÿš€

Command
opam list; echo; ulimit -Sv 16000000; timeout 8h opam install -y -v coq-compcert.3.3.0 coq.8.7.0
Return code
7936
Duration
29 m 0 s
Output
# Packages matching: installed
# Name              # Installed # Synopsis
base-bigarray       base
base-num            base        Num library distributed with the OCaml compiler
base-ocamlbuild     base        OCamlbuild binary and libraries 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.0       Formal proof management system
menhir              20180528    LR(1) parser generator
num                 0           The Num library for arbitrary-precision integer and rational arithmetic
ocaml               4.02.3      The OCaml compiler (virtual package)
ocaml-base-compiler 4.02.3      Official 4.02.3 release
ocaml-config        1           OCaml Switch Configuration
ocamlbuild          0           Build system distributed with the OCaml compiler since OCaml 3.10.0
ocamlfind           1.9.6       A library manager for OCaml
[NOTE] Package coq is already installed (current version is 8.7.0).
The following actions will be performed:
  - install coq-compcert 3.3.0
<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing  1/1: [coq-compcert.3.3.0: http]
[coq-compcert.3.3.0] downloaded from https://github.com/AbsInt/CompCert/archive/v3.3.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.02.3/bin" "-libdir" "/home/bench/.opam/ocaml-base-compiler.4.02.3/lib/compcert" "-install-coqdev" "-clightgen" "-coqdevdir" "/home/bench/.opam/ocaml-base-compiler.4.02.3/lib/coq/user-contrib/compcert" "-ignore-coq-version" (CWD=/home/bench/.opam/ocaml-base-compiler.4.02.3/.opam-switch/build/coq-compcert.3.3.0)
- Testing assembler support for CFI directives... yes
- Testing linker support for '-no-pie' / '-nopie' option... no
- Testing Coq... version 8.7.0 -- good!
- Testing OCaml... version 4.02.3 -- good!
- WARNING: some Intel processors of the Skylake and Kaby Lake generations
- have a hardware bug that can be triggered by this version of OCaml.
- To avoid this risk, it is recommended to use OCaml 4.05 or later.
- Testing OCaml .opt compilers... yes
- Testing Menhir... version 20180528 -- 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.02.3/bin
-     Runtime library provided...... true
-     Library files installed in.... /home/bench/.opam/ocaml-base-compiler.4.02.3/lib/compcert
-     Standard headers provided..... true
-     Standard headers installed in. /home/bench/.opam/ocaml-base-compiler.4.02.3/lib/compcert/include
-     Coq development installed in.. /home/bench/.opam/ocaml-base-compiler.4.02.3/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.02.3/.opam-switch/build/coq-compcert.3.3.0)
- make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.02.3/.opam-switch/build/coq-compcert.3.3.0'
- ocamlopt -o tools/ndfun str.cmxa tools/ndfun.ml
- menhir --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.02.3/.opam-switch/build/coq-compcert.3.3.0'
- make proof
- make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.02.3/.opam-switch/build/coq-compcert.3.3.0'
- COQC lib/Axioms.v
- COQC lib/Coqlib.v
- COQC flocq/Core/Fcore_Zaux.v
- COQC driver/Compopts.v
- COQC cparser/validator/Alphabet.v
- COQC cparser/validator/Tuples.v
- COQC cparser/Cabs.v
- COQC lib/Wfsimpl.v
- COQC cparser/validator/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/validator/Automaton.v
- COQC flocq/Core/Fcore_defs.v
- COQC lib/Lattice.v
- COQC lib/Postorder.v
- COQC common/Unityping.v
- COQC cparser/validator/Interpreter.v
- COQC cparser/validator/Validator_complete.v
- COQC cparser/validator/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/validator/Interpreter_complete.v
- COQC cparser/validator/Interpreter_correct.v
- COQC cparser/validator/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/validator/Main.v
- COQC cparser/Parser.v
- COQC flocq/Core/Fcore_rnd_ne.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_mult_error.v
- COQC flocq/Appli/Fappli_IEEE.v
- COQC flocq/Prop/Fprop_div_sqrt_error.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/Cexec.v
- COQC cfrontend/SimplExprspec.v
- COQC cfrontend/SimplLocalsproof.v
- COQC cfrontend/Cshmgenproof.v
- COQC cfrontend/Cminorgenproof.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/RTLgen.v
- COQC backend/Inlining.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 x86/ValueAOp.v
- COQC x86/ConstpropOp.v
- COQC backend/NeedDomain.v
- COQC backend/Allocation.v
- COQC backend/Tunneling.v
- COQC backend/Linear.v
- COQC backend/SelectDiv.v
- COQC backend/Tailcallproof.v
- COQC backend/ValueAnalysis.v
- COQC x86/ConstpropOpproof.v
- COQC x86/NeedOp.v
- COQC backend/Allocproof.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 x86/SelectLongproof.v
- COQC backend/Constprop.v
- COQC backend/CSE.v
- COQC backend/Deadcode.v
- COQC backend/Linearizeproof.v
- COQC backend/CleanupLabelsproof.v
- COQC backend/Debugvarproof.v
- COQC x86/Stacklayout.v
- COQC backend/SelectDivproof.v
- COQC backend/Constpropproof.v
- COQC backend/CSEproof.v
- COQC backend/Deadcodeproof.v
- COQC backend/Mach.v
- COQC x86/Asm.v
- COQC backend/Stacking.v
- COQC backend/Selectionproof.v
- COQC backend/Stackingproof.v
- COQC x86/Asmgen.v
- COQC backend/Asmgenproof0.v
- COQC x86/Asmgenproof1.v
- COQC x86/Asmgenproof.v
- COQC driver/Compiler.v
- COQC driver/Complements.v
- make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.02.3/.opam-switch/build/coq-compcert.3.3.0'
- make extraction
- make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.02.3/.opam-switch/build/coq-compcert.3.3.0'
- 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
[...] truncated
file.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
- OCAMLC   cparser/Diagnostics.mli
- OCAMLC   cparser/Cprint.mli
- OCAMLOPT lib/Responsefile.ml
- 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 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 cparser/Cabshelper.ml
- 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
- OCAMLOPT extraction/OrdersAlt.ml
- OCAMLOPT extraction/MSetInterface.ml
- OCAMLOPT cparser/Cutil.ml
- OCAMLC   extraction/Decidableplus.mli
- OCAMLC   extraction/Automaton.mli
- OCAMLOPT extraction/BinInt.ml
- OCAMLC   extraction/ZArith_dec.mli
- OCAMLC   extraction/Fcore_Zaux.mli
- OCAMLC   extraction/Fcore_FLT.mli
- OCAMLC   extraction/Zbool.mli
- OCAMLC   extraction/Int0.mli
- OCAMLC   extraction/Validator_safe.mli
- OCAMLC   extraction/Interpreter_correct.mli
- OCAMLC   extraction/FMapAVL.mli
- OCAMLC   extraction/Interpreter.mli
- 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_bracket.mli
- OCAMLC   extraction/Maps.mli
- OCAMLOPT extraction/Int0.ml
- OCAMLC   extraction/MSetAVL.mli
- OCAMLC   extraction/Lattice.mli
- OCAMLC   extraction/Iteration.mli
- OCAMLC   extraction/Unityping.mli
- OCAMLOPT cparser/Ceval.ml
- OCAMLOPT cparser/Builtins.ml
- OCAMLOPT extraction/Decidableplus.ml
- OCAMLC   extraction/Interpreter_safe.mli
- OCAMLOPT extraction/FMapAVL.ml
- OCAMLOPT cparser/ErrorReports.ml
- OCAMLOPT cparser/Checks.ml
- OCAMLC   extraction/Postorder.mli
- OCAMLC   extraction/IntvSets.mli
- OCAMLC   extraction/FSetAVLplus.mli
- OCAMLOPT extraction/Coqlib.ml
- OCAMLOPT extraction/Fcalc_bracket.ml
- OCAMLC   extraction/Fcalc_round.mli
- OCAMLOPT extraction/Maps.ml
- OCAMLC   extraction/Ordered.mli
- OCAMLOPT extraction/MSetAVL.ml
- OCAMLC   extraction/FSetAVL.mli
- OCAMLOPT extraction/Iteration.ml
- OCAMLC   extraction/Heaps.mli
- OCAMLOPT extraction/Unityping.ml
- OCAMLOPT cparser/Transform.ml
- OCAMLOPT cparser/Rename.ml
- OCAMLC   extraction/Validator_complete.mli
- OCAMLOPT cparser/Cflow.ml
- OCAMLOPT extraction/Postorder.ml
- OCAMLOPT extraction/IntvSets.ml
- OCAMLOPT extraction/FSetAVLplus.ml
- OCAMLOPT extraction/Fcalc_round.ml
- OCAMLC   extraction/Fappli_IEEE.mli
- OCAMLOPT extraction/Ordered.ml
- OCAMLOPT extraction/FSetAVL.ml
- OCAMLC   extraction/Registers.mli
- OCAMLOPT extraction/Lattice.ml
- OCAMLC   extraction/Kildall.mli
- OCAMLOPT cparser/StructPassing.ml
- OCAMLC   extraction/Interpreter_complete.mli
- OCAMLOPT cparser/PackedStructs.ml
- OCAMLOPT extraction/Fappli_IEEE.ml
- OCAMLC   extraction/Archi.mli
- OCAMLC   extraction/Fappli_IEEE_extra.mli
- OCAMLC   extraction/Fappli_IEEE_bits.mli
- OCAMLOPT extraction/Registers.ml
- OCAMLOPT extraction/Heaps.ml
- OCAMLC   extraction/Main.mli
- OCAMLC   x86/CBuiltins.ml
- OCAMLOPT extraction/Archi.ml
- OCAMLC   extraction/Integers.mli
- OCAMLOPT extraction/Fappli_IEEE_extra.ml
- OCAMLOPT extraction/Fappli_IEEE_bits.ml
- OCAMLOPT extraction/Kildall.ml
- OCAMLOPT x86/CBuiltins.ml
- OCAMLC   extraction/Switch.mli
- OCAMLOPT extraction/Integers.ml
- OCAMLC   extraction/Floats.mli
- 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
- OCAMLOPT extraction/Switch.ml
- 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   x86/Machregsaux.mli
- OCAMLC   extraction/Mach.mli
- OCAMLC   extraction/Memdata.mli
- OCAMLC   debug/DwarfTypes.mli
- OCAMLC   extraction/Asm.mli
- OCAMLOPT debug/DwarfUtil.ml
- OCAMLC   debug/DwarfPrinter.mli
- OCAMLC   extraction/Determinism.mli
- OCAMLC   extraction/Unusedglob.mli
- OCAMLC   extraction/SelectOp.mli
- OCAMLC   extraction/Renumber.mli
- OCAMLC   extraction/RTLgen.mli
- OCAMLC   cparser/ExtendedAsm.ml
- OCAMLC   extraction/ValueDomain.mli
- OCAMLC   extraction/Liveness.mli
- OCAMLC   extraction/Cminorgen.mli
- OCAMLC   extraction/CombineOp.mli
- OCAMLC   extraction/Asmgen.mli
- OCAMLC   backend/Asmexpandaux.mli
- OCAMLC   x86/AsmToJSON.mli
- OCAMLOPT lib/Camlcoq.ml
- OCAMLOPT extraction/AST.ml
- OCAMLC   extraction/Locations.mli
- OCAMLC   extraction/Memory.mli
- OCAMLC   debug/Debug.mli
- OCAMLC   backend/PrintAsm.mli
- OCAMLC   debug/DebugInformation.mli
- OCAMLC   extraction/Linear.mli
- File "debug/DebugInformation.mli", line 1:
- Error: Corrupted compiled interface
- lib/Camlcoq.cmi
- make[2]: *** [Makefile.extr:116: debug/DebugInformation.cmi] Error 2
- make[2]: *** Waiting for unfinished jobs....
- make[2]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.02.3/.opam-switch/build/coq-compcert.3.3.0'
- make[1]: *** [Makefile:164: ccomp] Error 2
- make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.02.3/.opam-switch/build/coq-compcert.3.3.0'
- 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.3.0 =================================#
# context              2.0.6 | linux/x86_64 | ocaml-base-compiler.4.02.3 | file:///home/bench/run/opam-coq-archive/released
# path                 ~/.opam/ocaml-base-compiler.4.02.3/.opam-switch/build/coq-compcert.3.3.0
# command              ~/.opam/opam-init/hooks/sandbox.sh build make -j4
# exit-code            2
# env-file             ~/.opam/log/coq-compcert-29052-e4db2f.env
# output-file          ~/.opam/log/coq-compcert-29052-e4db2f.out
### output ###
# [...]
# OCAMLC   backend/PrintAsm.mli
# OCAMLC   debug/DebugInformation.mli
# OCAMLC   extraction/Linear.mli
# File "debug/DebugInformation.mli", line 1:
# Error: Corrupted compiled interface
# lib/Camlcoq.cmi
# make[2]: *** [Makefile.extr:116: debug/DebugInformation.cmi] Error 2
# make[2]: *** Waiting for unfinished jobs....
# make[2]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.02.3/.opam-switch/build/coq-compcert.3.3.0'
# make[1]: *** [Makefile:164: ccomp] Error 2
# make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.02.3/.opam-switch/build/coq-compcert.3.3.0'
# make: *** [Makefile:139: all] Error 2
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build coq-compcert 3.3.0
+- 
- No changes have been performed
# Run eval $(opam env) to update the current shell environment
'opam install -y -v coq-compcert.3.3.0 coq.8.7.0' failed.
The middle of the output is truncated (maximum 20000 characters)

Installation size

No files were installed.

Uninstall ๐Ÿงน

Command
true
Return code
0
Missing removes
none
Wrong removes
none