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...
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.
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.
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.
Isn't Coq_rules.deps_of
what you want?
@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
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
?
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?
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.
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
btw, it should be dune coq top
. we don't want to pollute the toplevel subcommand namespace too much
OK cool, thanks! I'll give this a go, and ask more questions if I get stuck again.
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
but maybe that's a bad idea
It's a good idea if the alias is useful as something user facing. But if you don't, it's just not necessary.
It doesn't need to be user-facing if we handle all coqtop-like use cases, including coqidetop and wrappers.
(and soon also for vos mode)
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.
never used it but vscoq's GUI mentions hoqtop which IIUC is a wrapper used by some HoTT project
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.
hoqtop used to be a wrapper around coqtop before the noinit flag worked
Now everything works with standard coq and we don't really need to replace the coqtop that is being called
coqidetop is what is used by vscode, coqide in the background
there was a noinit bug? I thought hoqtop was just for convenience
For a while it wasn't implemented fully IIRC, hoq* was something to trick coq* into thinking the HoTT library was the stdlib.
I think the real reason was that it was setup before _CoqProject (and noinit?) even existed
Also this was finally merged
https://github.com/coq/coq/pull/186
https://github.com/HoTT/HoTT/issues/963
not enough stuff was done through Register so hott had a modified prelude, and so -coqlib had to be passed
or rather Register didn't exist
@Ali Caglayan should vscoq stop mentioning hoqidetop then, if it's that outdated?
Yes
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: Oct 13 2024 at 01:02 UTC