Always resolve files using Coq

[rlepigre]

In this proposal, the resolution is always done in the following way:

• If the give file path is absolute, keep it.
• Remove leading coq:// if present, for backward compatibility. I don't think it is useful anymore.
• Split the file name into two parts: a logical path (before the first /), and a remaining relative path.
  • Resolve the logical path using Coq, and turn it into a physical part.
  • Return the concatenation of the physical part and the relative path.

Example: if directory theory/dir is mapped to logical path my.project, then my.project/rest/of/path.elpi is mapped to theory/dir/rest_of_path.elpi. You get the same result if you use accumulate "my.project/rest/of/path". in an elpi file (note the absence of a .elpi extension in the string).

Note: this also removes the dune-workspace file, which I don't think should be there.

[gares]

It makes sense, but the failure in HB seems to signals that this patch wants dune as a build system and dune needs to understand the extra sources.

[rlepigre]

I'm not sure how this is specific to dune: independently of what build system you rely on, shouldn't the situation be the same? I mean, both make and dune rely on the compiler being passed -Q/-R, so the resolution should happen in the same way. Am I missing something here?

[rlepigre]

After some investigation, it seems to me that the issue for HB is that the HB folder is not mapped. Adding HB/ to all the paths to elpi files seems to fix the issue. Another approach would probably be to change -Q . HB into -Q HB HB and to move structures.v into the HB folder.

[gares]

ok, then there was an implicit ./ I guess... I'll look again at your code later today

[rlepigre]

Cool, thanks. I pushed what I have for HB here: https://github.com/rlepigre/hierarchy-builder/tree/new_elpi_resolver.

[gares]

Would you mind keeping a symlink to structures.v in the root for the sake of ci?

[rlepigre]

Would you mind keeping a symlink to structures.v in the root for the sake of ci?

Sure, I pushed a fix to my HB branch.

[rlepigre]

Another issue I have identified, but am not sure how to fix, is with the Elpi Print name "path/to/file". command. The involved code is here, and it basically treats "path/to/file" as a relative path from the current working directory. In a workspace build that cannot work, as coqc will be invoked from the workspace root, which is not necessarily the root of the coq-elpi repository. I'm not sure how to fix this in a satisfactory way though. Any idea @gares?

[rlepigre]

I guess one approach would be to again rely on the Coq to resolve a directory path, given as first member of the path.

[gares]

I guess one approach would be to again rely on the Coq to resolve a directory path, given as first member of the path.

That makes sense and also fix the ugly issue I have on proof general, since it runs coqtop from the directory where the .v file is, making Print behave differently depending your UI...

[rlepigre]

I guess one approach would be to again rely on the Coq to resolve a directory path, given as first member of the path.

That makes sense and also fix the ugly issue I have on proof general, since it runs coqtop from the directory where the .v file is, making Print behave differently depending your UI...

This should now be fixed, but I had to make the file argument of Elpi Print mandatory, which seems reasonable to me. Something we could do alternatively, if it is not given, is write to a temporary file and report its name with a user message, but I don't know that it is worth it.

[rlepigre]

@gares I confirmed that this MR makes it possible for us to use both elpi and coq-elpi as part of our dune workspace build, so we have started using it on our side. I'd be happy to push this MR through, but I'll need some guidance regarding what downstream projects need fixing, and how to test these fixes in CI. Do you use some kind of overlay mechanism like in the Coq repo?

[gares]

no, I add a commit that thinkers with the nix configuration, and then remove it before merging.

About HB, I think some fixes were merged in nix upstream, so https://github.com/math-comp/hierarchy-builder/pull/444/ should work. I'll try updating it.

[gares]

I can merge it. I let you have a look at the minor points above and possibly add a line to the Changelog file

[rlepigre]

Thanks @gares! I addressed the comments, and added a changelog entry.

[gares]

Thanks!

[FissoreD]

Hello, If I run make in master and try to interpret with vsCoq2 the following line: https://github.com/LPCIC/coq-elpi/blob/5aa6a283312f38bec6c018e7e491b80c2738bf6b/tests/test_link_order1.v#L27 I get this error message:

No loadpath found with logical name elpi.tests, cannot resolve file reference elpi.tests/test_link_order1.

And if I interpret this: https://github.com/LPCIC/coq-elpi/blob/5aa6a283312f38bec6c018e7e491b80c2738bf6b/apps/tc/examples/tutorial.v#L58

I get:

Multiple loadpaths found with logical name elpi.apps.tc.examples, while resolving file reference elpi.apps.tc.examples/TC.Solver:
- elpi.apps.tc.examples -> /home/dfissore/.../ce-master/apps/tc/examples
- elpi.apps.tc.examples -> /home/dfissore/.../ce-master/_build/default/apps/tc/examples

Am I missing something?

[gares]

I suspect the _CoqProject file contains 2 mappings for elpi.apps.tc.examples.