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.

Sign up for GitHub

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

Jump to bottom

Issue 5843: rename --without-K to --cubical-compatible #5862

Merged
merged 2 commits into from
Apr 13, 2022
Merged

Issue 5843: rename --without-K to --cubical-compatible #5862

merged 2 commits into from
Apr 13, 2022

Conversation

UlfNorell
Copy link
Member

No description provided.

@UlfNorell UlfNorell mentioned this pull request Apr 7, 2022
Closed
6 tasks
@UlfNorell UlfNorell merged commit 5054649 into master Apr 13, 2022
@UlfNorell UlfNorell deleted the issue5843 branch April 13, 2022 06:34
@andreasabel andreasabel linked an issue Apr 25, 2022 that may be closed by this pull request
Proposal: new flag --cubical-compatible replacing --without-K #5843
Closed
6 tasks
@andreasabel andreasabel added the without-K K-related restrictions to pattern matching, termination checking, indices, erasure label Apr 25, 2022
@andreasabel
Copy link
Member

The interaction test did not pass... https://github.com/agda/agda/runs/5866403832?check_suite_focus=true
It failed because of the the GHC_ENVIRONMENT misery, but it could be that there are other problems... (?)

@andreasabel andreasabel mentioned this pull request Apr 25, 2022
Merged
@andreasabel
Copy link
Member

but it could be that there are other problems... (?)

Fixed by 7ca527c .

@ncfavier
Copy link
Member

Yeah I just ran make test and answered "yes" to every question to generate that commit.

@andreasabel andreasabel added this to the 2.6.3 milestone Aug 31, 2022
@andreasabel andreasabel added the cubical Cubical Agda paraphernalia: Paths, Glue, partial elements, hcomp, transp label Aug 31, 2022
@andreasabel
Copy link
Member

andreasabel commented Aug 31, 2022 •
edited
Loading

2022-08-31: Revert this and rather use --cubical-compatible as the name of the flag of:

Amelia: --cubical-compatible should be a prerequisite to be importable from --cubical, it should fence in all the code that generates stuff used in --cubical modules.
Andreas: Note that < 2.6.3 Agda code will not work out of the box, might need --cubical-compatible added.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
cubical Cubical Agda paraphernalia: Paths, Glue, partial elements, hcomp, transp without-K K-related restrictions to pattern matching, termination checking, indices, erasure
Projects
None yet
Milestone
2.6.3
Development

Successfully merging this pull request may close these issues.

Proposal: new flag --cubical-compatible replacing --without-K
3 participants
@UlfNorell @andreasabel @ncfavier