still maintained?

[haselwarter]

Hi,

are there plans to update this library and keep it alive or is it abandoned?

cheers
Philipp

[Blaisorblade]

I also wondered, but see #7 for news; I just verified that branch 8.6-devel builds with Coq 8.6.1 (both the library and examples-plain).

[sfs]

Hi there! The library is alive and we are working on a successor. The plan is to publish the current version of Autosubst on opam and to at least maintain compatibility with future Coq versions.

[adrieng]

Hi! Any news on the autosubst/autosubst2 front? It would be really great to have autosubst available in OPAM.

[brendanzab]

Is there repository for the successor? Would be interesting to try it out! Been trying to get this version of autosubst working using a git submodule, but I can't figure out how to work Coq's package management :/

[RalfJung]

This repository seems to not be maintained; I have a fork at https://github.com/RalfJung/autosubst/ that I keep working with current versions of Coq.

[co-dan]

Thanks for maintaining an up-to date fork, Ralf!
If the original authors do not want to maintain this library anymore, then maybe it is a possibility to submit it to coq-community https://github.com/coq-community for community maintenance, since I believe there are multiple people who are still interested in using this library in their projects (me included :))

[RalfJung]

That makes sense. It just takes someone to actually pull this through. :)

(Btw, these days iris/examples, which depends on autosubst, is part of Coq CI. So we have a pretty good guarantee that autosubst will keep working.)

@adrieng
For autosubst 2, see https://www.ps.uni-saarland.de/extras/autosubst2/

[co-dan]

That makes sense. It just takes someone to actually pull this through. :)

Basically, for this to happen 1) the original authors of the package have to give consent or vanish and be really unresponsive, 2) someone needs to volunteer to be the community maintainer.
Since I cannot volunteer another person (like Ralf, wink wink) I can volunteer myself for it (shouldn't be too much work thanks for the CI that you mentioned).

I will try to contact the original maintainers and get their consent

[RalfJung]

I'm happy to co-maintain autosubst with you, if you need help. I assume "maintain" here means "keeping it working with later Coq versions", which so far was basically 0 effort. I don't think I'd be able to review PRs for new features or so.

[fpottier]

Just to chime in, it would be great to have an up-to-date version of this library (available via opam, if possible). I will have a look at Ralf's repository (thanks Ralf!).

[RalfJung]

There's a version available in the opam repo at https://gitlab.mpi-sws.org/iris/opam. I was holding off on submitting it to the Coq repo as it's just a personal fork currently.

In terms of "up-to-date", the coq86-devel branch in this repo and in my fork are in sync and reflect the latest state to my knowledge. It is compatible with a wide range of Coq versions including current master.

[fpottier]

Thanks Ralf. Are you aware that the coq86-devel branch gives rise to several warnings when compiled with Coq 8.12?

[RalfJung]

No I was not... I guess opam install coq-autosubst doesn't show these warnings. ;) But things should still work, and there should be no warnings for users of autosubst.

It looks like autosubst will become part of coq-community soon-ish. Then I guess we can decide on a minimal supported Coq version and fix deprecation warnings where possible.

[RalfJung]

All right, @co-dan and me have maintainer access now. We'll consolidate the various branches and then submit an opam package to the Coq opam repo.

[sfs]

Thank you, @co-dan and @RalfJung! Please let me know if you have any questions.

[RalfJung]

So I think we can close this issue; see #7 for getting an opam package into the Coq repo (and not just the dev version).