Stream: Coq devs & plugin devs

Topic: Ltac2 roadmap


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

view this post on Zulip Pierre-Marie Pédrot (May 19 2020 at 11:24):

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

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

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

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

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

view this post on Zulip Paolo Giarrusso (May 20 2020 at 12:14):

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

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

view this post on Zulip 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: Oct 21 2021 at 21:03 UTC