Gaëtan Gilbert (Dec 01 2022 at 16:36): Gaëtan Gilbert (Dec 01 2022 at 16:36):iris started failing in https://gitlab.com/coq/coq/-/jobs/3401776947 (iris examples commit c2f45c7140ec0191ad792ac984f14ef05389e875)
corresponding PR succeeded https://gitlab.com/coq/coq/-/jobs/3379861025 (iris examples commit 7b79d6e2fdbf0cedd80b9346da8b4fc9e7aaa424)
the error is
COQNATIVE theories/lecture_notes/coq_intro_example_1.vo
File "theories/lecture_notes/.coq-native/Niris_examples_lecture_notes_coq_intro_example_1.native", line 12, characters 15-86:
12 | (Obj.magic (Niris_heap_lang_lang.Construct_Niris_heap_lang_lang_heap_lang_expr_0_17((
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Unbound module Niris_heap_lang_lang
it seems something changed exposing a native compile bug?
cc @Ralf Jung
Guillaume Melquiond (Dec 01 2022 at 16:47):From a quick look at the logs, it just seems that the required native libraries were not installed (or perhaps not even compiled).
Guillaume Melquiond (Dec 01 2022 at 17:24):So, yes, they now explicitly pass -native-compiler no when compiling some early files, which breaks native_compute later on: https://gitlab.mpi-sws.org/iris/stdpp/-/commit/c25b43ed83ff78ae53c02a97b2b7e57307925276
Paolo Giarrusso (Dec 01 2022 at 19:13):iris never uses native_compute
Paolo Giarrusso (Dec 01 2022 at 19:14):nor does AFAIK the failing code (https://gitlab.mpi-sws.org/search?search=native_compute&nav_source=navbar&project_id=615&group_id=1795&search_code=true&repository_ref=master)
Paolo Giarrusso (Dec 01 2022 at 19:15):it seems that CI job fails because it's trying to build native libraries?
Paolo Giarrusso (Dec 01 2022 at 19:17):and from the context, I think Iris doesn't really object to building .coq-native files — some clients might _need_ to do that — they just want to ban native_compute from their own Coq sources (to limit their TCB)?
Guillaume Melquiond (Dec 01 2022 at 20:30):Paolo Giarrusso said:
it seems that CI job fails because it's trying to build native libraries?
That is the default behavior of Coq when configured with -native-compiler yes.
Paolo Giarrusso said:
and from the context, I think Iris doesn't really object to building
.coq-nativefiles — some clients might _need_ to do that — they just want to bannative_computefrom their own Coq sources (to limit their TCB)?
If the Iris people want to ban native_compute from their own Coq sources, they should configure their own Coq executable with -native-compiler no. Here, by forcefully passing -native-compiler no to the Coq executable of their users, they are overriding their choice. So, yes, that is really objecting to building native files.
Gaëtan Gilbert (Dec 01 2022 at 21:05):https://gitlab.mpi-sws.org/iris/examples/-/merge_requests/60
Ralf Jung (Dec 01 2022 at 21:10):If the Iris people want to ban native_compute from their own Coq sources, they should configure their own Coq executable with -native-compiler no. Here, by forcefully passing -native-compiler no to the Coq executable of their users, they are overriding their choice. So, yes, that is really objecting to building native files.
we just want native_compute disabled in iris. suggesting to rebuild coq for this is not reasonable IMO. And from the docs it is not at all clear that this choice affects downstream users. So dont read more into this than it is.
there doesnt seem to be a flag that controls native_compute use alone, so affecting the building of native libraries is a collateral side-effect.
our own iris/examples CI job also still works, so there must be something else that is happening here.
Paolo Giarrusso (Dec 01 2022 at 21:28):@Ralf Jung I doubt you actually need to rebuild Coq, unless somehow you have installed coq-native. I totally agree that the available options aren't really ideal for this usecase
Paolo Giarrusso (Dec 01 2022 at 21:29):(in fact, I recall native_compute usually falls back to vm_compute, and I don't know a way to disable that)
Paolo Giarrusso (Dec 02 2022 at 00:21):re "something else", I guess @Guillaume Melquiond 's point was that they used -native-compiler yes when building the Coq install used in CI, while you're using -native-compiler no?
Guillaume Melquiond said:
That is the default behavior of Coq when configured with
-native-compiler yes.
Those are still the two options with opam: https://github.com/ocaml/opam-repository/blob/master/packages/coq/coq.8.16.1/opam#L44.
Ralf Jung (Dec 02 2022 at 11:12):@Paolo Giarrusso I didnt use any flag when installing Coq. it's a default coq install, just with that flag passed in iris.
so it looks like there is an "ABI incompatibility" when
Théo Zimmermann (Dec 02 2022 at 12:32):Indeed, but it makes sense. -native-compiler no can indicate that your library is not compatible with the native compiler so Coq should not try to native compile it. And when you set -native-compiler yes when configuring Coq it amounts to passing -native-compiler yes by default for every use. Therefore, a reverse dependency of Iris will try to native compile Iris and this will fail. We could resolve this on our side (explicitly setting -native-compiler no for reverse dependencies of Iris since it is also on our side that Coq is configured with -native-compiler yes). OTOH, from what I understand, your goal is not really to disable the native compilation of Iris for your users, just for your own sake. In this case, I would recommend setting -native-compiler no in a specific CI job and possibly in your development workflow, but not in the opam package.
Karl Palmskog (Dec 02 2022 at 12:57):shouldn't this kind of requirement (a project that shouldn't be compiled with native) be solved at the opam level by adding a conflict with coq-native?
Guillaume Melquiond (Dec 02 2022 at 13:11):As far as Opam packages are concerned, yes. But for other distribution channels (or even manual compilation, as in the CI), this might not help.
Gaëtan Gilbert (Dec 05 2022 at 14:25):@Ralf Jung so how are we getting coq's ci fixed?
Ralf Jung (Dec 05 2022 at 16:29):I recall asking a question about this in one of the 5 locations that we discussed this problem but cannot find it right now...
Ralf Jung (Dec 05 2022 at 16:30):it was similar to this one though:
So... when a project uses native-compile no, then all their users also have to set that flag? That is surprising. In this case we probably want to remove this flag from Iris. Also the Coq docs need a big warning explaining this.
Ralf Jung (Dec 05 2022 at 16:31):ah it was here, above
Ralf Jung (Dec 05 2022 at 16:32):Indeed, but it makes sense
I guess it makes sense if you are deep in the weeds of coq. from a user perspective it makes no sense. certainly nothing warned us that setting this flag would have any impact whatsoeever on our users, and it's not how coq flags usually behave.
Ralf Jung (Dec 05 2022 at 16:33):Karl Palmskog said:
shouldn't this kind of requirement (a project that shouldn't be compiled with native) be solved at the opam level by adding a conflict with
coq-native?
we dont want it to be impossible to use iris with native-compile, we just dont want it to be built like that for us. usually when we pass coq flags, like to disable warnings, they have exactly this effect. native-compile however is a really strange flag it seems.
Ralf Jung (Dec 05 2022 at 16:34):@Gaëtan Gilbert Ill revert the changes on our side then
Théo Zimmermann (Dec 05 2022 at 16:45):Real "coq flags" (the one you can also set on the vernac side) do behave like this, but this is not such a flag.
Théo Zimmermann (Dec 05 2022 at 16:46):Clearly, we should improve the documentation at the very least.
Ralf Jung (Dec 05 2022 at 16:53):In this case, I would recommend setting -native-compiler no in a specific CI job and possibly in your development workflow, but not in the opam package.
Yeah makes sense, this is what we are going with now
Ralf Jung (Dec 05 2022 at 17:26):the update landed in iris/examples, so CI should work again, hopefully
Ralf Jung (Dec 05 2022 at 17:26):sorry this took so long
Last updated: Oct 12 2024 at 11:01 UTC