Paolo Giarrusso (Dec 02 2021 at 21:44): Paolo Giarrusso (Dec 02 2021 at 21:44):A colleague asked if it could work (which seems hard), but I've also seen noise recently about writing Coq's own Coq rules outside the core (in dune)?
Emilio Jesús Gallego Arias (Dec 02 2021 at 21:58):What's the use case?
Emilio Jesús Gallego Arias (Dec 02 2021 at 21:58):Indeed it is hard as of now, beyond the parameters we expose
Emilio Jesús Gallego Arias (Dec 02 2021 at 21:58):Dune build language is declarative
Emilio Jesús Gallego Arias (Dec 02 2021 at 21:58):users do specify what to build
Emilio Jesús Gallego Arias (Dec 02 2021 at 21:59):not how to build it
Emilio Jesús Gallego Arias (Dec 02 2021 at 21:59):that's private to the implementation [for obvious reasons]
Emilio Jesús Gallego Arias (Dec 02 2021 at 21:59):indeed we have a coq_dune generator, that we used to port Coq, that works super well, in this scenario Dune becomes a generic low-level build system such as others that are popular
Emilio Jesús Gallego Arias (Dec 02 2021 at 22:00):we plan to ressurect it
Paolo Giarrusso (Dec 02 2021 at 22:07):The specific example was timing invocations, and recover the timing even on cached builds.
Paolo Giarrusso (Dec 02 2021 at 22:08):But more generally, I'm going to invoke the "Growing a Language" argument by Guy Steele: nobody can possibly support all use-cases of the entire community.
Emilio Jesús Gallego Arias (Dec 02 2021 at 22:08):There is always a tradeoff
Emilio Jesús Gallego Arias (Dec 02 2021 at 22:09):indeed Dune doesn't mean to support all use cases I think
Emilio Jesús Gallego Arias (Dec 02 2021 at 22:09):but timing is indeed one we should add
Paolo Giarrusso (Dec 02 2021 at 22:09):(and as it happens, there are open feature requests even for lots of standard usecases)
Emilio Jesús Gallego Arias (Dec 02 2021 at 22:09):Dune is opinionated, so it takes a particular tradeoff
Emilio Jesús Gallego Arias (Dec 02 2021 at 22:10):you can go a different route but then you lose some advantages
Emilio Jesús Gallego Arias (Dec 02 2021 at 22:10):low level rules for example hardly compose
Emilio Jesús Gallego Arias (Dec 02 2021 at 22:10):but I agree that is good to support both cases, so coq_dune should be made to the public
Emilio Jesús Gallego Arias (Dec 02 2021 at 22:10):now the problem is that I have little time to work on it for now :S
Emilio Jesús Gallego Arias (Dec 02 2021 at 22:10):hopefully we can get some help at Inria
Paolo Giarrusso (Dec 02 2021 at 22:12):is the existing code available somewhere?
Paolo Giarrusso (Dec 02 2021 at 22:19):even if it doesn't work, it might be useful as a starting point.
Emilio Jesús Gallego Arias (Dec 02 2021 at 22:20):Yes it is!
Emilio Jesús Gallego Arias (Dec 02 2021 at 22:20):It's a bit in flux tho I recommend potential users to meet with me like 30 mins so we clean it up and put it back in the Coq repos
Emilio Jesús Gallego Arias (Dec 02 2021 at 22:20):latest version is in a PR
Emilio Jesús Gallego Arias (Dec 02 2021 at 22:22):https://github.com/coq/coq/pull/13364/files
Emilio Jesús Gallego Arias (Dec 02 2021 at 22:22):here it is, under test-suite tools
Emilio Jesús Gallego Arias (Dec 02 2021 at 22:22):test_suite/tools/gen_rules
Emilio Jesús Gallego Arias (Dec 02 2021 at 22:22):sorry
Emilio Jesús Gallego Arias (Dec 02 2021 at 22:23):It is pretty easy; so we could move that to a different tree and merge it easily
Rudi Grinberg (Dec 03 2021 at 19:54):Paolo Giarrusso said:
A colleague asked if it could work (which seems hard), but I've also seen noise recently about writing Coq's own Coq rules outside the core (in dune)?
What language would you propose instead of OCaml?
Rudi Grinberg (Dec 03 2021 at 19:59):Just to expand on what Emilio is saying, dune offers more than just an engine that runs build rules. For example, dune understand what libraries are and how to resolve them in a way that works transparently for installed/local libraries. Coq would gain a lot if it reused all these tried & tested components.
Last updated: Jun 03 2023 at 17:29 UTC