search

HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory
http://homotopytypetheory.org/
Other
1.23k stars 185 forks source link

bump min version to 8.19 #1985

Closed Alizter closed 3 weeks ago

Alizter commented 4 weeks ago

We bump our minimal Coq version to 8.19.

This version appears to have some better universe inference and will be useful for #1984.

I did a compatibility cleanup in No/Core.v.

I noticed that there is an 8.19 compatibility comment in Quotient.v but I couldn't work out what exactly could change. @jdchristensen would you mind taking a look at that file and dropping the 8.18 compat? (Alternatively, we can do that in a later PR it doesn't seem too pressing).

The draft PR #1862 can be undrafted after this.

jdchristensen commented 4 weeks ago

I did a compatibility cleanup in No/Core.v.

Did you forget to include this? Do you want me to push changes to Quotient.v to this PR?

Alizter commented 4 weeks ago

@jdchristensen Just forgot to push. You can go ahead and push changes to Quotient.v here.

jdchristensen commented 4 weeks ago

@Alizter This LGTM, but I don't know why the CI isn't running for my latest commit.

jdchristensen commented 4 weeks ago

Ok, the CI is running now, but one of the nix jobs is still at 8.18.

jdchristensen commented 4 weeks ago

I tried changing an "8.18" to "8.19" in flake.nix, but the build still seems to be using 8.18. I don't know anything about nix, so I'll leave this to @Alizter .

Alizter commented 4 weeks ago

@jdchristensen Yes, I forgot to change that. There was a new version of coq-lsp released so I'd lile to wait a tad longer before updating the nix stuff.

Alizter commented 3 weeks ago

I've updated the nix flake to a version that includes the latest coq-lsp which was released this week. The issue from before was because the Nix flake's lockfile was not updated, which can be done by nix flake check or nix develop. And since we are updating the lockfile I decided we might as well bump to the latest available packages.

This is now ready to be merged if you are fine with it @jdchristensen.

Alizter commented 3 weeks ago

I noticed you wrote LGTM before so I will take this as a green light and proceed.