Karl Palmskog (Jan 16 2023 at 14:41): Karl Palmskog (Jan 16 2023 at 14:41):The Coq Platform 2021.09.1 release notes contains this note:
Note on Serapi: The SerAPI executables like sertop require a --coqlib=${coqc -where} or similar option. The COQLIB environment variable is not used.
Can we make the programs like sertop respect COQLIB @Emilio Jesús Gallego Arias? I see something similar was done about COQPATH before (https://github.com/ejgallego/coq-serapi/issues/221).
Karl Palmskog (Jan 16 2023 at 14:43):background: the Coq Platform tries to make everything relocatable, since things like Snap Coq resides in non-standard locations.
Emilio Jesús Gallego Arias (Jan 16 2023 at 23:00):Sure, is there an issue open about it?
Karl Palmskog (Jan 16 2023 at 23:01):well, I was going to check before I create one, but I can do it tomorrow.
Emilio Jesús Gallego Arias (Jan 16 2023 at 23:09):Yes please create one and put in the 0.17 milestone, so we don't forget to fix this before the release.
Karl Palmskog (Jan 17 2023 at 08:15):@Michael Soegtrop I just tried reproducing the sertop+COQLIB issue you wrote about in the Platform release notes, and I'm not able to do this. Consider the following example, where I installed coq-serapi for 8.16 on OCaml 4.14.1, but call it with COQLIB for 8.16+4.11:
$ sertop --version
8.16.0+0.16.1
$ sertop
(Feedback((doc_id 0)(span_id 0)(route 0)(contents(FileLoaded Coq.Init.Prelude /path/to/.opam/4.14.1+flambda+coq.8.16/lib/coq/theories/Init/Prelude.vo))))
...
$ sertop --coqlib=/path/to/.opam/4.11+flambda+coq.8.16/lib/coq
sertop: internal error, uncaught exception:
(CErrors.UserError
( "The file /path/to/.opam/4.11+flambda+coq.8.16/lib/coq/theories/Init/Prelude.vo was compiled with OCaml\
\n4.11.1 while this instance of Coq was compiled with OCaml 4.14.1.\
\nCoq object files need to be compiled with the same OCaml toolchain to be compatible."))
$ COQLIB=/path/to/.opam/4.11+flambda+coq.8.16/lib/coq sertop
sertop: internal error, uncaught exception:
(CErrors.UserError
( "The file /path/to/.opam/4.11+flambda+coq.8.16/lib/coq/theories/Init/Prelude.vo was compiled with OCaml\
\n4.11.1 while this instance of Coq was compiled with OCaml 4.14.1.\
\nCoq object files need to be compiled with the same OCaml toolchain to be compatible."))
is COQLIB getting overwritten somewhere maybe? Because from what I can tell, sertop has no problems with it.
Michael Soegtrop (Jan 17 2023 at 08:26):Well maybe it is fixed meanwhile. As I said I discussed this to some length with @Emilio Jesús Gallego Arias and the conclusion was that SerTop does not use COQLIB. Let me test an installed version ...
Michael Soegtrop (Jan 17 2023 at 08:58):@Karl Palmskog : I think it has been fixed from 0.16.0 to 0.16.1 - in 0.16.0 it definitely does not work.
I am still in the progress of testing 0.16.1 - apparently the code signing for the Mac installers got messed up - the signatures are there but my Mac doesn't seem to accept them.
Karl Palmskog (Jan 17 2023 at 08:59):OK, that's good then, I'd consider the issue resolved. But we can double check for the release of SerAPI for 8.17.
Michael Soegtrop (Jan 17 2023 at 09:25):Indeed in the 2022.09.1 release it does work - if one uses one of the supplied shell starters which set COQLIB, sertop does work (it did not in the beta). What still does not work is that it detects the library path automatically from the binary location as all other coq tools do.
Michael Soegtrop (Jan 17 2023 at 09:26):I will adjust the ReadME.
Michael Soegtrop (Jan 17 2023 at 09:29):@Karl Palmskog : I updated the readme notes on SerAPI - can you please check?
Karl Palmskog (Jan 17 2023 at 09:33):looks good to me, but do you mean sertop should use the location of programs in the PATH to determine parameters?
Michael Soegtrop (Jan 17 2023 at 09:36):@Karl Palmskog : the other coq tools use their own binary path and check if they can find the Coq library at well defined relative locations to it. They also read an environment file which is in the same folder as the binary.
Michael Soegtrop (Jan 17 2023 at 09:38):So even when relocated they don't need any environment variables. Well at least this is the goal - CoqIDE needs some GTK related environment variables and a wrapper exe to set these on MacOS. One should also set these via the environment file, but this is not supported yet.
Michael Soegtrop (Jan 17 2023 at 09:41):In Coq Platform, Ocamlfind is patched to use a similar mechanism to find the ocaml libraries. Essentially it inspects the executables binary directory (can also be a shared library) and walks in parent direction until it finds a marker file or root. This is taken as installation root and the ocamlfind folder is defined relative to it. One should probably use this mechanism for everything.
Michael Soegtrop (Jan 17 2023 at 09:42): Karl Palmskog (Jan 17 2023 at 09:47):OK, I'll have to defer to @Emilio Jesús Gallego Arias whether this is feasible to do for the SerAPI tools.
Karl Palmskog (Jan 17 2023 at 09:48):but I'd consider that a new feature (compared to COQLIB, which is conventional)
Michael Soegtrop (Jan 17 2023 at 10:01):It would be good to have a consistent mechanism for all Coq tools ...
Karl Palmskog (Jan 17 2023 at 10:03):the question would be what you consider a Coq tool. It's unlikely that tools like sertop would move into the Coq repo. And the ecosystem with non-repo Coq-related tools like Alectryon is growing.
Michael Soegtrop (Jan 17 2023 at 10:16):IMHO every tool which accesses the Coq library should use a consistent mechanism to find it. Also other system adjustment settings should be managed in a consistent way. Possibly Coq should provide a library for this.
Emilio Jesús Gallego Arias (Jan 17 2023 at 10:54):Indeed the changelog says it was fixed in 0.16.1
Emilio Jesús Gallego Arias (Jan 17 2023 at 10:54):So that's a non-issue
Emilio Jesús Gallego Arias (Jan 17 2023 at 10:55):I'm unsure what you mean about "detects the library path automatically", if you set COQLIB, then no detection is going to happen.
To locate OCaml libraries, sertop and (coq-lsp) use ocamlfind
Michael Soegtrop (Jan 17 2023 at 11:03):@Emilio Jesús Gallego Arias : What I mean is that coqc works relocated without setting COQLIB - sertop doesn't. It is quie inconvenient to have to set COQLIB, especially if one works with different versions of Coq. But also beginners have issues with this (and there are beginners which want to use sertop).
Emilio Jesús Gallego Arias (Jan 17 2023 at 11:05):Ah, I see thanks
Emilio Jesús Gallego Arias (Jan 17 2023 at 11:07):Are you using coq_enviroment.txt ?
Michael Soegtrop (Jan 17 2023 at 11:31):I must admit I am not 100% sure how it works. I think it uses these paths in order of priority:
@Enrico Tassi is the expert. Which mechanism is used depends on the operating system - possibly for historic reasons. E.g. the Windows installer does create coq_environment.txt, the MacOS installer doesn't. The command line and COQLIB methods are not use by Coq Platform to avoid extra complexity for users which need to set this for some reason.
What I did are the patches to ocamlfind, so I can explain how these work.
Michael Soegtrop (Jan 17 2023 at 11:32):My point is that this is not entirely trivial and users can reasonably expect that one does not have to reverse engineer this in case it doesn't work for each individual executable one uses.
Emilio Jesús Gallego Arias (Jan 19 2023 at 23:01):Thanks @Michael Soegtrop , I was wondering about what indeed you did in the platform, I'm suprised to find that you only set cqo_environment.txt in windows.
Emilio Jesús Gallego Arias (Jan 19 2023 at 23:01):How does the MacOS installer locate coqlib then?
Michael Soegtrop (Jan 20 2023 at 08:00):As far as I know coqc takes its own path, and looks in ../lib/coq and checks if this looks like a Coq library. A MacOS DMG installer can't change any files (unlike the Windows NSIS installer), so it can't create a path adjsuted coq_environment.txt file. For this reason - afair - Enrico implemented the bin relative mechanism.
IMHO it would make sense to clean this up a bit and use the mechanism I implemented in OCamlfind - that is go upwards in the folder tree from the folder of the binary until one finds a special marker file (or file system root) and take this as the installation root folder and determine all paths relative to this. The plain ../lib/coq mechanism used by coqc does not work for OCamlfind because it is also used by shared libraries which are stored not in bin.
Last updated: Jun 11 2023 at 01:30 UTC