Stream: Coq Platform devs & users

Topic: 2022.09+beta1 release


view this post on Zulip Théo Zimmermann (Jun 17 2022 at 07:08):

As a follow-up of Wednesday's discussion, I wanted to insist on the fact that CEP#52 is pretty clear on the naming scheme for the Coq Platform. The reason why the Coq pre-release was renamed from beta to rc is precisely because publishing a beta release (not an rc) would be the role of the Platform. As a consequence, this means that this beta release can be more significantly different from the final 2022.09 Platform release than the 8.16+rc1 Coq release from the 8.16.0 release. In particular, it could have an incomplete package set (see the "core set" mention in the CEP) or one that includes non-released versions ("in accordance with upstreams").

view this post on Zulip Karl Palmskog (Jun 17 2022 at 07:29):

any chance for a paragraph or two on the background here? Did you make any decisions on Platform changes?

view this post on Zulip Karl Palmskog (Jun 17 2022 at 07:29):

for the record, I like the scheme with rc1, rc2, 8.X.0, and then Platform 202Y.Z

view this post on Zulip Théo Zimmermann (Jun 17 2022 at 07:40):

The background discussion is pretty much the follow-up of what was discussed here: the fact that it would take too long to make a Coq 8.16 Platform preview release to conflate it with the 2022.04.1 release containing Coq 8.15.2. Thus, that there would be a separate preview release for Coq 8.16, before the final release of 2022.09 with Coq 8.16. So I'm just reminding what we discussed when writing CEP#52 about how such (dedicated) preview releases should be named. For Coq 8.14 and 8.15, there was no such case because the preview release could be conflated with a release of a new version of the Platform, updating the default pick as well.

view this post on Zulip Karl Palmskog (Jun 17 2022 at 08:18):

since CEP52 doesn't explicitly talk about preview releases, maybe would be good to clarify how those are named/handled in some canonical way (or have I missed where this is done?)

view this post on Zulip Michael Soegtrop (Jun 17 2022 at 08:21):

I think a minor issue with the naming is that there is a version of the platform and a version of the individual picks.

I think it is reasonable to name the whole platform release 2022.09+beta1 (e.g.) and in it have a coq 8.16+beta1 pick (and all the other stable picks ...)

view this post on Zulip Théo Zimmermann (Jun 17 2022 at 08:30):

I think it is reasonable to name the whole platform release 2022.09+beta1 (e.g.) and in it have a coq 8.16+beta1 pick (and all the other stable picks ...)

Yes, I would do this if all the other picks did not change since the last release. If they did, then maybe this means that a new (normal) Platform release is in order (and it can include a beta pick).

view this post on Zulip Théo Zimmermann (Jun 17 2022 at 08:32):

Karl Palmskog said:

since CEP52 doesn't explicitly talk about preview releases, maybe would be good to clarify how those are named/handled in some canonical way (or have I missed where this is done?)

It talks about beta releases. Beta releases are pre-releases. So I don't get the distinction you make with preview releases.

view this post on Zulip Karl Palmskog (Jun 17 2022 at 08:36):

OK, so we conflate the following:

view this post on Zulip Karl Palmskog (Jun 17 2022 at 08:39):

if you want to be strict, you can have tags on GitHub that are not pre-releases - for example, 8.16+rc1 is not listed as a pre-release on GitHub: https://github.com/coq/coq/releases

view this post on Zulip Théo Zimmermann (Jun 17 2022 at 08:49):

Right. It seems that the CEP was insufficiently specific about this aspect: both Pierre-Marie and Guillaume did not create GitHub pre-releases for the rc tags but Gaëtan did.

view this post on Zulip Enrico Tassi (Jun 17 2022 at 10:39):

I don't think this detail should go to the CEP, but rather the release checklist.

view this post on Zulip Enrico Tassi (Jun 17 2022 at 10:40):

After all, this is what the RM follows

view this post on Zulip Enrico Tassi (Jun 17 2022 at 10:40):

I find the CEP even too detailed ;-)

view this post on Zulip Karl Palmskog (Jun 17 2022 at 11:27):

OK, fine by me, I was mainly asking for consistent agreed-on terminology, fine if this goes in checklist

view this post on Zulip Michael Soegtrop (Jul 06 2022 at 16:53):

@Karl Palmskog : I have quite a few opam packages were I just weakened version restrictions (Coq 8.16 and/or mathcomp 1.15). Should I submit the PR as one or separate? ( I believe I asked this before, but can't find the answer, sorry).

view this post on Zulip Karl Palmskog (Jul 06 2022 at 17:07):

@Michael Soegtrop for the Coq 8.16 ones, we can't test them with 8.16 if they are in released, so you can just submit them all in one go and do ci-skip for all of them. For the MathComp 1.15 ones, we can actually test in CI, so please submit only a few at a time in separate PRs (without ci-skip)

view this post on Zulip Michael Soegtrop (Jul 06 2022 at 17:18):

OK - I will try to optimize the "CI makes sense" of my PRs.

view this post on Zulip Michael Soegtrop (Jul 12 2022 at 12:51):

@Karl Palmskog : can you please have a look what is wrong with the ci-skip command in (https://github.com/coq/opam-coq-archive/pull/2231) - it doesn't seem to work.

view this post on Zulip Karl Palmskog (Jul 12 2022 at 13:01):

@Michael Soegtrop the problem is that you have to give the package versions as well. So for example:

ci-skip: coq-compcert-32.3.11

view this post on Zulip Karl Palmskog (Jul 12 2022 at 13:01):

but you don't have to change it for that one, we'll just let it time out and I can merge later today unless I see something weird.

view this post on Zulip Michael Soegtrop (Jul 12 2022 at 13:02):

Ah OK, thanks!

view this post on Zulip Michael Soegtrop (Aug 10 2022 at 13:46):

@Théo Zimmermann : to follow up on the naming discussion at the begin of this thread: I created a "preview" pick, but this lives only in the main branch and is not released. It is intended for package maintainers (it is mentioned in the auto generated issues). I will do a beta release hopefully next week (there are still quite a few packages which don't have working releases).

view this post on Zulip Michael Soegtrop (Aug 10 2022 at 13:48):

The tracker issue is here (https://github.com/coq/platform/issues/274). When the issues is named "Please create a tag" there are serious issues. When the issue is named "Please pick the version" there are at most minor issues like too tight opam version restrictions.

view this post on Zulip Théo Zimmermann (Aug 10 2022 at 13:52):

Thanks for taking care of creating these issues. I noticed that https://github.com/math-comp/real-closed/issues/48 says "Please pick the version you prefer" but currently uses a version called coq-mathcomp-real-closed.preview. Is this normal?

view this post on Zulip Michael Soegtrop (Aug 10 2022 at 15:41):

@Théo Zimmermann : thanks for spotting this - no this is not normal. It skipped my attention and I fixed it later in the scripts. I made a few changes in the opam package naming conventions which were not yet reflected in the scripts.

view this post on Zulip Théo Zimmermann (Aug 10 2022 at 15:42):

BTW, I forgot to say that the issue messages look very clear and much improved to me!

view this post on Zulip Michael Soegtrop (Aug 10 2022 at 15:44):

Thanks to a lot of feedback ;-)

view this post on Zulip Michael Soegtrop (Aug 10 2022 at 15:44):

I fixed the issue for "real-closed" (it should be "please tag" and not "please pick").

view this post on Zulip Pierre Roux (Aug 10 2022 at 16:43):

But why wasnt 'coq-mathcomp-real-closed.1.1.3` picked? it seems to work with 8.16 according to the repo?

view this post on Zulip Michael Soegtrop (Aug 10 2022 at 17:00):

@Pierre Roux : this is likely an error of me (I was away for a few weeks moving homes in the middle of the picking process which didn't make it easier).

view this post on Zulip Michael Soegtrop (Aug 10 2022 at 17:02):

I can conform that 1.1.3 works for me.

view this post on Zulip Pierre Roux (Aug 10 2022 at 17:04):

Great, thanks!

view this post on Zulip Michael Soegtrop (Aug 10 2022 at 17:28):

@Pierre Roux : I fixed the issue message, so if you want 1.1.3, you just need to close it.

view this post on Zulip Michael Soegtrop (Aug 11 2022 at 08:12):

An update on this: apparently GTK is broken in Homebrew since a few days and a few attempts to fix it in CI failed, so I need to setup a machine with homebrew (I am using MacPorts). This might take a bit to investigate.

view this post on Zulip Andrew Appel (Sep 15 2022 at 20:18):

Has the 2022.09+beta1 release happened yet? Is there a Windows binary, or an opam package? I don't see anything on the coq-platform github site.

view this post on Zulip Karl Palmskog (Sep 15 2022 at 20:34):

I'm sure Michael can give more details, but to my knowledge no release has happened yet. The only tickbox left in the tracker issue are some support package fixes, which are getting dealt with for example here.

view this post on Zulip Karl Palmskog (Sep 15 2022 at 20:36):

I guess we will see how adding Fiat Cryptography will pan out as well: https://github.com/coq/platform/issues/178

view this post on Zulip Théo Zimmermann (Sep 15 2022 at 20:44):

The most recent update was: https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/macOS.20Notarization.20by.20INRIA/near/298761035
Quoting Michael:

Main issue is adjusting the installers to the new library loader - I am working on it (and a few other issues).

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 08:39):

@Andrew Appel : not yet, but I am on it. The main issue is that there was a change in all coq executables which make them hard non relocatable - they have now a hard coded path to a config file in them, which is an absolute path in the .opam folder. If this path does not exist (which usually is not the case after installation) they stop immediately with an anomaly. This is new in 8.16 - a change in the way shared libraries are loaded.

One can redirect the config file path with an environment variable, but this is not terribly user friendly. I guess the Coq team would get flooded cause of the "please report" in the anomaly message.

So I decided to patch OCaml findlib such that it looks for its configuration file also in the path of the executable, so that I can leave copies of the config file (which contains paths which need to be patched by the installer) in all paths which contain executables. I just got this patch working (needs some more testing) but then also the installers need to be adjusted to create the patched config files - and then there are some more (minor) issues left.

So there are a few days to go, but I am close.

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 08:51):

P.S.: the patched ocamlfind looks first in the executable path, because if the hard coded .opam path does exist (which is the case e.g. if the installer was built on the same machine on which it is tested), it would pick up the wrong folder. Well it looks first in the env var, next in the exe path and then in the hard coded path.

view this post on Zulip Notification Bot (Sep 16 2022 at 08:53):

This topic was moved here from #Coq users > 2022.09+beta1 release by Michael Soegtrop.

view this post on Zulip Enrico Tassi (Sep 16 2022 at 10:21):

I'm wondering if one cannot just tweak how we call Findlib.init https://github.com/coq/coq/blob/master/sysinit/coqinit.ml#L147 since that API is very flexible (or call init_manually, just below http://projects.camlcity.org/projects/dl/findlib-1.9.5/doc/ref-html/lib/Findlib.html).

view this post on Zulip Enrico Tassi (Sep 16 2022 at 10:21):

Does findlib scan anyway the path it was compiled for?

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 11:41):

@Enrico Tassi : since quite a few executables are involved and I don't know if findlib init is called from a common place, I found it easier to patch findlib - it then also works for all other OCaml apps which might use it. Also I think it is technically the right thing to do to fix the infrastructure.

The unpatched findlib only looks in two places for the findlib.conf file:
1.) the place specified by the environment variable
2.) The hard coded path (derived in the configure file of findlib and patched into this OCaml file

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 11:42):

I also think that one might be able to convince the findlib authors to take such a patch - I guess hard non relocazability is also an issue for any form of OCaml installer.

view this post on Zulip Enrico Tassi (Sep 16 2022 at 11:44):

I'm fine to opt for this solution now, so that we can get things going. And I'm happy if they accept the patch. But if they don't I guess we can follow the other path. The point of sysinit (the Coq component) is to share common initialization code and argument parsing, so ideally all Coq binaries should use it. But I would not put my hand on fire, so I think your path is still safer given the circumstances/time constraints

view this post on Zulip Enrico Tassi (Sep 16 2022 at 11:46):

And I couldn't agree more that relocation of Ocaml binaries is a problem, but findlib is just one of the many bricks. If only it was part of OCaml itself, your patchs would have much more impact. :-/

view this post on Zulip Enrico Tassi (Sep 16 2022 at 11:48):

(ocaml gives you a low level API which we were using before 8.16... so others may do the same, with their home grown way of finding files)

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 11:48):

Agreed, lets follow my path now and see. Btw.: I also thought of binaries in add ons (say quickchick) which might use findlib (one day).

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 11:49):

@Enrico Tassi : another thing: do you have a pointer to the docs of snap path layout after installation? What is the absolute path of the bin and lib folder after a snap is installed?

view this post on Zulip Enrico Tassi (Sep 16 2022 at 11:51):

gares@ollypat:~$ find /snap/ -name coqc 2>/dev/null
/snap/coq-prover/30/coq-platform/2022-04-1/bin/coqc
/snap/coq-prover/29/coq-platform/2022-04-0/bin/coqc
/snap/bin/coqc
gares@ollypat:~$ ls -l /snap/coq-prover/
total 0
drwxr-xr-x 9 root root 119 avril 19 22:05 29
drwxr-xr-x 9 root root 119 juin  20 15:45 30
lrwxrwxrwx 1 root root   2 juin  27 10:53 current -> 30

view this post on Zulip Enrico Tassi (Sep 16 2022 at 11:52):

so I think /snap/coq-prover/current/coq-platform/$VERSION/ is the root

view this post on Zulip Enrico Tassi (Sep 16 2022 at 11:53):

And to take an example of stuff we load via findlib:

gares@ollypat:~$ find /snap/ -name ssreflect_plugin.cmxs 2>/dev/null
/snap/coq-prover/30/coq-platform/2022-04-1/lib/coq-core/plugins/ssreflect/ssreflect_plugin.cmxs

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 11:53):

Nasty. I guess the 29 and 30 are the snap upload numbers - which I don't know upfront?
But afaik snap supports some sort of post install script.

view this post on Zulip Enrico Tassi (Sep 16 2022 at 11:53):

yes they are that
but you can use the current symlink

view this post on Zulip Enrico Tassi (Sep 16 2022 at 11:54):

post install... let me check

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 11:55):

is /snap/bin/coqc a symlink? I wonder what OCaml Sys.executable_name gives in such cases.

view this post on Zulip Enrico Tassi (Sep 16 2022 at 11:56):

Don't worry about snap, since all binaries are actually wrapped in a shell script, let me find it

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 11:57):

Yes, one could set the environment variable there. But is the shell script not only for the "short name exported" executables? What about the others?

view this post on Zulip Enrico Tassi (Sep 16 2022 at 11:58):

https://github.com/coq/platform/blob/28cce1358b93ce2337215b3672c0305a35c119fd/linux/snap/snapcraft.yaml.in#L62
and the wrapper is
https://github.com/coq/platform/blob/28cce1358b93ce2337215b3672c0305a35c119fd/linux/snap/coq_wrapper
so I guess one should just add OCAMLPATH to the set of exported variables

view this post on Zulip Enrico Tassi (Sep 16 2022 at 12:00):

the only available binaries are the "apps:" in the link above. Then the fact that hey have a short name is another story, it does not change anything
if they call other binaries they should inherit the environment (unless one explicitly wipes it before exec)

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 12:01):

I see.

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 12:01):

I will patch the wrapper then. Btw.: doesn't snap have a way to set runtime environment variables?

view this post on Zulip Enrico Tassi (Sep 16 2022 at 12:02):

I think so, and we were using it, IIRC. but the "command chain thing seemed more powerful

view this post on Zulip Enrico Tassi (Sep 16 2022 at 12:04):

here an example: https://forum.snapcraft.io/t/declaratively-defining-environment-variables/175
but the wrapper seems simpler to me

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 12:04):

The env variable is OCAMLFIND_CONFbtw. See (https://github.com/ocaml/ocamlfind/blob/19b0334c467f97328d5005511c34ac9c36235efe/src/findlib/findlib.ml#L111).

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 12:05):

I would find the environment feature simpler, but this is opinion. I will patch the wrapper.

view this post on Zulip Enrico Tassi (Sep 16 2022 at 12:05):

if you follow the thread, it seems the "environment:" directive does not let you override PATH for example (or has some limitations), so people tend to prefer the wrapper

view this post on Zulip Enrico Tassi (Sep 16 2022 at 12:06):

I've no strong opinion, I'm just following the other sheeps ;-)

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 12:09):

I am a bit lost looking at the subtleties of the wrapper. Can you suggest a few lines? They should set OCAMLFIND_CONFto ˙$COQLIB/findlib.conf`

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 12:10):

should I just do an export?

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 12:10):

I don't understand the if chain at the end of the wrapper and if it should go somewhere there.

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 12:11):

Hmm, I guess a simple export should do the trick ...

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 12:16):

CI is running - MacOS and Snap should work now - I didn't look into Windows as yet.

view this post on Zulip Enrico Tassi (Sep 16 2022 at 13:48):

sorry, I was busy. Yes exporting should do it.

view this post on Zulip Enrico Tassi (Sep 16 2022 at 13:52):

IIRC it is just that /snap/bin/coqc really runs /snap/coq-prover/number/bla/bla/bin/coq_wrapper some-path-we-ignore/coqc and in turn the script execs /snap/coq-prover/number/bla/bla/bin/coqc in an environment we set up

view this post on Zulip Enrico Tassi (Sep 16 2022 at 13:53):

IIRC some-path-we-ignore is not absolute, it is relative to the snap root or something...

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 17:11):

@Enrico Tassi : can you please have a look at this : (https://github.com/coq/platform/actions/runs/3067761261/jobs/4957395421#step:7:1176). The smoke test on Mac via installer works now mostly, but it says it can't find elpi, although it does look in the folder where elpi is installed and the folder looks the same as in 8.15.2 (where it does work).

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 17:14):

A general status update: the ocamlfind patch works on mac and Linux, but not on Windows - I get strange errors there.
@gares: can you point me to the exe asside config file read code you added to CoqIDE a while back?

My patch is here : (https://github.com/coq/platform/blob/main/opam/opam-repository/packages/ocamlfind/ocamlfind.1.9.5/files/0001-Look-for-findlib.conf-in-folder-of-executable.patch)

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 17:27):

@Enrico Tassi : some more info on elpi: it works when I run the smoke test with the coqc from opam, but not after installation.
The elpi folder after installation looks like this:

coq-platform-main$ ls -l /Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq/user-contrib/elpi
total 6288
drwxr-xr-x  10 msoegtrop  admin      320 Sep 16 13:58 apps
-rw-r--r--   1 msoegtrop  admin    74301 Sep 16 13:58 coq-builtin.elpi
-rw-r--r--   1 msoegtrop  admin    32073 Sep 16 13:58 coq-lib.elpi
-rw-r--r--   1 msoegtrop  admin    37489 Sep 16 13:58 elpi-builtin.elpi
-rw-r--r--   1 msoegtrop  admin     1850 Sep 16 13:58 elpi.v
-rw-r--r--   1 msoegtrop  admin   255320 Sep 16 13:58 elpi.vo
-rw-r--r--   1 msoegtrop  admin    14917 Sep 16 13:58 elpi_elaborator.elpi
-rw-r--r--   1 msoegtrop  admin  2787808 Sep 16 13:58 elpi_plugin.cmxs

Should I put a copy of the findlib.conf file here? Since there are no executables, I assumed it is not necessary. Currently I have a findlib.conf file only in the bin folder.

view this post on Zulip Karl Palmskog (Sep 16 2022 at 17:33):

@Michael Soegtrop I can use GitHub's suggest feature to add the required changes to the z3_tptp PR if you want, but you'll have to accept the suggestions (https://github.com/ocaml/opam-repository/pull/22100)

view this post on Zulip Enrico Tassi (Sep 16 2022 at 18:46):

Michael Soegtrop said:

Enrico Tassi : can you please have a look at this : (https://github.com/coq/platform/actions/runs/3067761261/jobs/4957395421#step:7:1176). The smoke test on Mac via installer works now mostly, but it says it can't find elpi, although it does look in the folder where elpi is installed and the folder looks the same as in 8.15.2 (where it does work).

it seems Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq-elpi/is missing, while /Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq/user-contrib/elpi is there. Maybe I'm mistaken, but ...user-contrib/* is only taken into account if the plugin uses the "legacy" loading mechanisms, which is not the case for elpi. Did the script purge lib/coq-*? At some point all plugins will put code there (both the META file and the .cmxs).

view this post on Zulip Enrico Tassi (Sep 16 2022 at 18:48):

Many plugins which use both coq_makefile and dune were not fully ported to the new loading mechanism, and still rely on the legacy one. elpi does not use dune, so I could swhich to the new mechanism, maybe this is why the others are still working (thanks to the compat layer).

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:08):

@Enrico Tassi : the folder is there :

coq-platform-main$ cd /Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq-elpi/
coq-elpi$ ls -l
total 5456
-rw-r--r--  1 msoegtrop  admin      249 Sep 16 13:58 META
-rwxr-xr-x  1 msoegtrop  admin  2787808 Sep 16 13:58 elpi_plugin.cmxs

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:09):

Unless I'm mistaken, the log does not list it among the ones findlib scanned

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:09):

wait, is there really a double coq-elpi in the path?

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:09):

or it is a copy&paste error?

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:10):

Sorry, copy&paste

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:10):

I fixed it.

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:10):

ok, so the problem is that it is not scanned by findlib, dunno why

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:11):

the log says lib/coq-core/* and lib/coq/user-contrib/* but not lib/coq-*/*

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:11):

I am running it locally (get the same error) ...

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:12):

Indeed it does not scan it.

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:12):

maybe the config file for findlib you crafted does not recurse properly? (I don't know how this file is done)

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:13):

The file is:

lib$ cat findlib.conf
destdir="/Users/msoegtrop/.opam/__coq-platform.2022.09.0~8.16.0~2022.09~beta1/lib"
path="/Users/msoegtrop/.opam/__coq-platform.2022.09.0~8.16.0~2022.09~beta1/lib"
ocamlc="ocamlc.opt"
ocamlopt="ocamlopt.opt"
ocamldep="ocamldep.opt"
ocamldoc="ocamldoc.opt"

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:13):

Ähm sorry ...

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:13):

That was the original one (from lib)

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:14):

The one it uses is

bin$ cat findlib.conf
destdir="/Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib"
path="/Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib"
ocamlc="ocamlc.opt"
ocamlopt="ocamlopt.opt"
ocamldep="ocamldep.opt"

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:14):

I didn't read any docs about it, but not that much one can mess up.

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:15):

so ls /Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq-elpi says...?

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:15):

(just to double check there was a typo in your prev message)

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:15):

What I gave above:

coq-elpi$ ls /Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq-elpi
META            elpi_plugin.cmxs

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:16):

looks right then, so why it is not listed by the error message?!

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:16):

The META file is:

coq-elpi$ cat META
package "elpi" (
  description = "Coq Elpi"
  requires = "coq-core.plugins.ltac stdlib-shims elpi"
  archive(byte) = "elpi_plugin.cma"
  archive(native) = "elpi_plugin.cmxa"
  plugin(byte) = "elpi_plugin.cma"
  plugin(native) = "elpi_plugin.cmxs"
)

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:17):

Indeed that is the question.

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:18):

can you run ocamlfind query coq-elpi (using the env variables which make findlib looks for the conf file in the dmg)

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:18):

Let me check if equations works ...

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:19):

we should understand if the problem is findlib, or Coq, or both

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:19):

Let me first check if equations work, then I check the findlib query

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:20):

Interestingly equations does work, also coq-hammer e.g.

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:21):

Interestingly the coq-equations folder was not listed above either.

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:22):

yes, that may be the loading using legacy.
In Equations I bet it says Declare ML Module "coq-equations.plugin:equations_plugin".

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:22):

It gives both the new, findlib, name and the old name. In this case Coq uses the legacy mechanism IIRC.

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:22):

The next one which does not work is hierarchy builder.

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:23):

For sure elpi.v has only ML Module "coq-elpi.plugin" with no :elpi_plugin part

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:23):

HB uses elpi

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:23):

Yes, I know.

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:23):

Then coq-mathcomp-algebra-tactics fails (also elpi)

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:24):

Hum, can you try to run the smoke test on elpi or HB by passing, by hand, to coqc
-I /Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq-elpi?

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:25):

That extends the paths findlib scans

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:26):

Sure, will try. The smoke test finished - the only ones failing are those using elpi.

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:26):

The penalty for doing things properly ;-)

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:26):

"bleeding edge"

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:27):

anyway, you can also enable legacy loading for elpi in elpi.v, but won't work if you load, say, alectryon together with it... better than nothing.

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:27):

coqc -I /Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq-elpi tutorial_coq_elpi_command.v
File "./tutorial_coq_elpi_command.v", line 47, characters 0-30:
Error:
Findlib error: elpi not found in:

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:28):

in what?

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:29):

coqc -I /Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq-elpi tutorial_coq_elpi_command.v
File "./tutorial_coq_elpi_command.v", line 47, characters 0-30:
Error:
Findlib error: elpi not found in:
/Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq-elpi
/Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq/../coq-core/plugins/ltac2
/Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq/../coq-core/plugins/ssrmatching
/Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq/../coq-core/plugins/tutorial
/Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq/../coq-core/plugins/tutorial/p3
:

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:29):

So now it did look in lib/coq-elpi but didn't find it either.

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:30):

I wonder where the /coq/../coq-core/ comes from

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:30):

something is still fishy, shoudn't it say coq-elpi.plugin?

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:31):

these are paths we "build" and pass to Findlib.init in the sysinit/coqinit.ml file IIRC.

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:31):

Should it?

lib$ ls
bigarray            coq-elpi            coq-reduction-effects       findlib.conf            parsexp             stdlib-shims
biniou              coq-equations           coq-relation-algebra        gdk-pixbuf-2.0          ppx_compare         str
bytes               coq-gappa           coq-serapi          gtk-3.0             ppx_derivers            stublibs
camlp-streams           coq-hammer          coq-simple-io           libecm.la           ppx_deriving_yojson     threads
cmdliner            coq-hammer-tactics      coq-unicoq          menhir              ppx_hash            toplevel
compcert            coq-interval            coqide              menhirLib           ppx_import          unix
compiler-libs           coq-itauto          coqide-server           menhirSdk           ppx_sexp_conv           yojson
coq             coq-mathcomp-multinomials   dune-configurator       num             ppxlib              z3
coq-aac-tactics         coq-mathcomp-word       dylib               num-top             seq             zarith
coq-bignums         coq-mtac2           dynlink             ocaml               sexplib
coq-core            coq-paramcoq            easy-format         ocamldoc            sexplib0
coq-dpdgraph            coq-quickchick          findlib             ocamlgraph          stdlib

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:31):

Sorry to use you as an ssh session.. but:

coqtop -I /Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq-elpi
Declare ML Module "coq-elpi.plugin".

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:33):

The same:

bin$ ./coqtop -I /Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq-elpi
Welcome to Coq 8.16.0

Coq < Declare ML Module "coq-elpi.plugin".
Toplevel input, characters 0-36:
> Declare ML Module "coq-elpi.plugin".
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error:
Findlib error: coq-elpi.plugin not found in:
/Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq-elpi
/Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq/../coq-core/plugins/ltac2
/Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq/../coq-core/plugins/ssrmatching
/Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq/../coq-core/plugins/tutorial
/Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq/../coq-core/plugins/tutorial/p3
/Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq/../coq-core/plugins/tutorial/p2

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:34):

sorry Declare ML Module "coq-elpi.elpi".

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:35):

(but the error message prints the full packge name, I don't get how it can print only 'elpi' and in the previous attempt)

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:35):

The same:

bin$ ./coqtop -I /Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq-elpi
Welcome to Coq 8.16.0

Coq < Declare ML Module "coq-elpi.elpi".
[Loading ML file coq-elpi.elpi ... failed]
Toplevel input, characters 0-34:
> Declare ML Module "coq-elpi.elpi".
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error:
Findlib error: elpi not found in:
/Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq-elpi
/Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq/../coq-core/plugins/ltac2
/Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq/../coq-core/plugins/ssrmatching
/Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq/../coq-core/plugins/tutorial

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:35):

I mean, nobody should be doing Declare ML Module "elpi"

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:36):

Hum, OK, so the error message is different

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:36):

am I dreming?

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:36):

It is getting late, yes :-)

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:37):

Let me setup ocamlfind ...

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:38):

[Loading ML file coq-elpi.elpi ... failed]this is not in the logs, nor in the previous attempt.
So it gets printed only when the META file is found. IMO there are 2 problem:

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:39):

Last attempt before calling Morpheus hotline:

./coqtop -I /Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq-elpi -I ./coqtop -I /Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/elpi
Declare ML Module "coq-elpi.elpi".

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:40):

First the ocamlfind result:

bin$ ./ocamlfind query coq-elpi
/Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq-elpi

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:40):

Michael Soegtrop said:

Should it?

lib$ ls
bigarray            coq-elpi            coq-reduction-effects       findlib.conf            parsexp             stdlib-shims
biniou              coq-equations           coq-relation-algebra        gdk-pixbuf-2.0          ppx_compare         str
bytes               coq-gappa           coq-serapi          gtk-3.0             ppx_derivers            stublibs
camlp-streams           coq-hammer          coq-simple-io           libecm.la           ppx_deriving_yojson     threads
cmdliner            coq-hammer-tactics      coq-unicoq          menhir              ppx_hash            toplevel
compcert            coq-interval            coqide              menhirLib           ppx_import          unix
compiler-libs           coq-itauto          coqide-server           menhirSdk           ppx_sexp_conv           yojson
coq             coq-mathcomp-multinomials   dune-configurator       num             ppxlib              z3
coq-aac-tactics         coq-mathcomp-word       dylib               num-top             seq             zarith
coq-bignums         coq-mtac2           dynlink             ocaml               sexplib
coq-core            coq-paramcoq            easy-format         ocamldoc            sexplib0
coq-dpdgraph            coq-quickchick          findlib             ocamlgraph          stdlib

where is elpi?

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:40):

there should be both lib/elpi and lib/coq-elpi

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:40):

OK .... let me see

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:41):

Is this new in 8.16?

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:41):

There is none in 8.15.2 either.

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:41):

well, before 8.16 coq-elpi would statically link elpi

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:42):

I see.

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:42):

so it was not important
but now all is loaded "properly"

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:42):

Possibly elpi is on the exclusion list ...

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:42):

I'm sure I told you to kill it in the past, since it was not needed

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:42):

maybe it was windows...

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:43):

Yes - here we go:

PRIMARY_PACKAGES="$(opam list --installed-roots --short --columns=name | grep -v '^ocaml\|^opam\|^depext\|^conf\|^lablgtk\|^elpi' | tr -s '\n' ' ')"

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:43):

Let me try what happens if I remove it from there. Takes a few minutes ...

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:43):

(signing and all)

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:46):

Well we excluded things which are statically linked to save space.

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:47):

Now I get it findlib started to load coq-elpi.elpi which requires elpi, and that is where you get the second error message.

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:48):

But there is still the question "why lib/coq-elpi is not in the paths"...

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:48):

But it seems to find it ...

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:49):

well, when you pass -I

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:49):

Let's first test the new installer - almost done

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:50):

my understanding is that:

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:51):

We are making progress:

coqc  tutorial_coq_elpi_command.v
File "./tutorial_coq_elpi_command.v", line 47, characters 0-30:
Error:
Findlib error: ppx_deriving.runtime not found in:
/Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq/../coq-core/plugins/ltac2
/Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq/../coq-core/plugins/ssrmatching

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:51):

yes!

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:51):

one step further

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:52):

The elpi and coq-elpi folders are still not in the error message, though

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:52):

I have this:

# Packages linked into elpi

IGNORED_PACKAGES="${IGNORED_PACKAGES} elpi camlp5 ppxlib ppx_deriving ocaml-migrate-parsetree re"

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:52):

isn't there (at the very end) a .../lib

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:53):

yup, elpi needs:

  "stdlib-shims"
  "ppxlib" {>= "0.12.0" }
  "menhir" {>= "20211230" }
  "re" {>= "1.7.2"}
  "ppx_deriving" {>= "4.3"}

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:53):

Indeed - not sure what the other mess is about then - possibly things coqc does in findlib init.

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:54):

So I just delete these lines?

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:54):

you need to empy that line now

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:54):

OK - another 5 minutes ...

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:54):

camlp5 is no more a dependency, in case you you have it elsewhere

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:54):

but menhir is

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:55):

I don't think I need any runtime library from menhir, but well...

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:56):

I think menhir is anyway a primary package.

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:56):

So yes, I confirm that CI lists, in the very last line /Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib which I think is traversed recursively. My bad I did not see it before. I guess all the others are added by Coq one by one.

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:56):

In current picks at least.

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:57):

OK, what I meant is that I need it at compile time, but not at run time (it offers that possibility, but I don't use it)

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:58):

What I meant is that it doesn't matter because menhir is explicitly included in Coq Platform.

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:58):

OK

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:58):

It is a useful tool (I use it).

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:58):

eh eh, I know ;-)

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 19:59):

Actually IMHO the only parser generator which is usable.

view this post on Zulip Enrico Tassi (Sep 16 2022 at 19:59):

I had quite a fight with it, but it is clearly the best out there

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 20:00):

What I like is that it gives understandable examples for shift reduce conflicts.

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 20:00):

With bison or yacc this is unmanagebale for a large grammar.

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 20:00):

OK, the moment of truth ...

view this post on Zulip Enrico Tassi (Sep 16 2022 at 20:01):

that one is useful, but what I love the most is the error message thing. So that I can actually generate error message which don't include the names of the non terminals... And give examples of correct syntax...

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 20:02):

Yes, this is also very useful - although I mostly use it to parse e.g. C for analysis, where one can assume it doesn't have syntax errors.

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 20:02):

OK - next step:

coqc  tutorial_coq_elpi_command.v
File "./tutorial_coq_elpi_command.v", line 47, characters 0-30:
Error:
Findlib error: result not found in:
/Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq/../coq-core/plugins/ltac2
:
/Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib
required by `ppx_deriving.runtime'

view this post on Zulip Enrico Tassi (Sep 16 2022 at 20:03):

result is another library, a dependency of ppx deriving IIRC

view this post on Zulip Enrico Tassi (Sep 16 2022 at 20:03):

indeed

view this post on Zulip Enrico Tassi (Sep 16 2022 at 20:03):

I guess it is filtered somewhere

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 20:03):

OK, I also have:

IGNORED_PACKAGES="ocaml ocaml-variants ocaml-base-compiler base ocaml-compiler-libs ocaml-config ocaml-secondary-compiler ocamlfind-secondary"
IGNORED_PACKAGES="${IGNORED_PACKAGES} dune configurator sexplib0 csexp ocamlbuild result cppo"

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 20:04):

This was supposed to be required by ocamlc only.

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 20:04):

Or for developing OCaml code.

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 20:04):

Anything else I should remove from the list?

view this post on Zulip Enrico Tassi (Sep 16 2022 at 20:04):

among all these, the only one which speaks to me is result

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 20:04):

OK - 5 minutes ...

view this post on Zulip Enrico Tassi (Sep 16 2022 at 20:05):

wait

view this post on Zulip Enrico Tassi (Sep 16 2022 at 20:05):

$ ocamlfind query -r coq-elpi.elpi
/home/gares/.opam/4.09.1/lib/coq-core/config
/home/gares/.opam/4.09.1/lib/coq-core/boot
/home/gares/.opam/4.09.1/lib/ocaml
/home/gares/.opam/4.09.1/lib/ocaml
/home/gares/.opam/4.09.1/lib/ocaml
/home/gares/.opam/4.09.1/lib/coq-core/clib
/home/gares/.opam/4.09.1/lib/coq-core/lib
/home/gares/.opam/4.09.1/lib/coq-core/gramlib
/home/gares/.opam/4.09.1/lib/coq-core/vm
/home/gares/.opam/4.09.1/lib/ocaml
/home/gares/.opam/4.09.1/lib/coq-core/kernel
/home/gares/.opam/4.09.1/lib/coq-core/library
/home/gares/.opam/4.09.1/lib/coq-core/engine
/home/gares/.opam/4.09.1/lib/coq-core/pretyping
/home/gares/.opam/4.09.1/lib/zarith
/home/gares/.opam/4.09.1/lib/coq-core/interp
/home/gares/.opam/4.09.1/lib/coq-core/parsing
/home/gares/.opam/4.09.1/lib/coq-core/proofs
/home/gares/.opam/4.09.1/lib/coq-core/printing
/home/gares/.opam/4.09.1/lib/coq-core/tactics
/home/gares/.opam/4.09.1/lib/findlib
/home/gares/.opam/4.09.1/lib/findlib
/home/gares/.opam/4.09.1/lib/findlib
/home/gares/.opam/4.09.1/lib/coq-core/vernac
/home/gares/.opam/4.09.1/lib/coq-core/sysinit
/home/gares/.opam/4.09.1/lib/coq-core/stm
/home/gares/.opam/4.09.1/lib/coq-core/plugins/ltac
/home/gares/.opam/4.09.1/lib/stdlib-shims
/home/gares/.opam/4.09.1/lib/seq
/home/gares/.opam/4.09.1/lib/re
/home/gares/.opam/4.09.1/lib/re/str
/home/gares/.opam/4.09.1/lib/elpi/util
/home/gares/.opam/4.09.1/lib/elpi/lexer_config
/home/gares/.opam/4.09.1/lib/menhirLib
/home/gares/.opam/4.09.1/lib/result
/home/gares/.opam/4.09.1/lib/ppx_deriving/runtime
/home/gares/.opam/4.09.1/lib/elpi/parser
/home/gares/.opam/4.09.1/lib/elpi/trace/runtime
/home/gares/.opam/4.09.1/lib/elpi
/home/gares/.opam/4.09.1/lib/coq-elpi

view this post on Zulip Enrico Tassi (Sep 16 2022 at 20:06):

hum, it's a superset I'm afrid

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

That't wouldn't hurt - it automatically gets all dependencies from opam - we just manually exclude stuff.

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

So what should I unexclude?

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

And the dependencies are handled recursive

view this post on Zulip Enrico Tassi (Sep 16 2022 at 20:07):

the problem is that the exclusion mechanism is unsound, maybe X is unneded by elpi, but is required by foo

view this post on Zulip Enrico Tassi (Sep 16 2022 at 20:08):

this is what happened with result

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 20:08):

there were two exlcusion groups: elpi and OCaml.

view this post on Zulip Enrico Tassi (Sep 16 2022 at 20:09):

well, ok then.
I think I only need menhirLib at compile time, not sure it is worth it.
(ppx was huge).

view this post on Zulip Enrico Tassi (Sep 16 2022 at 20:10):

note that I think at runtime one only needs .cmxs, while these directories contains all other files, which are needed at compile time only.

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 20:10):

Possibly I need to include all OCaml libraries now. If I understand you right a lot of stuff which was statically linked before is now dynamically linked.

view this post on Zulip Enrico Tassi (Sep 16 2022 at 20:10):

all .cmi for example

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 20:10):

We also have file exnetsion exclusions ...

view this post on Zulip Enrico Tassi (Sep 16 2022 at 20:11):

yes, but these directories contain both files which are needed at compiler time (like the interface files) and at run time (the linked.cmxs)

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 20:11):

blacklist="(\.byte|\.cm[aiox]|\.cmxa|\.o|\.a|\.glob)$"

view this post on Zulip Enrico Tassi (Sep 16 2022 at 20:11):

ok, then you are good ;-)

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 20:12):

This is applied to all packages, unless they have a specific blacklist (which is rare - some GTK stuff).

view this post on Zulip Enrico Tassi (Sep 16 2022 at 20:12):

you also have .h files here and there

view this post on Zulip Enrico Tassi (Sep 16 2022 at 20:12):

/home/gares/.opam/4.09.1/lib/ocaml/caml/misc.h

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 20:13):

====================== SMOKE TEST SUCCESS ======================

view this post on Zulip Enrico Tassi (Sep 16 2022 at 20:13):

I also have .cmt and .cmti files (used only by UIs)

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 20:13):

One can scrutinize it a bit more, but I think a few h files make a noticeable difference in installer size - ocamlc does.

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

I am open to a PR :-)

view this post on Zulip Enrico Tassi (Sep 16 2022 at 20:14):

sure but

$ find /home/gares/.opam/4.09.1/lib/ocaml -name \*.cmt| du -sh
561M    .

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

So I should exclude cmt files and h files?

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

and cmti files?

view this post on Zulip Enrico Tassi (Sep 16 2022 at 20:15):

yes, but it seems they are all gzip friendly, unless I got my bash line wrong

view this post on Zulip Enrico Tassi (Sep 16 2022 at 20:16):

yes, *.cmt gzip to 26M

view this post on Zulip Enrico Tassi (Sep 16 2022 at 20:17):

you can kill them from the image for sure, but won't same much

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 20:17):

I think your line gives the total folder size. I guess an xargs missing?

view this post on Zulip Enrico Tassi (Sep 16 2022 at 20:18):

yes, I was wrong:

gares@ollypat:~/LPCIC/elpi$ find /home/gares/.opam/4.09.1/lib/ocaml -name \*.cmt| xargs cat |gzip|wc -c
26220621
gares@ollypat:~/LPCIC/elpi$ find /home/gares/.opam/4.09.1/lib/ocaml -name \*.cmt| xargs cat |wc -c
65298967

view this post on Zulip Enrico Tassi (Sep 16 2022 at 20:18):

time to sleep

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 20:19):

Coq-Platform~8.16.0~2022.09~beta1.app$ find . -name \*.cmt | xargs cat|wc -c
 239965799
Coq-Platform~8.16.0~2022.09~beta1.app$ find . -name \*.cmt | xargs cat|gzip|wc -c
 94406081

view this post on Zulip Michael Soegtrop (Sep 16 2022 at 20:19):

This is what is in the MacOS installer.

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

Indeed time to sleep! Have a good night and thanks for the help!

view this post on Zulip Enrico Tassi (Sep 16 2022 at 20:20):

Always a pleasure

view this post on Zulip Enrico Tassi (Sep 16 2022 at 20:20):

ciao

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

ciao

view this post on Zulip Paolo Giarrusso (Sep 16 2022 at 22:00):

You mentioned problems with Alectryon + Elpi, but I guess it was just for the installer and I shouldn't worry otherwise?

view this post on Zulip Enrico Tassi (Sep 17 2022 at 05:21):

The problem would show up if elpi was not using the new loading mechanism on ocaml 4.08 or newer.

I do use alectryon to build elpi's doc in CI, so it works.
Don't worry.

view this post on Zulip Michael Soegtrop (Sep 17 2022 at 07:38):

@Paolo Giarrusso : anyway the chat above was about not doing a quick and dirty solution (using legacy load) but the proper thing for the installers as well.

view this post on Zulip Paolo Giarrusso (Sep 17 2022 at 07:39):

Sounds good :-), and I stopped worrying

view this post on Zulip Michael Soegtrop (Sep 17 2022 at 16:02):

@Enrico Tassi : Can you please have a look at the snap CI : (https://github.com/coq/platform/actions/runs/3072641230/jobs/4965126429#step:6:1263)? Apparently the path to the config file is OK, but the paths in the config file are wrong - I guess this are the paths where the snap has been built. So I guess we anyway need some sort of post install script to patch the findlib config file. As far as I understand the x1 in the path is situation dependent.

view this post on Zulip Michael Soegtrop (Sep 17 2022 at 16:06):

I guess the snap folder itself is read only, so do we have to put the config file somewhere else?

Here it is recommended to do this in the wrapper.

Do you have a better idea?

view this post on Zulip Michael Soegtrop (Sep 17 2022 at 16:09):

A configure hook might also work.

view this post on Zulip Enrico Tassi (Sep 17 2022 at 20:30):

x1 is when a snap is installed from a local file (as in the smoke test) and not from the store which gives it a number

view this post on Zulip Enrico Tassi (Sep 17 2022 at 20:31):

IMO the problem is pruning, as yesterday, see: https://github.com/coq/platform/blob/af1597dd2d7f04ec801b54e694880b6c249ecb80/linux/snap/snapcraft.yaml.in#L29

view this post on Zulip Enrico Tassi (Sep 17 2022 at 20:31):

it prunes stdlib-shims, wihch gives the error

view this post on Zulip Michael Soegtrop (Sep 18 2022 at 10:43):

Yes, pruning might be part of it, but the path is also definitely wrong and needs to be fixed.

view this post on Zulip Michael Soegtrop (Sep 18 2022 at 11:01):

I try my luck with the install and/or configure hooks, but I am unsure if the can write to the $SNAP folder - this is not documented. If this does not work, I have to ponder what to do about this. I could write the findlib.conf file to $SNAP_DATA and add another patch to findlib to override the hard coded conf file path in each executable to point there. This of course would require that the $SNAP_DATA path is constant, which I am not sure of.

view this post on Zulip Michael Soegtrop (Sep 20 2022 at 09:41):

@Enrico Tassi : I did a local snap compile and install to experiment. One thing I don't understand is how coqc in /snap/coq-prover/current/.../bin works. As far as I understand it is not called via the wrapper - only the links under /snap/bin do this. So how does coqc know where to find its libraries?

view this post on Zulip Enrico Tassi (Sep 20 2022 at 09:44):

the wrapper exports COQLIB

view this post on Zulip Michael Soegtrop (Sep 20 2022 at 09:44):

Or asked in another way: any idea how I could get these executables to find findlib.conf? The snaps are immutable, so a configure hook can't place a patched .config file next to the binaries. And an unpatched config file would contain the wrong paths.

view this post on Zulip Michael Soegtrop (Sep 20 2022 at 09:45):

But how does coqc (rather than coq-prover.coqc) use the wrapper?

view this post on Zulip Michael Soegtrop (Sep 20 2022 at 09:46):

The snapcraft.yaml file defined 5 apps and these are declared to use the wrapper.

view this post on Zulip Michael Soegtrop (Sep 20 2022 at 09:46):

But how does it work when people put coqc under /snap/coq-prover/current/.../bin into the path?

view this post on Zulip Enrico Tassi (Sep 20 2022 at 09:46):

I'm sorry, but coqc is a symlink to coq-prover.coqc created by snap when it installs something from the store

view this post on Zulip Enrico Tassi (Sep 20 2022 at 09:46):

these symlinks are "in the store"

view this post on Zulip Enrico Tassi (Sep 20 2022 at 09:47):

(sorry got to go)

view this post on Zulip Michael Soegtrop (Sep 20 2022 at 09:47):

The apps are symlinks to snap.

view this post on Zulip Michael Soegtrop (Sep 20 2022 at 09:47):

coqc is an executable.

view this post on Zulip Michael Soegtrop (Sep 20 2022 at 09:47):

No symlink.

view this post on Zulip Michael Soegtrop (Sep 20 2022 at 09:47):

OK, let's discuss later.

view this post on Zulip Michael Soegtrop (Sep 20 2022 at 09:56):

@Enrico Tassi : I mean this:

/snap/coq-prover/x2/coq-platform/2022-09-0/bin$ ls -l coqc
-rwxr-xr-x 1 root root 66309560 Sep 20 10:53 coqc
/snap/coq-prover/x2/coq-platform/2022-09-0/bin$ file coqc
coqc: ELF 64-bit LSB pie executable, x86-64, version 1 (SYSV), dynamically linked, interpreter /lib64/ld-linux-x86-64.so.2, for GNU/Linux 3.2.0, BuildID[sha1]=29fc9e9ee7a076025329e7feca67e4a269d38709, with debug_info, not stripped

view this post on Zulip Michael Soegtrop (Sep 20 2022 at 09:59):

There must be some magic behind this, since it also needs to find all the libraries it was shipped with, but I don't understand it (and without understanding how this works, I can't fix the 8.16 ocamlfind issues).

view this post on Zulip Paolo Giarrusso (Sep 20 2022 at 10:08):

Naive Q: is PATH=/snap/coq-prover/x2/coq-platform/2022-09-0/bin:$PATH actually meant to be supported?

view this post on Zulip Michael Soegtrop (Sep 20 2022 at 10:09):

@Paolo Giarrusso well I didn't do this so I can't tell but as user of this it doesn't make too much sense when this would be not supported.

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

Also except for the 8.16 ocamlfind issuesd it seems to work. Magically coqc -where gives the right thing.

view this post on Zulip Michael Soegtrop (Sep 20 2022 at 10:11):

What I want to understand is what snap does to make it work. Or possibly coqc now uses a relative path to lib.

view this post on Zulip Michael Soegtrop (Sep 20 2022 at 10:13):

I can't simply use a relative path to findlib.conf, because findlib.conf itself contains paths, and these would be wrong. I would have to patch findlib to support relative paths in findlib.conf to make it work.

I currently see no other option. On MacOS it is simpler because the install path is fixed and on Windows the install location is writable. On snap the destination is variable and we have a monuted read only image.

view this post on Zulip Paolo Giarrusso (Sep 20 2022 at 10:14):

For me, env -i -- /Users/pgiarrusso1/.opam/4.14.0+flambda/bin/coqc -where on the raw binary gives the right output, so there's lib location magic in the binary itself

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

Yes. I wonder if this is somethign we (Coq) do or something snap does.

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

I guess snap has some machinery to make snaps reloctable.

view this post on Zulip Paolo Giarrusso (Sep 20 2022 at 10:15):

I'm implying Coq must do it, since my test is without snaps?

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

But I can't find docs for it.

view this post on Zulip Paolo Giarrusso (Sep 20 2022 at 10:15):

ah

view this post on Zulip Michael Soegtrop (Sep 20 2022 at 10:16):

But you did use a snapcraft created binary?

view this post on Zulip Michael Soegtrop (Sep 20 2022 at 10:16):

I mean something similar to what cygwin does.

view this post on Zulip Michael Soegtrop (Sep 20 2022 at 10:16):

For a cygwin app, /bin is something like C:\cygwin\bin.

view this post on Zulip Paolo Giarrusso (Sep 20 2022 at 10:16):

no, that's a macOS binary. But it seems to use an hardcoded path; it seems you might need to patch Coq itself to make it find findlib.conf relative to the binary?

view this post on Zulip Paolo Giarrusso (Sep 20 2022 at 10:17):

I say "hardcoded" based on this test:

$ cp /Users/pgiarrusso1/.opam/4.14.0+flambda/bin/coqc .
$ env -i -- ./coqc -where
/Users/pgiarrusso1/.opam/4.14.0+flambda/lib/coq

view this post on Zulip Michael Soegtrop (Sep 20 2022 at 10:17):

I already did patch ocamlfind to look for a copy next to coqc. This works on MacOS.

view this post on Zulip Michael Soegtrop (Sep 20 2022 at 10:18):

But it does not work for snap as explained above: the path is variable and the findlib.conf file is RO (in a mounted RO filesystem).

view this post on Zulip Michael Soegtrop (Sep 20 2022 at 10:18):

I would have to patch findlib further to allow relative paths in findlib.conf.

view this post on Zulip Paolo Giarrusso (Sep 20 2022 at 10:19):

I was suggesting translating https://github.com/coq/platform/blob/main/linux/snap/coq_wrapper into OCaml code into the coqc binary

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

Well, as I said in snap this does work. coqc -where gives the correct path.

view this post on Zulip Michael Soegtrop (Sep 20 2022 at 10:21):

How and why I can't tell.

view this post on Zulip Michael Soegtrop (Sep 20 2022 at 10:21):

What does not work is Ocamlfind.

view this post on Zulip Paolo Giarrusso (Sep 20 2022 at 10:22):

I get that, I suspect that's already for COQLIB, but not for OCAMLFIND_CONF...

view this post on Zulip Michael Soegtrop (Sep 20 2022 at 10:22):

Actually if snap really has a path translation deep in its guts, it might even work.

view this post on Zulip Paolo Giarrusso (Sep 20 2022 at 10:22):

hardcoding OCAMLFIND_CONF using SNAP wouldn't be great — but if OCAMLFIND_CONF="$(cd $(dirname $0)/../lib/findlib.conf; pwd)" works, it'd be reasonable

view this post on Zulip Michael Soegtrop (Sep 20 2022 at 10:23):

Again this does not work, because findlib.conf contains itself paths which need to be adjusted.

view this post on Zulip Michael Soegtrop (Sep 20 2022 at 10:23):

I already patched ocamlfind to find findlib.conf, just the contents of findlib.conf is wrong then, and since it is RO, I can't fix it.

view this post on Zulip Michael Soegtrop (Sep 20 2022 at 10:24):

In short: it is quite a mess and hard to fix.

view this post on Zulip Michael Soegtrop (Sep 20 2022 at 10:27):

I currently see two options:

Playing with env vars seems to be not feasible if we want putting coqc into the PATH work.

view this post on Zulip Enrico Tassi (Sep 20 2022 at 11:28):

I'm sorry but I'm away from my office, I can't really help now. My feeling is that in the short term it is easier to ship an empty findlib.conf in the snap (just to have a file) and do all the work in coq/sysinit/coqinit.ml when we call Findlib.init

view this post on Zulip Paolo Giarrusso (Sep 20 2022 at 11:36):

FWIW (and I could be wrong!), here's some of the existing code involved in coqc -where I found earlier:
https://github.com/coq/coq/blob/d9180a0774afd0f17d26c4828c8ee2c316a0571b/boot/env.ml#L35-L45
https://github.com/coq/coq/blob/d9180a0774afd0f17d26c4828c8ee2c316a0571b/sysinit/coqinit.ml#L91-L94

it doesn't seem to locate anything relative to the coqc binary path, but that's one option.

view this post on Zulip Michael Soegtrop (Sep 20 2022 at 12:35):

What I really would like to understand is how it comes that snap coqc -where works. I think we shouldn't exclude that snap is doing something fancy - I guess a lot of people would have this problem.

view this post on Zulip Michael Soegtrop (Sep 21 2022 at 18:17):

An update from the OCamlfind front: I now did a few more aggressive patches to OCamlfind, which make Coq and plugins relocatable on all platforms without requiring any environment variables. The changes are as follows:

This seems to work locally on all platforms even after installation - CI is running.

view this post on Zulip Paolo Giarrusso (Sep 21 2022 at 18:24):

Wondering, but this could be even more noise: could this patch be upstreamed and would it work quickly on Nix? “Scan upwards from coqc” risks listing “/nix/store" if something goes wrong (no config found!), and that's tricky (Agda once used a few GB of RAM trying to store the entire listing at once)

view this post on Zulip Paolo Giarrusso (Sep 21 2022 at 18:25):

But it does sound good, and there's no problem when properly installed I guess

view this post on Zulip Michael Soegtrop (Sep 22 2022 at 07:29):

@Paolo Giarrusso : I plan to put it upstream after a bit of review (and after the beta). I don't expect issues. The findlib.root file should always be there at the root of the Coq installation if there are paths which start with ... . If there are no paths starting with ..., the behavior is as before. Mixing the use of ... and not having a findlib.root file would be a configuration error.

I guess it is best to have a configure option "relative-paths" which enables both, looking for ... and creating the findlib.root file.

view this post on Zulip Michael Soegtrop (Sep 22 2022 at 08:32):

Puuh - there is some more work to do. The Mac installer works if built with MacPorts (local), but it does not work if built with Homebrew (CI). Also there are deviations in the snap ...

view this post on Zulip Michael Soegtrop (Sep 22 2022 at 15:58):

@Enrico Tassi : there is some more stuff going on around elpi on Mac: on Mac executables and shared libraries need to be patched from absolute paths to relative paths (using the macpack utility). Before 8.16 macpack found all dependencies and patched them. With 8.16 macpack doesn't seem to find all libraries, which also means that some dependants of libraries don't get patched to relative paths.

Elpi is missing the threads library (see https://github.com/coq/platform/actions/runs/3102147125/jobs/5025581286#step:7:811). It is indeed not there because macpack didn't find this dependency. But copying it over does not fix this, because it still wants the library from the .opam folder. Indeed if the .opam folder is still there (as in local builds), the elpi smoke test does work, even though the threads library is not in the application.

I tried to find out which file in elpi links the threads library (I guess /lib/ocaml/stublibs/dllthreads.so) but without success. Any ideas?

view this post on Zulip Michael Soegtrop (Sep 22 2022 at 16:34):

It might also be something special about the threads META file.
When the .opam folder is there, coqc reads these files:

  501  59777 coqc           7 /Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq/../coq-core/../coq-elpi/META
  501  59777 coqc           7 /Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq/../coq-core/../coq-core/META
  501  59777 coqc           7 /Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq/../coq-core/../stdlib-shims/META
  501  59777 coqc           7 /Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq/../coq-core/../elpi/META
  501  59777 coqc           7 /Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq/../coq-core/../threads/META
  501  59777 coqc           7 /Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq/../coq-core/../findlib/META
  501  59777 coqc           7 /Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq/../coq-core/../unix/META
  501  59777 coqc           7 /Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq/../coq-core/../str/META
  501  59777 coqc           7 /Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq/../coq-core/../zarith/META
  501  59777 coqc           7 /Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq/../coq-core/../dynlink/META
:

and lives a long and happy life.
In case the .opam folder is not there, it reads:

  501  61405 coqc           7 /Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq/../coq-core/../coq-elpi/META
  501  61405 coqc           7 /Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq/../coq-core/../coq-core/META
  501  61405 coqc           7 /Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq/../coq-core/../stdlib-shims/META
  501  61405 coqc           7 /Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq/../coq-core/../elpi/META
  501  61405 coqc           7 /Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq/../coq-core/../threads/META
  501  61405 coqc           7 /Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq/../coq-core/../findlib/META
  501  61405 coqc           7 /Applications/Coq-Platform~8.16.0~2022.09~beta1.app/Contents/Resources/lib/coq/../coq-core/../threads/META

and dies (observe that it reads threads/META twice).

Interestingly it never reads anything from .opam, but renaming .opam to .opam2 makes it fail. Rather mysterious ... .

view this post on Zulip Michael Soegtrop (Sep 22 2022 at 16:46):

Hmm - it might be the exists_if line in some of the META files:

lib$ find . -name "META" | xargs grep exists_if
./compiler-libs/META:  exists_if = "ocamloptcomp.cma"
./compiler-libs/META:  exists_if = "ocamltoplevel.cmxa"
./threads/META:  exists_if = "threads.cma"
./threads/META:  exists_if = "threads.cma"
./zarith/META:  exists_if = "zarith_top.cma"

Since we prune the cma files, I guess findlib concludes that threads does not exists ... .

How it finds the file in the opam folder I can't say - it shouldn't have absolute paths in it.

view this post on Zulip Enrico Tassi (Sep 22 2022 at 19:50):

I'm not so sure I follow, elpi is not linking the thread library. At least not directly. Sorry, I'm afraid I can't help.

view this post on Zulip Enrico Tassi (Sep 22 2022 at 19:52):

Wait, I think I fund where threads come from

view this post on Zulip Enrico Tassi (Sep 22 2022 at 19:52):

coq-elpi$ git grep -i thread
Makefile.examples.coq.conf:COQMF_CAMLFLAGS=-thread -rectypes -w -a+1..3-4+5..8-9+10..26-27+28..40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -bin-annot -safe-string -strict-sequence

view this post on Zulip Enrico Tassi (Sep 22 2022 at 19:53):

it is coq_makefile which links all plugins with threads

view this post on Zulip Enrico Tassi (Sep 22 2022 at 20:49):

about the META, the dependency must come from Coq's META (the one of coq-elpi does not mention threads)

view this post on Zulip Enrico Tassi (Sep 22 2022 at 20:50):

sorry, I'm not very helpful

view this post on Zulip Michael Soegtrop (Sep 23 2022 at 09:44):

@Enrico Tassi : I would say in the end OCamlfind does at runtime a lot of things which are only useful at compile time. E.g. why does it read the META files at all at run time? There is no useful information in there - neither names nor paths of shared libraries - just names of static libraries. The only file useful at runtime is findlib.conf.

I simply patched away the "exists_if" statements (which check for static libraries we purge) in the META files during installer generation, and now it works at least on Mac (even if .opam is not there). On snap there seems to be yet another issue with elpi.

In the end I think ocamlfind needs some major rework.

view this post on Zulip Enrico Tassi (Sep 23 2022 at 11:55):

There is no useful information in there - neither names nor paths of shared libraries

Hum, this is not true. You have

package "elpi" (
  description = "Coq Elpi"
  requires = "coq-core.plugins.ltac stdlib-shims elpi"
  archive(byte) = "elpi_plugin.cma"
  archive(native) = "elpi_plugin.cmxa"
  plugin(byte) = "elpi_plugin.cma"
  plugin(native) = "elpi_plugin.cmxs"
)

here plugin(native) is the name of the plugin, and requires tells you its dependencies

view this post on Zulip Enrico Tassi (Sep 23 2022 at 13:12):

Imo what you do at compile time by statically linking is roughly what you do at run time by loading a plugin. So the info in the META seems relevant

view this post on Zulip Enrico Tassi (Sep 23 2022 at 13:12):

I'm sorry it is cause so many troubles

view this post on Zulip Michael Soegtrop (Sep 23 2022 at 15:31):

Well it's not your fault - it is just that ocamlfind was not developed with installers in mind. But it can be fixed.

view this post on Zulip Michael Soegtrop (Sep 29 2022 at 11:22):

An update on the status: the issues introduced by using ocamlfind were so work intensive to fix that I decided to rework all installers (MacOS, snap, Windows) to use the same piece of code to extract stuff from Opam. Only the code which handles system dependencies is (naturally) different. This was quite a bit of work, but it fixed snap (mostly) without further work. Before snap had a negative file selection (remove unwanted stuff) while Windows and MacOS had positive file selection (select what you want) - naturally it is hard to merge changes from one style to another. Now all platforms use positive file selection (with some negative filters of course) and the same script.

I need to go through the issue list, but I hope that's it mostly (CI is running).

view this post on Zulip Andrew Appel (Sep 29 2022 at 14:54):

Question: When this 2022.09+beta1 is done, suppose within that Platform release I build (for example) MetaCoq, which uses ocamlfind to install its plugins. Will that cause any problems?

view this post on Zulip Karl Palmskog (Sep 29 2022 at 14:56):

I thought the regular Platform scripts were unaffected by the installer reworks?

view this post on Zulip Andrew Appel (Sep 29 2022 at 14:56):

In which case, perhaps the answer is "no problems to be expected" which would be nice.

view this post on Zulip Michael Soegtrop (Sep 29 2022 at 16:35):

@Andrew Appel : if you use compile from sources scripts there shouldn't be any issues - unless there are also issues with plain opam installations. The installers also work with ocamlfind (e.g. elpi and serapi use it), but most plugins use the legacy method, so this is not that well tested. It might happen that new issues arise.

Btw.: 2022.09 already contains MetaCoq in the "extended" section and the smoke test works also with installers.

view this post on Zulip Michael Soegtrop (Sep 29 2022 at 16:36):

And yes, the "compile from sources" scripts didn't have substantial changes.

view this post on Zulip Théo Zimmermann (Sep 29 2022 at 16:58):

@Michael Soegtrop Since September is almost over, and the final 2022.09.0 will come several weeks after the beta, would it make sense to rename it to 2022.10? I think the Snap track is not yet requested, so this is still possible.

view this post on Zulip Karl Palmskog (Sep 29 2022 at 17:06):

all the Platform plugins for 8.16.0 have at least run the usual Coq opam archive CI gauntlet (that's where we discovered problems with MetaCoq 1.0). So we have some evidence that the legacy method typically works out.

view this post on Zulip Michael Soegtrop (Sep 29 2022 at 18:12):

@Théo Zimmermann : it is a bit of work since I need to rebuild all my local switches (9 versions x 3 platforms) - otherwise I can't test or create readmes or the like. For Linux and Windows this is reasonably fast (I have a largish thread ripper workstation for that) but on Mac - on which I mostly work, it takes > 1 day.

view this post on Zulip Théo Zimmermann (Sep 29 2022 at 20:03):

OK never mind then

view this post on Zulip Michael Soegtrop (Sep 30 2022 at 07:36):

Update: CI is full green for the first time since I enabled an 8.16.0 based pick. The only hack is that I disabled MetCoq on Windows (there are build issues I need to investigate). And the .dev build needs a bit of work (I run it only daily, not in PRs / merges) but this is not an issue for a release.
There are a few issues for 2022.09 left I plan to handle today.
It might make sense if a few people review the issues I moved to 2023.03 (there is a milestone for that). If someone deems something in there utterly important, I am open to discussion. Everything I marked 2022.09 I plan to do today.

view this post on Zulip Andrew Appel (Sep 30 2022 at 12:27):

One of my research projects uses MetaCoq, but we don't urgently need it on Windows and especially not if it will delay the Coq Platform release, so I fully support omitting MetaCoq from the Windows platform for now.

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

which release of MetaCoq might be added? I hope it's 1.1, which didn't seem to have problems in the regular CI: https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-metacoq/coq-metacoq.1.1%2B8.16

view this post on Zulip Théo Zimmermann (Sep 30 2022 at 12:32):

Yes, AFAIU, 1.1 was released precisely in order to get into the Coq Platform.

view this post on Zulip Michael Soegtrop (Sep 30 2022 at 13:00):

I did a PR to fix Metacoq on Windows - see https://github.com/MetaCoq/metacoq/pull/765. A simple CRLF issue.

@Karl Palmskog : I don't think the Opam Coq CI tests on Windows. And yes, I am using 1.1+8.16.

view this post on Zulip Karl Palmskog (Sep 30 2022 at 13:01):

indeed, it only tests on Linux x86 ("regular")

view this post on Zulip Michael Soegtrop (Oct 10 2022 at 09:12):

The release is almost done - Windows installers are in signing.
@Enrico Tassi @Théo Zimmermann : I did the snapcraft track request here: https://forum.snapcraft.io/t/2022-09-track-creation-for-coq-prover/32117.

view this post on Zulip Michael Soegtrop (Oct 10 2022 at 09:14):

Sorry for all the delays - it was quite rough this time cause of the ocamlfind changes and hitting the 6h timouts in CI.
But now all is well and also the open issue count is less than half - a lot of long overdue small improvements.

view this post on Zulip Théo Zimmermann (Oct 10 2022 at 09:15):

Not to worry. I'm sorry that we were not of a bigger help.

view this post on Zulip Michael Soegtrop (Oct 10 2022 at 09:19):

No issue at all - I am happy when the Coq Core Team can concentrate on improving Coq.

view this post on Zulip Théo Zimmermann (Oct 11 2022 at 13:21):

Here is a proposal announcement:

Object: Coq Platform 2022.09.0 (including beta version for Coq 8.16.0 and a updated and extended package pick)

Dear Coq community,

On behalf of the Coq development team, the release manager of Coq 8.16, and the Coq Platform team, we are happy to announce the immediate availability of the Coq Platform 2022.09.0 release.

Release highlights:

The main supported version is:

Several compatibility versions with Coq 8.12 to 8.15 are available, including one for Coq 8.15 with a package collection that tries to be as similar as possible to the Coq 8.16.0 pick.

Installers for Coq 8.16 and Coq 8.15 with the beta package pick are available for Windows, macOS, and Linux (a Snap installer, that should be updated soon to include Coq 8.16).

You can also install the Coq Platform using opam-based scripts, which give you access to the main supported version, as well as any of the many compatibility versions.

To learn about the Coq Platform and get access to the installers, please refer to:

https://github.com/coq/platform/releases/tag/2022.09.0

We expect a new Platform release (2022.09.1) to happen in about 2 weeks, with a finalized package pick.

view this post on Zulip Michael Soegtrop (Oct 11 2022 at 13:29):

@Théo Zimmermann : thanks, looks good! Should we mention the timeline for the final release (about 2 weeks if all goes well)?

view this post on Zulip Théo Zimmermann (Oct 11 2022 at 13:29):

Ah right, I forgot!

view this post on Zulip Théo Zimmermann (Oct 11 2022 at 13:29):

How will it be called? 2022.09.1, I assume?

view this post on Zulip Karl Palmskog (Oct 11 2022 at 13:30):

@Théo Zimmermann maybe you want to highlight some of the new packages? Itauto, MathComp Algebra Tactics, MathComp Word

Edit: saw now this was included.

view this post on Zulip Karl Palmskog (Oct 11 2022 at 13:31):

I think MetaCoq deserves a mention though, even if it's only in "extended"...

view this post on Zulip Michael Soegtrop (Oct 11 2022 at 13:31):

@Théo Zimmermann : yes, this will be 2022.09.1 (the picks will be 2022.09 then).

view this post on Zulip Michael Soegtrop (Oct 11 2022 at 13:33):

I tend to agree with Karl that MetaCoq is important enough to mention that it is in extended now - which means there is a certain commitment to bting it into full and also that it is in the Coq Platform CI (which is a bit tougher cause of the multi platform aspect).

view this post on Zulip Michael Soegtrop (Oct 11 2022 at 13:34):

The same applies to bedrock2 and fiatcrypto btw.

view this post on Zulip Pierre Roux (Oct 11 2022 at 13:34):

Théo Zimmermann said:

Maybe mathcomp-algebra-tactics since mathcomp-algebra is already the name of one of the OPAM packages of MathComp?

view this post on Zulip Théo Zimmermann (Oct 11 2022 at 13:35):

Right, my mistake.

view this post on Zulip Michael Soegtrop (Oct 11 2022 at 13:36):

I think an important point about fiatcrypto is that it was really hard to compile before, because it depends on quite a few git repos, non of which had tags or releases. I think it is quite substantial, that there is a working opam package for fiat-crypto including all dependencies now.

view this post on Zulip Théo Zimmermann (Oct 11 2022 at 13:37):

OK, but I've already listed it in the (edited) announcement. Do I have to add anything else?

view this post on Zulip Michael Soegtrop (Oct 11 2022 at 13:38):

Ah yes, that's fine.

view this post on Zulip Karl Palmskog (Oct 11 2022 at 13:38):

insert the Snap link inline? https://snapcraft.io/coq-prover

view this post on Zulip Théo Zimmermann (Oct 11 2022 at 13:38):

What about the last sentence I've just added?

view this post on Zulip Michael Soegtrop (Oct 11 2022 at 13:39):

@Karl Palmskog : the snap is not there yet - I am waiting fo rthe track approval (should do it upfront next time).

view this post on Zulip Michael Soegtrop (Oct 11 2022 at 13:39):

But I could upload the snap file with instructions on how to install from a local snap (which is not complicated either).

view this post on Zulip Karl Palmskog (Oct 11 2022 at 13:40):

right, yes, but I was suggesting to insert the generic link, so people who don't even know about snap can see what it's about, and then that link will show the release when it's done

view this post on Zulip Michael Soegtrop (Oct 11 2022 at 13:40):

@Théo Zimmermann : the text is fine IMHO, including the last line.

view this post on Zulip Théo Zimmermann (Oct 11 2022 at 13:41):

OK, then I will send the announcement.

view this post on Zulip Michael Soegtrop (Oct 11 2022 at 13:41):

Well it is in the release notes linked above - we don't insert links to the other installers either.

view this post on Zulip Théo Zimmermann (Oct 11 2022 at 13:41):

There is a reason for that.

view this post on Zulip Théo Zimmermann (Oct 11 2022 at 13:41):

The other installers are part of the release we point to on GitHub.

view this post on Zulip Michael Soegtrop (Oct 11 2022 at 13:42):

So back to the question: should I upload the snap file with instructions (should be snap install --dangerous some_file.snap)

view this post on Zulip Théo Zimmermann (Oct 11 2022 at 13:43):

No

view this post on Zulip Michael Soegtrop (Oct 11 2022 at 13:43):

But I would say reagrding snap and installers the release notes are symmetric - they are all at the top.

view this post on Zulip Michael Soegtrop (Oct 11 2022 at 13:43):

Maybe the snap link should not be obscurified as much as I did ...

view this post on Zulip Théo Zimmermann (Oct 11 2022 at 13:44):

Your release notes are fine.

view this post on Zulip Michael Soegtrop (Oct 11 2022 at 13:44):

It is under "Beta Linux (Snap) installer for Coq 8.16".

view this post on Zulip Michael Soegtrop (Oct 11 2022 at 13:44):

Then I wouldn't put the snap link in the annoucement.

view this post on Zulip Théo Zimmermann (Oct 11 2022 at 13:44):

Yes, that's fine.

view this post on Zulip Théo Zimmermann (Oct 11 2022 at 13:44):

If you say so.

view this post on Zulip Michael Soegtrop (Oct 11 2022 at 13:45):

I would not include it for symmetry reasons.

view this post on Zulip Michael Soegtrop (Oct 11 2022 at 13:45):

Go for launch from my desk.

view this post on Zulip Théo Zimmermann (Oct 11 2022 at 13:46):

But it is not symmetric to the rest anyway since it is distributed on an external store and the binary installers for Windows and macOS are not (and are available for several versions).

view this post on Zulip Théo Zimmermann (Oct 11 2022 at 13:47):

Michael Soegtrop said:

Go for launch from my desk.

Your Go is a bit contradictory to me. Should I remove or not remove the inline link to Snapcraft that I've added ever since Karl asked for it?

view this post on Zulip Michael Soegtrop (Oct 11 2022 at 13:48):

Well yes, but they are all mentioned with equal weight right at the top of the release notes.

Sorry, I meant "go for launch" with the snap link removed.

view this post on Zulip Théo Zimmermann (Oct 11 2022 at 13:48):

OK

view this post on Zulip Michael Soegtrop (Oct 12 2022 at 12:52):

@Enrico Tassi : is there anything I need to do about https://forum.snapcraft.io/t/2022-09-track-creation-for-coq-prover/32117?

view this post on Zulip Andrew Appel (Oct 16 2022 at 15:37):

Unfortunately the "Interrupt doesn't fully work on Windows" issue is not any better in 2022.09+beta1. See my message at the Coq issue report. Still, as described in that message, there is a simple work-around, and in general I am delighted to have the Coq Platform 2022.09+beta1 release, because it fixes the Flocq3/Flocq4 problem among other things.

view this post on Zulip Michael Soegtrop (Oct 24 2022 at 12:42):

@Pierre-Marie Pédrot : Since I didn't get negative feedback on the beta besides the "Interrupt" issue on Windows - which can be worked around by starting CoqIDE in a specific way - I plan to do the final release soon. Do you plan a 8.16.1? If so when?

view this post on Zulip Pierre-Marie Pédrot (Oct 24 2022 at 12:44):

I don't have a precise schedule but right now I'm a bit slowed down by the fact that the CI does not properly run.

view this post on Zulip Pierre-Marie Pédrot (Oct 24 2022 at 12:44):

I'm a bit reluctant to backport patches without a full green CI but I think that at some point I won't have any other choice

view this post on Zulip Michael Soegtrop (Oct 24 2022 at 12:46):

So the answer is: "yes, I am planning for 8.16.1". If the main problem is VST I could do some studies on memory consumption.

view this post on Zulip Pierre-Marie Pédrot (Oct 24 2022 at 12:49):

all devs stressing the machines are problematic, e.g. fiat-crypto

view this post on Zulip Pierre-Marie Pédrot (Oct 24 2022 at 12:49):

for some reason now even the test-suite fails with stack overflow: https://github.com/coq/coq/pull/16034

view this post on Zulip Michael Soegtrop (Oct 24 2022 at 13:10):

Afaik the stack size for fiat-crypto had to be increased from 16M to 32M when flambda is enabled. It is quite imaginable that the 32M are very tight and minor changes break it.

view this post on Zulip Michael Soegtrop (Oct 24 2022 at 13:17):

@Pierre-Marie Pédrot : anyway, if you want me to look into the VST memory consumption I can e.g. make a local build and record the memory requirements of each coqc call. One should take this x2 + system overhead then for -j2. I did some tests in the past for the Coq Platform recommendations and found that with -j 2 it is fairly random if memory hungry files are compiled together or not.

view this post on Zulip Michael Soegtrop (Oct 24 2022 at 13:19):

I would rather invest some time here than live with an exclusion of VST from CI.

view this post on Zulip Michael Soegtrop (Oct 24 2022 at 13:23):

For things like stack size limits, I would recommend to determine a reasonably tight lower bound, use 1.5x that in CI and check the lower bound from time to time to avoid stack size regressions.

view this post on Zulip Théo Zimmermann (Oct 24 2022 at 15:03):

@Pierre-Marie Pédrot To avoid the CI issues, you could run the v8.16 CI on your own GitLab fork of Coq. Then you could enable shared runners there. I guess the allowance should be enough so that you can do all the things you need for 8.16.1.

view this post on Zulip Andrew Appel (Oct 24 2022 at 18:20):

Will there be a 32-bit-coq-for-windows binary in either the 2022.09+beta or the regular 2022.09 Platform release? My policy is that "VST always builds in 1GB-per-coqc-process when run in 32-bit mode". I would expect that in 64-bit mode it should always succeed in 2-GB-per-coqc-process" in a standard 64-bit install of Coq. If there is something in Coq 8.16 that uses more memory than that, I would be worried.
However, today I've been rebuilding VST (more than once) in my 64-bit-coq-on-Windows Coq 8.16 (from the Coq Platform 2022.09+beta), running 8 jobs on my 16GB machine, and I haven't had any problems.

view this post on Zulip Michael Soegtrop (Oct 24 2022 at 21:04):

@Andrew Appel : yes, the delivery will be the same as for the beta release (https://github.com/coq/platform/releases/tag/2022.09.0). Are there any issues with the 32 bit installers in there?

view this post on Zulip Andrew Appel (Oct 25 2022 at 11:53):

Oops. In reading the web page https://github.com/coq/platform/releases/tag/2022.09.0 I just saw "Recommended Binary Installers" at the top of the page (which did not include 32-bit Windows binary), and did not go down all the way to the bottom of the page (where the 32-bit Windows binary is found).

view this post on Zulip Théo Zimmermann (Oct 25 2022 at 11:55):

Yes, the idea of this new section is to help newcomers find their way, while expert users usually know what they are looking for =D

view this post on Zulip Michael Soegtrop (Oct 26 2022 at 08:05):

@Andrew Appel : yes the the 32 bit installer is not recommended, because some things don't compile with 2GB RAM (which is the per process limit on non server 32 bit Windows). For this reason several packages are excluded (UniMath and Bedrock/Fiat-crypto).

One can of course discuss this policy. On a Windows laptop with 4GB RAM, one might be better of with the 32 bit version, since it needs less RAM, but I am not sure how much less.

view this post on Zulip Théo Zimmermann (Oct 28 2022 at 07:51):

@Michael Soegtrop The new track was apparently created after Enrico's ping (16 days ago). Can we push the new package to this track? But since this is only a beta release, maybe this should only reach latest/beta and latest/edge but not latest/stable.

view this post on Zulip Michael Soegtrop (Oct 28 2022 at 08:08):

Yes, sorry forgot about it.

view this post on Zulip Michael Soegtrop (Nov 14 2022 at 16:06):

@Pierre-Marie Pédrot : just wanted to ask what the status of 8.16.1 is and if I possibly should do another Coq Platform release with 8.16.0.

view this post on Zulip Pierre-Marie Pédrot (Nov 14 2022 at 16:11):

I don't have a schedule, but I believe the 8.16.1 release should happen before the 8.17.0. I'll answer by a question then: who's taking care of that and when will it happen?

view this post on Zulip Michael Soegtrop (Nov 14 2022 at 16:34):

OK - back to the question if I should do a non preview release of the 8.16.0 pick - currently it is marked preview. What are the issues with 8.16.0 which speak against this?

view this post on Zulip Théo Zimmermann (Nov 15 2022 at 08:24):

IMHO 8.16.1 should happen as soon as necessary to enable the non-beta Coq Platform 2022.09.0 release to ship with a non-patched Coq.

view this post on Zulip Théo Zimmermann (Nov 15 2022 at 08:24):

Regarding 8.17, the topic is again on the agenda of the next Coq Call.

view this post on Zulip Karl Palmskog (Nov 15 2022 at 08:25):

how was Coq patched? I missed that part.

view this post on Zulip Karl Palmskog (Nov 15 2022 at 08:25):

(and shouldn't that patch then go in the opam repo?)

view this post on Zulip Théo Zimmermann (Nov 15 2022 at 08:26):

The Coq Platform release notes say:

There are two patches to CoqIDE included, which are not in the 8.16.0 release:

view this post on Zulip Karl Palmskog (Nov 15 2022 at 08:27):

hm, those sound like they might sense to add here: https://github.com/ocaml/opam-repository/tree/master/packages/coqide/coqide.8.16.0

view this post on Zulip Karl Palmskog (Nov 15 2022 at 08:28):

depending on how soon 8.16.1 is released, I guess

view this post on Zulip Pierre-Marie Pédrot (Nov 15 2022 at 09:22):

I'll backport as many PRs as possible to 8.16 for a fast release then

view this post on Zulip Michael Soegtrop (Nov 16 2022 at 09:30):

@Pierre-Marie Pédrot : indeed I think it is better to have a release soon and possibly a 8.16.2 later (this is not unheard of).

One severe issue in MacOS is btw. that it does not save preferences any more (I should have created an issue for this a while back ...)

view this post on Zulip Michael Soegtrop (Nov 18 2022 at 07:54):

A short status update from my side:

Otherwise I am not aware of issues.
@Pierre-Marie Pédrot : please ping me when you are ready.

view this post on Zulip Pierre-Marie Pédrot (Nov 18 2022 at 10:46):

I'm almost done, but given that we found not one but two soundness bugs yesterday, we'll have to fix them before proceeding...

view this post on Zulip Michael Soegtrop (Nov 18 2022 at 12:12):

IMHO it is also an option to release (pretty much) now and do another release as soon as the inconsistencies are fixed.

The inconsistencies are not nice of course, but most users are not that much affected by them. You can continue to develop your proofs and recheck with the next version.

view this post on Zulip Pierre-Marie Pédrot (Nov 18 2022 at 12:12):

the first one is very easy to fix, though

view this post on Zulip Pierre-Marie Pédrot (Nov 18 2022 at 12:13):

I'm just too lazy to write all the critical doc and what not, but the code fix in itself is a one-liner

view this post on Zulip Michael Soegtrop (Nov 18 2022 at 13:33):

And the 2nd one?

view this post on Zulip Pierre-Marie Pédrot (Nov 18 2022 at 13:42):

some broken primitive int / array implementation probably, but I didn't look into it in detail yet

view this post on Zulip Michael Soegtrop (Nov 18 2022 at 18:53):

OK. I would say we wait until mid next week and decide then if we do a release or not. I will have the CoqIDE preferences patch ready by then.

view this post on Zulip Théo Zimmermann (Nov 18 2022 at 21:51):

The two fixes for soundness bugs are already ready anyway.

view this post on Zulip Michael Soegtrop (Nov 20 2022 at 14:09):

I just did a PR for the CoqIDE fix - I didn't follow the details on running full CI - coqbot says I need it. Can someone do the magic please?

view this post on Zulip Michael Soegtrop (Nov 21 2022 at 17:23):

@Pierre-Marie Pédrot : you let me know if 8.16.1 is there?

view this post on Zulip Pierre-Marie Pédrot (Nov 21 2022 at 19:29):

yup, it will probably be tomorrow or the day after (I'm waiting for benches to finish on the soundness fixes)

view this post on Zulip Michael Soegtrop (Nov 25 2022 at 09:34):

@Pierre-Marie Pédrot : do you have an update on 8.16.1?

view this post on Zulip Pierre-Marie Pédrot (Nov 25 2022 at 10:23):

Yes, despite having taken a bit more than expected (and having a known soundness bug in 8.16.1) I'm virtually ready to tag.

view this post on Zulip Pierre-Marie Pédrot (Nov 25 2022 at 10:23):

if you see no problem I can do it right now

view this post on Zulip Pierre-Marie Pédrot (Nov 25 2022 at 10:25):

(will do by noon if I don't hear anybody screaming at me)

view this post on Zulip Karl Palmskog (Nov 25 2022 at 10:31):

has anything changed packaging wise? or can one just copy paste "old" 8.16.0 opam packages?

view this post on Zulip Pierre-Marie Pédrot (Nov 25 2022 at 10:32):

not that I know of

view this post on Zulip Karl Palmskog (Nov 25 2022 at 10:34):

but we should begin to add < "5" for OCaml, right?

view this post on Zulip Karl Palmskog (Nov 25 2022 at 10:34):

because 8.16 is not compatible with 5.0 beta, to my knowledge (not direct knowledge)

view this post on Zulip Pierre-Marie Pédrot (Nov 25 2022 at 10:39):

yes, Coq is currently incompatible with OCaml 5

view this post on Zulip Pierre-Marie Pédrot (Nov 25 2022 at 10:39):

(all historical Coq packages should be marked incompatible, actually)

view this post on Zulip Karl Palmskog (Nov 25 2022 at 10:44):

sure, but that one I will leave for opam repo devs (historical packages)

view this post on Zulip Karl Palmskog (Nov 25 2022 at 10:45):

I hope they do it soon, because all the people who like the hippest and latest stuff will likely install OCaml 5 soon and open issues everywhere when something doesn't work (compare: Mac M1/M2)

view this post on Zulip Guillaume Melquiond (Nov 25 2022 at 10:56):

Karl Palmskog said:

but we should begin to add < "5" for OCaml, right?

There is already conflicts: "base-nnp". Anything else would be redundant.

view this post on Zulip Michael Soegtrop (Nov 25 2022 at 11:48):

@Pierre-Marie Pédrot : I just double checked the commit list of the 8.16 branch with my issue list and all is fine. Please go ahead.

view this post on Zulip Pierre-Marie Pédrot (Nov 25 2022 at 12:13):

tag sent, all systems ready

view this post on Zulip Karl Palmskog (Nov 25 2022 at 19:19):

@Erik Martin-Dorel coq.8.16.1 is now out on opam

view this post on Zulip Karl Palmskog (Nov 25 2022 at 22:18):

coqide.8.16.1 also out now on opam

view this post on Zulip Michael Soegtrop (Nov 28 2022 at 10:59):

@Pierre-Marie Pédrot @Jason Gross : I have an odd issue with Coq-rewriter and Coq 8.16.1: on an Intel Mac it builds fine with 32 MB stack (ulimit -s 32768). On an Apple silicon Mac it does not build with almost twice as much stack. Unfortunately macOS has a hard limit of 65520kB stack size (seriously?). I expect that I am using native ARM Ocaml (it is definitely much faster than the Intel Mac, so I don't think it messed it up in a way which makes me work with Rosetta). Any thoughts?

Btw.: I wanted to also supply an Apple Silicon Coq Platform installer - but I might have to drop rewrite and fiat-crypto for this reason.

view this post on Zulip Michael Soegtrop (Nov 28 2022 at 11:02):

P.S.: I CCed Pierre-Marie above because I thought there is also a difference between 8.16.0 and 8.16.1 in that (I remember some discussions about this), but this does not seem to be the case.

view this post on Zulip Jason Gross (Nov 28 2022 at 12:27):

Ew, really? I'm happy to add a SKIP_ENORMOUS_STACK variable to the Makefile that disables the build of the things that need that much stack. If I'm recalling correctly, it's only solinas_reduction that needs this much stack? Is that right, or are there other targets that fail?

view this post on Zulip Jason Gross (Nov 28 2022 at 12:32):

I think we'd wrap https://github.com/mit-plv/fiat-crypto/blob/d72df784a772ea179243dde8a3ac04c59e3ce70d/Makefile.examples#L123 and the addition of solinas_reduction to https://github.com/mit-plv/fiat-crypto/blob/d72df784a772ea179243dde8a3ac04c59e3ce70d/Makefile.config#L53 in something like ifneq ($(SKIP_ENORMOUS_STACK),1) ... endif.

view this post on Zulip Jason Gross (Nov 28 2022 at 12:34):

Another alternative is that we could possibly set up the ARM build to use Haskell rather than ocamlopt to build extracted code? Idk if that's any better?

view this post on Zulip Jason Gross (Nov 28 2022 at 12:35):

And if you can let me know what's failing, it might be worth opening an issue on the OCaml bug tracker that compiling this file takes too much stack and ocamlopt should be more efficient, or at least have a mode for compiling with less stack?

view this post on Zulip Michael Soegtrop (Nov 28 2022 at 12:53):

@Jason Gross It is this file which fails at 64M stack size:

File "./src/Rewriter/Demo.v", line 20, characters 0-21:
Error: Stack overflow.

but afair it was a different one with 32M - maybe also a randomness in parallel build - I am rerunning it at 32M.

view this post on Zulip Jason Gross (Nov 28 2022 at 12:56):

Line 20 in Demo.v is Search, you should report an issue on the Coq bug tracker requesting that Search be more tail recursive if need be
https://github.com/mit-plv/rewriter/blob/d644f09c90513b0837c2f9f54fd0a19315ee31dd/src/Rewriter/Demo.v#L20

In the meantime you can just patch out that line?

view this post on Zulip Michael Soegtrop (Nov 28 2022 at 13:16):

Hmm OK - a Search (?x + 0 = ?x). really looks rather innocent.

Should I bisect the stack size needed on Intel for this?

view this post on Zulip Enrico Tassi (Nov 28 2022 at 13:18):

We have stack overflows problems on searches like that one using JScoq since many years.
The easy way out is to limit the search to a module, so that the number of results is smaller, eg Search ... inside module_name.

view this post on Zulip Enrico Tassi (Nov 28 2022 at 13:19):

Fixing the issue in Coq would surely be better, just wanted to share a quick work around.

view this post on Zulip Michael Soegtrop (Nov 28 2022 at 13:20):

@Enrico Tassi : can you imagine why ARM would take 2x the amount of stack than Intel?

view this post on Zulip Michael Soegtrop (Nov 28 2022 at 13:21):

@Jason Gross : yes sure I can patch this out. Let's see how far I get with Fiat crypto then ...

view this post on Zulip Enrico Tassi (Nov 28 2022 at 13:27):

Michael Soegtrop said:

Enrico Tassi : can you imagine why ARM would take 2x the amount of stack than Intel?

nope, CC @Gabriel Scherer which surely knows better than me if this is a known issue. Which OCaml version are we talking about BTW?

view this post on Zulip Michael Soegtrop (Nov 28 2022 at 13:29):

COQ_PLATFORM_OCAML_VERSION='4.13.1'

view this post on Zulip Michael Soegtrop (Nov 28 2022 at 13:31):

@Jason Gross : With the patch I get:

File "./src/Rewriter/Language/IdentifiersLibraryProofs.v", line 285, characters 12-29:
Error: Stack overflow.

view this post on Zulip Jason Gross (Nov 28 2022 at 13:48):

That is https://github.com/mit-plv/rewriter/blob/d644f09c90513b0837c2f9f54fd0a19315ee31dd/src/Rewriter/Language/IdentifiersLibraryProofs.v#LL285C13-L285C29 which is
https://github.com/mit-plv/rewriter/blob/d644f09c90513b0837c2f9f54fd0a19315ee31dd/src/Rewriter/Language/IdentifiersLibraryProofs.v#L176-L182
None of the tactics here are even recursive (they're all defined right above that tactic), so I don't see what could be taking up stack space. Could you get a stack trace?

view this post on Zulip Jason Gross (Nov 28 2022 at 13:50):

But it's starting to sound like OCaml / Coq on ARM aren't ready for serious development. These aren't even the parts of rewriter and Fiat Crypto that are known to stress various bits of the Coq toolchain

view this post on Zulip Michael Soegtrop (Nov 28 2022 at 14:01):

@Jason Gross : I guess it makes more sense to not ship rewriter and fiat-crypto with the ARM DMG (which I would anyway call experimental). Of course I will include it in the Intel DMG. This looks like we can't solve this between 12 and lunch.

view this post on Zulip Michael Soegtrop (Nov 28 2022 at 14:02):

Possibly I should try a newer OCaml ...

view this post on Zulip Michael Soegtrop (Nov 28 2022 at 14:05):

@Jason Gross : actually good news: for testing I put the stack size back to 32M. When I use 64M, coq rewriter and coq fiat-crypto run through :-)

view this post on Zulip Michael Soegtrop (Nov 28 2022 at 14:05):

So I will include them in the Apple silicon DMG

view this post on Zulip Gabriel Scherer (Nov 28 2022 at 15:12):

nope, CC @Gabriel Scherer which surely knows better than me if this is a known issue.

Stack usage is a system-dependent property, for example some platform may expect call-frame alignment guarantees that artificially inflate stack usage on small non-tail recursive functions. Reporting 2x stack usage differences in corner cases is not terribly surprising.

Note that OCaml 5 does not use the system stack for OCaml calls anymore, so this category of issue will magically disappear.
(OCaml 5 is still somewhat experimental, of course.)

view this post on Zulip Gabriel Scherer (Nov 28 2022 at 15:12):

(Minor note: having everything in a single Zulip thread made it a bit difficult for me to follow this sub-conversation, I would welcome a new topic if there is more about this specific issue.)


Last updated: Jan 30 2023 at 11:03 UTC