Add coq-autosubst to the platform

[haselwarter]

It could be useful to have Autosubst integrated in the platform. CC the maintainers: @RalfJung @co-dan

Autosubst is quite stable, and is used in various Iris developments. Ensuring that there are releases of the library (not "dev") that are compatible with current versions of Coq should be easy enough, and would help keeping these Iris developments updated.

Would this make sense?

[palmskog]

For reference, Autosubst is a pure Coq library that lives in Coq-community, where it has been maintained for the last few years.

[MSoegtropIMC]

There is a board which takes such decisions, but I don't see a good reason for not adding it.

Indeed adding it to Coq Platform should help to avoid the issue that it is not updated to latest Coq in due time discussed on Zulip today.

[MSoegtropIMC]

Out of curiosity: might this be useful to prove the context handling lemmas for reflexive tactics? Essentially one has already introduced context variables, properties of these, not yet introduced forall variables and properties of these and needs to reason about introduction and generalisation of variables, swapping the order of variables, swapping the order of premises and the like. I find proving such things quite annoying ...

[RalfJung]

No objections from my side, but I can't promise to have the time to do new autosubst releases after each Coq reease.

[MSoegtropIMC]

Are there chances that it will be community maintained?

[palmskog]

Since autosubst is a Coq-community project, I consider it by definition community maintained. Owners and other members of Coq-community can help out with autosubst compatibility and releases as necessary (cc: @Zimmi48).

[RalfJung]

Right, they can help -- but should there be someone assigned to be primarily responsible for this?

[palmskog]

@RalfJung how this usually works is that a Platform maintainer requests a new tag/release for a Platform release. If there is no reponse from project maintainers within some time period, the Platform maintainer can ask volunteers to help out, e.g., by pinging one of the Coq-community owners.

[MSoegtropIMC]

The main question is how complicated this development is and how likely it is that someone else can help out in due time. Since afaik from Zulip @haselwarter is working on this right now, we should wait until he is finished with the new release. He can then share his few on this.

[palmskog]

The PR from @haselwarter was merged (https://github.com/coq-community/autosubst/pull/32) and we did the release (https://github.com/coq/opam-coq-archive/pull/2624). I don't think it will take all that much to release new versions as Coq evolves, in fact autosubst is in Coq's CI (https://github.com/coq/coq/blob/master/dev/ci/ci-autosubst.sh).

[Zimmi48]

There is a board which takes such decisions, but I don't see a good reason for not adding it.

@MSoegtropIMC Can you say more about this? I was not aware that such a board had been created, and it doesn't look like it was documented.

[MSoegtropIMC]

The board will start its work from the 2023 autumn on. This has been discussed during the developer meeting last year and Yves Bertot invited the members. Unfortunately I am still so busy with fixing issues that it didn't come to "initialise" the board properly as yet, but everything which goes into the 2023 autumn release will be decided by the board.

[MSoegtropIMC]

FTR: the raw PR diff (https://patch-diff.githubusercontent.com/raw/coq-community/autosubst/pull/32.diff) has 521 lines. I would say it is quite feasible to have this community maintained, but we will discuss this in the board.