Rodolphe Lepigre (Sep 05 2024 at 11:54): Rodolphe Lepigre (Sep 05 2024 at 11:54):I am trying to set up a dune workspace where I'd like to include a checkout of both the elpi and coq-elpi repositories. Has anyone done that before? I am hitting the following issue:
File "./fmdeps/coq-elpi/theories/elpi.v", line 11, characters 0-47:
Error:
Anomaly
"Uncaught exception Failure("File elpi2html.elpi not found in: [...]")."
which seems to indicate that coq-elpi is unable to locate files provided by elpi. At first glance, I think I need to look into what is happening here, but before I do more digging I want to make sure I'm not missing something obvious.
Pierre Roux (Sep 05 2024 at 11:58):You can maybe take inspiration of math-comp's configuration https://github.com/math-comp/math-comp/blob/master/.nix/config.nix that uses the coq-nix-toolbox https://github.com/coq-community/coq-nix-toolbox
Rodolphe Lepigre (Sep 05 2024 at 11:59):Cool, thanks for the pointers!
Rodolphe Lepigre (Sep 05 2024 at 12:03):Actually, I'm not sure that's what I'm looking for, it seems more related to packaging rather than building several projects together. Or am I missing something?
Pierre Roux (Sep 05 2024 at 12:08):I don't know, you can probably explain what you want to do on #Nix and Coq Nix Toolbox devs & users to get more precise answers.
Rodolphe Lepigre (Sep 05 2024 at 12:15):Let me reformulate my question here (which is specifically about building coq_elpi): what I'd like to know is whether it is currently possible to build coq_elpi without having installed elpi, by building both together as part of a dune workspace. This might well not be currently supported due to the fact that this requires coq_elpi to know where to look for the elpi files, and it might only know how to look for the installed version (instead of local ones in the workspace).
Pierre Roux (Sep 05 2024 at 12:55):I'm not sure I understand precisely what you want to achieve. There is a Nix package in nixpkgs for coq-elpi (called coqPackages.coq-elpi) that has ocamlPackages.elpi as dependency. Do you want to use them or not and why so?
Enrico Tassi (Sep 05 2024 at 13:54):I never tried to compose the two projects in a single dune build.
The problem is minimal, elpi2html.elpi is distrbuted with elpi, but I'm fine just putting a copy in coq-elpi/elpi if that makes it easier to build the whole thing.
Enrico Tassi (Sep 05 2024 at 13:54):IIRC I pull a few hacks to actually load that file, so removing them is welcome.
Rodolphe Lepigre (Sep 05 2024 at 14:03):OK, thanks Enrico, I'll give this a try locally.
Rodolphe Lepigre (Sep 05 2024 at 14:04):Pierre Roux said:
I'm not sure I understand precisely what you want to achieve. There is a Nix package in nixpkgs for coq-elpi (called coqPackages.coq-elpi) that has ocamlPackages.elpi as dependency. Do you want to use them or not and why so?
No, I'm not interested in using nix packages, only in using the composition feature of dune.
Emilio Jesús Gallego Arias (Sep 05 2024 at 14:15):Hi @Rodolphe Lepigre happy to help with this if you need help.
Pierre Roux (Sep 05 2024 at 14:28):Sorry, I don't know why I misread dune for nix, so indeed, just ignore my comments.
Rodolphe Lepigre (Sep 05 2024 at 14:28):No worries!
Pierre Roux (Sep 05 2024 at 14:30):That being said, I'm still curious of your motivation.
Pierre Roux (Sep 05 2024 at 14:31):(but me knowing close to nothing about dune is probably why I don't get it)
Rodolphe Lepigre (Sep 05 2024 at 14:33):I actually found another issue trying to apply Enrico's suggestion. Even with just coq_elpi, if your dune workspace root is not the root of the coq_elpi repository then elpi files withing coq_elpi fail to be located correctly.
This can be reproduced by doing:
$ mkdir workspace && cd workspace
$ echo "(lang dune 3.8)" > dune-workspace
$ git clone git@github.com:LPCIC/coq-elpi.git
$ dune build
File "./coq-elpi/theories/elpi.v", line 12, characters 0-120:
Error:
Anomaly
"Uncaught exception Failure("File elpi/coq-lib-common.elpi not found in: [...]")."
Please report at http://coq.inria.fr/bugs/.
Raised at Elpi_util__Util.std_resolver.(fun) in file "src/utils/util.ml", line 652, characters 4-75
Called from Elpi_parser__Parse.Make.(fun) in file "src/parser/parse.ml", line 69, characters 17-50
[...]
I think the use case is the same for nix/toolbox, the bug is that somehow the "installation layout" is different in composition mode since elpi is not installed in ~/.opam but in _build/install and I guess I do something ugly
Rodolphe Lepigre (Sep 05 2024 at 14:34):Yeah, an environment variable probably needs to be read, I'll try to look into finding a fix later.
Enrico Tassi (Sep 05 2024 at 14:35):This is your enemy:
https://github.com/LPCIC/coq-elpi/blob/d6509831d6b85fd1905bf44e1f7eab45b22ae5bf/src/coq_elpi_programs.ml#L635-L693
Rodolphe Lepigre (Sep 05 2024 at 14:36):Pierre Roux said:
That being said, I'm still curious of your motivation.
Our ultimate goal is to be able to easily test bug fixes / features in our dependencies. One way to do that with dune is to set up a workspace with all the ocaml / coq deps you potentially want to tweak. That means that you can edit files in any involved package, and then recompile everything that needs to be with dune build, without having to fiddle with installation, opam packages and so on.
Enrico Tassi (Sep 05 2024 at 14:36):And these are the files being resolved "coq://elpi_elpi/elpi-command-template-synterp.elpi" "coq://elpi_elpi/elpi-command-template.elpi".
Rodolphe Lepigre (Sep 05 2024 at 14:37):Enrico Tassi said:
This is your enemy:
https://github.com/LPCIC/coq-elpi/blob/d6509831d6b85fd1905bf44e1f7eab45b22ae5bf/src/coq_elpi_programs.ml#L635-L693
Yeah, that's the code I linked above. I love the (* Hem, this sucks *) comment. :laughing:
Enrico Tassi (Sep 05 2024 at 14:38):yes but now that the html printer is there, I think that code is not relevant
Rodolphe Lepigre (Sep 05 2024 at 14:38):Ah, I see, OK.
Enrico Tassi (Sep 05 2024 at 14:38):I guess this does not find the .elpi file Loadpath.find_with_logical_path dp
Rodolphe Lepigre (Sep 05 2024 at 14:38):Note that there are other files that need to move (or be copied). At least one. Let me look it up.
Rodolphe Lepigre (Sep 05 2024 at 14:39):It is elpi-quoted_syntax.elpi I believe.
Enrico Tassi (Sep 05 2024 at 14:39):in your error, do the [...] say more?
Enrico Tassi (Sep 05 2024 at 14:39):yes, that one too
Rodolphe Lepigre (Sep 05 2024 at 14:39):Yeah, it's a list of paths that look kind of bonkers.
Enrico Tassi (Sep 05 2024 at 14:40):hum, these are passed to Coq via -Q and co... if these are not pointing to _build/... then
Rodolphe Lepigre (Sep 05 2024 at 14:40):Here is the full message I get locally:
File "./coq-elpi/theories/elpi.v", line 12, characters 0-120:
Error:
Anomaly
"Uncaught exception Failure("File elpi/coq-lib-common.elpi not found in:
/home/rodolphe/dev/bhv_8_19/coq-elpi-bug/_build/default/.,
/home/rodolphe/dev/bhv_8_19/_opam/lib/elpi,
/home/rodolphe/dev/bhv_8_19/coq-elpi-bug/_build/default/.,
/home/rodolphe/dev/bhv_8_19/coq-elpi-bug/_build/default/..,
/home/rodolphe/dev/bhv_8_19/_opam/lib/coq/user-contrib/elpi/")."
Please report at http://coq.inria.fr/bugs/.
Raised at Elpi_util__Util.std_resolver.(fun) in file "src/utils/util.ml", line 652, characters 4-75
Called from Elpi_parser__Parse.Make.(fun) in file "src/parser/parse.ml", line 69, characters 17-50
Called from Stdlib__List.map in file "list.ml", line 92, characters 20-23
Called from Elpi_parser__Grammar.Make._menhir_action_103 in file "src/parser/grammar.mly", line 132, characters 47-159
Called from Elpi_parser__Grammar.Make._menhir_run_532 in file "src/parser/grammar.ml", line 13105, characters 17-68
Called from Elpi_parser__Parse.Make.parse in file "src/parser/parse.ml", line 48, characters 12-32
Called from Elpi_parser__Parse.Make.(fun) in file "src/parser/parse.ml", line 85, characters 16-51
Called from Stdlib__List.map in file "list.ml", line 92, characters 20-23
Called from Elpi_parser__Parse.Make.program in file "src/parser/parse.ml", line 118, characters 27-42
[...]
(I split lines for readability, and I'll remove the tail of the backtrace since it's useless.)
Enrico Tassi (Sep 05 2024 at 14:42):I don't know if the (* Hem, this sucks *) code messes with that, but _build/default and _build/default/.. seem wrong... there should be a lib/elpi somewhere
Enrico Tassi (Sep 05 2024 at 14:42):there is one, but in _opam ;-)
Rodolphe Lepigre (Sep 05 2024 at 14:42):So, yeah, it is looking only under _build/default, not _build/default/coq_elpi in this case.
Enrico Tassi (Sep 05 2024 at 14:43):sorry, coq_elpi
Rodolphe Lepigre (Sep 05 2024 at 14:43):I guess the right thing to do would be to ask findlib where the elpi package is.
Rodolphe Lepigre (Sep 05 2024 at 14:43):This way we don't have to copy files form elpi into coq-elpi.
Enrico Tassi (Sep 05 2024 at 14:43):sure, but you said it does not work anyway...
Rodolphe Lepigre (Sep 05 2024 at 14:44):Yeah, there are indeed two problems.
Rodolphe Lepigre (Sep 05 2024 at 14:44):The other problem can be solved by looking under _build/install/... instead of _build/default probably. What do you think @Emilio Jesús Gallego Arias?
Enrico Tassi (Sep 05 2024 at 14:44):can you see how coqc is called?
Enrico Tassi (Sep 05 2024 at 14:45):is there a -Q or -R ?
Enrico Tassi (Sep 05 2024 at 14:45):that one seems faulty
Enrico Tassi (Sep 05 2024 at 14:45):in compose mode, I think
Rodolphe Lepigre (Sep 05 2024 at 14:46):(cd _build/default && /home/rodolphe/dev/bhv_8_19/_opam/bin/coqc -w +elpi.deprecated -bt -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -boot -I /home/rodolphe/dev/bhv_8_19/_opam/lib/coq-core/boot -I /home/rodolphe/dev/bhv_8_19/_opam/lib/coq-core/clib -I /home/rodolphe/dev/bhv_8_19/_opam/lib/coq-core/config -I /home/rodolphe/dev/bhv_8_19/_opam/lib/coq-core/engine -I /home/rodolphe/dev/bhv_8_19/_opam/lib/coq-core/gramlib -I /home/rodolphe/dev/bhv_8_19/_opam/lib/coq-core/interp -I /home/rodolphe/dev/bhv_8_19/_opam/lib/coq-core/kernel -I /home/rodolphe/dev/bhv_8_19/_opam/lib/coq-core/lib -I /home/rodolphe/dev/bhv_8_19/_opam/lib/coq-core/library -I /home/rodolphe/dev/bhv_8_19/_opam/lib/coq-core/parsing -I /home/rodolphe/dev/bhv_8_19/_opam/lib/coq-core/perf -I /home/rodolphe/dev/bhv_8_19/_opam/lib/coq-core/plugins/ltac -I /home/rodolphe/dev/bhv_8_19/_opam/lib/coq-core/pretyping -I /home/rodolphe/dev/bhv_8_19/_opam/lib/coq-core/printing -I /home/rodolphe/dev/bhv_8_19/_opam/lib/coq-core/proofs -I /home/rodolphe/dev/bhv_8_19/_opam/lib/coq-core/tactics -I /home/rodolphe/dev/bhv_8_19/_opam/lib/coq-core/vernac -I /home/rodolphe/dev/bhv_8_19/_opam/lib/coq-core/vm -I /home/rodolphe/dev/bhv_8_19/_opam/lib/elpi -I /home/rodolphe/dev/bhv_8_19/_opam/lib/elpi/lexer_config -I /home/rodolphe/dev/bhv_8_19/_opam/lib/elpi/parser -I /home/rodolphe/dev/bhv_8_19/_opam/lib/elpi/trace/runtime -I /home/rodolphe/dev/bhv_8_19/_opam/lib/elpi/util -I /home/rodolphe/dev/bhv_8_19/_opam/lib/findlib -I /home/rodolphe/dev/bhv_8_19/_opam/lib/menhirLib -I /home/rodolphe/dev/bhv_8_19/_opam/lib/ocaml -I /home/rodolphe/dev/bhv_8_19/_opam/lib/ocaml/threads -I /home/rodolphe/dev/bhv_8_19/_opam/lib/ppx_deriving/runtime -I /home/rodolphe/dev/bhv_8_19/_opam/lib/re -I /home/rodolphe/dev/bhv_8_19/_opam/lib/re/str -I /home/rodolphe/dev/bhv_8_19/_opam/lib/result -I /home/rodolphe/dev/bhv_8_19/_opam/lib/seq -I /home/rodolphe/dev/bhv_8_19/_opam/lib/stdlib-shims -I /home/rodolphe/dev/bhv_8_19/_opam/lib/zarith -I coq-elpi/src -I /home/rodolphe/dev/bhv_8_19/_opam/lib/coq/../coq-core/plugins/btauto -I /home/rodolphe/dev/bhv_8_19/_opam/lib/coq/../coq-core/plugins/cc -I /home/rodolphe/dev/bhv_8_19/_opam/lib/coq/../coq-core/plugins/derive -I /home/rodolphe/dev/bhv_8_19/_opam/lib/coq/../coq-core/plugins/extraction -I /home/rodolphe/dev/bhv_8_19/_opam/lib/coq/../coq-core/plugins/firstorder -I /home/rodolphe/dev/bhv_8_19/_opam/lib/coq/../coq-core/plugins/funind -I /home/rodolphe/dev/bhv_8_19/_opam/lib/coq/../coq-core/plugins/ltac -I /home/rodolphe/dev/bhv_8_19/_opam/lib/coq/../coq-core/plugins/ltac2 -I /home/rodolphe/dev/bhv_8_19/_opam/lib/coq/../coq-core/plugins/micromega -I /home/rodolphe/dev/bhv_8_19/_opam/lib/coq/../coq-core/plugins/nsatz -I /home/rodolphe/dev/bhv_8_19/_opam/lib/coq/../coq-core/plugins/number_string_notation -I /home/rodolphe/dev/bhv_8_19/_opam/lib/coq/../coq-core/plugins/ring -I /home/rodolphe/dev/bhv_8_19/_opam/lib/coq/../coq-core/plugins/rtauto -I /home/rodolphe/dev/bhv_8_19/_opam/lib/coq/../coq-core/plugins/ssreflect -I /home/rodolphe/dev/bhv_8_19/_opam/lib/coq/../coq-core/plugins/ssrmatching -I /home/rodolphe/dev/bhv_8_19/_opam/lib/coq/../coq-core/plugins/tauto -I /home/rodolphe/dev/bhv_8_19/_opam/lib/coq/../coq-core/plugins/tutorial/p0 -I /home/rodolphe/dev/bhv_8_19/_opam/lib/coq/../coq-core/plugins/tutorial/p1 -I /home/rodolphe/dev/bhv_8_19/_opam/lib/coq/../coq-core/plugins/tutorial/p2 -I /home/rodolphe/dev/bhv_8_19/_opam/lib/coq/../coq-core/plugins/tutorial/p3 -I /home/rodolphe/dev/bhv_8_19/_opam/lib/coq/../coq-core/plugins/zify -R /home/rodolphe/dev/bhv_8_19/_opam/lib/coq/theories Coq -Q coq-elpi/elpi elpi_elpi -R coq-elpi/theories elpi coq-elpi/theories/elpi.v)
The relevant bit is probably -Q coq-elpi/elpi elpi_elpi -R coq-elpi/theories elpi for your question.
Emilio Jesús Gallego Arias (Sep 05 2024 at 14:48):Rodolphe Lepigre said:
The other problem can be solved by looking under
_build/install/...instead of_build/defaultprobably. What do you think Emilio Jesús Gallego Arias?
Usually that's a bit of PITA, as pulling things from _build/install will load a lot of extra rules in Dune to account for the package install, which are often less incremental.
I don't recall how the elpi stuff worked, but it shouldn't be hard to fix it to use the same method that is used for .vo works.
Rodolphe Lepigre (Sep 05 2024 at 14:49):How does it work for .vo files?
Emilio Jesús Gallego Arias (Sep 05 2024 at 14:50):It uses -Q / -Rand loadpath.
Enrico Tassi (Sep 05 2024 at 14:52):Something is fishy, because elpi_elpi/whatever should be found by Loadpath.find_with_logical_path given the -Q above
Enrico Tassi (Sep 05 2024 at 14:56):sorry, I think I mislead you. The problem comes from the std_resolver
Emilio Jesús Gallego Arias (Sep 05 2024 at 14:56):Rodolphe Lepigre said:
I guess the right thing to do would be to ask findlib where the
elpipackage is.
I'm afraid findlib is not really usable on composed builds (and has other problems).
As discussed in https://github.com/ocaml/dune/pull/9591 , it is IMO best to either:
This is not hard to do, solution 1 makes dune usable just for elpi, solution 2 is more lightweight
Enrico Tassi (Sep 05 2024 at 14:57):I think the first file is found, then the file contains accumulate elpi/other-file and that goes trough the other ugly resolver
Rodolphe Lepigre (Sep 05 2024 at 14:58):Yeah, that would explain what I am seeing.
Enrico Tassi (Sep 05 2024 at 14:58):that resolver is really looking at the file system, and it does not find the file...
If I'm right the quickest fix should be to change the elpi code to call accumulate "coq://elpi..." instead.
Enrico Tassi (Sep 05 2024 at 14:59):I mean, use the same syntax I use in the .v file
Rodolphe Lepigre (Sep 05 2024 at 14:59):@Emilio Jesús Gallego Arias I agree these solutions are probably the right long-term plan, but I'd like to find a quick fix first.
Enrico Tassi (Sep 05 2024 at 15:00):In this case it seems a bug in my code, when elpi is used within Coq it should always use Coq's resolver, not the basic one
Emilio Jesús Gallego Arias (Sep 05 2024 at 15:01):@Rodolphe Lepigre Note that @Ali Caglayan 's patch already implements solution 2, so if we wanna schedule a slot to process it, shouldn't take long.
It would be great if you could find a quick solution, but I am not sure an incremental build can ever work with the current situation
Emilio Jesús Gallego Arias (Sep 05 2024 at 15:03):I had a look at current coq-elpi dune files, I think it is possible to you can get a quick fix
Rodolphe Lepigre (Sep 05 2024 at 15:05):Yeah, that is my hope. I think the rules are setup correctly, although they are not as fine-grained as they could be if there was better integration of elpi into dune.
Emilio Jesús Gallego Arias (Sep 05 2024 at 15:05):whether things will work depends on a behavior that is actually under specified in dune, regarding on when transitive deps are cleaned up in incremental builds. I think recent dune's won't do this, but indeed we should not rely on the trick of a theory having a dummy .v file pulling the .elpi files as a dep (for example coqdep won't see this)
Emilio Jesús Gallego Arias (Sep 05 2024 at 15:07):But anyways if you got a use for this I'd suggest we go like this:
This is still a PITA given that coqdep doesn't support -modules, so auto-generated .elpi files need to be put in place before we call coqdep, but can be workarounded using per_theory boundaries.
Emilio Jesús Gallego Arias (Sep 05 2024 at 15:08):What do you think?
Rodolphe Lepigre (Sep 05 2024 at 15:11):Yeah, that should be easy to put together, at least in a minimal version.
Rodolphe Lepigre (Sep 05 2024 at 15:19):@Emilio Jesús Gallego Arias, here is how you can create a minimal such workspace:
mkdir workspace
cd workspace
echo "(lang dune 3.8)" > dune-workspace
git clone --depth 1 git@github.com:LPCIC/elpi
git clone --depth 1 git@github.com:LPCIC/coq-elpi
git clone --depth 1 git@github.com:bedrocksystems/BRiCk.git
mv BRiCk/coq-lens .
rm -rf BRiCk
Great!
Last updated: Oct 13 2024 at 01:02 UTC