Stream: Elpi users & devs

Topic: `Elpi Accumulate File` and Coq's `LoadPath`


view this post on Zulip Jasper Haag (Feb 01 2022 at 13:43):

Is Coq's LoadPath related to the way in which Elpi Accumulate File functions? More generally, what is the appropriate way to Elpi Accumuluate Files from within a local project? I have the following directory structure:

foo
|- bar
   |- baz
      |- qux.v
      |- qux.elpi

and foo.bar.baz is a logical path in my Coq LoadPath with the appropriate physical path, but I can't seem to get the semantics "accumulate qux.elpi from the physical path for foo.bar.baz". In particular, stepping over Elpi Accumulate File "qux.elpi" from within qux.v succeeds, but invoking a build of this file from a containing folder of foo causes a failure.

view this post on Zulip Jasper Haag (Feb 01 2022 at 14:08):

Using Elpi Accumulate File "./a/b/c/foo/bar/baz/qux.elpi". from within qux.v succeeds when the build is invoked from the directory a but fails when attempting to step through qux.v, so I guess local-paths are interpreted relative to where the command was invoked?

If this is indeed the case, what should I do to support Elpi Accumulate File commands which need to be run in CI and by local developers?

view this post on Zulip Enrico Tassi (Feb 01 2022 at 15:34):

Hum, the path is relative to the root of the project. That works fine with vscoq and coq_makefile. I did not test proof general, maybe that is what you are using?

view this post on Zulip Enrico Tassi (Feb 01 2022 at 15:34):

In any case I'm not very fond of the current code to initialize paths:
https://github.com/LPCIC/coq-elpi/blob/master/src/coq_elpi_vernacular.ml#L180

view this post on Zulip Jasper Haag (Feb 01 2022 at 15:35):

Indeed I am using PG

view this post on Zulip Enrico Tassi (Feb 01 2022 at 15:35):

Imo the "." is what makes it work for me... so I guess PG changes directory to where the .v file is

view this post on Zulip Enrico Tassi (Feb 01 2022 at 15:36):

Not so sure what to suggest, other than I'm happy to merge any patch that makes this work ;-)

view this post on Zulip Jasper Haag (Feb 01 2022 at 15:37):

This is going to be problematic given our CI setup; in CI, we copy some files to a different path than what developers use locally, and that seems like it will break any Elpi Accumulate File clauses.

Do you think it would be reasonable to look in the LoadPath? I haven't done much ml hacking; what do you think something like that might entail?

view this post on Zulip Enrico Tassi (Feb 01 2022 at 15:37):

probably the most robust solution would be to be relative to the path of the .v file, but I'm not so sure I have it at hand

view this post on Zulip Enrico Tassi (Feb 01 2022 at 15:38):

Let me look at the API of Coq

view this post on Zulip Jasper Haag (Feb 01 2022 at 15:38):

I see. Indeed, "relative to the physical path of the .v file" would work for our use-case

view this post on Zulip Enrico Tassi (Feb 01 2022 at 15:46):

A quick ugly hack seems to be:

view this post on Zulip Jasper Haag (Feb 01 2022 at 15:47):

Let me try that out locally and see if I can get it working :~)

view this post on Zulip Enrico Tassi (Feb 01 2022 at 15:47):

Then we can think at a better solution, I can't find a way to know the path of the current file being checked

view this post on Zulip Jasper Haag (Feb 01 2022 at 15:47):

Gotcha

view this post on Zulip Enrico Tassi (Feb 01 2022 at 15:47):

sorry, even without the elpi/ part should work, since there is a ..

view this post on Zulip Enrico Tassi (Feb 01 2022 at 15:48):

I mean foo/elpi and COQPATH=foo

view this post on Zulip Jasper Haag (Feb 01 2022 at 16:00):

Concretely I actually have the following directory structure:

foo
|- bar
   |- elpi
      |- baz.v
      |- baz.elpi

To be clear, your suggestion is to include foo/bar in COQPATH and then Elpi Accumulate File "./elpi/baz.elpi" from within baz.v?

Presuming that is indeed your suggestion, I can report that it did not seem to work for me:

a$ COQPATH=b/c/d/foo/bar/ ./MYBUILD.py b/c/d/foo/bar/elpi/baz.v
...
Error:
File ./elpi/baz.elpi not found in: ., ./., ....../lib/elpi, ./., ./.., ............./uers-contrib/elpi

view this post on Zulip Jasper Haag (Feb 01 2022 at 16:09):

Regarding a potential "better way", could we make use of this part of the coq api to filter for physical paths which result in the same logical path as the one specified by the person invoking the command (i.e. Elpi Accumulate File "qux.elpi" From foo.bar.baz)?

view this post on Zulip Enrico Tassi (Feb 01 2022 at 16:38):

try to use $PWD in COQPATH

view this post on Zulip Enrico Tassi (Feb 01 2022 at 16:39):

I like your suggestion

view this post on Zulip Jasper Haag (Feb 01 2022 at 16:45):

D'oh, of course PWD is needed. This works locally so I can probably get something that works in CI and for individual developers. However, it is not very ergonomic; do you anticipate this change being quick, and should I take a stab at cutting an MR with the suggested changes?

view this post on Zulip Enrico Tassi (Feb 01 2022 at 16:49):

I can try it out tomorrow probably, but please open an issue.

view this post on Zulip Jasper Haag (Feb 01 2022 at 16:50):

I have a meeting but I'll open that issue in about an hour

view this post on Zulip Paolo Giarrusso (Feb 01 2022 at 16:52):

But so right now everything works _except_ stepping over Elpi Accumulate File in proof general?

view this post on Zulip Jasper Haag (Feb 01 2022 at 16:53):

It seems like that's the case, but I need to investigate a bit more after our meeting

view this post on Zulip Jasper Haag (Feb 01 2022 at 18:40):

https://github.com/LPCIC/coq-elpi/issues/336

view this post on Zulip Jasper Haag (Feb 01 2022 at 18:46):

Regarding Paolo's question, our CI setup actually does build things at a location which differs from that which developers use locally. Given that a temporary workaround using COQPATH would necessitate some annoying CI changes or local-development changes, we'll probably avoid using Elpi Accumulate File for now. This shouldn't be too onerous since we don't have very much elpi code which we want to share currently.

Would an eventual patch which adds more useful semantics for Elpi Accumulate File only end up in the 8.15-compatible version of elpi or would it be possible to also provide support for this in an 8.13 compatible version? We are currently blocked on an internal 8.15 bump due to some performance regressions that arose on our end and it is not clear when those will be resolved.

view this post on Zulip Enrico Tassi (Feb 01 2022 at 18:53):

Hum, I'm not super into making a release for 8.13... also I believe COQPATH works on 8.13 too. I'm happy to work on something for 8.15.

May I suggest another hack?

ln -s foo/bar/file.elpi .

and then foo/bar/file.v do Accumulate File "file.elpi".
This should work on vscode/coqc via the symlink, and also on emacs. (Or maybe do the symlink the other way around, depending on what is considered better).

Do you have windows devs? If not the hack may work.

view this post on Zulip Enrico Tassi (Feb 01 2022 at 18:56):

(I totally understand the pain you may have migrating to the new version of Coq, but I don't have the energy to make a release for Coq $V-2, sorry)

view this post on Zulip Jasper Haag (Feb 01 2022 at 19:36):

Re the 8.13 release: absolutely understood :~) I appreciate you taking the time out of your schedule to work on this feature in the first place!

I also appreciate the further suggestions regarding how we can mitigate this issue while retaining the use of Elpi Accumulate File in 8.13. Depending on how long our internal bump takes, we may end up implementing some of these strategies; in the near term will likely stick with (minor) code duplication in order to avoid build-changes

view this post on Zulip Jasper Haag (Feb 01 2022 at 19:40):

And to be clear, COQPATH does work locally/in CI. It's just that the necessary COQPATHs in these two use-cases are different, and changes to CI and/or local development workflows are not a positive value proposition given the other things we have on our plates at the moment.

view this post on Zulip Paolo Giarrusso (Feb 03 2022 at 12:32):

because of https://coq.zulipchat.com/#narrow/stream/253928-Elpi-users.20.26.20devs/topic/elpi.20and.20coqdep, the symlink doesn't work acceptably on dune (except via hacks involving Ctrl-C).

view this post on Zulip Paolo Giarrusso (Feb 03 2022 at 12:33):

and I expect COQPATH doesn't work too reliably locally either, except for the very constrained case you run a separate Emacs or VSCode inside a shell where you set the right one.

view this post on Zulip Enrico Tassi (Feb 03 2022 at 13:07):

I've implemented the loadpath proposal, I'm just cleaning the API (on the elpi side) then I shall open a PR on coq-elpi.


Last updated: Feb 04 2023 at 01:03 UTC