search

agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
454 stars 139 forks source link

Prepare for Agda 2.6.3 #948

Closed felixwellen closed 1 year ago

felixwellen commented 2 years ago

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 commented 2 years ago

The unresolved metas may have to do with the fix for https://github.com/agda/agda/pull/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 commented 1 year ago

@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 commented 1 year ago

@felixwellen lol did I do it right? I suck at github you know.. made a PR: https://github.com/agda/cubical/pull/953

felixwellen commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

Questions from the outside:

felixwellen commented 1 year ago

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

@mortberg : Does that sound reasonable to you?

mortberg commented 1 year ago

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 commented 1 year ago

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

felixwellen commented 1 year ago

releasing is now #956

felixwellen commented 1 year ago

@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 commented 1 year ago

@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 commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

@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 95499d95. I tried nix flake update again and it did not change flake.lock.

MatthiasHu commented 1 year ago

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

felixwellen commented 1 year ago

Yes, please!

MatthiasHu commented 1 year ago

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 commented 1 year ago

But the nix-ci workflow does indeed fail, I got it to run here: https://github.com/MatthiasHu/cubical/pull/1

guilhermehas commented 1 year ago

I made a pull request compile using Nix and Agda 2.6.3. https://github.com/agda/cubical/pull/959

felixwellen commented 1 year ago

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

felixwellen commented 1 year ago

The PR was already discussed -> merging.

iblech commented 1 year ago

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