Skip to content

[ ci ] bump Agda version - #3125

Open
gallais wants to merge 6 commits into
agda:masterfrom
gallais:bump-ci
Open

gallais wants to merge 6 commits into
agda:masterfrom
gallais:bump-ci

Conversation

@gallais

@gallais gallais commented Oct 19, 2026 •

Copy link
Copy Markdown
Member

I'm guessing this is going to choke on #3012

@jamesmckinna

jamesmckinna commented Oct 29, 2026 •

Copy link
Copy Markdown
Collaborator

I'm guessing this is going to choke on #3012

Does this now block on resolving the experimental vs. agda-master question? Or, indeed, on the relative status of v2.9.0-{rc1|rc2|...} ahead of any possible merge?

@gallais

gallais commented Oct 30, 2026

Copy link
Copy Markdown
Member Author

Does this now block on resolving the experimental vs. agda-master question?

This is targeting master so is orthogonal to this question

gallais and others added 4 commits October 30, 2026 10:01
- `Data.Record` needs a `ETA_EQUALITY` pragma to suppress the `UnguardedEtaRecord` warning.
- `Reflection.AST.Traversal` needs an explicit declaration of `no-eta-equality`.
  This was previously inferred.

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants