@Yannick Forster Is Autosubst 2 publicly available? Would it work with two kinds of variables, each one bounded with a one of two binders?
Official link: https://www.ps.uni-saarland.de/extras/autosubst2/ @Jan Tusil . I think the answer is yes.
It's a bit unfortunate the code is not available on GitHub, but only via a tarball.
Judging from https://github.com/Blaisorblade/autosubst2-proto/blob/master/as2.cabal (from a snapshot coined on GitHub), the code seems likely to bitrot sooner or later, without a modicum of maintenance.
if only we had some pipeline/infrastructure to maintain generally useful Coq tools :upside_down:
I was indeed thinking of coq-community
, but since there’s more Haskell code than Coq code, I wondered a moment.
but Autosubst2 has indeed the potential to be extremely useful.
I think that part might be doable on top of the Docker image infrastructure. But the heavy lifting would be the social engineering. You could open an issue and ping in authors and other possibly interested parties.
with a github repo, at least users could swap notes with each other on bugs/issues/..., send MR, track changes...
AFAIK all authors have moved on, even autosubst1 qualifies as “abandoned”
I think so too, but the etiquette is to do the pinging nevertheless. Either directly or out-of-band.
I must say, they did fix one bug I reported. Via email. After a while (weeks? months?), but IIUC Steven Schäfer’s now at Google, and others have probably graduated.
hopefully @Yannick Forster knows more since IIUC he works at the same institute?
Kathrin is still at Princeton I believe?
oh right https://www.ps.uni-saarland.de/~kstark/
it's indeed interesting how many coordination problems just proper GitHub repo management solves (central location for issues, PRs)
for a while we had developments that depended on a certain hard-to-locate fork+branch of Paramcoq, but I think everything has been smooth sailing now since it was centralized, and hopefully it and similar repos will be part of the platform for "more" canonization
also really happy to see stuff like this (getting rid of the last few Admitted
) for a project that was stuck in limbo for quite some time: https://github.com/coq-community/gaia/commit/f83e81929c74352f4e2915da6c3a767d03e85f81
@Jan Tusil The most up-to-date release of Autosubst 2 corresponds to the CPP '19 paper (https://doi.org/10.1145/3293880.3294101) and is indeed the one linked by Paolo
@Karl Palmskog I think I know what the current state is :) (although I'm not officially involved in the Autosubst projects). Autosubst 1 is largely abandoned (Tobias and Steven both moved to Google), but we're in the process of transferring the repo to coq-community. Autosubst 2 is still actively maintained and developed by Kathrin. I know that a GitHub repo with lots of cleanups, improvements and all the features from the Coq á la Carte paper from this year's CPP is on the top of her list and should be released relatively soon
@Yannick Forster I see. Autosubst1 is welcome to coq-community, of course (if you want I can help facilitate the move). Good to hear that Autosubst2 is being improved/maintained.
Ah. For Autosubst1, do you know that @Ralf Jung has been maintaining it for a while (it's used in some Iris examples)?
@Paolo Giarrusso IIRC you suggested we could move it to coq-community or so?
EDIT: oh, you said that above :D
Maintenance was trivial so far, I cannot even remember the last time I had to patch it
I tagged you now just to avoid having 2 different maintained repos.
I guess the advantage would be that everybody would know where to find Autosubst1
oh because @Yannick Forster said they are moving autosubst1 to coq-community? good call
so autosubst1 has already diverged into different repos? :sad:
We want to move Autosubst1 to coq-community where it will be maintained by Ralf :) But I didn't follow up on the emails by Kathrin and Dan on this yet
Karl Palmskog said:
so autosubst1 has already diverged into different repos? :sad:
not really, I have a fork but upstream's https://github.com/uds-psl/autosubst/commits/coq86-devel is in the same state
I also maintain an opam package which points to my fork so I can update it easily
My suggestion would be that we transfer the uds-psl/autosubst
repo to coq-community
and then make Ralf the maintainer there
sure. maybe we can also add @Dan Frumin (Gitter import) who AFAIK is using autosubst a lot (unlike me^^)
and maybe @Paolo Giarrusso
probably @Dan Frumin
I just disabled the "(Gitter import)" account.
Yeah, I think it would be a good move forward. I tried to contact the PSL people about the ownership of the autosubst but didn't manage to get into contact with someone who is currently maintaining the library, so I think it qualified for the coq-community
rules
@Dan Frumin so you can confirm you would like to be co-maintainer with Ralf of autosubst1 if the repo moved to coq-community?
@Karl Palmskog yes
OK, unless someone beats me to it, I will open the GitHub issue later today, and we can coordinate the details of the transfer there
Dan Frumin said:
Yeah, I think it would be a good move forward. I tried to contact the PSL people about the ownership of the autosubst but didn't manage to get into contact with someone who is currently maintaining the library, so I think it qualified for the
coq-community
rules
@Yannick Forster is one of those people :)
Is it easiest if we transfer the uds-psl/autosubst
repo, or easier if you fork the repo in coq-community
?
I don't mind either and am happy to transfer at any time when you prompt me
We favor transfers when we can.
Allright. I'll wait for the GitHub issue then and we take it from there!
Last updated: May 31 2023 at 03:30 UTC