-
Notifications
You must be signed in to change notification settings - Fork 50
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Coq-elpi 1.15.5 -- warning 69 is an error #384
Comments
I'll look into the warning, but please read the correct make invocation from the opam file |
I found a workaround. We can include the following variable declaration before 'make build':
This is just what is already generated and placed into Makefile.coq.conf during building, with "+69" changed to "-69". |
It's more a workaround than a fix, isn't it? |
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 math-comp/hierarchy-builder#320 for a report on that. |
In the Debian package, this patch is applied:
|
That's much neater; thanks a bunch!
|
I was suggesting to empty OCAMLWARN, as I do in the opam package |
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!
|
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:
the problem is that warnings are errors, so that means the build stops.
The text was updated successfully, but these errors were encountered: