Skip to content

Implement a --cubical=no-glue option#7861

Merged
jespercockx merged 11 commits intoagda:masterfrom
yeejian-tan:no-glue
Oct 16, 2025
Merged

Implement a --cubical=no-glue option#7861
jespercockx merged 11 commits intoagda:masterfrom
yeejian-tan:no-glue

Conversation

@yeejian-tan
Copy link
Copy Markdown
Contributor

@yeejian-tan yeejian-tan commented May 5, 2025 •
edited
Loading

This pull request aims to implement a --cubical-without-glue pragma option that allows one to use Cubical features, but disallowing the primitive Glue type. This is in anticipation of my ongoing project to implement Cubical with UIP as mentioned in #3750 .

The key changes made were

  • addition of the --cubical-without-glue flag with tests
  • ensuring no importation of Glue into files with --cubical-without-glue flag by a custom InfectiveImport record
  • a new Cubical variant via the CWithoutGlue :: Cubical datatype constructor
  • many modules with --erased-cubical which do not use Glue in erased positions are changed to --cubical-without-glue instead

A question I have in mind: now that we will have 3 different cubical options (not counting --cubical-compatible): Full, Erased, and WithoutGlue, perhaps it is more ergonomic/intuitive to unify the command line flags (--cubical, --erased-cubical, --cubical-without-glue) that set the same variable into --cubical=[full,erased,noglue] instead (with --cubical meaning --cubical=full by default)?

This is my first time contributing to Agda, please let me know if there is anything I missed. Many thanks in advance!

andreasabel
andreasabel reviewed May 5, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@andreasabel andreasabel left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'd approve; but merging has to wait until after the 2.8.0 release

@andreasabel andreasabel added the cubical Cubical Agda paraphernalia: Paths, Glue, partial elements, hcomp, transp label May 5, 2025
@andreasabel andreasabel added this to the 2.9.0 milestone May 5, 2025
@nad
Copy link
Copy Markdown
Collaborator

nad commented May 6, 2025

Documentation is missing.

Is the idea that it should be possible to import modules that use --cubical-without-glue from modules that use --erased-cubical or --cubical?

@nad
Copy link
Copy Markdown
Collaborator

nad commented May 6, 2025

This is in anticipation of my ongoing project to implement Cubical with UIP as mentioned in #3750 .

Please discuss the design of such a feature before you implement it.

@yeejian-tan yeejian-tan force-pushed the no-glue branch 2 times, most recently from 6ca176e to 3a758f7 Compare May 6, 2025 14:58
@plt-amy
Copy link
Copy Markdown
Member

plt-amy commented May 6, 2025

It would be good to have a decision on #7835 before adding yet another module-level variant of cubical agda.

@yeejian-tan
Copy link
Copy Markdown
Contributor Author

yeejian-tan commented May 6, 2025 •
edited
Loading

Documentation is missing.

I have just added some minimal documentation (for the flag and on the Cubical page), let me know if you think we need more.

Is the idea that it should be possible to import modules that use --cubical-without-glue from modules that use --erased-cubical or --cubical?

Yes, that is what I have in mind.

@nad
Copy link
Copy Markdown
Collaborator

nad commented May 6, 2025

I think the documentation should include something about how the options interact (which is somewhat complicated in the case of --erased-cubical and --cubical).

@yeejian-tan yeejian-tan force-pushed the no-glue branch 2 times, most recently from c1bfd10 to 59e6946 Compare May 7, 2025 13:26
@yeejian-tan
Copy link
Copy Markdown
Contributor Author

yeejian-tan commented May 7, 2025 •
edited
Loading

I think the documentation should include something about how the options interact (which is somewhat complicated in the case of --erased-cubical and --cubical).

59e6946 adds more detailed documentation as a subsection. I also included a table on how they interact, please let me know if there is any mistake:

image

@andreasabel
Copy link
Copy Markdown
Member

andreasabel commented May 28, 2025 •
edited
Loading

--cubical=[full,erased,noglue]

no-glue please.

Should --cubical-compatible be writeable as --cubical=compatible as well? I'd think so.

@andreasabel andreasabel added the pr: squash-me This PR needs squashing label Jul 6, 2025
@andreasabel
Copy link
Copy Markdown
Member

andreasabel commented Jul 6, 2025

@Mergifyio rebase

@mergify
Copy link
Copy Markdown

mergify bot commented Jul 6, 2025

rebase

✅ Branch has been successfully rebased

@yeejian-tan
Change Cubical flags to take string arguments
924541d 
The flag --cubical now takes a string as input.
Empty string `--cubical` or `--cubical=full` represents full Cubical,
`--cubical=compatible` aliases `--cubical-compatible`,
`--cubical=erased` aliases `--erased-cubical`,
and `--cubical=no-glue` replaces the previously implemented `--cubical-without-glue`.
@yeejian-tan
fixup! documentation for --cubical-without-glue
77242dd
@yeejian-tan
fixup! Change Cubical flags to take string arguments
bd2635d
@yeejian-tan
fixup! Change Cubical flags to take string arguments
66d2d8a
@yeejian-tan
Copy link
Copy Markdown
Contributor Author

yeejian-tan commented Jul 29, 2025 •
edited
Loading

This is now ready for another round of review.

The technical changes stay the same, while the --cubical-without-glue flag is renamed into --cubical=no-glue, along with the aliasing of the other cubical-related flags (--cubical[=full], --cubical=compatible, and --cubical=erased). The changes are summarised in CHANGELOG.md, put here for easy reference:

  • added a --cubical=no-glue variant
  • Consolidated Cubical-related flags to
    Old New
    --cubical --cubical, or --cubical=full
    --erased-cubical --erased-cubical, or --cubical=erased
    --cubical-compatible --cubical-compatible, or --cubical=compatible
    - --cubical=no-glue

The user manual is also updated.

I kept all the old flags for backwards compatibility, but new flags are shown in documentation, code comment, and error messages to "prepare" the users for the shift. We can schedule the deprecation for another release if we wanted to.

@yeejian-tan yeejian-tan requested a review from andreasabel July 29, 2025 10:20
@yeejian-tan yeejian-tan changed the title Implement a --cubical-without-glue option Implement a --cubical=no-glue option Jul 29, 2025
@andreasabel
Copy link
Copy Markdown
Member

andreasabel commented Oct 15, 2025

Agda dev meeting 2025-10-15: sorry for the delay in handling this. This PR has proponents and no opponents, so we agree to merge it (if review process is successful). @jespercockx will handle it.

jespercockx
jespercockx approved these changes Oct 15, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@jespercockx jespercockx left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I looked through this PR and everything looks good for it to be merged!

@jespercockx
Copy link
Copy Markdown
Member

jespercockx commented Oct 15, 2025 •
edited
Loading

I brought this back up to date with current master (doing a merge since it's anyway the plan to squash this PR).

(Edit: one advantage of doing a merge commit is that it makes Github prevent me from accidentally rebasing this PR instead of squashing it.)

@jespercockx jespercockx removed the request for review from andreasabel October 15, 2025 15:32
@jespercockx
Copy link
Copy Markdown
Member

jespercockx commented Oct 16, 2025

Let's merge this now and see what people have to say about it before the release of 2.9!

@jespercockx jespercockx merged commit 4bcf57c into agda:master Oct 16, 2025
25 checks passed
andreasabel
andreasabel reviewed Oct 25, 2025
View reviewed changes
@yeejian-tan yeejian-tan mentioned this pull request Dec 18, 2025
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@andreasabel andreasabel andreasabel left review comments

@jespercockx jespercockx jespercockx approved these changes

Assignees

@jespercockx jespercockx

Labels

cubical Cubical Agda paraphernalia: Paths, Glue, partial elements, hcomp, transp pr: squash-me This PR needs squashing

Projects

None yet

Milestone

2.9.0

Development

Successfully merging this pull request may close these issues.

5 participants

@yeejian-tan @nad @plt-amy @andreasabel @jespercockx