Compilation fails with current Coq 8.6 branch

[RalfJung]

I am getting the following error when compiling ssreflect master (b0c734b) against Coq v8.6 (96ed527):

$ nice make -j5
Generating Makefile.coq for Coq v8.6 with COQBIN=/home/r/bin/coq-8.6/bin/
# Override COQDEP to find only the "right" copy .ml files
COQDEP ssreflect_plugin.mlpack
CAMLDEP -pp ssreflect.ml4
Redundant [TYPED AS] clause in [ARGUMENT EXTEND ssrindex].
COQDEP tuple.v
COQDEP prime.v
COQDEP path.v
COQDEP generic_quotient.v
COQDEP fintype.v
COQDEP finset.v
COQDEP fingraph.v
COQDEP finfun.v
COQDEP div.v
COQDEP choice.v
COQDEP binomial.v
COQDEP bigop.v
COQDEP ssrnat.v
COQDEP ssrfun.v
COQDEP ssreflect.v
COQDEP ssrbool.v
COQDEP seq.v
COQDEP eqtype.v
COQDEP all_ssreflect.v
CAMLC -pp -c ssreflect.ml4
Redundant [TYPED AS] clause in [ARGUMENT EXTEND ssrindex].
File "ssreflect.ml4", line 675, characters 55-68:
Warning 3: deprecated: Util.String.set
Use Bytes.set instead.
File "ssreflect.ml4", line 755, characters 25-37:
Warning 3: deprecated: Util.String.set
Use Bytes.set instead.
File "ssreflect.ml4", line 756, characters 19-31:
Warning 3: deprecated: Util.String.set
Use Bytes.set instead.
File "ssreflect.ml4", line 756, characters 33-45:
Warning 3: deprecated: Util.String.set
Use Bytes.set instead.
File "ssreflect.ml4", line 757, characters 5-44:
Warning 3: deprecated: Util.String.set
Use Bytes.set instead.
File "ssreflect.ml4", line 1252, characters 10-24:
Warning 3: deprecated: Util.String.set
Use Bytes.set instead.
File "ssreflect.ml4", line 4441, characters 26-123:
Warning 40: this record of type Proofview.Goal.enter contains fields that are 
not visible in the current scope: enter.
They will not be selected if the type becomes unknown.
File "ssreflect.ml4", line 1049, characters 6-9:
Warning 26: unused variable fmt.
File "ssreflect.ml4", line 1053, characters 6-13:
Warning 26: unused variable tacname.
CAMLC -pack -o ssreflect_plugin.cmo
make[1]: *** No rule to make target 'ssreflect_plugin.mllib', needed by 'ssreflect_plugin.cmxa'.  Stop.
Makefile:24: recipe for target 'all' failed
make: *** [all] Error 2

[ejgallego]

Does the problem go away if you do git clean -fxd ? Indeed the makefile has been broken for while (ie #52)

[ejgallego]

Note that compilation works for me.

[RalfJung]

Yes, I did the git clean -xfd. I also tried sequential building, to no avail.

[RalfJung]

I guess this is probably a coq_makefile bug... which exact version of Coq did you compile against?

[ejgallego]

coq: 472914e
math-comp: b0c734b
ocaml: 4.03.0
os: Debian unstable / Ubuntu (both work)

Maybe make sure that the mathcomp/Make file is clean with git checkout, git clean won't do it.

[RalfJung]

Indeed that file was not clean, strange. I certainly did not edit it myself. And even after cleaning it, the after some experiments I again found an extra line (ssreflect_plugin.mlpack) in there. Seems like something in the build process is modifying the file?

Anyway, after cleaning and updating both repositories, things now work. Thanks for your help :)

[RalfJung]

Seems like something in the build process is modifying the file?

Just to add to this, I can actually reproduce this:

• git clean -xfd && git reset --hard HEAD
• make && make install

Now git diff shows

diff --git a/mathcomp/ssreflect/Make b/mathcomp/ssreflect/Make
index a10b9c5..993c0a7 100644
--- a/mathcomp/ssreflect/Make
+++ b/mathcomp/ssreflect/Make
@@ -22,3 +22,4 @@ ssreflect.ml4

 -I .
 -R . mathcomp.ssreflect
+ssreflect_plugin.mlpack

[ejgallego]

Yeah this is a bit painful and a bug in make system.

[ejgallego]

Maybe you could reopen the bug and title "make is not idempotent"

[RalfJung]

I feel like that's a new bug.