Fix Coq version for coq-compcert.3.6

[clarus]

Logs:

Command
opam list; echo; ulimit -Sv 4000000; timeout 2h opam install -y -v coq-compcert.3.6 coq.8.11.0
Return code
7936
Duration
4 m 27 s
Output
# Packages matching: installed
# Name              # Installed # Synopsis
base-bigarray       base
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.0      Formal proof management system
menhir              20190924    An LR(1) parser generator
num                 1.3         The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml               4.09.0      The OCaml compiler (virtual package)
ocaml-base-compiler 4.09.0      Official release 4.09.0
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.0).
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.09.0/bin" "-libdir" "/home/bench/.opam/ocaml-base-compiler.4.09.0/lib/compcert" "-install-coqdev" "-clightgen" "-coqdevdir" "/home/bench/.opam/ocaml-base-compiler.4.09.0/lib/coq/user-contrib/compcert" "-ignore-coq-version" (CWD=/home/bench/.opam/ocaml-base-compiler.4.09.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.0 -- UNSUPPORTED
- Warning: this version of Coq is unsupported, proceed at your own risks.
- Testing OCaml... version 4.09.0 -- good!
- Testing OCaml .opt compilers... yes
- Testing Menhir... version 20190924 -- 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.09.0/bin
-     Runtime library provided...... true
-     Library files installed in.... /home/bench/.opam/ocaml-base-compiler.4.09.0/lib/compcert
-     Standard headers provided..... true
-     Standard headers installed in. /home/bench/.opam/ocaml-base-compiler.4.09.0/lib/compcert/include
-     Coq development installed in.. /home/bench/.opam/ocaml-base-compiler.4.09.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.09.0/.opam-switch/build/coq-compcert.3.6)
- make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.09.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/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.09.0/.opam-switch/build/coq-compcert.3.6'
- make proof
- make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.09.0/.opam-switch/build/coq-compcert.3.6'
- COQC lib/Axioms.v
- COQC lib/Coqlib.v
- COQC flocq/Core/Zaux.v
- COQC driver/Compopts.v
- COQC MenhirLib/Alphabet.v
- COQC cparser/Cabs.v
- COQC lib/Wfsimpl.v
- COQC MenhirLib/Grammar.v
- COQC MenhirLib/Validator_classes.v
- COQC flocq/Core/Raux.v
- COQC flocq/Core/Digits.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/Automaton.v
- COQC lib/Intv.v
- COQC lib/Maps.v
- COQC lib/Zbits.v
- COQC flocq/Core/Defs.v
- COQC MenhirLib/Validator_safe.v
- COQC MenhirLib/Validator_complete.v
- COQC flocq/Core/Float_prop.v
- COQC flocq/Core/Round_pred.v
- COQC lib/Lattice.v
- COQC lib/Postorder.v
- COQC common/Unityping.v
- COQC MenhirLib/Interpreter.v
- COQC flocq/Core/Generic_fmt.v
- COQC flocq/Calc/Bracket.v
- COQC flocq/Calc/Operations.v
- COQC MenhirLib/Interpreter_complete.v
- COQC MenhirLib/Interpreter_correct.v
- COQC flocq/Core/Ulp.v
- COQC flocq/Calc/Div.v
- COQC flocq/Calc/Sqrt.v
- COQC flocq/Prop/Sterbenz.v
- COQC MenhirLib/Main.v
- COQC flocq/Core/Round_NE.v
- COQC cparser/Parser.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/Calc/Round.v
- COQC flocq/Prop/Relative.v
- COQC flocq/Prop/Round_odd.v
- COQC flocq/IEEE754/Binary.v
- COQC flocq/Prop/Plus_error.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/Ordered.v
- COQC lib/Floats.v
- File "./lib/Ordered.v", line 177, characters 0-4:
- Error:  (in proof eq_refl): Attempt to save an incomplete proof
- 
- make[1]: *** [Makefile:195: lib/Ordered.vo] Error 1
- make[1]: *** Waiting for unfinished jobs....
- make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.09.0/.opam-switch/build/coq-compcert.3.6'
- make: *** [Makefile:136: 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.09.0 | file:///home/bench/run/opam-coq-archive/released
# path                 ~/.opam/ocaml-base-compiler.4.09.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-26991-2dea01.env
# output-file          ~/.opam/log/coq-compcert-26991-2dea01.out
### output ###
# [...]
# COQC lib/IEEE754_extra.v
# COQC x86_32/Archi.v
# COQC lib/Integers.v
# COQC lib/Ordered.v
# COQC lib/Floats.v
# File "./lib/Ordered.v", line 177, characters 0-4:
# Error:  (in proof eq_refl): Attempt to save an incomplete proof
# 
# make[1]: *** [Makefile:195: lib/Ordered.vo] Error 1
# make[1]: *** Waiting for unfinished jobs....
# make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.09.0/.opam-switch/build/coq-compcert.3.6'
# make: *** [Makefile:136: 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.0' failed.

[xavierleroy]

Thanks for the fix. I confirm the master CompCert sources are compatible with Coq 8.11.0, thanks to AbsInt/CompCert#316 .

[clarus]

Top!