Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Build cubical with latest Agda master (2022-05-09) #791

Merged
merged 1 commit into from
May 12, 2022

Conversation

andreasabel
Copy link
Member

I noticed yesterday that the latest cubical does not build with the latest agda. This PR should fix this.

  • 2 hidden arguments that can no longer be inferred: fixed by providing these arguments
  • a regression in the termination checker: fixed by turning the index of IW into a parameter

If you agree and merge this, the submodule pin for cubical in the agda repo can be moved forward.

On another note, it would be good if you would test cubical also with the latest agda, just to get alerted of breakages. Maybe you can add such to your CI, using the deploys of Agda (https://github.com/agda/agda/actions/workflows/deploy.yml)

@andreasabel andreasabel added the agda Agda implementation issues label May 10, 2022
@andreasabel andreasabel merged commit 89fb736 into master May 12, 2022
@andreasabel andreasabel deleted the unsolved-meta-FinData branch May 12, 2022 11:22
@andreasabel
Copy link
Member Author

Build on 2.6.3 (of the merge commit for this PR) broken by:

So, current master isn't ready for 2.6.3.

@mortberg
Copy link
Collaborator

Were we going to make a branch called Agda-dev that is kept up to date with Agda master?

I have no clue how the CI works, so if someone can set up what Andreas suggests that would be great! Maybe @ecavallo knows how to do it?

@ecavallo
Copy link
Collaborator

Yeah, I can have a go

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
agda Agda implementation issues
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants