Stream: Coq devs & plugin devs

Topic: Ltac2 roadmap

Kenji Maillard (May 18 2020 at 13:48):

I was wondering if there was a global roadmap for Ltac2 (by which I mean something written down and not only inside @Pierre-Marie Pédrot 's head ;) ). There are a few places where I would like to contribute but I'm not too sure how to proceed, for now I'm listing a few of those below.

• Documentation of Ltac2 is somewhat lacking: it often makes reference to some implicit knowledge about its ideal model (operational semantics, behaviour of the "tactic monad" see #12261 , what is effectful or not e.g. taking a reference to a toplevel globally defined Coq constant is effectful see #11086).
• There are quite a few extensions/feature requests (views for intro-patterns, deep pattern-matching...) that users are waiting for (Ltac2 is still quite new and barebone)
• In a slightly more exotic direction, mixing ssr-style with Ltac2 seems currently quite a dangerous task: are there ideas on how to proceed to lessen the gap ?

Pierre-Marie Pédrot (May 19 2020 at 11:24):

I currently don't have any clear roadmap, at most a few TODOs.

Pierre-Marie Pédrot (May 19 2020 at 11:24):

Ltac2 needs polishing and library development, but this is a task that is better performed by its power users I believe.

Théo Zimmermann (May 19 2020 at 14:08):

There needs to be a roadmap about how to make accessible all built-in tactics without having to wait for a user to request one after the other.

Théo Zimmermann (May 19 2020 at 14:09):

We talked about having a tactics plugin defining some syntax and independent of Ltac / Ltac2. Is this something realistic?

Paolo Giarrusso (May 20 2020 at 12:13):

Relevantly, many power users (or at least, stdpp/Iris, not sure for others) need/want to support multiple Coq releases — so if extensions to the library can be implemented in an external library that needn’t depend on a specific Coq version, that’d be cool.

Paolo Giarrusso (May 20 2020 at 12:14):

(To the extent that’s possible without much extra effort, of course)

Paolo Giarrusso (May 20 2020 at 12:24):

In turn, such questions affect how quickly Ltac2 is tried out by early adopters, bugs are reported, and so on. I guess these sorts of software engineering/ecosystem management are close to Théo’s research interests, tho I don’t know of specifically applicable research...

Ralf Jung (May 22 2020 at 07:40):

Relevantly, many power users (or at least, stdpp/Iris, not sure for others) need/want to support multiple Coq releases

in particular, so far we are using ltac2 just in an experiment. but already then we realized that there was a breaking change between Coq 8.10 and Coq 8.11 in a way that we cannot make that experiment compatible with both versions. before we use ltac2 in Iris master, we'll have to figure out some way to ensure that we remain cross-coq-version-compatible.

Last updated: Jun 08 2023 at 04:01 UTC