Stream: Dune devs & users

Topic: Customizing Coq rules without OCaml code


view this post on Zulip 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)?

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 21:58):

What's the use case?

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 21:58):

Indeed it is hard as of now, beyond the parameters we expose

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 21:58):

Dune build language is declarative

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 21:58):

users do specify what to build

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 21:59):

not how to build it

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 21:59):

that's private to the implementation [for obvious reasons]

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 22:00):

we plan to ressurect it

view this post on Zulip Paolo Giarrusso (Dec 02 2021 at 22:07):

The specific example was timing invocations, and recover the timing even on cached builds.

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 22:08):

There is always a tradeoff

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 22:09):

indeed Dune doesn't mean to support all use cases I think

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 22:09):

but timing is indeed one we should add

view this post on Zulip Paolo Giarrusso (Dec 02 2021 at 22:09):

(and as it happens, there are open feature requests even for lots of standard usecases)

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 22:09):

Dune is opinionated, so it takes a particular tradeoff

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 22:10):

you can go a different route but then you lose some advantages

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 22:10):

low level rules for example hardly compose

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 22:10):

hopefully we can get some help at Inria

view this post on Zulip Paolo Giarrusso (Dec 02 2021 at 22:12):

is the existing code available somewhere?

view this post on Zulip Paolo Giarrusso (Dec 02 2021 at 22:19):

even if it doesn't work, it might be useful as a starting point.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 22:20):

Yes it is!

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 22:20):

latest version is in a PR

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 22:22):

https://github.com/coq/coq/pull/13364/files

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 22:22):

here it is, under test-suite tools

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 22:22):

test_suite/tools/gen_rules

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 22:22):

sorry

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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: Feb 04 2023 at 02:03 UTC