# 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
conf-findutils 1 Virtual package relying on findutils
conf-m4 1 Virtual package relying on m4
coq 8.11.dev 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"
authors: "Xavier Leroy <xavier.leroy@inria.fr>"
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 = "darwin"}
"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/"]
]
depends: [
"coq" {>= "8.7.0"}
"menhir" {>= "20190626"}
"ocaml" {>= "4.05.0"}
]
synopsis: "The CompCert C compiler"
tags: [
"category:CS/Semantics and Compilation/Compilation"
"category:CS/Semantics and Compilation/Semantics"
"keyword:C"
"keyword:compiler"
"logpath:compcert"
"date:2019-09-17"
]
url {
src: "https://github.com/AbsInt/CompCert/archive/v3.6.tar.gz"
checksum: "sha256=7a77839f6b990ab632ba14feccf4f17da189f0e3b95d6ce2ef0986e4caebc575"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-compcert.3.6 coq.8.11.devDry 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.6 coq.8.11.devopam list; echo; ulimit -Sv 4000000; timeout 2h opam install -y -v coq-compcert.3.6 coq.8.11.dev# 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 conf-findutils 1 Virtual package relying on findutils conf-m4 1 Virtual package relying on m4 coq 8.11.dev Formal proof management system menhir 20190924 An 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.11.dev). The following actions will be performed: - install coq-compcert 3.6 <><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><> Processing 1/1: [coq-compcert.3.6: http] [coq-compcert.3.6] downloaded from https://github.com/AbsInt/CompCert/archive/v3.6.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.6) - Testing assembler support for CFI directives... yes - Testing linker support for '-no-pie' / '-nopie' option... no - Testing Coq... version 8.11+alpha -- UNSUPPORTED - Warning: this version of Coq is unsupported, proceed at your own risks. - Testing OCaml... version 4.05.0 -- good! - Testing OCaml .opt compilers... yes - Testing Menhir... version 20190924 -- good! - Testing GNU make... version 4.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.6) - make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-compcert.3.6' - ocamlopt -o tools/ndfun str.cmxa tools/ndfun.ml - menhir --coq --coq-lib-path compcert.MenhirLib --coq-no-version-check cparser/Parser.vy - Preprocessing x86/SelectOp.vp - Preprocessing backend/SelectDiv.vp - Preprocessing x86/ConstpropOp.vp - Preprocessing x86/SelectLong.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.6' - make proof - make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-compcert.3.6' - COQC lib/Axioms.v - COQC flocq/Core/Zaux.v - COQC lib/Coqlib.v - COQC driver/Compopts.v - COQC MenhirLib/Alphabet.v - COQC cparser/Cabs.v - COQC lib/Wfsimpl.v - COQC MenhirLib/Validator_classes.v - COQC MenhirLib/Grammar.v - COQC flocq/Core/Raux.v - COQC flocq/Core/Digits.v - COQC MenhirLib/Automaton.v - COQC lib/Intv.v - COQC lib/Maps.v - COQC lib/Zbits.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 MenhirLib/Validator_safe.v - COQC MenhirLib/Validator_complete.v - COQC flocq/Core/Defs.v - COQC lib/Lattice.v - COQC lib/Postorder.v - COQC common/Unityping.v - COQC MenhirLib/Interpreter.v - COQC flocq/Core/Float_prop.v - COQC flocq/Core/Round_pred.v - COQC MenhirLib/Interpreter_complete.v - COQC MenhirLib/Interpreter_correct.v - COQC flocq/Calc/Bracket.v - COQC flocq/Calc/Operations.v - COQC flocq/Core/Generic_fmt.v - COQC flocq/Calc/Div.v - COQC flocq/Core/Ulp.v - COQC flocq/Calc/Sqrt.v - COQC flocq/Prop/Sterbenz.v - COQC MenhirLib/Main.v - COQC cparser/Parser.v - COQC flocq/Core/Round_NE.v - COQC flocq/Core/FIX.v - COQC flocq/Core/FLX.v - COQC flocq/Core/FLT.v - COQC flocq/Core/FTZ.v - COQC flocq/Core/Core.v - COQC flocq/Prop/Double_rounding.v - COQC flocq/Prop/Relative.v - COQC flocq/Calc/Round.v - COQC flocq/Prop/Round_odd.v - COQC flocq/Prop/Plus_error.v - COQC flocq/IEEE754/Binary.v - COQC flocq/Prop/Mult_error.v - COQC flocq/Prop/Div_sqrt_error.v - COQC flocq/IEEE754/Bits.v - COQC lib/IEEE754_extra.v - COQC x86_32/Archi.v - COQC lib/Integers.v - COQC lib/Floats.v - COQC lib/Ordered.v - File "./lib/Ordered.v", line 177, characters 0-4: - Error: (in proof eq_refl): Attempt to save an incomplete proof - - Makefile:193: recipe for target 'lib/Ordered.vo' failed - make[1]: *** [lib/Ordered.vo] Error 1 - make[1]: *** Waiting for unfinished jobs.... - make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-compcert.3.6' - Makefile:135: recipe for target 'all' failed - make: *** [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.6 ===================================# # context 2.0.5 | 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.6 # command ~/.opam/opam-init/hooks/sandbox.sh build make -j4 # exit-code 2 # env-file ~/.opam/log/coq-compcert-31295-2dea01.env # output-file ~/.opam/log/coq-compcert-31295-2dea01.out ### output ### # [...] # COQC lib/Integers.v # COQC lib/Floats.v # COQC lib/Ordered.v # File "./lib/Ordered.v", line 177, characters 0-4: # Error: (in proof eq_refl): Attempt to save an incomplete proof # # Makefile:193: recipe for target 'lib/Ordered.vo' failed # make[1]: *** [lib/Ordered.vo] Error 1 # make[1]: *** Waiting for unfinished jobs.... # make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-compcert.3.6' # Makefile:135: recipe for target 'all' failed # make: *** [all] Error 2 <><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><> +- The following actions failed | - build coq-compcert 3.6 +- - No changes have been performed # Run eval $(opam env) to update the current shell environment 'opam install -y -v coq-compcert.3.6 coq.8.11.dev' failed.
No files were installed.
true