Paolo Giarrusso (Sep 15 2020 at 09:40): 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?
Emilio Jesús Gallego Arias (Sep 15 2020 at 16:05):Indeed, this is still lacking, but it is a high priority feature.
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?
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.
Paolo Giarrusso (Sep 16 2020 at 19:25):ah. mapping foo.bar to user-theories/foo/bar might not be general.
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
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
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
Paolo Giarrusso (Sep 17 2020 at 07:55):“won’t be compatible with coq_makefile” where’s the roadmap for ever deprecating coq_makefile?
Paolo Giarrusso (Sep 17 2020 at 07:56):my questions in the last few days amount to significant objections.
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?
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:
copy_files -R is already hard (I don’t get why)I’m sure there are reasons, and I asked about them a few days ago (after all, I also use dune)...
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.
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
Paolo Giarrusso (Sep 17 2020 at 08:15):and not just resistance by inertia
Paolo Giarrusso (Sep 17 2020 at 08:16):but I’m sure @Théo Zimmermann appreciates the complexities of these “community” decisions :-)
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.
Paolo Giarrusso (Sep 17 2020 at 08:19):appreciate as in “understand well”, but I had a typo (now fixed) :-)
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:
- no programming at all in dune (except by generating dune files as text)
- no programming in OCaml except through upstream patches
- no parametric rules
- somehow
copy_files -Ris already hard (I don’t get why)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.
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
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.
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)
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
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
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
Thanks for motivating the design. That makes sense for the coq part. However, I have a program that generates .v files; now what?
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).
Karl Palmskog (Sep 17 2020 at 20:06):@Paolo Giarrusso example of .v generation: https://github.com/palmskog/fitch/blob/master/coq/dune
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
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
Paolo Giarrusso (Sep 17 2020 at 20:09):in any case, there is no need to trade off declarative builds against extensibility.
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)
Paolo Giarrusso (Sep 17 2020 at 20:09):sure, that’s indeed the workaround :-)
Karl Palmskog (Sep 17 2020 at 20:10):PL researchers trade extensibility against predictability/guarantees all the time, arguably
Paolo Giarrusso (Sep 17 2020 at 20:10):you can have an extensible system that lets you implement declarative tasks, but also extensions.
Paolo Giarrusso (Sep 17 2020 at 20:11):indeed, you have tradeoffs in e.g. how dynamic your dependencies can be.
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.
Paolo Giarrusso (Sep 17 2020 at 20:12):@Karl Palmskog my basic answer is “Growing a language”
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 :-)
Karl Palmskog (Sep 17 2020 at 20:13):plenty of examples of successful languages that haven't grown much, if at all
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
Karl Palmskog (Sep 17 2020 at 20:14):non-success-story of growing something: browser extensions
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.
Karl Palmskog (Sep 17 2020 at 20:16):so I disagree about the general qualitative argument that "extensions should (always) be possible"
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
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
Paolo Giarrusso (Sep 17 2020 at 20:17):maybe there could be progress on what makes sense in this example.
Paolo Giarrusso (Sep 17 2020 at 20:18):and some of the limitations don’t seem about extensibility either.
Paolo Giarrusso (Sep 17 2020 at 20:18):but is the plan for dune to _not_ offer support for plugins?
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.
Paolo Giarrusso (Sep 17 2020 at 20:19):I didn’t say “system software”
Paolo Giarrusso (Sep 17 2020 at 20:20):I didn’t say that either
Karl Palmskog (Sep 17 2020 at 20:20):I was giving an example what the argument could look like
Paolo Giarrusso (Sep 17 2020 at 20:20):users of programming languages (which include build languages) will need to have custom extensions
Paolo Giarrusso (Sep 17 2020 at 20:20):some could go into the language, but some don’t make sense for all users.
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.
Karl Palmskog (Sep 17 2020 at 20:22):if you allow full programmability inside Dune in OCaml, what can you guarantee?
Paolo Giarrusso (Sep 17 2020 at 20:23):I’m not necessarily attached to plugins.
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.
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.
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
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...
Paolo Giarrusso (Sep 17 2020 at 20:25):what _are_ the usual Dune properties?
Paolo Giarrusso (Sep 17 2020 at 20:26):I’ve asked, a while ago, for a design rationale
Paolo Giarrusso (Sep 17 2020 at 20:26):you’ve explained a bit more now, but I’ve never seen a design document.
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
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?
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.
Paolo Giarrusso (Sep 17 2020 at 20:28):I do ask that coq_makefile is left alive
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)
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
Paolo Giarrusso (Sep 17 2020 at 20:30):good to hear that — that wasn’t clear above :-)
Karl Palmskog (Sep 17 2020 at 20:30):Coq project build practice evolution is extremely slow
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?
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
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.
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
Paolo Giarrusso (Sep 17 2020 at 20:36):that doesn’t seem evidence that abstraction mechanisms in dune scripts prevent its goals.
Paolo Giarrusso (Sep 17 2020 at 20:37):there’s a gulf between arbitrary computations, and no abstraction.
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.)
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”
Paolo Giarrusso (Sep 17 2020 at 20:39):Well! There are tons of build systems with various amounts of programmability, and tradeoffs between them.
Paolo Giarrusso (Sep 17 2020 at 20:39):up to now, I don’t think dune has _specific_ problems preventing extensions.
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.
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.
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)
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
Karl Palmskog (Sep 17 2020 at 21:16):I guess they might be like ad-hoc axioms in Coq... caveat emptor
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.
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.
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.
Paolo Giarrusso (Sep 17 2020 at 21:20):_ahem_
Paolo Giarrusso (Sep 17 2020 at 21:20):Dhall is based on the Calculus of Constructions, apparently.
Paolo Giarrusso (Sep 17 2020 at 21:21):and a normalizer.
Rudi Grinberg (Sep 17 2020 at 21:21):Yeah, dhall is good. The dependency tree is massive though
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.
Paolo Giarrusso (Sep 17 2020 at 21:22):but luckily, I think a few of its authors are available around here.
Paolo Giarrusso (Sep 17 2020 at 21:23):;-)
Karl Palmskog (Sep 17 2020 at 21:23):ahhh, configuration languages. Has anyone theoretically justified them yet?
Rudi Grinberg (Sep 17 2020 at 21:23):To contrast with dhall, check out bazel's skylarg language. :sick:
Karl Palmskog (Sep 17 2020 at 21:24):"inspired by Python3" :fear:
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 :-)
Rudi Grinberg (Sep 17 2020 at 21:25):With good error messages :)
Paolo Giarrusso (Sep 17 2020 at 21:25):just Gallina, a normalizer, and convenient primitives to write configurations
Paolo Giarrusso (Sep 17 2020 at 21:25):ohohohoh, shots fired :-)
Karl Palmskog (Sep 17 2020 at 21:25):what do they use dependent types for?
Paolo Giarrusso (Sep 17 2020 at 21:26):good question, no clue!
Paolo Giarrusso (Sep 17 2020 at 21:26):guess they wanted something powerful and non-Turing complete
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.
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
Paolo Giarrusso (Sep 17 2020 at 21:26):and oh, well, GADTs without hacks
Emilio Jesús Gallego Arias (Oct 30 2020 at 15:51):@Paolo Giarrusso I have a prototype ready for a PR
Emilio Jesús Gallego Arias (Oct 30 2020 at 15:51):to be included in Dune 2.8
Emilio Jesús Gallego Arias (Oct 30 2020 at 15:51):let me know if you would be interested in testing
Paolo Giarrusso (Oct 30 2020 at 22:42):Hey! I'm slightly swamped, but I am still interested
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.
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
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)
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)
Paolo Giarrusso (Oct 30 2020 at 22:50):@Karl Palmskog I'm a bit confused by that issue, I _do_ use theories
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
Paolo Giarrusso (Oct 30 2020 at 22:51):okay, not sure about that
Karl Palmskog (Oct 30 2020 at 22:51):so hopefully this is something Emilio will test
Paolo Giarrusso (Oct 30 2020 at 22:52):right now I _can_ use theories but only inside a single dune-project
Paolo Giarrusso (Oct 30 2020 at 22:53):but I still understand very little of dune :-|, sadly (time is what it is)
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
Paolo Giarrusso (Oct 30 2020 at 22:55):ah, I thought coq-hammer had all in a single repo
Paolo Giarrusso (Oct 30 2020 at 22:55):and a single dune-project ?
Karl Palmskog (Oct 30 2020 at 22:56):it does have everything under one dune-project
Paolo Giarrusso (Oct 30 2020 at 22:56):exactly
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)
Paolo Giarrusso (Oct 30 2020 at 22:56):ah, I misread
Paolo Giarrusso (Oct 30 2020 at 22:58):I see — for now theories _forces_ building everything together, and you don't want that
Karl Palmskog (Oct 30 2020 at 22:58):right now, if I have (theories Hammer.Tactics) then I cannot have coq-hammer-tactics installed
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
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
Paolo Giarrusso (Oct 31 2020 at 16:55):I’d already be happy with not removing dune-project files
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?
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.
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.
Paolo Giarrusso (Nov 29 2020 at 01:14):but that’s not what the text is saying
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.
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.
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.
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 13 2024 at 01:02 UTC