Stream: Miscellaneous

Topic: Autosubst1 and Autosubst2


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Nov 11 2020 at 22:05):

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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Nov 11 2020 at 22:20):

but Autosubst2 has indeed the potential to be extremely useful.

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip Paolo Giarrusso (Nov 11 2020 at 22:21):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Nov 11 2020 at 22:23):

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

view this post on Zulip Karl Palmskog (Nov 11 2020 at 22:24):

Kathrin is still at Princeton I believe?

view this post on Zulip Paolo Giarrusso (Nov 11 2020 at 22:25):

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Nov 12 2020 at 10:30):

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

view this post on Zulip Paolo Giarrusso (Nov 12 2020 at 10:30):

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

view this post on Zulip Ralf Jung (Nov 12 2020 at 10:36):

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

view this post on Zulip Karl Palmskog (Nov 12 2020 at 10:37):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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^^)

view this post on Zulip Ralf Jung (Nov 12 2020 at 10:40):

and maybe @Paolo Giarrusso

view this post on Zulip Paolo Giarrusso (Nov 12 2020 at 10:41):

probably @Dan Frumin

view this post on Zulip Théo Zimmermann (Nov 12 2020 at 10:42):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Dan Frumin (Nov 12 2020 at 13:19):

@Karl Palmskog yes

view this post on Zulip 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

view this post on Zulip 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 :)

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Nov 12 2020 at 13:32):

We favor transfers when we can.

view this post on Zulip 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: Aug 19 2022 at 20:03 UTC