Paolo Giarrusso (Feb 17 2022 at 12:36): Paolo Giarrusso (Feb 17 2022 at 12:36):dune coqtop foo.v should build all dependencies of foo.v. Internally, should we add a new rule doing that (by refactoring coq_rules), or is there an API to extract the dependencies "from outside" (say, from a type of Action)?
We were wondering today, and @Rodolphe Lepigre was looking for the latter; I conjectured such a generic API might not exist with dynamic dependencies, since the last action can always add new dependencies...
Rodolphe Lepigre (Feb 17 2022 at 12:39):Surely, there must be a way to get the dependencies into the same state as dune build path/to/file.vo right before calling coqc on path/to/file.v. But that's not at all obvious how to do that to me.
Paolo Giarrusso (Feb 17 2022 at 12:43):Hm, "Build systems à la carte" has a hint:
DUNE (JaneStreet,2018) is a build system designed for OCaml/Reason projects. Its original implementation used arrows (Hughes, 2000) rather than monads to model dynamic dependencies, which simplified static dependency approximation. DUNE was later redesigned to use a flavour of selective functors (Mokhov et al., 2019), making it a closer fit to our abstractions.
Paolo Giarrusso (Feb 17 2022 at 12:44):note it's talking of static dependency _approximation_, which means you can do more than I conjectured, but maybe not enough: all our interesting dependencies are somewhat dynamic.
Rudi Grinberg (Feb 17 2022 at 15:38):Isn't Coq_rules.deps_of what you want?
Rudi Grinberg (Feb 17 2022 at 16:09):@Rodolphe Lepigre your coqtop action should depend on the result of deps_of. That will make sure that once it is executed, all the dependencies of file.v are built
Rodolphe Lepigre (Feb 17 2022 at 16:15):OK that makes sense, however what I still don't understand is how to invoke such an action. Should it be something similar to the (unexposed) Coq_rules.setup_rule?
Rudi Grinberg (Feb 17 2022 at 16:23):There are two steps:
I can explain how to do 2, but it depends how you want to expose it. You want to have a subcommand, right?
Rodolphe Lepigre (Feb 17 2022 at 16:26):Yeah, what I have so far is a new command (in bin/coqtop.ml) that is basically copied form bin/exec.ml. It is invoked as dune coqtop FILE.v -- ARGS, and currently it builds FILE.vo and then invokes coqtop on FILE.v, which is not what we want but I started simple.
Rudi Grinberg (Feb 17 2022 at 16:32):Yeah, so you're pretty close. You need to build coqtop.exe (if it's in the workspace) and the dependencies only. Action_builder.run is what you need to transform the result of deps_of into a build request
Rudi Grinberg (Feb 17 2022 at 16:33):btw, it should be dune coq top. we don't want to pollute the toplevel subcommand namespace too much
Rodolphe Lepigre (Feb 17 2022 at 16:34):OK cool, thanks! I'll give this a go, and ask more questions if I get stuck again.
Emilio Jesús Gallego Arias (Feb 17 2022 at 17:16):Nice! Rudy the thing is that we were thinking if introducing an alias for the deps would make sense, so the stuff in bin/ just builds the alias
Emilio Jesús Gallego Arias (Feb 17 2022 at 17:16):but maybe that's a bad idea
Rudi Grinberg (Feb 17 2022 at 17:48):It's a good idea if the alias is useful as something user facing. But if you don't, it's just not necessary.
Paolo Giarrusso (Feb 17 2022 at 18:20):It doesn't need to be user-facing if we handle all coqtop-like use cases, including coqidetop and wrappers.
Paolo Giarrusso (Feb 17 2022 at 18:20):(and soon also for vos mode)
MackieLoeffel (Feb 17 2022 at 18:36):The list of different coqtop-like things you mention could also be seen as an argument in favor having the alias. I could imagine that there could be usecases for such an alias (e.g. custom wrappers for coqtop), but they are probably not very common.
Paolo Giarrusso (Feb 17 2022 at 19:52):never used it but vscoq's GUI mentions hoqtop which IIUC is a wrapper used by some HoTT project
Paolo Giarrusso (Feb 17 2022 at 19:53):I'm also not too familiar with coqidetop — many arguments are the same; it also get some networking parameters, but I hope they can just be passed through transparently.
Ali Caglayan (Feb 17 2022 at 20:17):hoqtop used to be a wrapper around coqtop before the noinit flag worked
Ali Caglayan (Feb 17 2022 at 20:18):Now everything works with standard coq and we don't really need to replace the coqtop that is being called
Ali Caglayan (Feb 17 2022 at 20:18):coqidetop is what is used by vscode, coqide in the background
Gaëtan Gilbert (Feb 17 2022 at 20:18):there was a noinit bug? I thought hoqtop was just for convenience
Ali Caglayan (Feb 17 2022 at 20:23):For a while it wasn't implemented fully IIRC, hoq* was something to trick coq* into thinking the HoTT library was the stdlib.
Ali Caglayan (Feb 17 2022 at 20:24):I think the real reason was that it was setup before _CoqProject (and noinit?) even existed
Ali Caglayan (Feb 17 2022 at 20:25):Also this was finally merged
Ali Caglayan (Feb 17 2022 at 20:26):https://github.com/coq/coq/pull/186
Ali Caglayan (Feb 17 2022 at 20:26):https://github.com/HoTT/HoTT/issues/963
Gaëtan Gilbert (Feb 17 2022 at 20:30):not enough stuff was done through Register so hott had a modified prelude, and so -coqlib had to be passed
Gaëtan Gilbert (Feb 17 2022 at 20:30):or rather Register didn't exist
Paolo Giarrusso (Feb 17 2022 at 21:00):@Ali Caglayan should vscoq stop mentioning hoqidetop then, if it's that outdated?
Ali Caglayan (Feb 17 2022 at 21:00):Yes
Emilio Jesús Gallego Arias (Feb 18 2022 at 08:04):Paolo Giarrusso said:
Hm, "Build systems à la carte" has a hint:
DUNE (JaneStreet,2018) is a build system designed for OCaml/Reason projects. Its original implementation used arrows (Hughes, 2000) rather than monads to model dynamic dependencies, which simplified static dependency approximation. DUNE was later redesigned to use a flavour of selective functors (Mokhov et al., 2019), making it a closer fit to our abstractions.
@Paolo Giarrusso this is not true anymore I think, the static dependency optimization was removed and now dune is fully dynamic
Last updated: Apr 20 2024 at 00:02 UTC