Compilation error with Coq 8.5.0

[clarus]

The OPAM Bench got an error for MirrorCore 1.0.0 with Coq 8.5.0 and 6 compilation threads:

# 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.0  Formal proof management system.
coq-ext-lib    0.9.2  A library of Coq definitions, theorems, and tactics.
The following actions will be performed:
  - install coq-mirror-core 1.0.0
=-=- Gathering sources =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
[coq-mirror-core: http] Command started
[coq-mirror-core: http] Command started
[coq-mirror-core.1.0.0] https://github.com/gmalecha/mirror-core/archive/v1.0.0.tar.gz downloaded
=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
[coq-mirror-core: make] Command started
[ERROR] The compilation of coq-mirror-core failed at "make -j6".
[coq-mirror-core: rm] Command started
#=== ERROR while installing coq-mirror-core.1.0.0 =============================#
# opam-version         1.2.2
# os                   linux
# command              make -j6
# path                 /home/bench/.opam/system/build/coq-mirror-core.1.0.0
# compiler             system (4.02.3)
# exit-code            2
# env-file             /home/bench/.opam/system/build/coq-mirror-core.1.0.0/coq-mirror-core-11495-e7966f.env
# stdout-file          /home/bench/.opam/system/build/coq-mirror-core.1.0.0/coq-mirror-core-11495-e7966f.out
# stderr-file          /home/bench/.opam/system/build/coq-mirror-core.1.0.0/coq-mirror-core-11495-e7966f.err
### stdout ###
# [...]
# "coqc"  -q  -Q "theories" MirrorCore -Q "examples" McExamples -I "src" -I "/home/bench/.opam/system/lib/coq//user-contrib/PluginUtils"   theories/EnvI
# "coqc"  -q  -Q "theories" MirrorCore -Q "examples" McExamples -I "src" -I "/home/bench/.opam/system/lib/coq//user-contrib/PluginUtils"   theories/OpenT
# "coqc"  -q  -Q "theories" MirrorCore -Q "examples" McExamples -I "src" -I "/home/bench/.opam/system/lib/coq//user-contrib/PluginUtils"   theories/Generic
# Makefile.coq:519: recipe for target 'theories/CtxLogic.vo' failed
# Makefile.coq:519: recipe for target 'theories/TypesI.vo' failed
# Makefile.coq:519: recipe for target 'theories/EnvI.vo' failed
# Makefile.coq:519: recipe for target 'theories/ExprI.vo' failed
# Makefile.coq:519: recipe for target 'theories/OpenT.vo' failed
# make[1]: Leaving directory '/home/bench/.opam/system/build/coq-mirror-core.1.0.0'
# Makefile:2: recipe for target 'coq' failed
### stderr ###
# [...]
# File "./theories/EnvI.v", line 5, characters 15-32:
# Error: Unable to locate library MirrorCore.TypesI.
# make[1]: *** [theories/EnvI.vo] Error 1
# File "./theories/ExprI.v", line 11, characters 15-37:
# Error: Unable to locate library MirrorCore.Util.Compat.
# make[1]: *** [theories/ExprI.vo] Error 1
# File "./theories/OpenT.v", line 7, characters 15-30:
# Error: Unable to locate library MirrorCore.EnvI.
# make[1]: *** [theories/OpenT.vo] Error 1
# make: *** [coq] Error 2
=-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
The following actions failed
  - install coq-mirror-core 1.0.0
No changes have been performed

[gmalecha]

Is there a way to get the full output? It appears that coq_makefile didn't generate a good dependency graph, and I can not duplicate the problem on my machine.

[clarus]

There are no full outputs yet, so I restarted the bench system with the -v option for OPAM.

It seems that coq_makefile is not very reliable for projects with .ml files. The relation-algebra package got a similar error: https://github.com/damien-pous/relation-algebra/issues/1. I wonder if generating two Makefile, one for the .ml files and the other for .v files, could fix the issue.

[gmalecha]

This seems to be resolved (perhaps improvements to coq_makefile).