Stream: Miscellaneous

Topic: Autosubst1 and Autosubst2

Jan Tusil (Nov 11 2020 at 21:27):

@Yannick Forster Is Autosubst 2 publicly available? Would it work with two kinds of variables, each one bounded with a one of two binders?

Paolo Giarrusso (Nov 11 2020 at 21:42):

Official link: https://www.ps.uni-saarland.de/extras/autosubst2/ @Jan Tusil . I think the answer is yes.

Paolo Giarrusso (Nov 11 2020 at 21:45):

It's a bit unfortunate the code is not available on GitHub, but only via a tarball.

Paolo Giarrusso (Nov 11 2020 at 21:50):

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.

Karl Palmskog (Nov 11 2020 at 22:05):

if only we had some pipeline/infrastructure to maintain generally useful Coq tools :upside_down:

Paolo Giarrusso (Nov 11 2020 at 22:18):

I was indeed thinking of coq-community, but since there’s more Haskell code than Coq code, I wondered a moment.

Paolo Giarrusso (Nov 11 2020 at 22:20):

but Autosubst2 has indeed the potential to be extremely useful.

Karl Palmskog (Nov 11 2020 at 22:21):

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.

Paolo Giarrusso (Nov 11 2020 at 22:21):

with a github repo, at least users could swap notes with each other on bugs/issues/..., send MR, track changes...

Paolo Giarrusso (Nov 11 2020 at 22:21):

AFAIK all authors have moved on, even autosubst1 qualifies as “abandoned”

Karl Palmskog (Nov 11 2020 at 22:22):

I think so too, but the etiquette is to do the pinging nevertheless. Either directly or out-of-band.

Paolo Giarrusso (Nov 11 2020 at 22:23):

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.

Paolo Giarrusso (Nov 11 2020 at 22:23):

hopefully @Yannick Forster knows more since IIUC he works at the same institute?

Karl Palmskog (Nov 11 2020 at 22:24):

Kathrin is still at Princeton I believe?

Paolo Giarrusso (Nov 11 2020 at 22:25):

oh right https://www.ps.uni-saarland.de/~kstark/

Karl Palmskog (Nov 11 2020 at 22:27):

it's indeed interesting how many coordination problems just proper GitHub repo management solves (central location for issues, PRs)

Karl Palmskog (Nov 11 2020 at 22:30):

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

Karl Palmskog (Nov 11 2020 at 22:32):

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

Yannick Forster (Nov 12 2020 at 07:51):

@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

Yannick Forster (Nov 12 2020 at 07:55):

@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

Karl Palmskog (Nov 12 2020 at 08:18):

@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.

Paolo Giarrusso (Nov 12 2020 at 10:23):

Ah. For Autosubst1, do you know that @Ralf Jung has been maintaining it for a while (it's used in some Iris examples)?

Ralf Jung (Nov 12 2020 at 10:28):

@Paolo Giarrusso IIRC you suggested we could move it to coq-community or so?
EDIT: oh, you said that above :D

Ralf Jung (Nov 12 2020 at 10:28):

Maintenance was trivial so far, I cannot even remember the last time I had to patch it

Paolo Giarrusso (Nov 12 2020 at 10:30):

I tagged you now just to avoid having 2 different maintained repos.

Paolo Giarrusso (Nov 12 2020 at 10:30):

I guess the advantage would be that everybody would know where to find Autosubst1

Ralf Jung (Nov 12 2020 at 10:36):

oh because @Yannick Forster said they are moving autosubst1 to coq-community? good call

Karl Palmskog (Nov 12 2020 at 10:37):

so autosubst1 has already diverged into different repos? :sad:

Yannick Forster (Nov 12 2020 at 10:37):

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

Ralf Jung (Nov 12 2020 at 10:37):

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

Ralf Jung (Nov 12 2020 at 10:38):

I also maintain an opam package which points to my fork so I can update it easily

Yannick Forster (Nov 12 2020 at 10:38):

My suggestion would be that we transfer the uds-psl/autosubstrepo to coq-community and then make Ralf the maintainer there

Ralf Jung (Nov 12 2020 at 10:39):

sure. maybe we can also add @Dan Frumin (Gitter import) who AFAIK is using autosubst a lot (unlike me^^)

Ralf Jung (Nov 12 2020 at 10:40):

and maybe @Paolo Giarrusso

Paolo Giarrusso (Nov 12 2020 at 10:41):

probably @Dan Frumin

Théo Zimmermann (Nov 12 2020 at 10:42):

I just disabled the "(Gitter import)" account.

Dan Frumin (Nov 12 2020 at 13:00):

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

Karl Palmskog (Nov 12 2020 at 13:16):

@Dan Frumin so you can confirm you would like to be co-maintainer with Ralf of autosubst1 if the repo moved to coq-community?

Dan Frumin (Nov 12 2020 at 13:19):

@Karl Palmskog yes

Karl Palmskog (Nov 12 2020 at 13:20):

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

Ralf Jung (Nov 12 2020 at 13:23):

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 :)

Yannick Forster (Nov 12 2020 at 13:24):

Is it easiest if we transfer the uds-psl/autosubst repo, or easier if you fork the repo in coq-community?

Yannick Forster (Nov 12 2020 at 13:24):

I don't mind either and am happy to transfer at any time when you prompt me

Théo Zimmermann (Nov 12 2020 at 13:32):

We favor transfers when we can.

Yannick Forster (Nov 12 2020 at 14:22):

Allright. I'll wait for the GitHub issue then and we take it from there!

Last updated: Dec 07 2023 at 06:38 UTC