Put autosubst on Coq's opam

[RalfJung]

it would be great if autosubst was available on Coq's opam at https://github.com/coq/opam-coq-archive/. That would make it much easier projects already using opam to also depend on autosubst.

I can help writing the opam file, if you want.

[landaro]

Sounds like an interesting idea. We do however have a successor in development, that will probably take the form of an external tool, which won't be distributable via opam, as far as I can tell. Maybe we could discuss this offline when you are in Saarbrücken.

[RalfJung]

FYI, in order to be able to use Autosubst in our CI, I have now written an opam file and added it to our opam repository at https://gitlab.mpi-sws.org/FP/opam-dev/tree/master/packages/coq-autosubst/coq-autosubst.dev.coq86. I'm happy to switch to something more official once that exists :)

[RalfJung]

Any news on this? All you need to do is push some kind of tag for the 8.6 branch (which btw works fine on 8.7 and 8.8), i.e. give a version number to d0d7355 -- then I can submit a package to the official Coq opam archive.

[RalfJung]

A dev version exists in Coq's extra-dev repository. However, I propose once we did the planned changes we also cut a release so we can have a package in the regular repository.

[co-dan]

@RalfJung what kind of changes would you like to make before making a release?
Apart from fixing warning I mean

[RalfJung]

Fixing warnings, and maybe examples/ssr can be made to work with the part of ssreflect that is shipped with Coq?

[co-dan]

I'll take a look at the ssr examples then

[RalfJung]

The examples need eqtype, which AFAIK is not shipped with Coq, so they will still need to depend on coq-mathcomp-ssreflect I think. That's fine, but we should update the version number we mention in the README; 1.7 is kind of ancient.^^

Also see #12: make all is currently broken due to some ssreflect notation conflict starting with Coq 8.11.

[co-dan]

You can rewrite the example with the ssreflect that is shipped with Coq, I think.
In particular, the issue #12 does not arise if you use Coq's ssr., e.g. this works (for Coq 8.12 at least) https://gist.github.com/co-dan/1033faa3349fd9e91da97adfb03c4f7a

[RalfJung]

I wonder if that will still work once you get to eqtype. I guess you'll see.^^

[co-dan]

Maybe I am doing something incorrect, but Coq's ssreflect does not include eqtype, so I removed it from the import list.

[RalfJung]

Coq's ssreflect does not include eqtype

Right, that's what I meant. I expected you'd have to use the one from ssreflect itself then.

But maybe that import was unused to begin with?

[co-dan]

Maybe I misunderstood you, regarding the ssreflect examples.
Removing eqtype does require some changes to the code, as I've started in this branch: https://github.com/co-dan/autosubst/tree/ssr

But I guess what you had in mind is not rewriting the examples to work with Coq's ssr, but rather fixing the examples to still work with mathcomp's ssr?

[RalfJung]

I am fine either way. If it is possible to avoid eqtype, that seems like a reasonable approach as well.

[RalfJung]

We now have CI set up for PRs, and the examples are passing CI. I think we are ready for a release!

@co-dan any objections to tagging the current repository state for an opam release? I can do the opam packaging.
Looking at https://github.com/coq-community/autosubst/tags, the next version would be called "1.7", so unless someone object I am going to go with that.

[co-dan]

Beautiful. Let's go for that.

[RalfJung]

I made a PR for the releasing the opam package: coq/opam#1527

Closing this issue then. Thanks @co-dan and @palmskog for the help. :)