Karl Palmskog (Nov 27 2020 at 08:52): Karl Palmskog (Nov 27 2020 at 08:52):@Christian Doczkal maybe we shouldn't have Dune in the reglang README after all. I was using it mainly for CI reasons (test both Dune+OPAM and coq_makefile+Nix), but this plan died with Travis limits.
Karl Palmskog (Nov 27 2020 at 08:53):a better plan might be to not advertise Dune "requirements" in mainstream projects until Dune support for Coq reaches 1.0
Christian Doczkal (Nov 27 2020 at 09:52):@Karl Palmskog Well, I set the dune flag so that the generated opam file matches the one in the repository, that also changed the generated readme. I don't get the dune "hype" anyway. So, as far as I am concerned, I'm fine with just removing the dune switch and go back to the tried and trusted make :shrug:
Karl Palmskog (Nov 27 2020 at 09:58):Dune already dominates the OCaml ecosystem, and that's when the hype starts to get real with compositional builds. Right now, I was using it to get some extra testing in CI
Karl Palmskog (Nov 27 2020 at 10:00):@Christian Doczkal do we have a merging policy for Reglang (and other stuff like comp-dec-pdl)? Do you prefer squash merges?
Christian Doczkal (Nov 27 2020 at 10:06):@Karl Palmskog , I don't think we have a policy. For small things like this I indeed have a slight preference for a linear history through squash-merges. For "interesting" changes I prefer merge commits. And for the others I am the only maintainer, so I reserve myself the right to push things directly to master if I see fit (in particular backwards-compatible build fixes mandated by changes in mathcomp), and merge other peoples PRs using merge commits :smile:
Emilio Jesús Gallego Arias (Nov 27 2020 at 16:00):Dune provides some features that make actual builds much much faster in some circumstances [and sound, which make + coq is not]
Emilio Jesús Gallego Arias (Nov 27 2020 at 16:00):So that's the main reason
Emilio Jesús Gallego Arias (Nov 27 2020 at 16:00):not so much of a hype
Emilio Jesús Gallego Arias (Nov 27 2020 at 16:01):that's just on "basic" builds, once you get to composed builds the speed difference is dramatic
Christian Doczkal (Nov 27 2020 at 16:42):@Emilio Jesús Gallego Arias I don't even know what a "composed" build is or how the choice of tool which calls coqc does affect soundness of the tool being called.
Emilio Jesús Gallego Arias (Nov 27 2020 at 16:44):Yeah, I wonder how to best document this, Coq's dune readme has some information, composed means you drop several libraries in your workspace, the build tool can wee thru library boundaries and rebuild what is needed. Soundness in this case is of the build system itself, in the sense that doing build + edit + build produces correct results. This is not the case with make as it won't for example clean correctly stale .vo files
Emilio Jesús Gallego Arias (Nov 27 2020 at 16:45):My point is that it is not a _hype_ but more of a desire to used more advanced tools with more features that actually matter a lot in some cases
Christian Doczkal (Nov 27 2020 at 16:50):Ah, don't get hung up on me calling it a "hype". There was a reason why I put this in quotes. I assumed that there are good reasons to use a build system that understands the things it is building over a generic build system like make. Still, my feeling is that this requires changing quite a few of the habits and workflows that have been established for the combination of coq and make and that at this point for a lot of people there is no real incentive disrupt their workflows by switching to dune.
Emilio Jesús Gallego Arias (Nov 27 2020 at 16:55):Change of workflow is indeed never easy, however, and keeping in mind that dune + coq is still experimental, real use data shows that there are quite a lot of incentives for a lot of users, for example those creating packages, and those using multiple libs. I'm not hung up, tho a bit puzzled on why, if you are not familiar with the new tooling and its capabilities and motivation, would make a negative judgement on it, and go as far as to assert a generalized statement about incentives when actual adoption doesn't support it
Emilio Jesús Gallego Arias (Nov 27 2020 at 17:11):Note that I don't mean the above in any negative way, I'm just trying to understand why we got so much negative feedback about Dune when it will be actually be a net gain for everyone [except me :)] , in most cases the negative feedback was actually hard to handle because the problematics pointed out were not such
Paolo Giarrusso (Nov 27 2020 at 17:59):It's been suggested multiple times that coq_makefile will be deprecated or removed, forcing migration. That's a clear cost.
Paolo Giarrusso (Nov 27 2020 at 18:01):Also, if a package author uses dune, and I'm not a dune expert, that's a learning cost on people using/developing the package.
Paolo Giarrusso (Nov 27 2020 at 18:04):simply because of the learning curve in using it.
Paolo Giarrusso (Nov 27 2020 at 18:05):E.g. opam builds with dune, and it builds correctly using the commands they give — but if I try slight variations such as dune exec opam (or IIRC dune build) I get compile errors
Paolo Giarrusso (Nov 27 2020 at 18:07):I guess that’s me using it wrong, but I haven’t been able to understand the dune manual in the time budget I had.
Emilio Jesús Gallego Arias (Nov 27 2020 at 18:41):yes there is a cost, it is normal, but there are also large benefits, so IMHO so make the discussion fair both should be pointed out
Emilio Jesús Gallego Arias (Nov 27 2020 at 18:41):in our experience, the time spent in making a package use dune, is quickly offset by the time saved in builds or packaging
Christian Doczkal (Nov 27 2020 at 19:50):@Emilio Jesús Gallego Arias I'm not sure where you see a "negative judgment" on my part. In fact, my feeling (not judgment) that "for a lot of people there is no real incentive disrupt their workflows by switching to dune" is not a contradiction to dune being of great value for a lot of other people who are more strongly affected by the shortcomings of make than the likes of me. It's just that, so far, I have not seen anyone advertise dune in such a way that I would say: "great, that's a reason for me to ditch make for Coq projects.
Paolo Giarrusso (Nov 28 2020 at 04:04):+1 to Christian; last I asked similar question, somebody eventually pointed me to a paper on selective functors, IIRC, which started answering these questions.
Paolo Giarrusso (Nov 28 2020 at 04:08):re benefits, I like dune caching and compositional builds (even the limited forms available today for Coq).
Paolo Giarrusso (Nov 28 2020 at 04:10):But you were puzzling about the “negative feedback”, so it’s not clear whether dune benefits are even on-topic.
Paolo Giarrusso (Nov 28 2020 at 04:17):from the outside, it seems that dune ranks close to other “steep-learning curve” technology — things like Nix, Bazel, Haskell, org-mode, git, sbt ... — which promise significant benefits after their steep learning curve, but which are painful if you’re not an expert.
Paolo Giarrusso (Nov 28 2020 at 04:22):(and then dune+coq is experimental enough that I wouldn’t know how to ever _switch_)
Paolo Giarrusso (Nov 28 2020 at 04:42):Of course, you Emilio are a dune expert so you're not experiencing the "novice user" scenario, and the "curse of knowledge" hides that.
Paolo Giarrusso (Nov 28 2020 at 04:46):Last: my examples promise benefits, but it's unclear if they deliver, and for some it's hard to tell. For dune at least you can measure build times (even if I haven't seen actual benchmarks), but other factors are harder to measure.
Théo Zimmermann (Nov 28 2020 at 15:51):The learning curve may be steep for advance usages, but I'm pretty confident that we should eventually be able to provide a very nice experience to Coq users, who won't have to learn much about Dune (at least for pure Coq projects), and an improved experience for users of Coq's extraction.
Théo Zimmermann (Nov 28 2020 at 15:52):In particular, it should be possible to provide a dune init coq command that will do all the basic setup you need for a new project.
Théo Zimmermann (Nov 28 2020 at 15:53):(cc @Rudi Grinberg, I'm not sure whether you're following this discussion, but you might be interested)
Karl Palmskog (Nov 28 2020 at 17:02):for a pure Coq project, it's typically easy to support both coq_makefile and Dune at the same time. Hence, the goal is to support Dune for all pure Coq projects in coq-community, whenever coq_makefile builds can be kept as-is.
Rudi Grinberg (Nov 28 2020 at 17:38):Paolo Giarrusso said:
from the outside, it seems that dune ranks close to other “steep-learning curve” technology — things like Nix, Bazel, Haskell, org-mode, git, sbt ... — which promise significant benefits after their steep learning curve, but which are painful if you’re not an expert.
What is so difficult about learning dune? The language is very high level and there's not much flexibility (as users often complain). It seems to have a much smaller surface than make or sbt. It's true that support for coq is currently in an unpolished state, but don't you think it would be pretty simple once it's fully supported?
Kenji Maillard (Nov 28 2020 at 17:43):Rudi Grinberg said:
What is so difficult about learning dune?
Vocabulary: dune defines its own concepts (workspace, targets/alias, stanza, rules, composability, ...), not all of these are easy to grasp and the dune documentation is not doing such a great job explaining pedagogically and/or extensively.
Karl Palmskog (Nov 28 2020 at 17:58):the question is how many people trying Dune out are actually reading the documentation at all. The best resource is often existing build scripts, and we don't have a ton of those for Coq at the moment.
Emilio Jesús Gallego Arias (Nov 28 2020 at 17:59):I guess my perceived negativity stems from the use of hype, that is defined as "extravagant or intensive publicity or promotion", so certainly I think using hype is not correct in our case, IMHO.
There are other advantages to dune such as dune-release which fully automates opam release, etc... but in this case it seems to boil down to the discoverability of the Dune Coq's readme and the guide in discuss; that's a pervasible problem for Coq in general, and we tried some efforts to improve it but so far without much success [mostly because lack of consensus]. Also we adopted a pretty bad transition strategy, the PR switching Coq's CI to dune has the absolute record for the PR with the most negative feedback ever.
That is not exclusive to Coq, but after this experience I cannot recommend anyone to invest time in improving Coq infrastructure. I strongly puzzles me that most of the negative feedback has come from uninformed positions [and I'm not singleing out anyone here], looks like when you get a bad paper review to me. In my view, constructive interactions work differently, for example, by first asking "hey, how can I learn Coq + Dune, is there any resource? What are the advantages? Why are you doing this?" Even looking at Coq's reference manual would solve many of these questions.
I agree with @Kenji Maillard in the Dune documentation has even taken a step back, we are aware of it and hopefully we get some cycles to improve.
Christian Doczkal (Nov 28 2020 at 19:17):Okay, let me try to be at least a little bit constructive and report on my impression after readingthe guide on discuss:
This guide contains literally nothing that I can relate to. I use Coq for pure library development on top of published stable libraries that I install via opam. I do not want to care about how those libraries are built and it would never occur to me to dump my files into their folders or vice-versa. So, I see no use for myself for compositional builds (from the little I understand about them) nor for linking to C. And I have no idea what the other features are, the guide doesn't tell.
In fact, I finally got used to separating my build infrastructure (Makefile, _CoqProject, etc.) from the theory files (theories/*.v) and now the guide tells me I must put the dune file into the theories folder. That makes me balk just a little.
Also, my understanding is that all IDEs for Coq require a _CoqProject file for theory development. Once I have that, and a very generic Makefile, I literally just have to invoke make and start/continue developing. So, please tell me, which part of my workflow, if any, would be simplified by using dune?
(For CI and opam publishing I fill out a meta.yml and then just run generate.sh from https://github.com/coq-community/templates/)
I also searched for dune in the Coq manual, and found the Building a Coq Project with Dune section. It's starts with two warnings: It's experimental, please look at the upstream documentation; the link goes to huge "wall of text" table of contents that I closed immediately. And the rest of the section just pales in comparison to all the features advertised by the "Building with coq_makefile" section just above.
Rudi Grinberg (Nov 28 2020 at 20:46):Kenji Maillard said:
Rudi Grinberg said:
What is so difficult about learning dune?
Vocabulary: dune defines its own concepts (workspace, targets/alias, stanza, rules, composability, ...), not all of these are easy to grasp and the dune documentation is not doing such a great job explaining pedagogically and/or extensively.
While there's a lot of concepts, you don't need to know anything about them until you need to use them. I'd like to work improve the documentation, so if there are any specific concepts that aren't well explained, I'd be happy to rewrite the sections.
Rudi Grinberg (Nov 28 2020 at 20:50):@Christian Doczkal If you don't like it, there's actually no need to write separate dune files anymore. You can move your dune file to the top of your project and then surround everything and use the subdir stanza: (subdir theories/ <contents of dune file>).
Gaëtan Gilbert (Nov 28 2020 at 20:52):unquoted dir name?
Rudi Grinberg (Nov 28 2020 at 20:53):Gaëtan Gilbert said:
unquoted dir name?
If there's no spaces in the path, quotes are not necessary.
Rudi Grinberg (Nov 28 2020 at 20:54):@Christian Doczkal how well does the generic makefile support mixed ocaml/coq projects? E.g. there's a coq plugin written in OCaml.
Karl Palmskog (Nov 28 2020 at 21:03):Dune has an edge in supporting extraction-based OCaml projects. They can be done with makefiles, but very hacky and hard to maintain. However, this is not a use case he considered, as per above
Karl Palmskog (Nov 28 2020 at 21:09):@Rudi Grinberg is "one dune file at the root" the recommended way to organize a project now? I thought it made sense to have different dune files in the codebase to separate concerns, etc.
Rudi Grinberg (Nov 28 2020 at 21:19):Karl Palmskog said:
Dune has an edge in supporting extraction-based OCaml projects. They can be done with makefiles, but very hacky and hard to maintain. However, this is not a use case he considered, as per above
Yeah, I think that's the most convincing reason to use dune today. If there's extraction or a plugin written in OCaml, dune probably works better. Otherwise, there's not much advantage.
Rudi Grinberg (Nov 28 2020 at 21:20):Karl Palmskog said:
Rudi Grinberg is "one
dunefile at the root" the recommended way to organize a project now? I thought it made sense to have differentdunefiles in the codebase to separate concerns, etc.
I still prefer separate dune files. If nothing else, it allows you to move and rename directories freely. subdir is mostly useful when generating dune files. But I also know that some people prefer to keep the build files in one place.
Karl Palmskog (Nov 28 2020 at 21:25):another not-so-obvious reason to bet on Dune going forward: it will likely receive many more maintenance engineering hours than coq_makefile could ever hope for. But I think we need to have both Coq+Dune 1.0 and Dune as part of the Coq platform (audited/sanctioned Dune releases for Coq stable releases) to win people over.
Karl Palmskog (Nov 28 2020 at 21:37):right now, Dune 2.5 is already by default in all Coq Docker images, so no cost to use it there, for example
Rudi Grinberg (Nov 28 2020 at 21:41):Would it help users if dune generated _CoqProject files?
Karl Palmskog (Nov 28 2020 at 21:44):right now, since most projects are using coq_makefile or homegrown makefiles, most have already written _CoqProjectmanually. The main use case I see is when people migrate fully to Dune and don't want one more metadata file to keep track of
Gaëtan Gilbert (Nov 28 2020 at 21:46):ides understanding dune files without _coqproject would work too
Rudi Grinberg (Nov 28 2020 at 21:50):Gaëtan Gilbert said:
ides understanding dune files without _coqproject would work too
It would be quite hard for the IDE's to follow dune's frontend I think. With OCaml, we have dune generating something that tools can understand (.merlin files).
Rudi Grinberg (Nov 28 2020 at 21:51):Though we've in the process of removing .merlin files in favor of merlin querying dune direclty for this information. It's still essentially the same metadata however.
Karl Palmskog (Nov 28 2020 at 21:52):I think the ideal is something similar to for merlin, i.e., IDEs simply query Dune instead of having a file format as middle man
Karl Palmskog (Nov 28 2020 at 21:53):what worries me is that ProofGeneral now even has its own build system, so we get even more fracturing
Emilio Jesús Gallego Arias (Nov 28 2020 at 22:06):For me, the 3 key advantages for the Coq user are:
Emilio Jesús Gallego Arias (Nov 28 2020 at 22:07):Legacy IDEs should use dune coqtop , more modern ones should just talk to the LSP server
Emilio Jesús Gallego Arias (Nov 28 2020 at 22:08):For the Coq developer, there are so many advantages even with the current state that I can just skip them, on the order of dozen of hours likely saved per month of bulid time
Emilio Jesús Gallego Arias (Nov 28 2020 at 22:08):Also, the dune coq.theory language is much easier to use than _CoqProject, at many levels
Rudi Grinberg (Nov 28 2020 at 22:11):Emilio Jesús Gallego Arias said:
Legacy IDEs should use
dune coqtop, more modern ones should just talk to the LSP server
What's dune coqtop? :)
Karl Palmskog (Nov 28 2020 at 22:12):the dune-release advantage is not great at the moment, since one is setting up packages to become unusable in the future (as (coq 0.2) becomes unsupported)
Emilio Jesús Gallego Arias (Nov 28 2020 at 22:27):What's dune coqtop? :)
Hopefully the dune utop equivalent for Coq, that's an easy way to start an interactive session, hope to submit the PR soon.
the dune-release advantage is not great at the moment, since one is setting up packages to become unusable in the future (as (coq 0.2) becomes unsupported)
Indeed that would require adding an upper bound on dune, we still need to see how much we will support that version. Maybe it can be supported long-term? I dunno, but you are right.
Rudi Grinberg (Nov 28 2020 at 22:29):Is it easy to maintain support for 0.2? It can certainly be done if it's not adding much overhead, no?
Emilio Jesús Gallego Arias (Nov 28 2020 at 22:34):Rudi Grinberg said:
Is it easy to maintain support for 0.2? It can certainly be done if it's not adding much overhead, no?
I think so, however I preferred to err on the cautious side and not commit to an specific support timeframe yet, until we hit 1.0. It is a pity that we didn't hit 1.0 indeed as there is not a lot to do, but unfortunately I've been too busy to submit the few remaining patches, basically compositionality, but my branch looks almost ready.
Rudi Grinberg (Nov 28 2020 at 23:05):Emilio Jesús Gallego Arias said:
Rudi Grinberg said:
Is it easy to maintain support for 0.2? It can certainly be done if it's not adding much overhead, no?
I think so, however I preferred to err on the cautious side and not commit to an specific support timeframe yet, until we hit 1.0. It is a pity that we didn't hit 1.0 indeed as there is not a lot to do, but unfortunately I've been too busy to submit the few remaining patches, basically compositionality, but my branch looks almost ready.
Aren't coq builds already compositional? IIRC, it's installed libraries that don't work?
Emilio Jesús Gallego Arias (Nov 29 2020 at 00:00):We are missing the inter-scope public libraries registration, but I have a tree that should do the job. For the installed ones, we need a lazy lookup of user-contrib that I didn't write yet, but should be doable
Paolo Giarrusso (Nov 29 2020 at 01:27):@Christian Doczkal re compositional builds, maybe you don’t need them — but they are helpful for anybody who needs coordinated changes across multiple repositories. Say you add a missing lemma to a dependency and want to then use it. With coq_makefile, you’d patch the dependency, do a new build, then run make clean in your library because none of the results can be trusted, and _then_ recompile your library from scratch. A combined build can try to reuse much more work.
Rudi Grinberg (Nov 29 2020 at 01:36):Emilio Jesús Gallego Arias said:
We are missing the inter-scope public libraries registration, but I have a tree that should do the job. For the installed ones, we need a lazy lookup of
user-contribthat I didn't write yet, but should be doable
I might give reading user-contrib a try if you're busy. Is it straightforward?
Paolo Giarrusso (Nov 29 2020 at 01:42):Rudi Grinberg said:
While there's a lot of concepts, you don't need to know anything about them until you need to use them. I'd like to work improve the documentation, so if there are any specific concepts that aren't well explained, I'd be happy to rewrite the sections.
That doesn't match my experience — e.g. when building opam, I made the mistake of using dune build instead of dune build --profile=release --promote-install-files opam-installer.install opam.install, and then I got 40 lines of compile errors. In fact, not even that — I built the code correctly, then used dune exec -- opam list and got the compile errors.
Paolo Giarrusso (Nov 29 2020 at 01:46):I'm happy to cargo-cult all those options, but I have no idea what's going on, which for me would never happen with make.
Paolo Giarrusso (Nov 29 2020 at 01:51):(Admittedly, that's because I've read the entire manual of GNU make ages ago, but that's a valid use case)
Christian Doczkal (Nov 29 2020 at 10:21):Paolo Giarrusso said:
Say you add a missing lemma to a dependency and want to then use it. With coq_makefile, you’d patch the dependency, do a new build, then run
make cleanin your library because none of the results can be trusted, and _then_ recompile your library from scratch. A combined build can try to reuse much more work.
If I understand correctly, this requires that your dependency is (a) completely under your control and (b) does not observe a code reviewing discipline, and (c) you don't care whether your code compiles with stable releases of your dependency. My main dependency is mathcomp. So when I notice a lemma (or a collection thereof) is missing, I prove them locally and then create a PR. Between the creation of the PR and its merging, there is usually multiple code review cycles, often including renamings and changes to the statement. So this might run over the course of a week or more, and will then get included in the next bi-annual release. Once the PR is merged, I can adapt the local lemmas to match those that were merged and I remove them once I drop support for the oldest stable release that does not contain them. With two supported versions of mathcomp, that's 6 to 12 months later.
The only times I build coq, mathcomp, and then my own code in order is when updating my opam dev switch in order to understand CI failures for the dev branch. This happens maybe every month or two, so there are always changes to coq itself, after which one presumably should rebuild everything. So I'm not sure whether compositional builds would help here or not.
Christian Doczkal (Nov 29 2020 at 10:25):What would be nice if there was a way to keep separate the generated files from different opam switches, so that one would not always have to go though a make clean; make when switching between dev and stable (without having multiple local working copies, that is).
Paolo Giarrusso (Nov 29 2020 at 12:35):(c) is required, but (a) and (b) aren’t, as long as it makes sense to write a patch to your code before the upstream code is merged. But most examples I have in mind do involve coordinated ownership.
Paolo Giarrusso (Nov 29 2020 at 12:36):On “different opam switches”, build profiles _might_ be helpful there.
Paolo Giarrusso (Nov 29 2020 at 12:38):(and build caching certainly is, AFAICS)
Paolo Giarrusso (Nov 29 2020 at 12:39):Another point for compositional builds is that, actually, you might not need rebuild the whole of coq and math-comp to build your library, even if they are from different maintainers. Just build your library and whatever’s needed. The size of savings is, again, variable.
Christian Doczkal (Nov 29 2020 at 12:51):Yes, I suppose the savings are non-existent if your own preliminaries file imports files like all_ssreflector all_algebra, etc. If I understand correctly, this turns these files into synchronization barriers. :shrug:
Paolo Giarrusso (Nov 29 2020 at 12:54):Yeah. Compositional builds AFAIK resemble merging all the _CoqProject files together.
Emilio Jesús Gallego Arias (Nov 29 2020 at 16:11):Indeed dune documentation needs work, hopefully we get to work on it a bit more. Used to be better with a concrete section for Coq users in the manual, but it was merged into the stanza reference. Note that we have termed dune support experimental, as to give a warning to users, that doesn't mean it doesn't have advantages. Relative to the questions above:
make clean; make: this already works. dune will track correctly the dependency on coqc and rebuild if coqc has changed, no more make cleanneeded. This is what we mean about "soundness" of the build. Moreover, if you enable the cache build artifacts are globally re-used.all_ssreflect etc are not a big problem, as the dependencies are correctly tracked, so if you update seq.v only that file and all_ssreflect will be build, that is true tho that if the hash of all_ssreflect changes, all their deps will be rebuilt. There is ongoing to work to address that but will require more granularity.The point is that if you are using dune you just do dune build [or make if you use a template that will call it] and you don't have to worry about it. Other useful feature is simultaneous compilation w.r.t. several switches, so you can tell dune, "hey, build everything against both Coq 8.11 and Coq 8.12", by using opam switches.
Emilio Jesús Gallego Arias (Nov 29 2020 at 16:13):On key point of dune is that doing dune build @check is so fast [and correct] that you don't worry about it. Coq still needs more work as to enable the skip of proofs in that mode for example, but we will get there. As a reference, for the OCaml part, I have bound M-c in emacs to the @check target and it usually checks all my ML Coq code + plugins in a second [due to fast build mode]
Emilio Jesús Gallego Arias (Nov 29 2020 at 16:14):Other things that are correctly tracked are for example cmdline flags to both OCaml and Coq, etc... So for example if you use two switches as @Christian Doczkal proposed, you quickly have net time savings.
Christian Doczkal (Nov 29 2020 at 16:38):Emilio Jesús Gallego Arias said:
Other useful feature is simultaneous compilation w.r.t. several switches, so you can tell dune, "hey, build everything against both Coq 8.11 and Coq 8.12", by using opam switches.
So after almost two days of exchanging messages about dune you have finally managed to mention a feature of dune that seems useful enough to me to get me interested. :tada:
I just wish that I could find any documentation on this feature, the "OPAM integration" section of the dune manual says nothing about this and neither does the scarce documentation on the Coq side.
Emilio Jesús Gallego Arias (Nov 29 2020 at 16:43):[but indeed see my comments about the doc, all this got inlined in dune-files so it is hard to find]
So after almost two days of exchanging messages about dune you have finally managed to mention a feature of dune that seems useful enough to me to get me interested.
You only had to ask :D , there are too many differences as to be able to make a synthetic summary of make vsdune. Build systems à la carte makes a good overview of the fundamentals.
For example, if you use more than one opam switch you will see large gains from dune + cache, and will have the peace of mind of not having to ask when to run make clean
Emilio Jesús Gallego Arias (Nov 29 2020 at 16:49):Note that for two opam switches there are two dual setups:
--workspace option to use the file only when you want to do the 2 builds. Christian Doczkal (Nov 29 2020 at 17:03):@Emilio Jesús Gallego Arias thanks for the pointers. I suppose these "dual" setups are not mutually exclusive. So assuming I have a workspace with 2-3 switches, one of them also being the currently active opam switch, and I run dune build --workspace .... Will the build for the current switch be separate from a normal build, or will it be the same? And if one of the builds for non-active switches fails, how do I get an Emacs/PG in the same context to see why the build failed and fix it? (I'm thinking about the rare but annoying task of creating backward-compatible fixes for changes in dependencies.)
Paolo Giarrusso (Nov 29 2020 at 17:03):syncronization barrier: all_ssreflect etc are not a big problem, as the dependencies are correctly tracked, so if you update seq.v only that file and all_ssreflect will be build, that is true tho that if the hash of all_ssreflect changes, all their deps will be rebuilt. There is ongoing to work to address that but will require more granularity.
Won't I get extra spurious dependencies if I import all_ssreflect instead of a specific file? My scenario was "you import ssreflect.a, ssreflect.b changes, no rebuild needed"? Deducing that .b is unused seems pretty hard when accounting for typeclasses/canonical structures/other global side effects.
Paolo Giarrusso (Nov 29 2020 at 17:06):e.g., even if ssreflect.b is never mentioned in the client, changes to ssreflect.b can still require recompiling the client:ssreflect.b could use Remove Hint, or add a new Hint that has higher precedence, or change a global flag, or Require a new module that does any of those things.
Emilio Jesús Gallego Arias (Nov 29 2020 at 17:09):@Christian Doczkal , they are not, but there is the default context, that will track your current opam , so what you get is _build/default and _build/context1 etc... so YMMV. Integration of this with PG etc... leaves quite a lot to be desired, well, it is not existent at the moment as nobody found the cycles to do it. Best is to just use tell PG to use _build/default using _CoqProject.
Emilio Jesús Gallego Arias (Nov 29 2020 at 17:10):I already have a bit of elisp that tells PG to use a particular coq version, so indeed it wouldn't be difficult at all, just nobody found the time.
Emilio Jesús Gallego Arias (Nov 29 2020 at 17:11):@Paolo Giarrusso dependencies are tracked on a per-file hash, so indeed, if you import all_ssreflect you likely will hit a large rebuild.
Emilio Jesús Gallego Arias (Nov 29 2020 at 17:12):But we are working on making that more granular, so we can see across Exports for example.
Christian Doczkal (Nov 29 2020 at 17:16):Well, I guess this just makes me complain some more about the lack of documentation. The _CoqProject file is necessary for IDEs and coq_makefile (with the information required by the latter subsuming the former). Unfortunately, neither the dune manual nor the section on dune in the Coq manual mentions the _CoqProject file. :sad:
Christian Doczkal (Nov 29 2020 at 17:24):But can't one do something with opam --switch <something> exec emacs ... to get an Emacs to run in one of the "other" switches, possibly passing an option to emacs (via something placed in .emacs) to enable emacs to use the right build subdirectory?
Paolo Giarrusso (Nov 29 2020 at 19:51):This point is unfortunately only documented in IDE issues, and it’s probably one reason for the “experimental” marker. But it does seem like dune <options> exec <show prefix> might work, when all that must happen is prepend a path to the one in _CoqProject.
Paolo Giarrusso (Nov 29 2020 at 19:54):I’m sure it’s not a 100% solution, but I’ve never run into a scenario where it’d cause trouble.
Rudi Grinberg (Nov 29 2020 at 22:14):@Emilio Jesús Gallego Arias do you recall why coq was moved to a separate section in the docs? that doesn't make sense to me.
Emilio Jesús Gallego Arias (Nov 29 2020 at 22:33):@Rudi Grinberg you mean moved to or from?
Rudi Grinberg (Nov 29 2020 at 22:37):Yes, I meant from, sorry. It doesn't make sense to me to merge docs for coq and ocaml
Emilio Jesús Gallego Arias (Nov 29 2020 at 22:37):It was done in the manual rework PR a few releases ago.
Emilio Jesús Gallego Arias (Nov 29 2020 at 22:38):Yeah I also found it a step backwards.
Théo Zimmermann (Dec 01 2020 at 16:39):This PR of mine was a reaction to that change: https://github.com/ocaml/dune/pull/2601
It also links to the PR that did the documentation rework.
Rudi Grinberg (Dec 02 2020 at 22:20):Théo Zimmermann said:
This PR of mine was a reaction to that change: https://github.com/ocaml/dune/pull/2601
It also links to the PR that did the documentation rework.
What do you think of writing a coq chapter in the dune manual? I think that we'd benefit quite a bit from a section that is written from the coq user's point of view. Unfortunately, I don't have the background to write such a thing.
Emilio Jesús Gallego Arias (Dec 02 2020 at 22:57):We have some bits already in Coq's manual an in a discourse post, also the documentation of dune previous versions had an entry https://github.com/ocaml/dune/blob/1.9.1/doc/coq.rst
Paolo Giarrusso (Dec 02 2020 at 23:20):Coq chapter in the dune manual?
Agreed — part of the target audience doesn't really know much about OCaml, or OCaml-at-scale
Last updated: Jun 03 2023 at 17:29 UTC