error during make

[davidenitti]

I have this error when installing:

make
make[1]: Entering directory '/home/davide/code/coq/FormalML'
COQDEP VFILES
COQC coq/lib_utils/LibUtilsCoqLibAdd.v
COQC coq/lib_utils/LibUtilsLift.v
COQC coq/lib_utils/LibUtilsListAdd.v
COQC coq/lib_utils/LibUtilsStringAdd.v
COQC coq/lib_utils/LibUtilsAssoc.v
File "./coq/lib_utils/LibUtilsAssoc.v", line 1502, characters 14-40:
Error: No such bound variable dec0 (possible names are: dec, l, a and b).

make[2]: *** [Makefile.coq:793: coq/lib_utils/LibUtilsAssoc.vo] Error 1
make[1]: *** [Makefile.coq:409: all] Error 2
make[1]: Leaving directory '/home/davide/code/coq/FormalML'
make: *** [Makefile:9: coq] Error 2

I kind of solved replacing dec0 with dec (but I'm not sure is ok)
but now I get this error

make
make[1]: Entering directory '/home/davide/code/coq/FormalML'
COQDEP VFILES
COQC coq/lib_utils/LibUtilsAssoc.v
COQC coq/lib_utils/LibUtilsSortingAdd.v
COQC coq/lib_utils/LibUtilsSublist.v
COQC coq/lib_utils/LibUtilsBag.v
COQC coq/lib_utils/LibUtilsCompat.v
COQC coq/lib_utils/LibUtilsBindings.v
COQC coq/lib_utils/LibUtilsBindingsNat.v
COQC coq/lib_utils/LibUtilsClosure.v
COQC coq/lib_utils/LibUtilsDigits.v
File "./coq/lib_utils/LibUtilsDigits.v", line 154, characters 80-81:
Error: The reference H was not found in the current environment.

make[2]: *** [Makefile.coq:793: coq/lib_utils/LibUtilsDigits.vo] Error 1
make[1]: *** [Makefile.coq:409: all] Error 2
make[1]: Leaving directory '/home/davide/code/coq/FormalML'
make: *** [Makefile:9: coq] Error 2

I managed to fix second error by installing it in a new switch with opam switch create nnsopt 4.07.0, maybe some version of the default switch is not compatible, in any case I still have the first error and other similar that I fixed as said before (removing the 0 from the name of the variable) but now I have this:

File "./coq/utils/RealAdd.v", line 5318, characters 19-29:
Error: The reference Qreals.Q2R was not found in the current environment.

[shinnar]

Hi! What version of Coq are you using? We currently use 8.12.2. Something in the 8.12 line should work, but we have not tested with newer versions, and it is very likely that things break due to changes in hypothesis naming and such.

If this is a problem for your intended use case (e.g. if you are thinking of using it as part of another development), please tell us, and what version of Coq you need to use.

[davidenitti]

thanks, I managed to compile it by downgrading coq, do you know how I can import the library in coqide? (I'm new with coq)

[shinnar]

Inspired by your post, I just updated our repo to support coq 8.16.1 (it should still support 8.12.2 as well, so no need to change back)

[shinnar]

If you use opam, running something like opam install . in the FormalML directory should work

[davidenitti]

thank you very much, with the new updated version of the code when I import FormalML.ProbTheory.Event I have this error:
Compiled library FormalML.ProbTheory.Event (in file /home/davide/code/coq/FormalML/coq/ProbTheory/Event.vo) makes inconsistent assumptions over library Coq.Init.Ltac
do you know how to fix this?
I'm doing coqide -R /home/davide/code/coq/FormalML/coq/ FormalML
because even installing with opam install . I can't find it without specifying the library
(with the old code and old version of coqide 8.12.2 it was working)

[shinnar]

try make cleanand then either make or opam install . btw, you can run make -j 4 or something similar to compile some files in parallel, if your machine has multiple cores and enough memory

[kodyvajjha]

@davidenitti if you are using proof general + emacs, there is a flag coq-compile-before-require-toggle which you can set to recompile all the files that you import using Require. Within CoqIde there is also a Compile > Make option that I see which might help, although I haven't tried it myself.

[davidenitti]

thanks it works now, but I still have to specify the library in the call: coqide -R FormalML/coq FormalML, not sure if there is a way to automatically find the library. (I installed with opam install with the new code).
if also there is any paper that explain the library would be great.
thank you very much for the support!

[shinnar]

I would recommend putting that in a _CoqProject file (which lives in your top level directory): you can create such a file with -R FormalML/coq FormalML as the only line in it. CoqIDE, as well as other coq tools should read that file and add the argument for you

[shinnar]

Section 3 of https://arxiv.org/pdf/2202.05959.pdf gives highlights of some of the development, although we have added more since then (also, it is of course simplified).