Stream: MetaCoq

Topic: MetaCoq 1.0 problems for 8.16


view this post on Zulip 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

view this post on Zulip Yannick Forster (Sep 07 2022 at 11:04):

I'm on it :)

view this post on Zulip 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

view this post on Zulip Yannick Forster (Sep 07 2022 at 12:11):

Ah, maybe the artifact contains the information I ned

view this post on Zulip Karl Palmskog (Sep 07 2022 at 12:28):

@Yannick Forster here is one log: opam-build_4.09.0.zip

view this post on Zulip 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\")")

view this post on Zulip Karl Palmskog (Sep 07 2022 at 12:30):

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

view this post on Zulip Yannick Forster (Sep 07 2022 at 12:41):

Yeah, it is. I think @Matthieu Sozeau has figured it out

view this post on Zulip Yannick Forster (Sep 07 2022 at 12:41):

Trying to reproduce locally again with a better understanding what went wrong

view this post on Zulip 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

view this post on Zulip Yannick Forster (Sep 07 2022 at 12:44):

PR here: https://github.com/MetaCoq/metacoq/pull/748

view this post on Zulip Karl Palmskog (Sep 07 2022 at 12:44):

let me know if I can do anything to help

view this post on Zulip Matthieu Sozeau (Sep 07 2022 at 12:49):

BTW we found out why Coq's CI did not catch this as well

view this post on Zulip Pierre-Marie P├ędrot (Sep 07 2022 at 12:55):

what was the reason?

view this post on Zulip Matthieu Sozeau (Sep 07 2022 at 14:08):

Missing a target in all: , as all: was defined twice in the Makefile

view this post on Zulip 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?

view this post on Zulip Karl Palmskog (Sep 07 2022 at 15:37):

I guess the alternative is MetaCoq 1.0.1+8.16 or similar

view this post on Zulip Matthieu Sozeau (Sep 08 2022 at 14:57):

We'll do a 1.1 soon actually

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip Yannick Forster (Sep 08 2022 at 15:58):

Yes

view this post on Zulip Matthieu Sozeau (Sep 08 2022 at 16:00):

Yes

view this post on Zulip Karl Palmskog (Sep 08 2022 at 16:22):

OK, then I'll take care of the opam archive PR like that.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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 :)

view this post on Zulip Karl Palmskog (Sep 12 2022 at 13:03):

OK, sure, then I'll try to patch when I get a spare moment

view this post on Zulip 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

view this post on Zulip Michael Soegtrop (Sep 20 2022 at 07:15):

Anything I need to do in Coq Platform?

view this post on Zulip Karl Palmskog (Sep 20 2022 at 07:19):

MetaCoq is not part of the Coq Platform yet, right?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Matthieu Sozeau (Sep 20 2022 at 11:27):

I think so

view this post on Zulip Matthieu Sozeau (Sep 20 2022 at 11:27):

Yes, we want in!

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Michael Soegtrop (Sep 20 2022 at 14:38):

@Matthieu Sozeau : my plan is to patch Ocamlfind as follows:

This should work painlessly with all programs which use ocamlfind.

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Sep 22 2022 at 10:21):

Let's be in the extended level for now, I'll put up a request

view this post on Zulip Matthieu Sozeau (Sep 22 2022 at 13:03):

https://github.com/coq/platform/issues/292


Last updated: Feb 04 2023 at 03:30 UTC