Michael Soegtrop (Oct 16 2020 at 08:30): Michael Soegtrop (Oct 16 2020 at 08:30):I just wanted to give a short status update. I am still working on getting all my opam patches upstream. This week the gappa package has been merged to main opam which was not that trivial because it also added some C++ infrastructure packages like bison, flex and automake which was a bit of effort to get through opam's multi platform CI (which I learned to appreciate). I would say 90% of my patches are upstream meanwhile, but some still need to propagate to the MinGW opam repo.
One important piece still missing is the adwaita icon theme required by CoqIDE which for whatever reason seams to require slightly different setup and/or test instructions on each Linux distro - the last remaining ones tested in opam CI and failing are OpenSuse and CentOS. I setup the VMs for this yesterday - I have a fairy complete set now :-)
I btw. decided that I am going to support those OS platforms which are tested in opam CI. The largest effort in multi platform support is setting up the test infrastructure and this exists already with the opam CI.
Théo Zimmermann (Oct 16 2020 at 12:26):I btw. decided that I am going to support those OS platforms which are tested in opam CI. The largest effort in multi platform support is setting up the test infrastructure and this exists already with the opam CI.
That's great to hear!
Michael Soegtrop (Jun 14 2023 at 13:33):I just want to let the community know that I am still struggling at various fronts - the most severe is that LXD is well and thoroughly broken and so far any attempt to discuss it with the developers, to work around it or to fix it failed. So I now decided to switch to another virtualisation system to build snaps - which is a bit of effort (no pre built GitHub integration).
I have a bit less pressure with other projects now, so I hope I can finish this within two weeks.
Sorry for the delays, but this release really everything broke - every other week something new and the bandwidth I can spare for this was simply insufficient to keep up with the breakage.
Michael Soegtrop (Jun 14 2023 at 13:39):One more note on LXD: the really bad thing is that they back merged the bug into each and every installable version of LXD available on snap. Attempts to bisect this failed because the amount of changes was quite large and LXD runs fine for a few hours with the bug, so it is really hard to test. The issue also depends on load, so it is hard to reproduce locally (I need to hook up slow low memory machines and artificially load them). Meanwhile there seem to be ways to reproduce it reliably in a few minutes reported upstream, but no solution as yet.
Michael Soegtrop (Jul 10 2023 at 08:05):Sorry, I am still on it. Last week I fixed Mac (the Homebrew repo got inconsistent and GitHub couldn't fix it so some work around was required) and the 128k command line length issues on Linux by back merging a change to coq_makefile by @Gaëtan Gilbert (why neither Mac nor Cygwin on Windows have such a restriction but Linux has I really can't understand). Over the weekend apparently gtk-sourceview broke for 64 bit Windows and I still have the move away from LXD in the snap build which likely remains to be broken for the foreseeable future.
Théo Zimmermann (Jul 10 2023 at 08:12):Regarding LXD, FWIW, @Enrico Tassi never managed to have LXD run locally anyway so had to use a different containerization to have local builds. I don't recall the name.
Michael Soegtrop (Jul 10 2023 at 08:22):Yes, I experimented with alternatives. It is easy locally, but not so easy to set up in CI - things like group management and access rights to system semaphore files for the CI runner user without logging out and the like. Also building snaps with LXD is supported by a ready to use GitHub action one has to reimplement if one moves to something else. All doable, but it takes more time than I would like it to take with the limited bandwidth I have.
Théo Zimmermann (Jul 10 2023 at 08:27):Right, but is fixing CI a priority for the next release (given how it anyway doesn't work for building the actual release because of timeout issues)?
Théo Zimmermann (Jul 10 2023 at 08:28):With all the problems we have had with GitHub Actions for the Coq Platform CI, maybe it also means we should explore something else (e.g., GitLab-CI based).
Michael Soegtrop (Jul 10 2023 at 08:34):Since up to now I always had at least two open problems I didn't get into the situation to ask me this question as yet. But indeed I plan to release as soon as I get all other problems fixed - which unfortunately currently come in about as fast as I can fix them ...
Michael Soegtrop (Jul 10 2023 at 08:37):And yes, we should move to something else also because of the 6h limitation - it is not good that I have to build the installers locally. But the problems I had recently are not related to GitHub - or at least not related to having Coq Platform CI running on GitHub (but e.g. the issue that Homebrew is hosted on GitHub and git claims that the repo is broken and denies to clone it - from time to time ...).
Michael Soegtrop (Jul 10 2023 at 09:15):I also have plans to split up the build into packages, but I would prefer to do this after the .vo files are compatible between 64 bit architectures, so that I can build one set of .vo files for all platforms. I am not sure how complicated this would be - as far as I know the issue are different native C integer sizes which are visible in the OCaml serialisation format (int is 32 bit on 64 bit Windows but 64 bit on Mac and Linux afair).
Paolo Giarrusso (Jul 10 2023 at 09:44):vo files include hashes of native binaries, so that seems hopeless?
Théo Zimmermann (Jul 10 2023 at 09:45):AFAIK there are no specific plans to make vo files compatible across architectures or compiler versions. You may want to discuss this with @Pierre-Marie Pédrot to figure out whether it is realistic or not that this will happen in the future.
Gaëtan Gilbert (Jul 10 2023 at 09:48):those hashes aren't checked so they're not a great obstacle
they're mostly there so that dune works (otherwise if you change eg ltac_plugin, Ltac.vo wouldn't change and nothing else gets recompiled)
Paolo Giarrusso (Jul 10 2023 at 09:50):but even without dune, they're desired so that if you change ltac_plugin the code refuses to load Ltac.vo? (I thought they predated dune)
Michael Soegtrop (Jul 10 2023 at 10:12):We discussed VO compatibility on the Coq Workshop last year. Afair there was some consensus on that it wouldn't be easy but not that hard either to achieve and that it is more than a nice to have to grow Coq Platform further.
Michael Soegtrop (Jul 10 2023 at 10:15):It is of course also possible to have an installer which downloads .vo packages as needed without having .vo compatibility, but making this reasonably well behaved would also be quite a bit of effort.
Gaëtan Gilbert (Jul 10 2023 at 10:17):Paolo Giarrusso said:
but even without dune, they're desired so that if you change ltac_plugin the code refuses to load Ltac.vo? (I thought they predated dune)
it doesn't refuse to load Ltac.vo
Emilio Jesús Gallego Arias (Jul 10 2023 at 13:14):Dune could indeed add a dependency to the binaries as it can compute the transitive deps, this does however adds a lot of nodes to the build graph; indeed what notion of "security" or loading soundness to apply in this case is kinda open.
Michael Soegtrop (Aug 02 2023 at 13:50):After several months of one OS platform failing after the other, CI is green again with all bells and whistles turned on :-)
Last updated: Apr 20 2024 at 10:02 UTC