2022.09+beta1 release · Coq Platform devs & users

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").

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?

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

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.

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?)

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 ...)

Théo Zimmermann (Jun 17 2022 at 08:30):

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).

Théo Zimmermann (Jun 17 2022 at 08:32):

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

Karl Palmskog (Jun 17 2022 at 08:36):

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

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.

Enrico Tassi (Jun 17 2022 at 10:39):

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

Enrico Tassi (Jun 17 2022 at 10:40):

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

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).

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)

Michael Soegtrop (Jul 06 2022 at 17:18):

Michael Soegtrop (Jul 12 2022 at 12:51):

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

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.

Michael Soegtrop (Jul 12 2022 at 13:02):

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).

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.

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?

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.

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!

Michael Soegtrop (Aug 10 2022 at 15:44):

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

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?

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).

Michael Soegtrop (Aug 10 2022 at 17:02):

Pierre Roux (Aug 10 2022 at 17:04):

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.

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.

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.

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.

Karl Palmskog (Sep 15 2022 at 20:36):

Théo Zimmermann (Sep 15 2022 at 20:44):

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.

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.

Enrico Tassi (Sep 16 2022 at 10:21):

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

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.

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

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. :-/

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)

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).

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?

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

Enrico Tassi (Sep 16 2022 at 11:52):

Enrico Tassi (Sep 16 2022 at 11:53):

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

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.

Enrico Tassi (Sep 16 2022 at 11:53):

Enrico Tassi (Sep 16 2022 at 11:54):

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.

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

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?

Enrico Tassi (Sep 16 2022 at 11:58):

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)

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?

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

Enrico Tassi (Sep 16 2022 at 12:04):

Michael Soegtrop (Sep 16 2022 at 12:04):

Michael Soegtrop (Sep 16 2022 at 12:05):

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

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

Enrico Tassi (Sep 16 2022 at 12:06):

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`

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.

Michael Soegtrop (Sep 16 2022 at 12:11):

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.

Enrico Tassi (Sep 16 2022 at 13:48):

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

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...

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).

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?

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.

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)

Enrico Tassi (Sep 16 2022 at 18:46):

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).

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).

Michael Soegtrop (Sep 16 2022 at 19:08):

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

Enrico Tassi (Sep 16 2022 at 19:09):

Michael Soegtrop (Sep 16 2022 at 19:10):

Enrico Tassi (Sep 16 2022 at 19:10):

Enrico Tassi (Sep 16 2022 at 19:11):

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

Michael Soegtrop (Sep 16 2022 at 19:11):

Michael Soegtrop (Sep 16 2022 at 19:12):

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)

Michael Soegtrop (Sep 16 2022 at 19:13):

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"

Michael Soegtrop (Sep 16 2022 at 19:13):

Michael Soegtrop (Sep 16 2022 at 19:14):

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"

Michael Soegtrop (Sep 16 2022 at 19:14):

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...?

Enrico Tassi (Sep 16 2022 at 19:15):

Michael Soegtrop (Sep 16 2022 at 19:15):

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

Enrico Tassi (Sep 16 2022 at 19:16):

Michael Soegtrop (Sep 16 2022 at 19:16):

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"
)

Michael Soegtrop (Sep 16 2022 at 19:17):

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)

Michael Soegtrop (Sep 16 2022 at 19:18):

Enrico Tassi (Sep 16 2022 at 19:19):

Michael Soegtrop (Sep 16 2022 at 19:19):

Michael Soegtrop (Sep 16 2022 at 19:20):

Michael Soegtrop (Sep 16 2022 at 19:21):

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".

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.

Michael Soegtrop (Sep 16 2022 at 19:22):

Enrico Tassi (Sep 16 2022 at 19:23):

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

Enrico Tassi (Sep 16 2022 at 19:23):

Michael Soegtrop (Sep 16 2022 at 19:23):

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?

Enrico Tassi (Sep 16 2022 at 19:25):

Michael Soegtrop (Sep 16 2022 at 19:26):

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

Michael Soegtrop (Sep 16 2022 at 19:26):

Enrico Tassi (Sep 16 2022 at 19:26):

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.

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:

Enrico Tassi (Sep 16 2022 at 19:28):

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
:

Michael Soegtrop (Sep 16 2022 at 19:29):

Michael Soegtrop (Sep 16 2022 at 19:30):

Enrico Tassi (Sep 16 2022 at 19:30):

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.

Michael Soegtrop (Sep 16 2022 at 19:31):

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

Enrico Tassi (Sep 16 2022 at 19:31):

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

Michael Soegtrop (Sep 16 2022 at 19:33):

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

Enrico Tassi (Sep 16 2022 at 19:34):

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)

Michael Soegtrop (Sep 16 2022 at 19:35):

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

Enrico Tassi (Sep 16 2022 at 19:35):

Enrico Tassi (Sep 16 2022 at 19:36):

Michael Soegtrop (Sep 16 2022 at 19:36):

Michael Soegtrop (Sep 16 2022 at 19:37):

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:

Enrico Tassi (Sep 16 2022 at 19:39):

./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".

Michael Soegtrop (Sep 16 2022 at 19:40):

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

Enrico Tassi (Sep 16 2022 at 19:40):

Michael Soegtrop (Sep 16 2022 at 19:40):

Michael Soegtrop (Sep 16 2022 at 19:41):

Enrico Tassi (Sep 16 2022 at 19:41):

Michael Soegtrop (Sep 16 2022 at 19:42):

Enrico Tassi (Sep 16 2022 at 19:42):

Michael Soegtrop (Sep 16 2022 at 19:42):

Enrico Tassi (Sep 16 2022 at 19:42):

Michael Soegtrop (Sep 16 2022 at 19:43):

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

Michael Soegtrop (Sep 16 2022 at 19:43):

Michael Soegtrop (Sep 16 2022 at 19:46):

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.

Enrico Tassi (Sep 16 2022 at 19:48):

Michael Soegtrop (Sep 16 2022 at 19:48):

Enrico Tassi (Sep 16 2022 at 19:49):

Michael Soegtrop (Sep 16 2022 at 19:49):

Enrico Tassi (Sep 16 2022 at 19:50):

Michael Soegtrop (Sep 16 2022 at 19:51):

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

Enrico Tassi (Sep 16 2022 at 19:51):

Michael Soegtrop (Sep 16 2022 at 19:52):

# Packages linked into elpi

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

Enrico Tassi (Sep 16 2022 at 19:52):

Enrico Tassi (Sep 16 2022 at 19:53):

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

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.

Michael Soegtrop (Sep 16 2022 at 19:54):

Enrico Tassi (Sep 16 2022 at 19:54):

Michael Soegtrop (Sep 16 2022 at 19:54):

Enrico Tassi (Sep 16 2022 at 19:54):

Enrico Tassi (Sep 16 2022 at 19:55):

Michael Soegtrop (Sep 16 2022 at 19:56):

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.

Michael Soegtrop (Sep 16 2022 at 19:56):

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)

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.

Enrico Tassi (Sep 16 2022 at 19:58):

Michael Soegtrop (Sep 16 2022 at 19:58):

Enrico Tassi (Sep 16 2022 at 19:58):

Michael Soegtrop (Sep 16 2022 at 19:59):

Enrico Tassi (Sep 16 2022 at 19:59):

Michael Soegtrop (Sep 16 2022 at 20:00):

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

Michael Soegtrop (Sep 16 2022 at 20:00):

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...

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.

Michael Soegtrop (Sep 16 2022 at 20:02):

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'

Enrico Tassi (Sep 16 2022 at 20:03):

Michael Soegtrop (Sep 16 2022 at 20:03):

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"

Michael Soegtrop (Sep 16 2022 at 20:04):

Enrico Tassi (Sep 16 2022 at 20:04):

Michael Soegtrop (Sep 16 2022 at 20:04):

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

Enrico Tassi (Sep 16 2022 at 20:06):

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.

Michael Soegtrop (Sep 16 2022 at 20:07):

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

Enrico Tassi (Sep 16 2022 at 20:08):

Michael Soegtrop (Sep 16 2022 at 20:08):

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).

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.

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.

Enrico Tassi (Sep 16 2022 at 20:10):

Michael Soegtrop (Sep 16 2022 at 20:10):

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)

Michael Soegtrop (Sep 16 2022 at 20:11):

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

Enrico Tassi (Sep 16 2022 at 20:11):

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).

Enrico Tassi (Sep 16 2022 at 20:12):

Michael Soegtrop (Sep 16 2022 at 20:13):

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

Enrico Tassi (Sep 16 2022 at 20:13):

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.

Michael Soegtrop (Sep 16 2022 at 20:14):

Enrico Tassi (Sep 16 2022 at 20:14):

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

Michael Soegtrop (Sep 16 2022 at 20:15):

Enrico Tassi (Sep 16 2022 at 20:15):

Enrico Tassi (Sep 16 2022 at 20:16):

Enrico Tassi (Sep 16 2022 at 20:17):

Michael Soegtrop (Sep 16 2022 at 20:17):

Enrico Tassi (Sep 16 2022 at 20:18):

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

Enrico Tassi (Sep 16 2022 at 20:18):

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

Michael Soegtrop (Sep 16 2022 at 20:19):

Michael Soegtrop (Sep 16 2022 at 20:20):

Enrico Tassi (Sep 16 2022 at 20:20):

Michael Soegtrop (Sep 16 2022 at 20:20):

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?

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.

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.

Paolo Giarrusso (Sep 17 2022 at 07:39):

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.

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?

Michael Soegtrop (Sep 17 2022 at 16:09):

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

Enrico Tassi (Sep 17 2022 at 20:31):

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.

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.

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?

Enrico Tassi (Sep 20 2022 at 09:44):

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.

Michael Soegtrop (Sep 20 2022 at 09:45):

Michael Soegtrop (Sep 20 2022 at 09:46):

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

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?

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

Enrico Tassi (Sep 20 2022 at 09:46):

Enrico Tassi (Sep 20 2022 at 09:47):

Michael Soegtrop (Sep 20 2022 at 09:47):

Michael Soegtrop (Sep 20 2022 at 09:56):

/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

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).

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?

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.

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.

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.

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.

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

Michael Soegtrop (Sep 20 2022 at 10:14):

Michael Soegtrop (Sep 20 2022 at 10:15):

Paolo Giarrusso (Sep 20 2022 at 10:15):

Michael Soegtrop (Sep 20 2022 at 10:15):

Paolo Giarrusso (Sep 20 2022 at 10:15):

Michael Soegtrop (Sep 20 2022 at 10:16):

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?

Paolo Giarrusso (Sep 20 2022 at 10:17):

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

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.

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).

Michael Soegtrop (Sep 20 2022 at 10:18):

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

Michael Soegtrop (Sep 20 2022 at 10:20):

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

Michael Soegtrop (Sep 20 2022 at 10:21):

Paolo Giarrusso (Sep 20 2022 at 10:22):

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

Michael Soegtrop (Sep 20 2022 at 10:22):

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

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

Michael Soegtrop (Sep 20 2022 at 10:23):

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

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.

Michael Soegtrop (Sep 20 2022 at 10:24):

Michael Soegtrop (Sep 20 2022 at 10:27):

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

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

Paolo Giarrusso (Sep 20 2022 at 11:36):

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

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.

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.

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)

Paolo Giarrusso (Sep 21 2022 at 18:25):

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.

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 ...

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?

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

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

Michael Soegtrop (Sep 22 2022 at 16:46):

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.

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.

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

Enrico Tassi (Sep 22 2022 at 19:53):

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)

Enrico Tassi (Sep 22 2022 at 20:50):

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.

Enrico Tassi (Sep 23 2022 at 11:55):

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

Michael Soegtrop (Sep 23 2022 at 12:10):

# Specifications for the "threads" library:
version = "[distributed with Ocaml]"
description = "Multi-threading"
requires(mt,mt_vm) = "threads.vm"
requires(mt,mt_posix) = "threads.posix"
directory = "^"
type_of_threads = "posix"

browse_interfaces = ""

warning(-mt) = "Linking problems may arise because of the missing -thread or -vmthread switch"
warning(-mt_vm,-mt_posix) = "Linking problems may arise because of the missing -thread or -vmthread switch"

package "vm" (
  # --- Bytecode-only threads:
  requires = "unix"
  directory = "+vmthreads"
  exists_if = "threads.cma"
  archive(byte,mt,mt_vm) = "threads.cma"
  version = "[internal]"
)

package "posix" (
  # --- POSIX-threads:
  requires = "unix"
  directory = "+threads"
  exists_if = "threads.cma"
  archive(byte,mt,mt_posix) = "threads.cma"
  archive(native,mt,mt_posix) = "threads.cmxa"
  version = "[internal]"
)

package "none" (
  error = "threading is not supported on this platform"
  version = "[internal]"
)

which has the only effect that it does not work if there is no threads.cma file at runtime - which I don't think makes sense.

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

Enrico Tassi (Sep 23 2022 at 13:12):

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.

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).

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?

Karl Palmskog (Sep 29 2022 at 14:56):

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

Andrew Appel (Sep 29 2022 at 14:56):

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

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.

Michael Soegtrop (Sep 29 2022 at 16:36):

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.

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.

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.

Théo Zimmermann (Sep 29 2022 at 20:03):

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.

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.

Karl Palmskog (Sep 30 2022 at 12:29):

Théo Zimmermann (Sep 30 2022 at 12:32):

Michael Soegtrop (Sep 30 2022 at 13:00):

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

Karl Palmskog (Sep 30 2022 at 13:01):

Michael Soegtrop (Oct 10 2022 at 09:12):

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.

Théo Zimmermann (Oct 10 2022 at 09:15):

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.

Théo Zimmermann (Oct 11 2022 at 13:21):

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)?

Théo Zimmermann (Oct 11 2022 at 13:29):

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

Karl Palmskog (Oct 11 2022 at 13:31):

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).

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).

Michael Soegtrop (Oct 11 2022 at 13:34):

Pierre Roux (Oct 11 2022 at 13:34):

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

Théo Zimmermann (Oct 11 2022 at 13:35):

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.

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?

Michael Soegtrop (Oct 11 2022 at 13:38):

Karl Palmskog (Oct 11 2022 at 13:38):

Théo Zimmermann (Oct 11 2022 at 13:38):

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).

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).

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

Michael Soegtrop (Oct 11 2022 at 13:40):

Théo Zimmermann (Oct 11 2022 at 13:41):

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.

Théo Zimmermann (Oct 11 2022 at 13:41):

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)

Théo Zimmermann (Oct 11 2022 at 13:43):

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.

Michael Soegtrop (Oct 11 2022 at 13:43):

Théo Zimmermann (Oct 11 2022 at 13:44):

Michael Soegtrop (Oct 11 2022 at 13:44):

Théo Zimmermann (Oct 11 2022 at 13:44):

Michael Soegtrop (Oct 11 2022 at 13:45):

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).

Théo Zimmermann (Oct 11 2022 at 13:47):

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?

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.

Théo Zimmermann (Oct 11 2022 at 13:48):

Michael Soegtrop (Oct 12 2022 at 12:52):

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.

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?

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.

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

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.

Pierre-Marie Pédrot (Oct 24 2022 at 12:49):

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.

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.

Michael Soegtrop (Oct 24 2022 at 13:19):

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

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.

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.

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.

Michael Soegtrop (Oct 24 2022 at 21:04):

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).

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

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.

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.

Michael Soegtrop (Oct 28 2022 at 08:08):

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.

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?

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?

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.

Théo Zimmermann (Nov 15 2022 at 08:24):

Karl Palmskog (Nov 15 2022 at 08:25):

Théo Zimmermann (Nov 15 2022 at 08:26):

Karl Palmskog (Nov 15 2022 at 08:27):

Karl Palmskog (Nov 15 2022 at 08:28):

Pierre-Marie Pédrot (Nov 15 2022 at 09:22):

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 ...)

Michael Soegtrop (Nov 18 2022 at 07:54):

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

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...

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.

Pierre-Marie Pédrot (Nov 18 2022 at 12:12):

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

Michael Soegtrop (Nov 18 2022 at 13:33):

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

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.

Théo Zimmermann (Nov 18 2022 at 21:51):

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?

Michael Soegtrop (Nov 21 2022 at 17:23):

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)

Michael Soegtrop (Nov 25 2022 at 09:34):

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.

Pierre-Marie Pédrot (Nov 25 2022 at 10:23):

Pierre-Marie Pédrot (Nov 25 2022 at 10:25):

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?

Pierre-Marie Pédrot (Nov 25 2022 at 10:32):

Karl Palmskog (Nov 25 2022 at 10:34):

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

Pierre-Marie Pédrot (Nov 25 2022 at 10:39):

Karl Palmskog (Nov 25 2022 at 10:44):

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)

Guillaume Melquiond (Nov 25 2022 at 10:56):

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.

Stream: Coq Platform devs & users

Topic: 2022.09+beta1 release

Théo Zimmermann (Jun 17 2022 at 07:08):

Karl Palmskog (Jun 17 2022 at 07:29):

Karl Palmskog (Jun 17 2022 at 07:29):

Théo Zimmermann (Jun 17 2022 at 07:40):

Karl Palmskog (Jun 17 2022 at 08:18):

Michael Soegtrop (Jun 17 2022 at 08:21):

Théo Zimmermann (Jun 17 2022 at 08:30):

Théo Zimmermann (Jun 17 2022 at 08:32):

Karl Palmskog (Jun 17 2022 at 08:36):

Karl Palmskog (Jun 17 2022 at 08:39):

Théo Zimmermann (Jun 17 2022 at 08:49):

Enrico Tassi (Jun 17 2022 at 10:39):

Enrico Tassi (Jun 17 2022 at 10:40):

Enrico Tassi (Jun 17 2022 at 10:40):

Karl Palmskog (Jun 17 2022 at 11:27):

Michael Soegtrop (Jul 06 2022 at 16:53):

Karl Palmskog (Jul 06 2022 at 17:07):

Michael Soegtrop (Jul 06 2022 at 17:18):

Michael Soegtrop (Jul 12 2022 at 12:51):

Karl Palmskog (Jul 12 2022 at 13:01):

Karl Palmskog (Jul 12 2022 at 13:01):

Michael Soegtrop (Jul 12 2022 at 13:02):

Michael Soegtrop (Aug 10 2022 at 13:46):

Michael Soegtrop (Aug 10 2022 at 13:48):

Théo Zimmermann (Aug 10 2022 at 13:52):

Michael Soegtrop (Aug 10 2022 at 15:41):

Théo Zimmermann (Aug 10 2022 at 15:42):

Michael Soegtrop (Aug 10 2022 at 15:44):

Michael Soegtrop (Aug 10 2022 at 15:44):

Pierre Roux (Aug 10 2022 at 16:43):

Michael Soegtrop (Aug 10 2022 at 17:00):

Michael Soegtrop (Aug 10 2022 at 17:02):

Pierre Roux (Aug 10 2022 at 17:04):

Michael Soegtrop (Aug 10 2022 at 17:28):

Michael Soegtrop (Aug 11 2022 at 08:12):

Andrew Appel (Sep 15 2022 at 20:18):

Karl Palmskog (Sep 15 2022 at 20:34):

Karl Palmskog (Sep 15 2022 at 20:36):

Théo Zimmermann (Sep 15 2022 at 20:44):

Michael Soegtrop (Sep 16 2022 at 08:39):

Michael Soegtrop (Sep 16 2022 at 08:51):

Enrico Tassi (Sep 16 2022 at 10:21):

Enrico Tassi (Sep 16 2022 at 10:21):

Michael Soegtrop (Sep 16 2022 at 11:41):

Michael Soegtrop (Sep 16 2022 at 11:42):

Enrico Tassi (Sep 16 2022 at 11:44):

Enrico Tassi (Sep 16 2022 at 11:46):

Enrico Tassi (Sep 16 2022 at 11:48):

Michael Soegtrop (Sep 16 2022 at 11:48):

Michael Soegtrop (Sep 16 2022 at 11:49):

Enrico Tassi (Sep 16 2022 at 11:51):

Enrico Tassi (Sep 16 2022 at 11:52):

Enrico Tassi (Sep 16 2022 at 11:53):

Michael Soegtrop (Sep 16 2022 at 11:53):

Enrico Tassi (Sep 16 2022 at 11:53):

Enrico Tassi (Sep 16 2022 at 11:54):

Michael Soegtrop (Sep 16 2022 at 11:55):

Enrico Tassi (Sep 16 2022 at 11:56):

Michael Soegtrop (Sep 16 2022 at 11:57):

Enrico Tassi (Sep 16 2022 at 11:58):

Enrico Tassi (Sep 16 2022 at 12:00):

Michael Soegtrop (Sep 16 2022 at 12:01):

Michael Soegtrop (Sep 16 2022 at 12:01):

Enrico Tassi (Sep 16 2022 at 12:02):

Enrico Tassi (Sep 16 2022 at 12:04):

Michael Soegtrop (Sep 16 2022 at 12:04):

Michael Soegtrop (Sep 16 2022 at 12:05):

Enrico Tassi (Sep 16 2022 at 12:05):

Enrico Tassi (Sep 16 2022 at 12:06):

Michael Soegtrop (Sep 16 2022 at 12:09):

Michael Soegtrop (Sep 16 2022 at 12:10):

Michael Soegtrop (Sep 16 2022 at 12:10):

Michael Soegtrop (Sep 16 2022 at 12:11):

Michael Soegtrop (Sep 16 2022 at 12:16):

Enrico Tassi (Sep 16 2022 at 13:48):

Enrico Tassi (Sep 16 2022 at 13:52):

Enrico Tassi (Sep 16 2022 at 13:53):

Michael Soegtrop (Sep 16 2022 at 17:11):