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
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.
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?
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?
In any case I'm not very fond of the current code to initialize paths:
Indeed I am using PG
Imo the "." is what makes it work for me... so I guess PG changes directory to where the .v file is
Not so sure what to suggest, other than I'm happy to merge any patch that makes this work ;-)
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?
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
Let me look at the API of Coq
I see. Indeed, "relative to the physical path of the .v file" would work for our use-case
A quick ugly hack seems to be:
Let me try that out locally and see if I can get it working :~)
Then we can think at a better solution, I can't find a way to know the path of the current file being checked
sorry, even without the
elpi/ part should work, since there is a
Concretely I actually have the following directory structure:
foo |- bar |- elpi |- baz.v |- baz.elpi
To be clear, your suggestion is to include
COQPATH and then
Elpi Accumulate File "./elpi/baz.elpi" from within
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)?
try to use $PWD in COQPATH
I like your suggestion
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?
I can try it out tomorrow probably, but please open an issue.
I have a meeting but I'll open that issue in about an hour
But so right now everything works _except_ stepping over
Elpi Accumulate File in proof general?
It seems like that's the case, but I need to investigate a bit more after our meeting
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.
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 .
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.
(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)
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
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.
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
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.
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