Jasper Haag (Feb 01 2022 at 13:43): 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.
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?
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?
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
Jasper Haag (Feb 01 2022 at 15:35):Indeed I am using PG
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
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 ;-)
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?
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
Enrico Tassi (Feb 01 2022 at 15:38):Let me look at the API of Coq
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
Enrico Tassi (Feb 01 2022 at 15:46):A quick ugly hack seems to be:
Jasper Haag (Feb 01 2022 at 15:47):Let me try that out locally and see if I can get it working :~)
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
Jasper Haag (Feb 01 2022 at 15:47):Gotcha
Enrico Tassi (Feb 01 2022 at 15:47):sorry, even without the elpi/ part should work, since there is a ..
Enrico Tassi (Feb 01 2022 at 15:48):I mean foo/elpi and COQPATH=foo
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
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)?
Enrico Tassi (Feb 01 2022 at 16:38):try to use $PWD in COQPATH
Enrico Tassi (Feb 01 2022 at 16:39):I like your suggestion
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?
Enrico Tassi (Feb 01 2022 at 16:49):I can try it out tomorrow probably, but please open an issue.
Jasper Haag (Feb 01 2022 at 16:50):I have a meeting but I'll open that issue in about an hour
Paolo Giarrusso (Feb 01 2022 at 16:52):But so right now everything works _except_ stepping over Elpi Accumulate File in proof general?
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
Jasper Haag (Feb 01 2022 at 18:40):https://github.com/LPCIC/coq-elpi/issues/336
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.
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.
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)
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
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.
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).
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.
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: Oct 13 2024 at 01:02 UTC