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
I'm on it :)
@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
Ah, maybe the artifact contains the information I ned
@Yannick Forster here is one log: opam-build_4.09.0.zip
the error might be have to do with Dynlink plugin stuff?
- coq_makefile -f _CoqProject -o Makefile.coq - make -f Makefile.coq TIMED= - make: 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
Yeah, it is. I think @Matthieu Sozeau has figured it out
Trying to reproduce locally again with a better understanding what went wrong
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
PR here: https://github.com/MetaCoq/metacoq/pull/748
let me know if I can do anything to help
BTW we found out why Coq's CI did not catch this as well
what was the reason?
Missing a target in
all: , as
all: was defined twice in the Makefile
is it going to be a re-release of 1.0 for 8.16? So the only thing that changes is the archive SHA?
I guess the alternative is MetaCoq 1.0.1+8.16 or similar
We'll do a 1.1 soon actually
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
fine with me to do 1.1. We will have to ping @Michael Soegtrop for opinions if there's any Platform hurry
We just discussed with Yannick and a fast and easy solution is to just comment the translations package (nobody's relying on that afaik)
@Matthieu Sozeau just so I understand, we remove the
coq-metacoq-translations.1.0+8.16 package completely?
OK, then I'll take care of the opam archive PR like that.
one option to think about: we can add back the translations package, but with a patch in the opam repo for the build
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.
@Karl Palmskog That would be the patch you need then: https://github.com/MetaCoq/metacoq/commit/1b0993e57255c08e368082bc257a9f873ddbb1dd
(I've not tried patching of opam packages, so if you have the know how you'll be faster :)
OK, sure, then I'll try to patch when I get a spare moment
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
Anything I need to do in Coq Platform?
MetaCoq is not part of the Coq Platform yet, right?
But now that 1.0 is out, it might be a good idea to add it to platform, don't you think?
Michael wrote so: https://coq.zulipchat.com/#narrow/stream/237658-MetaCoq/topic/opam.20install.20metacoq-template.20.20does.20not.20work.20on.20MacOs/near/280197826
@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?
I think so
Yes, we want in!
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
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.
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.
Ha damn, that might impact metacoq quite strongly , there's a chain of dynamic ocaml libraries produced in it
@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
This should work painlessly with all programs which use ocamlfind.
@Matthieu Sozeau : I just finished the above patch(es) and it seems to work. Do you think it would work for MetaCoq as well?
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)
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).
@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.
Let's be in the extended level for now, I'll put up a request
Last updated: May 31 2023 at 04:01 UTC