Breaking changes in Coq 8.5~beta3

Apparently, the bench cannot compile the 1.1.0~beta2 version of coq:template-coq on coq.8.5~beta3 too. I updated the dependencies in e20de0711cf70ba01382b352ae196330d78c45f8.

Output of opam list:


# Installed packages for system:
base-bigarray       base  Bigarray library distributed with the OCaml compiler
base-threads        base  Threads library distributed with the OCaml compiler
base-unix           base  Unix library distributed with the OCaml compiler
camlp5              6.14  Preprocessor-pretty-printer of OCaml
coq            8.5~beta3  Formal proof management system.

Output of opam install -y coq:template-coq.1.1.0~beta2:

The following actions will be performed:
  - install coq:template-coq 1.1.0~beta2
=-=- Gathering sources =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
[coq:template-coq: from released] Command started
[coq:template-coq: http] Command started
[coq:template-coq: http] Command started
[coq:template-coq.1.1.0~beta2] https://github.com/gmalecha/template-coq/archive/v1.1.0-beta2.tar.gz downloaded
=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
[coq:template-coq: make] Command started
[ERROR] The compilation of coq:template-coq failed at "make -j4".
[coq:template-coq: rm] Command started
#=== ERROR while installing coq:template-coq.1.1.0~beta2 ======================#
# opam-version         1.2.2
# os                   linux
# command              make -j4
# path                 /home/bench/.opam/system/build/coq:template-coq.1.1.0~beta2
# compiler             system (4.02.2)
# exit-code            2
# env-file             /home/bench/.opam/system/build/coq:template-coq.1.1.0~beta2/coq:template-coq-14720-d2d111.env
# stdout-file          /home/bench/.opam/system/build/coq:template-coq.1.1.0~beta2/coq:template-coq-14720-d2d111.out
# stderr-file          /home/bench/.opam/system/build/coq:template-coq.1.1.0~beta2/coq:template-coq-14720-d2d111.err
### stdout ###
# [...]
# /usr/local/bin/ocamldep.opt -slash -I "src" -pp '/home/bench/.opam/system/bin/camlp5o -I /usr/local/lib/ocaml/ -I /usr/local/lib/ocaml/threads/ -I "/home/bench/.opam/system/lib/coq/kernel" -I "/home/bench/.opam/system/lib/coq/lib" -I "/home/bench/.opam/system/lib/coq/library" -I "/home/bench/.opam/system/lib/coq/parsing" -I "/home/bench/.opam/system/lib/coq/pretyping" -I "/home/bench/.opam/system/lib/coq/interp" -I "/home/bench/.opam/system/lib/coq/printing" -I "/home/bench/.opam/system/lib/coq/intf" -I "/home/bench/.opam/system/lib/coq/proofs" -I "/home/bench/.opam/system/lib/coq/tactics" -I "/home/bench/.opam/system/lib/coq/tools" -I "/home/bench/.opam/system/lib/coq/toplevel" -I "/home/bench/.opam/system/lib/coq/stm" -I "/home/bench/.opam/system/lib/coq/grammar" -I "/home/bench/.opam/system/lib/coq/config" -I "/home/bench/.opam/system/lib/coq//plugins/btauto" -I "/home/bench/.opam/system/lib/coq//plugins/cc" -I "/home/bench/.opam/system/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/system/lib/coq//plugins/derive" -I "/home/bench/.opam/system/lib/coq//plugins/extraction" -I "/home/bench/.opam/system/lib/coq//plugins/firstorder" -I "/home/bench/.opam/system/lib/coq//plugins/fourier" -I "/home/bench/.opam/system/lib/coq//plugins/funind" -I "/home/bench/.opam/system/lib/coq//plugins/micromega" -I "/home/bench/.opam/system/lib/coq//plugins/nsatz" -I "/home/bench/.opam/system/lib/coq//plugins/omega" -I "/home/bench/.opam/system/lib/coq//plugins/quote" -I "/home/bench/.opam/system/lib/coq//plugins/romega" -I "/home/bench/.opam/system/lib/coq//plugins/rtauto" -I "/home/bench/.opam/system/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/system/lib/coq//plugins/syntax" -I "/home/bench/.opam/system/lib/coq//plugins/xml" compat5.cmo pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma grammar.cma -loc loc -impl' -impl "src/reify.ml4" > "src/reify.ml4.d" || ( RV=$?; rm -f "src/reify.ml4.d"; exit ${RV} )
# "coqdep" -c -Q "theories" Template -I "src" "theories/Ast.v" > "theories/Ast.v.d" || ( RV=$?; rm -f "theories/Ast.v.d"; exit ${RV} )
# "coqdep" -c -Q "theories" Template -I "src" "theories/Template.v" > "theories/Template.v.d" || ( RV=$?; rm -f "theories/Template.v.d"; exit ${RV} )
# "coqc"  -q  -Q "theories" Template -I "src"   theories/Ast
# /usr/local/bin/ocamlc.opt -c -rectypes -thread  -I "src" -I "/home/bench/.opam/system/lib/coq/kernel" -I "/home/bench/.opam/system/lib/coq/lib" -I "/home/bench/.opam/system/lib/coq/library" -I "/home/bench/.opam/system/lib/coq/parsing" -I "/home/bench/.opam/system/lib/coq/pretyping" -I "/home/bench/.opam/system/lib/coq/interp" -I "/home/bench/.opam/system/lib/coq/printing" -I "/home/bench/.opam/system/lib/coq/intf" -I "/home/bench/.opam/system/lib/coq/proofs" -I "/home/bench/.opam/system/lib/coq/tactics" -I "/home/bench/.opam/system/lib/coq/tools" -I "/home/bench/.opam/system/lib/coq/toplevel" -I "/home/bench/.opam/system/lib/coq/stm" -I "/home/bench/.opam/system/lib/coq/grammar" -I "/home/bench/.opam/system/lib/coq/config" -I "/home/bench/.opam/system/lib/coq//plugins/btauto" -I "/home/bench/.opam/system/lib/coq//plugins/cc" -I "/home/bench/.opam/system/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/system/lib/coq//plugins/derive" -I "/home/bench/.opam/system/lib/coq//plugins/extraction" -I "/home/bench/.opam/system/lib/coq//plugins/firstorder" -I "/home/bench/.opam/system/lib/coq//plugins/fourier" -I "/home/bench/.opam/system/lib/coq//plugins/funind" -I "/home/bench/.opam/system/lib/coq//plugins/micromega" -I "/home/bench/.opam/system/lib/coq//plugins/nsatz" -I "/home/bench/.opam/system/lib/coq//plugins/omega" -I "/home/bench/.opam/system/lib/coq//plugins/quote" -I "/home/bench/.opam/system/lib/coq//plugins/romega" -I "/home/bench/.opam/system/lib/coq//plugins/rtauto" -I "/home/bench/.opam/system/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/system/lib/coq//plugins/syntax" -I "/home/bench/.opam/system/lib/coq//plugins/xml" -I /home/bench/.opam/system/lib/camlp5 -pp '/home/bench/.opam/system/bin/camlp5o -I /usr/local/lib/ocaml/ -I /usr/local/lib/ocaml/threads/ -I "/home/bench/.opam/system/lib/coq/kernel" -I "/home/bench/.opam/system/lib/coq/lib" -I "/home/bench/.opam/system/lib/coq/library" -I "/home/bench/.opam/system/lib/coq/parsing" -I "/home/bench/.opam/system/lib/coq/pretyping" -I "/home/bench/.opam/system/lib/coq/interp" -I "/home/bench/.opam/system/lib/coq/printing" -I "/home/bench/.opam/system/lib/coq/intf" -I "/home/bench/.opam/system/lib/coq/proofs" -I "/home/bench/.opam/system/lib/coq/tactics" -I "/home/bench/.opam/system/lib/coq/tools" -I "/home/bench/.opam/system/lib/coq/toplevel" -I "/home/bench/.opam/system/lib/coq/stm" -I "/home/bench/.opam/system/lib/coq/grammar" -I "/home/bench/.opam/system/lib/coq/config" -I "/home/bench/.opam/system/lib/coq//plugins/btauto" -I "/home/bench/.opam/system/lib/coq//plugins/cc" -I "/home/bench/.opam/system/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/system/lib/coq//plugins/derive" -I "/home/bench/.opam/system/lib/coq//plugins/extraction" -I "/home/bench/.opam/system/lib/coq//plugins/firstorder" -I "/home/bench/.opam/system/lib/coq//plugins/fourier" -I "/home/bench/.opam/system/lib/coq//plugins/funind" -I "/home/bench/.opam/system/lib/coq//plugins/micromega" -I "/home/bench/.opam/system/lib/coq//plugins/nsatz" -I "/home/bench/.opam/system/lib/coq//plugins/omega" -I "/home/bench/.opam/system/lib/coq//plugins/quote" -I "/home/bench/.opam/system/lib/coq//plugins/romega" -I "/home/bench/.opam/system/lib/coq//plugins/rtauto" -I "/home/bench/.opam/system/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/system/lib/coq//plugins/syntax" -I "/home/bench/.opam/system/lib/coq//plugins/xml" compat5.cmo pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma grammar.cma -loc loc -impl' -impl src/reify.ml4
# /usr/local/bin/ocamlopt.opt -c -rectypes -thread  -I "src" -I "/home/bench/.opam/system/lib/coq/kernel" -I "/home/bench/.opam/system/lib/coq/lib" -I "/home/bench/.opam/system/lib/coq/library" -I "/home/bench/.opam/system/lib/coq/parsing" -I "/home/bench/.opam/system/lib/coq/pretyping" -I "/home/bench/.opam/system/lib/coq/interp" -I "/home/bench/.opam/system/lib/coq/printing" -I "/home/bench/.opam/system/lib/coq/intf" -I "/home/bench/.opam/system/lib/coq/proofs" -I "/home/bench/.opam/system/lib/coq/tactics" -I "/home/bench/.opam/system/lib/coq/tools" -I "/home/bench/.opam/system/lib/coq/toplevel" -I "/home/bench/.opam/system/lib/coq/stm" -I "/home/bench/.opam/system/lib/coq/grammar" -I "/home/bench/.opam/system/lib/coq/config" -I "/home/bench/.opam/system/lib/coq//plugins/btauto" -I "/home/bench/.opam/system/lib/coq//plugins/cc" -I "/home/bench/.opam/system/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/system/lib/coq//plugins/derive" -I "/home/bench/.opam/system/lib/coq//plugins/extraction" -I "/home/bench/.opam/system/lib/coq//plugins/firstorder" -I "/home/bench/.opam/system/lib/coq//plugins/fourier" -I "/home/bench/.opam/system/lib/coq//plugins/funind" -I "/home/bench/.opam/system/lib/coq//plugins/micromega" -I "/home/bench/.opam/system/lib/coq//plugins/nsatz" -I "/home/bench/.opam/system/lib/coq//plugins/omega" -I "/home/bench/.opam/system/lib/coq//plugins/quote" -I "/home/bench/.opam/system/lib/coq//plugins/romega" -I "/home/bench/.opam/system/lib/coq//plugins/rtauto" -I "/home/bench/.opam/system/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/system/lib/coq//plugins/syntax" -I "/home/bench/.opam/system/lib/coq//plugins/xml" -I /home/bench/.opam/system/lib/camlp5 -pp '/home/bench/.opam/system/bin/camlp5o -I /usr/local/lib/ocaml/ -I /usr/local/lib/ocaml/threads/ -I "/home/bench/.opam/system/lib/coq/kernel" -I "/home/bench/.opam/system/lib/coq/lib" -I "/home/bench/.opam/system/lib/coq/library" -I "/home/bench/.opam/system/lib/coq/parsing" -I "/home/bench/.opam/system/lib/coq/pretyping" -I "/home/bench/.opam/system/lib/coq/interp" -I "/home/bench/.opam/system/lib/coq/printing" -I "/home/bench/.opam/system/lib/coq/intf" -I "/home/bench/.opam/system/lib/coq/proofs" -I "/home/bench/.opam/system/lib/coq/tactics" -I "/home/bench/.opam/system/lib/coq/tools" -I "/home/bench/.opam/system/lib/coq/toplevel" -I "/home/bench/.opam/system/lib/coq/stm" -I "/home/bench/.opam/system/lib/coq/grammar" -I "/home/bench/.opam/system/lib/coq/config" -I "/home/bench/.opam/system/lib/coq//plugins/btauto" -I "/home/bench/.opam/system/lib/coq//plugins/cc" -I "/home/bench/.opam/system/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/system/lib/coq//plugins/derive" -I "/home/bench/.opam/system/lib/coq//plugins/extraction" -I "/home/bench/.opam/system/lib/coq//plugins/firstorder" -I "/home/bench/.opam/system/lib/coq//plugins/fourier" -I "/home/bench/.opam/system/lib/coq//plugins/funind" -I "/home/bench/.opam/system/lib/coq//plugins/micromega" -I "/home/bench/.opam/system/lib/coq//plugins/nsatz" -I "/home/bench/.opam/system/lib/coq//plugins/omega" -I "/home/bench/.opam/system/lib/coq//plugins/quote" -I "/home/bench/.opam/system/lib/coq//plugins/romega" -I "/home/bench/.opam/system/lib/coq//plugins/rtauto" -I "/home/bench/.opam/system/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/system/lib/coq//plugins/syntax" -I "/home/bench/.opam/system/lib/coq//plugins/xml" compat5.cmo pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma grammar.cma -loc loc -impl' -impl src/reify.ml4
# Makefile.coq:336: recipe for target 'src/reify.cmo' failed
# Makefile.coq:339: recipe for target 'src/reify.cmx' failed
# make[1]: Leaving directory '/home/bench/.opam/system/build/coq:template-coq.1.1.0~beta2'
# Makefile:2: recipe for target 'coq' failed
### stderr ###
# Error: This variant expression is expected to have type
# [...]
#        The constructor [] does not belong to type option
# make[1]: *** [src/reify.cmo] Error 2
# make[1]: *** Waiting for unfinished jobs....
# File "src/reify.ml4", line 646, characters 3-5:
# Error: This variant expression is expected to have type
#          Vernacexpr.lident list option
#        The constructor [] does not belong to type option
# make[1]: *** [src/reify.cmx] Error 2
# make: *** [coq] Error 2
=-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
The following actions failed
  - install coq:template-coq 1.1.0~beta2
No changes have been performed

gmalecha / template-coq

Breaking changes in Coq 8.5~beta3 #21