Karl Palmskog (Sep 07 2022 at 11:03): Karl Palmskog (Sep 07 2022 at 11:03):I already pinged Matthieu and Yannick, but any other MetaCoq devs/experts are also welcome to weigh in on the CI problems here for Coq 8.16.0: https://github.com/coq/opam-coq-archive/pull/2288
Yannick Forster (Sep 07 2022 at 11:04):I'm on it :)
Yannick Forster (Sep 07 2022 at 12:05):@Karl Palmskog I can't reproduce the problem locally. The log and artifact don't really mention the exact error. Is there the possibility to get access to the output file metioned here https://gitlab.com/coq/opam-coq-archive/-/jobs/2990478305#L2137
Yannick Forster (Sep 07 2022 at 12:11):Ah, maybe the artifact contains the information I ned
Karl Palmskog (Sep 07 2022 at 12:28):@Yannick Forster here is one log: opam-build_4.09.0.zip
Karl Palmskog (Sep 07 2022 at 12:29):the error might be have to do with Dynlink plugin stuff?
- coq_makefile -f _CoqProject -o Makefile.coq
- make -f Makefile.coq TIMED=
- make[1]: Entering directory '/builds/coq/opam-coq-archive/opam-root-4.09.0-2.1.2-sandbox/4.09.0/.opam-switch/build/coq-metacoq-translations.1.0+8.16/translations'
- COQDEP VFILES
- COQC sigma.v
- COQC MiniHoTT.v
- File "./sigma.v", line 2, characters 0-47:
- Error:
- Dynlink error: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"../template-coq/./src/template_coq.cmxs: cannot open shared object file: No such file or directory\")")
or could it be that the translations package needs to have things locally built? When we build using opam packages, the other packages are already installed in user-contrib
Yannick Forster (Sep 07 2022 at 12:41):Yeah, it is. I think @Matthieu Sozeau has figured it out
Yannick Forster (Sep 07 2022 at 12:41):Trying to reproduce locally again with a better understanding what went wrong
Yannick Forster (Sep 07 2022 at 12:44):Yes, so: make -C template-coq all install and then make -C template-coq clean and then make -C translations all install reproduces the opam situation, and the clean is crucial to reproduce. It then indeed fails, with exactly the dynlink error. We need a new release for MetaCoq to solve the issue
Yannick Forster (Sep 07 2022 at 12:44):PR here: https://github.com/MetaCoq/metacoq/pull/748
Karl Palmskog (Sep 07 2022 at 12:44):let me know if I can do anything to help
Matthieu Sozeau (Sep 07 2022 at 12:49):BTW we found out why Coq's CI did not catch this as well
Pierre-Marie Pédrot (Sep 07 2022 at 12:55):what was the reason?
Matthieu Sozeau (Sep 07 2022 at 14:08):Missing a target in all: , as all: was defined twice in the Makefile
Karl Palmskog (Sep 07 2022 at 15:37):is it going to be a re-release of 1.0 for 8.16? So the only thing that changes is the archive SHA?
Karl Palmskog (Sep 07 2022 at 15:37):I guess the alternative is MetaCoq 1.0.1+8.16 or similar
Matthieu Sozeau (Sep 08 2022 at 14:57):We'll do a 1.1 soon actually
Matthieu Sozeau (Sep 08 2022 at 14:58):We can make a 1.0.1 just for 8.16 if necessary (the bug only happens in 8.16) if time presses for the platform
Karl Palmskog (Sep 08 2022 at 15:03):fine with me to do 1.1. We will have to ping @Michael Soegtrop for opinions if there's any Platform hurry
Matthieu Sozeau (Sep 08 2022 at 15:31):We just discussed with Yannick and a fast and easy solution is to just comment the translations package (nobody's relying on that afaik)
Karl Palmskog (Sep 08 2022 at 15:56):@Matthieu Sozeau just so I understand, we remove the coq-metacoq-translations.1.0+8.16 package completely?
Yannick Forster (Sep 08 2022 at 15:58):Yes
Matthieu Sozeau (Sep 08 2022 at 16:00):Yes
Karl Palmskog (Sep 08 2022 at 16:22):OK, then I'll take care of the opam archive PR like that.
Karl Palmskog (Sep 08 2022 at 18:34):one option to think about: we can add back the translations package, but with a patch in the opam repo for the build
Michael Soegtrop (Sep 09 2022 at 07:20):The platform picking is more or less done, but I still have to fix issues on all platforms caused by the new library loader, so there is time. My plan is to do the beta mid next week, so Monday is fine for the beta.
Matthieu Sozeau (Sep 12 2022 at 12:57):@Karl Palmskog That would be the patch you need then: https://github.com/MetaCoq/metacoq/commit/1b0993e57255c08e368082bc257a9f873ddbb1dd
Matthieu Sozeau (Sep 12 2022 at 12:57):(I've not tried patching of opam packages, so if you have the know how you'll be faster :)
Karl Palmskog (Sep 12 2022 at 13:03):OK, sure, then I'll try to patch when I get a spare moment
Karl Palmskog (Sep 20 2022 at 06:28):OK, just to flag up here as well, patch was done now, all MetaCoq 1.0 packages are in 8.16: https://github.com/coq/opam-coq-archive/pull/2305
Michael Soegtrop (Sep 20 2022 at 07:15):Anything I need to do in Coq Platform?
Karl Palmskog (Sep 20 2022 at 07:19):MetaCoq is not part of the Coq Platform yet, right?
Bas Spitters (Sep 20 2022 at 10:34):But now that 1.0 is out, it might be a good idea to add it to platform, don't you think?
Paolo Giarrusso (Sep 20 2022 at 11:23):Michael wrote so: https://coq.zulipchat.com/#narrow/stream/237658-MetaCoq/topic/opam.20install.20metacoq-template.20.20does.20not.20work.20on.20MacOs/near/280197826
Paolo Giarrusso (Sep 20 2022 at 11:25):@Bas Spitters But being in the platform puts a maintenance obligation on metacoq's maintainers, so I guess it's not Michael's decision? I thought @Yannick Forster / @Matthieu Sozeau were in favor, but I can't actually find that, and that thread seems the closest thing?
Matthieu Sozeau (Sep 20 2022 at 11:27):I think so
Matthieu Sozeau (Sep 20 2022 at 11:27):Yes, we want in!
Karl Palmskog (Sep 20 2022 at 11:36):to make it easier to track the inclusion process, we usually encourage creating a Platform inclusion issue for new packages, see here for an example: https://github.com/coq/platform/issues/265
Michael Soegtrop (Sep 20 2022 at 12:37):Sorry I was unclear - my question was if I should include it now. Afair the result of the last discussion (can't find it right now) was to include it when 1.0 is out.
Michael Soegtrop (Sep 20 2022 at 12:38):I am still having rather severe issues with the hard non reloctability introduced by using findlib, so there is a bit of time left for the beta.
Matthieu Sozeau (Sep 20 2022 at 14:33):Ha damn, that might impact metacoq quite strongly , there's a chain of dynamic ocaml libraries produced in it
Michael Soegtrop (Sep 20 2022 at 14:38):@Matthieu Sozeau : my plan is to patch Ocamlfind as follows:
... meaning Ocamlfind should search the folder of the current executable upstream until it reaches / or a folder containing the empty file ocamlfindroot.This should work painlessly with all programs which use ocamlfind.
Michael Soegtrop (Sep 20 2022 at 16:40):@Matthieu Sozeau : I just finished the above patch(es) and it seems to work. Do you think it would work for MetaCoq as well?
Matthieu Sozeau (Sep 20 2022 at 16:45):I'm not sure I get everything, but it should yes. In MetaCoq / master we let ocamlfind lookup the plugins (we're not using the compatibility stuff)
Michael Soegtrop (Sep 20 2022 at 16:53):If you use Ocamlfind and nothing else, you should be fine. The above patches make Ocamlfind relocatable in a quite robust and OS independent way (to be tested on all platforms). Some installed platforms like Snap are quite nasty because they have variable install paths but an immutable installation image (snap mounts a RO filesystem image to the install location).
Michael Soegtrop (Sep 22 2022 at 10:20):@Matthieu Sozeau @Yannick Forster : is there a conclusion on the "include in Coq Platform" question? If so, please create a request issue in Coq Platform github. Please state if it should go into the "extended/experimental" or the "full/normal" section. Things in the "full" section should not expect dramatic API changes, which would put a lot of effort on users to do compatibility fixes when switching to the next release. In the "extended" level there is no such restriction.
Matthieu Sozeau (Sep 22 2022 at 10:21):Let's be in the extended level for now, I'll put up a request
Matthieu Sozeau (Sep 22 2022 at 13:03):https://github.com/coq/platform/issues/292
Last updated: May 31 2023 at 04:01 UTC