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.
I currently don't have any clear roadmap, at most a few TODOs.
Ltac2 needs polishing and library development, but this is a task that is better performed by its power users I believe.
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.
We talked about having a tactics plugin defining some syntax and independent of Ltac / Ltac2. Is this something realistic?
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.
(To the extent that’s possible without much extra effort, of course)
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...
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: Dec 05 2023 at 06:01 UTC