Stream: SerAPI

Topic: Differences in loadpaths between coqtop and sertop

Alex Sanchez-Stern (Feb 17 2023 at 21:40):

Hey all. I know SerAPI is being deprecated, but I'm still working with it on some of my Coq projects that use Coq 8.10, and I've run into something weird. When building QuickChick for Coq 8.10 (https://github.com/QuickChick/QuickChick/tree/8.10), in the toplevel folder if I run coqtop with the flags from the _CoqProject, and run "Require Import QuickChickInterface.", it imports fine. However, if I open sertop instead, running the vernac statements that coorespond to the flags, and then run '(Add () "Require Import QuickChickInterface.")', it gives me an error that it couldn't find QuickChickInterface. I found that if I run '(Add () "Add LoadPath \".\".")', then it starts behaving like coqtop. Can someone explain this difference in behavior?

Paolo Giarrusso (Feb 17 2023 at 21:44):

QuickChickInterface is misplaced — it's not in src

Paolo Giarrusso (Feb 17 2023 at 21:45):

I'm no serapi user, but assuming serapi 8.10 won't get bugfixes, I'd try moving it into src

Alex Sanchez-Stern (Feb 17 2023 at 21:47):

Yeah but if it's in a place that Coq 8.10 doesn't support, then why does coqtop import it okay?

Paolo Giarrusso (Feb 17 2023 at 21:48):

Maybe Coq 8.10 does support it. But what quickchick is doing is so unusual that, even if that coqtop feature were documented, my first (naive) instinct is to consider deprecating it.

Alex Sanchez-Stern (Feb 17 2023 at 21:53):

Sure, I'm not a maintainer of QuickChick though, I don't have the power to change that file. I'm just trying to figure out why sertop and coqtop have such different behavior about imports.

Gaëtan Gilbert (Feb 17 2023 at 22:14):

I don't know what serapi does but coqtop/coqc add the current directory to the known paths
sort of like -Q . "" but without recursing into subdirectories IIUC

Paolo Giarrusso (Feb 17 2023 at 22:15):

and that seems to be done not in "core" Coq but in the "driver"?
https://github.com/coq/coq/blob/v8.16/sysinit/coqloadpath.ml#L74
https://github.com/coq/coq/blob/v8.16/checker/checker.ml#L128

Gaëtan Gilbert (Feb 17 2023 at 22:16):

what is "driver"?

Paolo Giarrusso (Feb 17 2023 at 22:17):

code that can differ between the different "top-level" binaries

Alex Sanchez-Stern (Feb 17 2023 at 22:20):

I thought -Q didn't recurse into subdirectories, that's what -R does. So it sounds like maybe putting Add LoadPath ".". at the top of every file would make them behave the same?

Paolo Giarrusso (Feb 17 2023 at 22:21):

-Q directory_path logical_path maps the entire tree rooted in directory_path to logical_path _and subtrees_

Alex Sanchez-Stern (Feb 17 2023 at 22:22):

Then what does "-R" do? My understanding was that -Q was "Add LoadPath" and -R was "Add Rec LoadPath"

Paolo Giarrusso (Feb 17 2023 at 22:28):

They are documented as equivalent (https://coq.inria.fr/refman/proof-engine/vernacular-commands.html#coq:cmd.Add-LoadPath), but the semantics is tricky.

if you had -Q theories QuickChick or respectively -R theories QuickChick, then theories/foo/bar.v is available in both cases, but with -Q, its logical path is only QuickChick.foo.bar — so Require QuickChick.foo.bar works but Require foo.bar fails. With -R, using Require foo.bar will also work.

Paolo Giarrusso (Feb 17 2023 at 22:28):

and I'm now trying to understand if Require bar works as well in the 2nd case. EDIT: yes.

Gaëtan Gilbert (Feb 17 2023 at 22:33):

the logical path of theories/foo/bar doesn't change, the only difference between -R and -Q is that Require accepts any suffix for -R paths but requires a full path for -Q paths
From Require behaves the same for -R and -Q btw

Paolo Giarrusso (Feb 17 2023 at 22:37):

@Gaëtan Gilbert so adding the current directory via Add LoadPath "." behaves like -Q and does _not_ reproduce coqtop's built-in semantics, because -Q/Add LoadPath adds a subtree while . is only for files directly in the current folder?

Gaëtan Gilbert (Feb 17 2023 at 22:42):

yes

Alex Sanchez-Stern (Feb 17 2023 at 23:21):

Ahh hmm. So there's actually no way to reproduce coqtops behaviour in sertop?

Alex Sanchez-Stern (Feb 17 2023 at 23:24):

Though using Add LoadPath "." seems to work fine for this particular case

Paolo Giarrusso (Feb 17 2023 at 23:42):

Yeah, it just seems likely to add more ways to require other files... You can probably Require Import src.QuickChick...., but it doesn't seem to likely to cause problems on existing code

Emilio Jesús Gallego Arias (Feb 18 2023 at 14:26):

Indeed there are some differences, @Alex Sanchez-Stern I'd suggest opening a bug / PR, I'm happy to patch SerAPI 8.10 if you need it.

Emilio Jesús Gallego Arias (Feb 18 2023 at 14:26):

The history of why sertop / coqtop differ is actually quite long, and comes back to the first toplevel I implemented for jsCoq in 2015

Emilio Jesús Gallego Arias (Feb 18 2023 at 14:28):

Back in the day, as I was also building a set of packages to distribute with jsCoq, I thought it was a good idea to correct some weird behaviurs, in particular, use -Q for the stdlib, and remove the . implicit assignement, as anyways back in the day the virtual FS we used could not actually use readdir

Emilio Jesús Gallego Arias (Feb 18 2023 at 14:28):

Also back in the day there was nothing like the sysinit directory in Coq, so I had to rewrite the init code

Emilio Jesús Gallego Arias (Feb 18 2023 at 14:28):

SerAPI inherited these differences, and we never got the cycles to reconcile them.

Emilio Jesús Gallego Arias (Feb 18 2023 at 14:29):

coq-lsp also uses its own code, it has more capabilities than coq's own sysinit (for example we now support multiple _CoqProjects in a single process)

Emilio Jesús Gallego Arias (Feb 18 2023 at 14:29):

but it'd be great if we could reconcile them

Emilio Jesús Gallego Arias (Feb 18 2023 at 14:30):

but yeah it seems to me that manpower is lacking for that

Emilio Jesús Gallego Arias (Feb 18 2023 at 14:30):

There is some plans (jointly with @Ali Caglayan ) as to actually make library handling more uniform, which is IMHO a good thing, but that's being dicussed in the dune channel.

Emilio Jesús Gallego Arias (Feb 18 2023 at 14:32):

By the way even if we used the word "deprecated" for SerAPI, it is more accurate to say "in maintenance-only mode"

Emilio Jesús Gallego Arias (Feb 18 2023 at 14:33):

That is to say, no new feature requests are likely to be implemented, nor planned, but actually this has a very good reason, and it is because they can't be usually implemented properly using the Coq's APIs SerAPI uses

Emilio Jesús Gallego Arias (Feb 18 2023 at 14:34):

@Alex Sanchez-Stern to patch you problem you need to update this function:
https://github.com/ejgallego/coq-serapi/blob/v8.10/serapi/serapi_paths.ml#L23

Emilio Jesús Gallego Arias (Feb 18 2023 at 14:37):

to add to the list the corresponding path:

   { recursive = false;
      path_spec = VoPath { unix_path = ".";
                           coq_path = Libnames.default_root_prefix;
                           implicit = false;
                           has_ml = AddTopML }

Alex Sanchez-Stern (Feb 20 2023 at 18:50):

Okay, thanks! I probably don't need to make the patch for now, but if I run into more problems due to this on other projects I'll integrate the patch.

Alex Sanchez-Stern (Feb 21 2023 at 23:43):

I ended up running into more loadpath issues in building VST on coq 8.10, so I decided to make the patch you suggested (https://github.com/ejgallego/coq-serapi/compare/v8.10...loadpath-compatibility). However, that doesn't seem to make sertop behave fully like coqc/coqtop in terms of load paths, because I still can't build VST.

In the file compcert/flocq/Core/Core.v in VST (commit 84ede1cf708dd13b38dd4c3089ddf6f470c15093), there's a Require Export Raux that works fine in coqc, but fails with Unable to locate library Raux. in sertop. The module it's trying to import also exists in compcert/flocq/Core/, so it's probably pulling it in based on the local path of the compiled file. VST also uses -Q compcert/flocq compcert.flocq, so both the Core.v file that's failing and the Raux file it wants should be in the compcert.flocq module somewhere I think.

Emilio Jesús Gallego Arias (Feb 22 2023 at 01:00):

@Alex Sanchez-Stern seems to me that coq_makefile is using -R and sertop is being called with -Q ?

Alex Sanchez-Stern (Feb 22 2023 at 18:03):

Doesn't look like it from what I can see, the _CoqProject in that directory only uses -Q

Alex Sanchez-Stern (Feb 22 2023 at 18:30):

Ooh but it looks like there are special makefile targets for stuff within Compcert

Alex Sanchez-Stern (Feb 22 2023 at 18:37):

Oh it looks like the _CoqProject I was using isn't the original either, I didn't notice because it's gitignored.

Emilio Jesús Gallego Arias (Feb 22 2023 at 18:45):

Yeah that's such a pita, coq-lsp should hide all that away from users hopefully

Alex Sanchez-Stern (Feb 22 2023 at 18:45):

coq-lsp will replace Makefiles?

Emilio Jesús Gallego Arias (Feb 22 2023 at 19:04):

coq-lsp tries to guess how to build the projects, this is something I could have added to SerAPI, but I had to write the document manager first

Emilio Jesús Gallego Arias (Feb 22 2023 at 19:05):

so indeed, it should shield most of the pain from users I hope

Emilio Jesús Gallego Arias (Feb 22 2023 at 19:05):

still if there is some strange stuff it may not work, but indeed, coq-lsp is in the process of having full project build capability, as LSP requires

Emilio Jesús Gallego Arias (Feb 22 2023 at 19:06):

Actually I'd like to some very "fancy" things in terms of moving to a very different build model, but I'm limited by Coq API and the manpower / coordination to make that changes happen

Emilio Jesús Gallego Arias (Feb 22 2023 at 19:06):

But as of today for example, coq-lsp understands the structure of a project with mulitple _COqProjects

Emilio Jesús Gallego Arias (Feb 22 2023 at 19:06):

like metacoq

Emilio Jesús Gallego Arias (Feb 22 2023 at 19:07):

also it can save .vo files, so soon we will see auto-build

Alex Sanchez-Stern (Feb 22 2023 at 19:07):

Okay nice!

Last updated: Jun 10 2023 at 23:01 UTC