Stream: Dune devs & users

Topic: Workspace configuration

Emilio Jesús Gallego Arias (Nov 30 2020 at 15:59):

@Kenji Maillard proposes that dune-workspace files can actually contain configuration of working projects, so it is not necessary to bring all sources under the same dir. This should be easy to do, dune already has the dirs notion, and some proposals of this style have arisen, as of example to allow:

(package
  (name foo)
  (git repos branch)
  ....)

Emilio Jesús Gallego Arias (Nov 30 2020 at 15:59):

You still need to "root" at a directory where the object files will be stored, as indeed you may need a common build dir for the composed objects.

Kenji Maillard (Nov 30 2020 at 16:11):

I still have troubles to understand how that should work. I have often repos that are not pure coq (there is a mix of coq code, agda code, some tex, other things...) so I'm usually relying on specific opam switches. Could I set up a dune workspace by specifying that it has to work with a specific opam switch and fetch all dependencies there ?

Emilio Jesús Gallego Arias (Nov 30 2020 at 16:22):

Yup, dune workspaces allow you to define already the concrete opam switch or switches you want that to be compiled. Dune is at its core a generic build system, so anything that can be expressed as a rule {deps} -[action]-> {targets} should work, with some limitations, such as targets should be in the same dir as the incremental engine works at a directory-level granularity for lazily evaluating /loading rule changes

Emilio Jesús Gallego Arias (Nov 30 2020 at 16:22):

So there is still missing support in the sense that the workspace is build from scanning from the root

Emilio Jesús Gallego Arias (Nov 30 2020 at 16:22):

that is what we could lift

Emilio Jesús Gallego Arias (Nov 30 2020 at 16:22):

and specify a grafting on the directory tree

Emilio Jesús Gallego Arias (Nov 30 2020 at 16:23):

"workspace" indeed contains stuff such as the path, etc....

Rudi Grinberg (Dec 01 2020 at 21:49):

@Kenji Maillard note that you can already do switch selection in a workspace file. So what Emilio describes is a reasonable extension.

Last updated: Jun 03 2023 at 18:01 UTC