Ralf Jung (Dec 16 2020 at 17:34): Ralf Jung (Dec 16 2020 at 17:34):Hi all, in particular @Pierre-Marie Pédrot,
we'd like to start using Ltac2 in Iris. As a start, we just plan to use it to convert between idents and strings, but more may follow.
However, since Iris is on Coq's CI, this means that breaking changes to the ltac2 interface we use will fail Coq's CI. And since Iris commits to supporting at least the two most recent stable versions of Coq, we cannot land any change that wouldn't work on those versions. What should we take into account when using Ltac2? Is there a subset that is deemed "stable enough" so that we can use it without causing problems for future Ltac2 development?
You can see the code we want to land at https://gitlab.mpi-sws.org/iris/string-ident/-/blob/master/theories/ltac2_string_ident.v
Cc @Robbert Krebbers @Tej Chajed
Théo Zimmermann (Dec 16 2020 at 18:29):This is great news! Without having active users of Ltac2 in CI, it's harder to guarantee any kind of strong compatibility, so this should help a lot toward stabilizing Ltac2.
Théo Zimmermann (Dec 16 2020 at 18:31):AFAIU the high-level API should be mostly stable and it's only the low-level stuff that may not be so.
Ralf Jung (Dec 16 2020 at 19:15):are the APIs we are using considered high-level or low-level?
Théo Zimmermann (Dec 16 2020 at 19:27):That's the important question, I guess, but I'm not qualified to answer.
Pierre-Marie Pédrot (Dec 16 2020 at 19:34):I think most functions are somewhat stable, excepted the low-level term functions that are exported in Unsafe.
Pierre-Marie Pédrot (Dec 16 2020 at 19:34):From these, one should design a higher-level, more robust API.
Pierre-Marie Pédrot (Dec 16 2020 at 19:34):Hopefully the reliance on Ltac2 will help carving out what is needed.
Ralf Jung (Dec 16 2020 at 20:52):we used to use Unsafe before https://gitlab.mpi-sws.org/iris/string-ident/-/commit/16282df9bc695311322b277757855e1cdc5a4cc3 but Tej managed to avoid it
Ralf Jung (Dec 16 2020 at 20:52):and I guess this means we'll not add code to Iris that uses Unsafe
Last updated: Apr 18 2024 at 22:02 UTC