ยซ Up

compcert 3.6 Error ๐Ÿ”ฅ

Context

# 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"
}

Lint

Command
true
Return code
0

Dry install ๐Ÿœ๏ธ

Dry install with the current Coq version:

Command
opam install -y --show-action coq-compcert.3.6 coq.8.11.dev
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 2h opam install -y --deps-only coq-compcert.3.6 coq.8.11.dev
Return code
0
Duration
1 m 0 s

Install ๐Ÿš€

Command
opam list; echo; ulimit -Sv 4000000; timeout 2h opam install -y -v coq-compcert.3.6 coq.8.11.dev
Return code
7936
Duration
3 m 0 s
Output
# 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.

Installation size

No files were installed.

Uninstall ๐Ÿงน

Command
true
Return code
0
Missing removes
none
Wrong removes
none