Stream: Coq Platform devs & users

Topic: Serapi in snap

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

@Emilio Jesús Gallego Arias : I have issues with sertop under snap - it works fine on MacOS and Windows. I get:

/snap/coq-prover/current/coq-platform/bin$ ./sertop
sertop: internal error, uncaught exception:
        Vernacentries.UnmappedLibrary(0, _)

/snap/coq-prover/current/coq-platform/bin$ ldd ./sertop
    linux-vdso.so.1 (0x00007fffd2126000)
    libgmp.so.10 => /lib/x86_64-linux-gnu/libgmp.so.10 (0x00007f0e9728e000)
    libpthread.so.0 => /lib/x86_64-linux-gnu/libpthread.so.0 (0x00007f0e97289000)
    libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x00007f0e92919000)
    libdl.so.2 => /lib/x86_64-linux-gnu/libdl.so.2 (0x00007f0e97284000)
    libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x00007f0e926f1000)
    /lib64/ld-linux-x86-64.so.2 (0x00007f0e97324000)

The error message is not informative, so I have no clue what to do. All other things I test (elpi, coq-hammer with z3, ...) work on snap.

Any idea?

Paolo Giarrusso (Sep 29 2022 at 12:50):

Could using strace and looking for open help? I also thought of ltrace and dlopen, but probably that's not the backend being used

Paolo Giarrusso (Sep 29 2022 at 12:51):

(sorry if it's just noise, and feel free to ignore)

Emilio Jesús Gallego Arias (Sep 29 2022 at 14:19):

It looks like it couldn't find COQLIB

Emilio Jesús Gallego Arias (Sep 29 2022 at 14:19):

exception printing....

Emilio Jesús Gallego Arias (Sep 29 2022 at 14:20):

Likely it says UnMappedLibrary(0, Coq.Init.Prelude)

Enrico Tassi (Sep 29 2022 at 14:24):

hum, is sertop is started as all other apps (eg via the wrapper)?

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

@Enrico Tassi : I didn't start it via the wrapper. Actually everything also works without the wrapper directly started from the bin folder (including elpi). Just sertop doesn't.

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

@Emilio Jesús Gallego Arias : I will try setting COQLIB.

Emilio Jesús Gallego Arias (Sep 29 2022 at 19:43):

you can also pass --coqlib option

Emilio Jesús Gallego Arias (Sep 29 2022 at 19:43):

tho sertop will look where Coq was configured

Emilio Jesús Gallego Arias (Sep 29 2022 at 19:43):

Can you patch it / pull from a branch? I can try to fix the exn printer

Enrico Tassi (Sep 29 2022 at 19:44):

doesn't sertop use Coq's initialization code? There is a lot of code to try to find a value for "coqlib".

Emilio Jesús Gallego Arias (Sep 29 2022 at 19:53):

No, it does not use Coq's code

Michael Soegtrop (Sep 30 2022 at 07:30):

Emilio Jesús Gallego Arias said:

No, it does not use Coq's code

I guess this is the root cause then - I guess not many people used sertop in a relocated installation. When I started to make installers for Coq, quite a bit of effort went into making Coq installations path relocatable.

But I think it is not a problem for 2022.09 as long as we document the issue and a work around.

@Emilio Jesús Gallego Arias : yes I can easily work with patches or pull from a branch - just send me the patch file or what should go into the source section of the opam file.

Théo Zimmermann (Sep 30 2022 at 08:49):

Why not use the wrapper?

Michael Soegtrop (Sep 30 2022 at 09:33):

The wrapper is only applied to the predefined apps. I would like to achieve that one also can use coq by simply setting the PATH to the corresponding snap bin folder. It is not that convenient to use the wrapper "manually".

Michael Soegtrop (Sep 30 2022 at 12:07):

@Emilio Jesús Gallego Arias : I tried exporting COQLIB and calling sertop --coqlib=$COQLIB. The first does not work, the latter does work.

I will document that this is so, but would appreciate if sertop would use the same mechanisms as Coq does to find the coq library.

Emilio Jesús Gallego Arias (Oct 01 2022 at 08:29):

I will take time for sertop to use Coq mechanisms, sertop init setup is way older than the new sysinit in Coq

Emilio Jesús Gallego Arias (Oct 01 2022 at 08:29):

and not exactly compatible, as it uses a different design philosophy

Emilio Jesús Gallego Arias (Oct 01 2022 at 08:30):

It was my hope that we could have upstreamed it (as with some other many improvements that first landed in SerAPI) but in the end we didn't coordiante and a different effort landed.

Michael Soegtrop (Oct 01 2022 at 10:53):

@Emilio Jesús Gallego Arias : I think long term it is worth the effort to share the init code - it is a lot of work to test such post install system dependent behavior, since for each test one has to create a (signed) installer and install it - separately for 3 platforms.

Emilio Jesús Gallego Arias (Oct 01 2022 at 12:17):

Sure

Michael Soegtrop (Oct 07 2022 at 09:20):

@Emilio Jesús Gallego Arias : I find it quite unfortunate that sertop does not honor the COQLIB environment variable - in an installed / relocated environment one must always use --coqlib. Any chance to fix this for the non beta release in 2 weeks?

Emilio Jesús Gallego Arias (Oct 07 2022 at 12:37):

Sure, we can fix that. Where is the documentation for the current relocation system for Coq?

Michael Soegtrop (Oct 07 2022 at 13:10):

@Emilio Jesús Gallego Arias : I don't know much about how coqc finds the Coq library - Afaik @Enrico Tassi is the expert here.

Ocamlfind should work out of the box. I patched it is as follows:

• search folders upwards from the folder of the current executable until a folder with an (empty) file findlib.root is found or / is reached
• search paths compiled into executables (say for META files) are given relative to this path
• when creating installers, exists_if lines are deleted from META files - they usually refer to static libraries (.cma) files which are not installed

With this sertop works fine on all platforms, except that I need to give --coqlib=$(coqc -where) or equivalent.

See (https://github.com/coq/platform/tree/main/opam/opam-repository/packages/ocamlfind/ocamlfind.1.9.5%7Erelocatable) for the ocamlfind patch (reviews welcome).

Enrico Tassi (Oct 07 2022 at 13:29):

Can't you just use Coq sysinit component to initialize coq? That component should honor COQLIB, but more importantly, will make setop always initialize Coq as coqtop/coqc/... does.

Emilio Jesús Gallego Arias (Oct 07 2022 at 13:49):

I could use sysinit but that will require time to port SerAPI to sysinit. In fact serinit was written after my suggestion to follow the approach that sertop has been doing since a while, but sadly the code is not compatible.

Emilio Jesús Gallego Arias (Oct 07 2022 at 13:49):

sertop / jscoq / etc... have been using their own sysinit since they were written, at the time there was not sysinit I could use

Michael Soegtrop (Oct 07 2022 at 14:31):

Does sertop support another env var to set the path to the Coq library?

Emilio Jesús Gallego Arias (Oct 07 2022 at 14:38):

No, if the cmdline argument is not set, it uses what was given in configure

Emilio Jesús Gallego Arias (Oct 07 2022 at 14:39):

I am not sure Coq should support tho different values of install than the ones given at configure

Emilio Jesús Gallego Arias (Oct 07 2022 at 14:39):

at least not without futher cleanup of the way we handle the env

Emilio Jesús Gallego Arias (Oct 07 2022 at 14:40):

It is fine to honor COQLIB, but the whole setup doesn't seem robust / maintenable to me

Emilio Jesús Gallego Arias (Oct 07 2022 at 14:52):

To be relocatable a lot of design decisions need to be deterimed, how to find files in that, precedence of files, etc...

Emilio Jesús Gallego Arias (Oct 07 2022 at 14:53):

Ad-hoc setup on this is bad

Théo Zimmermann (Oct 07 2022 at 14:56):

Well, we already rely on this property to get binary installers that were built with opam but do not need opam at run time.

Michael Soegtrop (Oct 07 2022 at 15:19):

@Emilio Jesús Gallego Arias : all binary installers (macOS, Windows, Ubuntu snap) move the binaries and libraries into different folders as they have been compiled in. For macOS this folder is fixed (unless the user renames it manually), for Windows and snap it is unknown at compile time. On Windows it is arbitrary (users choice) and on snap it contains a system dependent version number, which is updated each time you update snap. It does not depend on how many updates I upload to snap, but on how many updates the user downloads from snap.

There is not much we can do about this. I find the "findlib.root" method reasonably robust and efficient and think we could use it for Coq as well.

In any case I think there should be a way to set this via environment variables.

Emilio Jesús Gallego Arias (Oct 07 2022 at 15:25):

https://github.com/ejgallego/coq-serapi/pull/281 should have the ser* family of functions to recognize coqlib

Emilio Jesús Gallego Arias (Oct 07 2022 at 15:27):

Michael Soegtrop said:

Emilio Jesús Gallego Arias : all binary installers (macOS, Windows, Ubuntu snap) move the binaries and libraries into different folders as they have been compiled in. For macOS this folder is fixed (unless the user renames it manually), for Windows and snap it is unknown at compile time. On Windows it is arbitrary (users choice) and on snap it contains a system dependent version number, which is updated each time you update snap. It does not depend on how many updates I upload to snap, but on how many updates the user downloads from snap.

There is not much we can do about this. I find the "findlib.root" method reasonably robust and efficient and think we could use it for Coq as well.

In any case I think there should be a way to set this via environment variables.

Indeed that's a problem for windows and snap, and indeed I'm happy if we adopt an official solution for this coming from upstream. It is a losing battle for us to try to make OCaml binaries relocatable if this is not supported upstream.

Note that the folder that is passed to configure is not the compile folder but the _install_ folder.

Emilio Jesús Gallego Arias (Oct 07 2022 at 15:27):

I introduced the boot library to the purpose of indeed have a file-system access and resolution in Coq in a central place, which is the first step.

Emilio Jesús Gallego Arias (Oct 07 2022 at 15:28):

but quite a lot of work is still needed, right now there is a mess here

Emilio Jesús Gallego Arias (Oct 07 2022 at 15:28):

so I can't support investing time in solutions that are not principled, Coq has been suffering the problem of adding half-baked, non principled solutions for a long time (which is normal due to the research nature of the software), but we got to stop doing this

Emilio Jesús Gallego Arias (Oct 07 2022 at 15:29):

Boot.Env does provide a principled API start

Michael Soegtrop (Oct 07 2022 at 16:55):

@Emilio Jesús Gallego Arias : I am having discussions with the OCaml team from time to time about this, but it is hard to get something done. I would say Coq is by far the biggest user of OCaml relocation, so I guess we need to explore solutions and push them upstream.

Emilio Jesús Gallego Arias (Oct 07 2022 at 17:26):

how does opam-bin work?

Michael Soegtrop (Oct 07 2022 at 17:44):

I don't think opam-bin helps us. We want native installers for macOS, Windows and Snap.

Emilio Jesús Gallego Arias (Oct 07 2022 at 18:00):

I was under the impression that doing such things was on their roadmap, anyways the maintain a set of patches to make stuff relocatable

Michael Soegtrop (Oct 07 2022 at 18:14):

I can't derive this from their documentation. As far as I understand this, it is a method to extend opam in such a way that one does not need to compile things from sources, but instead download precompiled packages.
I looked at their relocation patches, but they still assume some opam switch directory structure and opam infrastructure, which we don't have in installers.

Michael Soegtrop (Oct 07 2022 at 18:14):

Of course opam-bin might be a reasonable thing to support from us - compiling Coq stuff again and again is producing CO2, but this is a different story.

Michael Soegtrop (Oct 07 2022 at 18:15):

As far as I can tell Coq Platform is currently the most advanced and flexible way to create system independent installers from opam switches.

Emilio Jesús Gallego Arias (Oct 10 2022 at 13:56):

@Michael Soegtrop the new serapi version should be merged to the opam repos today

Michael Soegtrop (Oct 10 2022 at 14:18):

@Emilio Jesús Gallego Arias : perfect, thanks! It will be too late for the 2022.09 beta, but I will update it in the release (ETA 2 weeks).

Last updated: Jun 03 2023 at 03:01 UTC