Update to Agda 2.6.4

[fredrik-bakke]

Bumps the Agda version to 2.6.4 and sets the --level-universe flag.

[fredrik-bakke]

It seems the new version is not yet available from the required resources, so this PR will have to sit in the meantime.

[EgbertRijke]

It seems the new version is not yet available from the required resources, so this PR will have to sit in the meantime.

I was just gonna say, it is not on brew yet

[fredrik-bakke]

A thought: with the new --no-allow-unsolved-metas flag, I wonder if we can streamline the formalization process by assuming --allow-unsolved-metas by default, but setting --no-allow-unsolved-metas in everything.lagda.md. This way, I assume* the code will not typecheck with make check, but you don't have to write in {-# OPTION --allow-unsolved-metas #-} while formalizing. This also makes the cleanup process easier.

[fredrik-bakke]

If you're as eager as me, you can download the cask for 2.6.4 here and try* install from your local file using

brew install --build-from-source agda.rb

[fredrik-bakke]

Also, before this is merged, the flake.nix file needs to be updated somehow. Currently, it contains the following comment

    # Unstable is needed for Agda 2.6.3, latest stable 22.11 only has 2.6.2.2

However, I don't see how to update the file to use 2.6.4

[VojtechStep]

Also, before this is merged, the flake.nix file needs to be updated somehow. Currently, it contains the following comment

    # Unstable is needed for Agda 2.6.3, latest stable 22.11 only has 2.6.2.2

However, I don't see how to update the file to use 2.6.4

The file that needs updating is flake.lock; that tracks which version of the nixpkgs package collection we're using, and it's updated with nix flake update. However the latest package set still doesn't have Agda 2.6.4, see https://search.nixos.org/packages?channel=unstable&show=agda, and there isn't yet a PR updating it.

[EgbertRijke]

If you're as eager as me, you can download the cask for 2.6.4 here and try* install from your local file using

brew install --build-from-source agda.rb

I'm not that adventurous with my agda-installation:) I've installed it with brew, and it updates whenever updates come through brew. I found that this setup works much better for me than if I fiddle with the installation myself. So I'll wait patiently until it is on brew:)

[fredrik-bakke]

Enabling the --level-universe flag will require some more deliberation before it can be implemented.

[EgbertRijke]

It looks like there are other occurrences of '2.6.3', because when I did a global search-replace it found 11 instances.

[fredrik-bakke]

Thanks! I'll look into it

[EgbertRijke]

I'm also quite puzzled why agda 2.6.4 is still unknown to our CI. Did we set up something incorrectly, or is it really taking this long for the new release version to be recognized?

[fredrik-bakke]

Maybe I set up something wrong in this PR. This would make sense given the discrepancy you previously pointed out.

[fredrik-bakke]

Give me a little bit of time and I can investigate it

[fredrik-bakke]

Still seems like 2.6.4 isn't available for the CI tooling. I don't know much beyond that though. Also, Agda 2.6.4 is not available for Nix either, and I think we should wait to merge this PR until it is.

[EgbertRijke]

I agree with you, it doesn't make much sense to merge this PR until 264 is available for the CI.

[VojtechStep]

@fredrik-bakke if you bump the wenkokke/setup-agda GitHub action in all the CI files from v2.0.0 to v2.1.0 then it should recognize Agda 2.6.4. Also we should get 2.6.4 in nixpkgs any day now, the PR was merged yesterday (branch progress tracker). Though we might still want to wait a little bit with this one, since @maybemabeline apparently uses Arch and that's still on 2.6.3.

[VojtechStep]

Nix already has 2.6.4 (though it doesn't show on the website, not sure why)

[fredrik-bakke]

Oh. Well then. That leaves the Arch situation, how can we track that?

[fredrik-bakke]

By the way, do you know if the two "required checks" for 2.6.3 will update when the branch is merged?

[VojtechStep]

Oh. Well then. That leaves the Arch situation, how can we track that?

We can keep checking the pacman page, or we can ask @maybemabeline to ping us once she gets the update.

By the way, do you know if the two "required checks" for 2.6.3 will update when the branch is merged?

I'd think so - usually the "expected" checks are taken from the master/target branch, so that you don't accidentally/maliciously remove previously required checks; so once this PR gets merged, the default expected check would change from {macOS,ubuntu}-2.6.3 to {macOS,ubuntu}-2.6.4.

[fredrik-bakke]

Good point, thanks!

[VojtechStep]

Oh and just because Agda 2.6.4 is available from nixpkgs doesn't mean that we're pulling it, we need to update the flake.lock file as well; I think it'd be easiest if I made a PR to your branch, I should have some time in the afternoon.

[VojtechStep]

fredrik-bakke#3

[VojtechStep]

As mentioned on Discord, Agda 2.6.4 is available on Arch, so there should be nothing blocking this PR any longer.

[VojtechStep]

I'd think so - usually the "expected" checks are taken from the master/target branch, so that you don't accidentally/maliciously remove previously required checks; so once this PR gets merged, the default expected check would change from {macOS,ubuntu}-2.6.3 to {macOS,ubuntu}-2.6.4.

I think this is wrong, actually - apparently "required checks" isn't an automatic thing, it's a branch protection rule that can be configured via the GitHub UI in repository settings (Settings > Branches > edit protection rule "Require status checks to pass before merging"), but I don't have rights to access that part of the repository settings.

[fredrik-bakke]

Me neither. We will have to wait until @EgbertRijke sees this.