Stream: Dune devs & users

Topic: Compositional Coq builds


view this post on Zulip Paolo Giarrusso (Sep 15 2020 at 09:40):

Since at Bedrock Systems we have multiple Coq repositories, I tried composing builds by putting multiple projects together. Is it correct that, for now, I have to patch the dune builds to have a single dune-project? Is that limitation easier to lift in the future?

view this post on Zulip Emilio Jesús Gallego Arias (Sep 15 2020 at 16:05):

Indeed, this is still lacking, but it is a high priority feature.

view this post on Zulip Rudi Grinberg (Sep 15 2020 at 16:16):

@Emilio Jesús Gallego Arias Just curious, what's preventing this at the moment, is it just the missing scoping mechanism we have for OCaml libraries? Or is there still some upwork remaining in coq?

view this post on Zulip Emilio Jesús Gallego Arias (Sep 16 2020 at 11:59):

Main point to figure out is what the rules for detecting public installed libs are; we cannot rely on ocamlfind as OCaml does. The whole thing is a bit messy, but I think I got a good idea on how to move forward. Anyways I hope in the CUDW we can do a task-force and actually move beyond the current installation layout.

view this post on Zulip Paolo Giarrusso (Sep 16 2020 at 19:25):

ah. mapping foo.bar to user-theories/foo/bar might not be general.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 16 2020 at 20:03):

Yeah, we need to come out with a better setup for libs, unfortunately that won't be compatible with coq-makefile, so i'll be coq lang 2.0

view this post on Zulip Emilio Jesús Gallego Arias (Sep 16 2020 at 20:03):

for now yeah, no other choice than to do that kind of mapping :S

view this post on Zulip Emilio Jesús Gallego Arias (Sep 16 2020 at 20:04):

which is pretty expensive by the was as Dune has to scan the full of user-contrib :S

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 07:55):

“won’t be compatible with coq_makefile” where’s the roadmap for ever deprecating coq_makefile?

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 07:56):

my questions in the last few days amount to significant objections.

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 07:59):

if you want to add some library database, then can you add a command that can be used without dune?

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 08:09):

to be more explicit, coq_makefile can compose with arbitrary extensions in Makefile.coq.local, while (today) dune allows:

I’m sure there are reasons, and I asked about them a few days ago (after all, I also use dune)...

view this post on Zulip Enrico Tassi (Sep 17 2020 at 08:11):

If you want each library to install a manifest file in a precise place, then I don't see why coq_makefile cannot be patched to do the same.

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 08:14):

... TLDR there’s going to be lots of resistance to a forcing something so limiting, unless you involve users in the decision early on

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 08:15):

and not just resistance by inertia

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 08:16):

but I’m sure @Théo Zimmermann appreciates the complexities of these “community” decisions :-)

view this post on Zulip Théo Zimmermann (Sep 17 2020 at 08:16):

Not sure what you mean by "appreciates" in this context, but I sure agree with you.

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 08:19):

appreciate as in “understand well”, but I had a typo (now fixed) :-)

view this post on Zulip Emilio Jesús Gallego Arias (Sep 17 2020 at 13:47):

Paolo Giarrusso said:

to be more explicit, coq_makefile can compose with arbitrary extensions in Makefile.coq.local, while (today) dune allows:

I’m sure there are reasons, and I asked about them a few days ago (after all, I also use dune)...

I don't think lack of programability is a bad thing, indeed I think it is a good thing. For a system such as Coq, I think users should say _what_ to build, not _how_ to do it. That is to say, the dune language should remain declarative.

This is obviously more limited, but on the other hand it provides a better abstraction setup, and in particular it allows developers to change _how_ things are built without impacting users. If you got some very special needs already you can hook dune to your own build system.

The default install layout for Coq packages has a huge downside and it is that once a package is installed, it is not possible to hide it. Already nix is doing things differently and coq dune 2.0 will do too I hope.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 17 2020 at 14:16):

A good example of this is instrumentation; imagine I want to build a Coq theory with some instrumentation. If you can program your own build rules, we have little hope to make it work with your setup

view this post on Zulip Rudi Grinberg (Sep 17 2020 at 18:29):

Moreover, you can mix OCaml and Coq seamlessly in a single project. Good luck doing that with coq_makefile.

view this post on Zulip Karl Palmskog (Sep 17 2020 at 18:32):

mixing can be done, but it's absolutely terrible to get incremental builds for an extraction-based project (using coq_makefile)

view this post on Zulip Karl Palmskog (Sep 17 2020 at 18:33):

I would probably use Dune with the "submake" functionality if I got stuck somewhere, rather than abandon Dune completely

view this post on Zulip Karl Palmskog (Sep 17 2020 at 18:36):

the sad reality, however, is that many (maybe even most projects outside coq-community and Coq's CI and the contribs) are using completely home-made Makefiles

view this post on Zulip Karl Palmskog (Sep 17 2020 at 18:37):

consider this relatively high-profile project: https://github.com/vrahli/Velisarios/blob/master/Makefile

PBFT/PBFTview_changes_are_received.vo : PBFT/PBFTview_changes_are_received.v PBFT/PBFTview_change_somewhere_in_log.vo
    coqc -R coq-tools util -R model model -R components components -R PBFT PBFT -R PrimaryBackup PrimaryBackup -R runtime runtime -R TwoThirds TwoThirds PBFT/PBFTview_changes_are_received.v

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 20:04):

Thanks for motivating the design. That makes sense for the coq part. However, I have a program that generates .v files; now what?

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 20:05):

“You can hook dune to your build system” how? Right now, I can generate a dune file that lists one rule for each .v file (all copies of the same rule).

view this post on Zulip Karl Palmskog (Sep 17 2020 at 20:06):

@Paolo Giarrusso example of .v generation: https://github.com/palmskog/fitch/blob/master/coq/dune

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 20:07):

Thanks, I have N rules like that — I asked about %.v : %.bar rules in another thread here

view this post on Zulip Karl Palmskog (Sep 17 2020 at 20:07):

I guess I was thinking of this: https://dune.readthedocs.io/en/stable/foreign-code.html#foreign-build-sandboxing

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 20:09):

in any case, there is no need to trade off declarative builds against extensibility.

view this post on Zulip Karl Palmskog (Sep 17 2020 at 20:09):

ah I misunderstood then, I thought it was quite clear the current conclusion seemed to be to use your favorite language to generate the dune rules/files (for %.v: %.bar)

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 20:09):

sure, that’s indeed the workaround :-)

view this post on Zulip Karl Palmskog (Sep 17 2020 at 20:10):

PL researchers trade extensibility against predictability/guarantees all the time, arguably

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 20:10):

you can have an extensible system that lets you implement declarative tasks, but also extensions.

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 20:11):

indeed, you have tradeoffs in e.g. how dynamic your dependencies can be.

view this post on Zulip Karl Palmskog (Sep 17 2020 at 20:11):

for example, if the majority of users of Dune don't need %.v : %.bar the right design decision could be to force everyone who does to generate dune files.

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 20:12):

@Karl Palmskog my basic answer is “Growing a language”

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 20:13):

it’s probably a matter of opinion, but that research program was the foundation of my supervisor’s research program :-)

view this post on Zulip Karl Palmskog (Sep 17 2020 at 20:13):

plenty of examples of successful languages that haven't grown much, if at all

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 20:14):

@Karl Palmskog on your example, maybe there’s a couple of users who need that extension, but another couple of users need their own extension, and so on

view this post on Zulip Karl Palmskog (Sep 17 2020 at 20:14):

non-success-story of growing something: browser extensions

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 20:16):

no clue on browser extensions (other than, I wouldn’t use a browser without); I agree that there’s plenty of languages that are not extensible enough for users.

view this post on Zulip Karl Palmskog (Sep 17 2020 at 20:16):

so I disagree about the general qualitative argument that "extensions should (always) be possible"

view this post on Zulip Karl Palmskog (Sep 17 2020 at 20:17):

both Chrome and Firefox extensions have died multiple times over, and are consistently broken as browsers evolve

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 20:17):

well, I don’t think I’ll convince you, but you won’t convince me either I guess

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 20:17):

maybe there could be progress on what makes sense in this example.

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 20:18):

and some of the limitations don’t seem about extensibility either.

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 20:18):

but is the plan for dune to _not_ offer support for plugins?

view this post on Zulip Karl Palmskog (Sep 17 2020 at 20:19):

but what's the core of your argument? System software should be extensible because... [...] even at the cost of predictability/guarantees/etc.

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 20:19):

I didn’t say “system software”

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 20:20):

I didn’t say that either

view this post on Zulip Karl Palmskog (Sep 17 2020 at 20:20):

I was giving an example what the argument could look like

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 20:20):

users of programming languages (which include build languages) will need to have custom extensions

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 20:20):

some could go into the language, but some don’t make sense for all users.

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 20:21):

and I don’t think the “predictability” argument applies, since the present limitations prevent things that don’t violate the guarantees.

view this post on Zulip Karl Palmskog (Sep 17 2020 at 20:22):

if you allow full programmability inside Dune in OCaml, what can you guarantee?

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 20:23):

I’m not necessarily attached to plugins.

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 20:23):

programming language design is a thing, and we have solutions to design languages with restricted side effects.

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 20:24):

in Haskell, you could design an embedded DSL and its semantics, and make it as restrictive as you’d like.

view this post on Zulip Karl Palmskog (Sep 17 2020 at 20:25):

if you design an extension DSL and publish a paper proving the usual Dune properties are preserved, I'm sure they will discuss it

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 20:25):

I realize that might not be as easy in another language, but I don’t think this part was a problem in SBT...

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 20:25):

what _are_ the usual Dune properties?

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 20:26):

I’ve asked, a while ago, for a design rationale

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 20:26):

you’ve explained a bit more now, but I’ve never seen a design document.

view this post on Zulip Karl Palmskog (Sep 17 2020 at 20:26):

I think this is the closest to a formalization: https://www.staff.ncl.ac.uk/andrey.mokhov/selective-functors.pdf

view this post on Zulip Karl Palmskog (Sep 17 2020 at 20:27):

but if you suggest an extension framework, shouldn't the burden fall on you to formalize the missing parts, if indeed parts are missing?

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 20:28):

I mean, I’m not trying to place burdens, I’m asking questions and trying to understand.

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 20:28):

I do ask that coq_makefile is left alive

view this post on Zulip Karl Palmskog (Sep 17 2020 at 20:28):

here is the general pen-and-paper formalization of build systems that above paper builds on: https://www.cambridge.org/core/journals/journal-of-functional-programming/article/build-systems-a-la-carte-theory-and-practice/097CE52C750E69BD16B78C318754C7A4 (preprint: https://github.com/snowleopard/build/releases/download/jfp-submission/jpf-submission.pdf)

view this post on Zulip Karl Palmskog (Sep 17 2020 at 20:29):

coq_makefile is not going to go away anytime soon. the most that might happen is that the community starts to maintain it instead of Coq devs

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 20:30):

good to hear that — that wasn’t clear above :-)

view this post on Zulip Karl Palmskog (Sep 17 2020 at 20:30):

Coq project build practice evolution is extremely slow

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 20:31):

in any case, if that paper formalizes dune, does that mean that newtype Task k v = Task{ run:: forall f . Selective f => (k->f v)->f v} is the necessary type?

view this post on Zulip Karl Palmskog (Sep 17 2020 at 20:31):

to my understanding, it's general model that at some high level corresponds to the basic ideas behind Dune

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 20:33):

more weakly: at a quick look, that paper does explain part of the rationale of dune (static overapproximation), then designs the core of a DSL to support it.

view this post on Zulip Karl Palmskog (Sep 17 2020 at 20:33):

I tried to summarize the status of build system formalization in our TACAS paper: http://users.ece.utexas.edu/~gligoric/papers/PalmskogETAL20Chip.pdf#page=15

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 20:36):

that doesn’t seem evidence that abstraction mechanisms in dune scripts prevent its goals.

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 20:37):

there’s a gulf between arbitrary computations, and no abstraction.

view this post on Zulip Karl Palmskog (Sep 17 2020 at 20:37):

on the other hand, is there evidence that it will work well? (Be maintainable, used by many users, etc.)

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 20:38):

and in-between, there’s “use a pure FP language to generate the dune script with something better than string concatenation”

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 20:39):

Well! There are tons of build systems with various amounts of programmability, and tradeoffs between them.

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 20:39):

up to now, I don’t think dune has _specific_ problems preventing extensions.

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 20:41):

that was my key argument. That doesn’t mean that somebody has to do it for me :-). Worst-case, somebody could build a DSL to generate dune scripts in a nicer way.

view this post on Zulip Rudi Grinberg (Sep 17 2020 at 21:12):

Paolo Giarrusso said:

but is the plan for dune to _not_ offer support for plugins?

The plan is to certainly offer plugins. However, we'd prefer to do this by exposing an OCaml based API.

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 21:14):

fine with me, tho some of @Karl Palmskog’s question apply to such plugins (how do you enforce the guarantees on them)

view this post on Zulip Karl Palmskog (Sep 17 2020 at 21:15):

right, I'm not sure if it's easy to enforce things like pureness, or at least absence of IO, etc., in OCaml

view this post on Zulip Karl Palmskog (Sep 17 2020 at 21:16):

I guess they might be like ad-hoc axioms in Coq... caveat emptor

view this post on Zulip Rudi Grinberg (Sep 17 2020 at 21:16):

Regarding pattern rules as in make: This is just one of many examples where dune's language falls short. We're incredibly hesitant to pile on features on the dune language because we've seen how things like make, cmake, etc have turned out. Ideally, we'd have something like dhall for configuring builds. Unfortunately, there's nothing dhall-like available in the OCaml world, and it's quite a huge task to implement a high quality PL from scratch.

view this post on Zulip Rudi Grinberg (Sep 17 2020 at 21:18):

Karl Palmskog said:

right, I'm not sure if it's easy to enforce things like pureness, or at least absence of IO, etc., in OCaml

There were some ideas. In the end, I think we'll just need to provide an API and warn the users not to do any IO outside of it.

view this post on Zulip Rudi Grinberg (Sep 17 2020 at 21:20):

One idea was to embed an ocaml interpreter in dune itself (such a thing is already written) and to modify it to only access a primitive standard library that doesn't permit IO. However, it would still be possible to write non terminating program. That's not ideal.

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 21:20):

_ahem_

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 21:20):

Dhall is based on the Calculus of Constructions, apparently.

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 21:21):

and a normalizer.

view this post on Zulip Rudi Grinberg (Sep 17 2020 at 21:21):

Yeah, dhall is good. The dependency tree is massive though

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 21:21):

I hear a OCaml implementation of CC exist, tho I’ll admit it is not obvious how to repurpose it for the task.

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 21:22):

but luckily, I think a few of its authors are available around here.

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 21:23):

;-)

view this post on Zulip Karl Palmskog (Sep 17 2020 at 21:23):

ahhh, configuration languages. Has anyone theoretically justified them yet?

view this post on Zulip Rudi Grinberg (Sep 17 2020 at 21:23):

To contrast with dhall, check out bazel's skylarg language. :sick:

view this post on Zulip Karl Palmskog (Sep 17 2020 at 21:24):

"inspired by Python3" :fear:

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 21:24):

let me be more explicit: in PL terms, ignoring concrete syntax and such details, Dhall is nothing but a small Coq implementation :-)

view this post on Zulip Rudi Grinberg (Sep 17 2020 at 21:25):

With good error messages :)

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 21:25):

just Gallina, a normalizer, and convenient primitives to write configurations

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 21:25):

ohohohoh, shots fired :-)

view this post on Zulip Karl Palmskog (Sep 17 2020 at 21:25):

what do they use dependent types for?

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 21:26):

good question, no clue!

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 21:26):

guess they wanted something powerful and non-Turing complete

view this post on Zulip Rudi Grinberg (Sep 17 2020 at 21:26):

Paolo Giarrusso said:

ohohohoh, shots fired :-)

Ha, I'm not saying coq's bad. Dhall is really going out of it's way to give good error messages.

view this post on Zulip Karl Palmskog (Sep 17 2020 at 21:26):

starting from a clean slate (and no need of DTT), I would implement a language as a subset of CakeML, verified bootstrapped compiler for free

view this post on Zulip Paolo Giarrusso (Sep 17 2020 at 21:26):

and oh, well, GADTs without hacks

view this post on Zulip Emilio Jesús Gallego Arias (Oct 30 2020 at 15:51):

@Paolo Giarrusso I have a prototype ready for a PR

view this post on Zulip Emilio Jesús Gallego Arias (Oct 30 2020 at 15:51):

to be included in Dune 2.8

view this post on Zulip Emilio Jesús Gallego Arias (Oct 30 2020 at 15:51):

let me know if you would be interested in testing

view this post on Zulip Paolo Giarrusso (Oct 30 2020 at 22:42):

Hey! I'm slightly swamped, but I am still interested

view this post on Zulip Emilio Jesús Gallego Arias (Oct 30 2020 at 22:44):

Ok great, thanks a lot, will send you the branch , if you are using opam doing a new switch [for safety] + opam pin dune should do the trick.

I'd like to be sure it works in your use case as this is one of the main roadblocks to having a stable version of Coq dune support.

view this post on Zulip Karl Palmskog (Oct 30 2020 at 22:45):

one good test case might be CoqHammer, see discussion here: https://github.com/lukaszcz/coqhammer/issues/92

view this post on Zulip Karl Palmskog (Oct 30 2020 at 22:45):

I commented out the compositional stuff there in preparation of 2.8 (when they can hopefully be commented in)

view this post on Zulip Paolo Giarrusso (Oct 30 2020 at 22:49):

2 testers sound better — and since CoqHammer's fully open source, I'm sure it's entitled to better support.

(Part of Bedrock's stack is open-source as well, but you really need internal parts to reap the benefits)

view this post on Zulip Paolo Giarrusso (Oct 30 2020 at 22:50):

@Karl Palmskog I'm a bit confused by that issue, I _do_ use theories

view this post on Zulip Karl Palmskog (Oct 30 2020 at 22:51):

the basic problem is that you want to be able to compose with both local and installed parts

view this post on Zulip Paolo Giarrusso (Oct 30 2020 at 22:51):

okay, not sure about that

view this post on Zulip Karl Palmskog (Oct 30 2020 at 22:51):

so hopefully this is something Emilio will test

view this post on Zulip Paolo Giarrusso (Oct 30 2020 at 22:52):

right now I _can_ use theories but only inside a single dune-project

view this post on Zulip Paolo Giarrusso (Oct 30 2020 at 22:53):

but I still understand very little of dune :-|, sadly (time is what it is)

view this post on Zulip Karl Palmskog (Oct 30 2020 at 22:53):

to me, full compositional support means you can combine any of: multiple local Git-based projects with their own dune-project and installed libraries

view this post on Zulip Paolo Giarrusso (Oct 30 2020 at 22:55):

ah, I thought coq-hammer had all in a single repo

view this post on Zulip Paolo Giarrusso (Oct 30 2020 at 22:55):

and a single dune-project ?

view this post on Zulip Karl Palmskog (Oct 30 2020 at 22:56):

it does have everything under one dune-project

view this post on Zulip Paolo Giarrusso (Oct 30 2020 at 22:56):

exactly

view this post on Zulip Karl Palmskog (Oct 30 2020 at 22:56):

but what we want to be possible is that a user can have, say, coq-hammer-tactics installed, and then build the plugin locally - and also at the same time allow building both components from scratch (without changing the build scripts)

view this post on Zulip Paolo Giarrusso (Oct 30 2020 at 22:56):

ah, I misread

view this post on Zulip Paolo Giarrusso (Oct 30 2020 at 22:58):

I see — for now theories _forces_ building everything together, and you don't want that

view this post on Zulip Karl Palmskog (Oct 30 2020 at 22:58):

right now, if I have (theories Hammer.Tactics) then I cannot have coq-hammer-tactics installed

view this post on Zulip Emilio Jesús Gallego Arias (Oct 31 2020 at 16:16):

Great, we will try with Coq Hammer too, thanks; as of now I haven't implemented support for user-contrib yet, doing that properly is a bit annoying as you need to walk the filesystem "on-demand" as otherwise resolution could get very expensive on large installed bases, but will get to it

view this post on Zulip Emilio Jesús Gallego Arias (Oct 31 2020 at 16:16):

but indeed, at best, detecting things in user-contrib will remain, at best, a heuristic, until we move to a per-package solution

view this post on Zulip Paolo Giarrusso (Oct 31 2020 at 16:55):

I’d already be happy with not removing dune-project files

view this post on Zulip Paolo Giarrusso (Nov 28 2020 at 04:37):

Hm, I'm wondering if https://dune.readthedocs.io/en/stable/usage.html#finding-the-root means one could get compositional builds across multiple dune-project by adding a dune-workspace file... But I'm confused, since those docs spell out rules for finding dune-workspace, but the rules for dune-project are not specified and seem different?

view this post on Zulip Paolo Giarrusso (Nov 28 2020 at 04:39):

Strictly speaking, these two sentences seem contradictory:

The root of the current workspace is determined by looking up a dune-workspace or dune-project file in the current directory and parent directories.
More precisely, it will choose the outermost ancestor directory containing a dune-workspace file as root.

view this post on Zulip Théo Zimmermann (Nov 28 2020 at 15:55):

Are they? IIRC, it is always possible to drop a dune project in a subfolder of another dune project or even to combine several dune projects by putting them in multiple subfolders and creating a dune-workspace at the root.

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 01:14):

but that’s not what the text is saying

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 01:15):

The second sentence specifies, unambiguously, that the root is determined by looking up dune-workspace. Of course that’s mistaken.

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 01:15):

The first sentence uses a disjunction, and doesn’t specify the priority between dune-project and dune-workspace.

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 01:17):

Finally, I’ve composed coq builds using dune-project, but I’ve had to remove the dune-project of the inner project to make it work. I know that’s because Coq compositional builds aren’t fully supported yet, but that doesn’t help me form a mental picture.

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 01:19):

The background is me complaining that the dune manual is obscure, giving it another chance, and running into issues within the first five minutes.


Last updated: Oct 16 2021 at 09:07 UTC