Coq-elpi 1.15.5 -- warning 69 is an error

[SnarkBoojum]

I'm trying to see how I'll get the whole Coq ecosystem updated in Debian when Coq 8.16 will be released, and I'm surprised to be stuck with coq-elpi 1.15.5: it doesn't build!

There are many warning 69 occurrences in src/coq_elpi_HOAS.ml ; here is one:

File "src/coq_elpi_HOAS.ml", line 2567, characters 2-22:
2567 |   uloc : Loc.t option;
         ^^^^^^^^^^^^^^^^^^^^
Error (warning 69 [unused-field]): record field uloc is never read.
(However, this field is used to build or mutate values.)

the problem is that warnings are errors, so that means the build stops.

[gares]

I'll look into the warning, but please read the correct make invocation from the opam file

[chipsf]

I found a workaround. We can include the following variable declaration before 'make build':

COQMF_CAMLFLAGS="-thread -rectypes -w -a+1..3-4+5..8-9+10..26-27+28..40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68-69-70 -bin-annot -safe-string -strict-sequence" make build

This is just what is already generated and placed into Makefile.coq.conf during building, with "+69" changed to "-69". Of course, you'll have to add your own other environment variables at compile time.

[SnarkBoojum]

It's more a workaround than a fix, isn't it?

[chipsf]

It is; I edited my other comment above. It looks like coq-elpi 1.16.0 builds correctly, but that may or may not actually be the case. When trying to build hierarchy-builder, it looked like Coq wasn't able to import coq-elpi; see also https://github.com/math-comp/hierarchy-builder/issues/320 for a report on that.

[SnarkBoojum]

In the Debian package, this patch is applied:

Description: make warning 69 just a warning
Author: Julien Puydt
Forwarded: https://github.com/LPCIC/coq-elpi/issues/384

--- coq-elpi.orig/Makefile.coq.local
+++ coq-elpi/Makefile.coq.local
@@ -1,6 +1,6 @@
 CAMLPKGS+= -package elpi,stdlib-shims
 CAMLFLAGS+= -bin-annot -g
-OCAMLWARN+=-warn-error -32
+OCAMLWARN+=-warn-error -32-69

 theories/elpi.vo: $(wildcard elpi/*.elpi)

[chipsf]

That's much neater; thanks a bunch!

[gares]

I was suggesting to empty OCAMLWARN, as I do in the opam package

[chipsf]

That way works for me too, and it's even neater than before, so I made the change. Yikes, it is right in the opam package and I didn't even see it... thanks for your patience!