Prepare for Agda 2.6.3

[felixwellen]

So far, this is only an update of jesper's #921, which just renames --experimental-lossy-unification to --lossy-unification. I updated to see, if there are problems with the upcoming new agda release - turns out there are unresolved metas with the current master of agda (e.g. in Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda).

[plt-amy]

The unresolved metas may have to do with the fix for agda/agda#6219 ("may" because I haven't looked: I promised myself I'd take today off... sigh). Sadly we don't yet understand the interaction between injectivity analysis and HITs, so disallowing it is the best I can do for now.

[felixwellen]

@aljungstrom can you fill in the implicit arguments in CupProductTensor that agda 2.6.3 cannot figure out?
Feel free to add commits to this PR.

[aljungstrom]

@felixwellen lol did I do it right? I suck at github you know.. made a PR: #953

[felixwellen]

Thanks for looking into it. Seems good to me gitwise. If you have the rights (you do if you are a member of the agda github space), you can just directly push commits to fcherubini/issue1625-rename-flag.

[felixwellen]

Not sure if I really see all the members of the agda space, but if I do, you are not a member... So I guess making a PR on my PR was the best you could do.

[felixwellen]

Now we are prepared for the new agda release - once it is out we can switch to the tag 'v2.6.3' (now it is 'release-2.6.3').
If anyone has the time (and knowledge):
With @andreasabel 's help, I added a workaround (in fix-whitespace.yaml) for the problem, that the current ci-script checks out 'agda' to the workdir which also contains our checkout of cubical. This is a problem now, because there are bad whitespaces somewhere in the agda-tests...

[andreasabel]

Questions from the outside:

• Is this PR still a draft or is it ready now?
• Who will merge it when the time comes? Maybe assign this PR to the right person.

[felixwellen]

I'm not entirely sure what to do, but I guess the following makes sense:

• release the current version of the cubical library as '0.4'
• check RELEASE.md
• set the current version of cubical to '0.5'
• wait until agda 2.6.3 is released
• make this PR use 'v2.6.3' of agda (instead of 'release-2.6.3')
• merge this PR

@mortberg : Does that sound reasonable to you?

[mortberg]

I'm not entirely sure what to do, but I guess the following makes sense:

* [ ]  release the current version of the cubical library as '0.4'

* [ ]  check RELEASE.md

* [ ]  set the current version of cubical to '0.5'

* [ ]  wait until agda 2.6.3 is released

* [ ]  make this PR use 'v2.6.3' of agda (instead of 'release-2.6.3')

* [ ]  merge this PR

@mortberg : Does that sound reasonable to you?

Yes, this sounds good to me. Thanks for taking care of making things working with the new release!

I'm not sure, but maybe your checklist should be added to https://github.com/agda/cubical/blob/master/RELEASE.md ?

Does one have to do anything for the NIX stuff?

[felixwellen]

I'll merge the nix stuff now, so it will be in cubical-0.4.

[felixwellen]

releasing is now #956

[felixwellen]

@guilhermehas I'm a bit confused about the behaviour of ci-nix. Why doesn't it check this branch (which I just rebased)? If I guess correctly, it will check once I merge this PR. And then it will fail as long as nixpkgs is still on agda 2.6.2.2...

[guilhermehas]

@guilhermehas I'm a bit confused about the behaviour of ci-nix. Why doesn't it check this branch (which I just rebased)? If I guess correctly, it will check once I merge this PR. And then it will fail as long as nixpkgs is still on agda 2.6.2.2...

You are right. It just goes to CI if it merged into master or if you change any nix or lock file in some pull request.
I don't know if there is one way to trigger the Nix CI if you want. Maybe @MatthiasHu knows.

In addition, I have seen that Agda already has flake.nix file. So I have to figure out how to use it to compile the library.

[MatthiasHu]

You can use the workflow_dispatch trigger in addition to push and pull_request to allow manually triggering the ci job.

It kind of makes sense that @felixwellen 's force push didn't trigger the ci-nix, since none of the new commits touch flake.nix or flake.lock. (But would it be different if master would be merged into this branch instead of a rebase??)

[MatthiasHu]

In addition, I have seen that Agda already has flake.nix file. So I have to figure out how to use it to compile the library.

Is this to avoid the ci job failing until agda 2.6.3 is in nixpkgs, or do you think it is generally better to use the agda flake in the cubical flake instead of using the agda package from nixpkgs?

[guilhermehas]

In addition, I have seen that Agda already has flake.nix file. So I have to figure out how to use it to compile the library.

Is this to avoid the ci job failing until agda 2.6.3 is in nixpkgs, or do you think it is generally better to use the agda flake in the cubical flake instead of using the agda package from nixpkgs?

My idea was to avoid ci job failing, but I don't know which of these two options @felixwellen prefers.

[felixwellen]

My idea was to avoid ci job failing, but I don't know which of these two options @felixwellen prefers.

I don't have an opinion on that. If agda 2.6.3 is out and it takes to long for that to get into nixpkgs, I might just deactivate the ci job. Once agda 2.6.3 is in nixpkgs, we can switch it on again.
@MatthiasHu can you nix flake update on this branch and push the commit?
That's something we should do anyway and then we actually see, if ci-nix really fails.

[MatthiasHu]

@MatthiasHu can you nix flake update on this branch and push the commit?

Umm... the flake.lock in this branch already contains the new "rev" for nixpkgs, since we did that in 95499d9. I tried nix flake update again and it did not change flake.lock.

[MatthiasHu]

But I can push a commit with the workflow_dispatch in ci-nix.yaml if you want?

[felixwellen]

Yes, please!

[MatthiasHu]

Done, but it does not work in this PR, because "To trigger the workflow_dispatch event, your workflow must be in the default branch." as I now finally found in the github docs.

[MatthiasHu]

But the nix-ci workflow does indeed fail, I got it to run here: MatthiasHu#1

[guilhermehas]

I made a pull request compile using Nix and Agda 2.6.3.
#959

[felixwellen]

So, to summarize: Once agda 2.6.3 is out, we have to

• change the line with the agda version in flake.nix to

  inputs.agda.url = "github:agda/agda/?ref=v2.6.3";

• change AGDA_BRANCH in ci-ubuntu.yml to v2.6.3

[felixwellen]

The PR was already discussed -> merging.

[iblech]

Awesome, thanks to the merge the Nix package for cubical does not need to manually pull this PR in any longer. :-)