Stream: Dune devs & users

Topic: Dune internals: build a target `--only-deps`


view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Rudi Grinberg (Feb 17 2022 at 15:38):

Isn't Coq_rules.deps_of what you want?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Rudi Grinberg (Feb 17 2022 at 16:23):

There are two steps:

  1. Create the rule (this is where you need the deps)
  2. Execute it

I can explain how to do 2, but it depends how you want to expose it. You want to have a subcommand, right?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 17 2022 at 17:16):

but maybe that's a bad idea

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Feb 17 2022 at 18:20):

(and soon also for vos mode)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Feb 17 2022 at 20:17):

hoqtop used to be a wrapper around coqtop before the noinit flag worked

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Feb 17 2022 at 20:18):

coqidetop is what is used by vscode, coqide in the background

view this post on Zulip Gaëtan Gilbert (Feb 17 2022 at 20:18):

there was a noinit bug? I thought hoqtop was just for convenience

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Feb 17 2022 at 20:24):

I think the real reason was that it was setup before _CoqProject (and noinit?) even existed

view this post on Zulip Ali Caglayan (Feb 17 2022 at 20:25):

Also this was finally merged

view this post on Zulip Ali Caglayan (Feb 17 2022 at 20:26):

https://github.com/coq/coq/pull/186

view this post on Zulip Ali Caglayan (Feb 17 2022 at 20:26):

https://github.com/HoTT/HoTT/issues/963

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Feb 17 2022 at 20:30):

or rather Register didn't exist

view this post on Zulip Paolo Giarrusso (Feb 17 2022 at 21:00):

@Ali Caglayan should vscoq stop mentioning hoqidetop then, if it's that outdated?

view this post on Zulip Ali Caglayan (Feb 17 2022 at 21:00):

Yes

view this post on Zulip 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: Jan 30 2023 at 19:04 UTC