Skip to content

Proper RR typechecker - #19290

Open
yannl35133 wants to merge 5 commits into
rocq-prover:masterfrom
Yann-Leray:rewrite-rules
Open

Proper RR typechecker#19290
yannl35133 wants to merge 5 commits into
rocq-prover:masterfrom
Yann-Leray:rewrite-rules

Conversation

@yannl35133

@yannl35133 yannl35133 commented Jun 27, 2024 •
edited
Loading

Copy link
Copy Markdown
Contributor

@coqbot-app coqbot-app Bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Jun 27, 2024
@coqbot-app coqbot-app Bot added needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. and removed needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. labels Jul 26, 2024
@yannl35133
yannl35133 marked this pull request as ready for review July 26, 2024 12:59
@yannl35133
yannl35133 requested review from a team as code owners July 26, 2024 12:59
@yannl35133

yannl35133 commented Jul 26, 2024

Copy link
Copy Markdown
Contributor Author

It remains to be decided of what to do when the rule breaks SR: right now, coqc emits a warning but coqchk fails (hence the test failures)

@yannl35133
yannl35133 requested a review from a team as a code owner July 26, 2024 13:36
@github-actions github-actions Bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Jul 30, 2024
@coqbot-app

coqbot-app Bot commented Aug 29, 2024

Copy link
Copy Markdown
Contributor

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

@coqbot-app coqbot-app Bot added the stale This PR will be closed unless it is rebased. label Aug 29, 2024
@coqbot-app coqbot-app Bot removed needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. stale This PR will be closed unless it is rebased. labels Sep 5, 2024
@github-actions github-actions Bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Sep 10, 2024
@coqbot-app coqbot-app Bot removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Sep 17, 2024
@coqbot-app coqbot-app Bot removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Sep 10, 2025
@yannl35133 yannl35133 removed the needs: merge of dependency This PR depends on another PR being merged first. label Sep 10, 2025
@yannl35133
yannl35133 marked this pull request as ready for review September 10, 2025 10:23
@yannl35133

yannl35133 commented Sep 10, 2025

Copy link
Copy Markdown
Contributor Author

I marked the PR as open for review, even though it fails to compile starting from commit 6.
The first 5 can be reviewed independently, they don't even talk of rewrite rules.
The 6th commit needs an answer from @ppedrot regarding his latest changes in environ.ml.

SkySkimmer
SkySkimmer reviewed Oct 6, 2025
View reviewed changes
Comment thread engine/uState.ml Outdated
@github-actions github-actions Bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Oct 7, 2025
@coqbot-app coqbot-app Bot removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Oct 10, 2025
@github-actions github-actions Bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Oct 14, 2025
@coqbot-app

coqbot-app Bot commented Nov 13, 2025

Copy link
Copy Markdown
Contributor

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

@coqbot-app coqbot-app Bot added the stale This PR will be closed unless it is rebased. label Nov 13, 2025
@coqbot-app coqbot-app Bot removed needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. stale This PR will be closed unless it is rebased. labels Nov 17, 2025
@coqbot-app

coqbot-app Bot commented Dec 18, 2025

Copy link
Copy Markdown
Contributor

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

@yannl35133

yannl35133 commented Jan 5, 2026

Copy link
Copy Markdown
Contributor Author

What's the policy (or what should the policy be) regarding the minimum that rocqchk should verify for constr ?
I'm pretty sure that, currently, all constr appearing in a vo file are at minimum typechecked before continuing, but if we want to skip some checks for rewrite rules (so as not to introduce "safe unification" in the kernel), we have to be sure what checks should remain.

  • if typecheck: we need support for evar typing and defined evar substitution (the latter is already possible in cclosure and conversion in fact); I guess we would need to typecheck all evar types and definitions as well, but that seems reasonable if we do that for the rhs already. We could even do the full check with proper universe constraint support (as in, test for all combinations of predicative/impredicative for all sort variables), or relaxed (unsafe)
  • do we at least make sure the term is closed? closed for universe variables? closed for environment variables?

@SkySkimmer

SkySkimmer commented Jan 5, 2026

Copy link
Copy Markdown
Contributor

rocqchk could just fail if there are rewrite rules

@coqbot-app

coqbot-app Bot commented Jan 19, 2026

Copy link
Copy Markdown
Contributor

This PR was not rebased after 30 days despite the warning, it is now closed.

@yannl35133 yannl35133 mentioned this pull request Apr 14, 2026
Open
@yannl35133

yannl35133 commented Jul 26, 2026

Copy link
Copy Markdown
Contributor Author

@coqbot run full ci

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

Reviewers

@jfehrle jfehrle jfehrle left review comments
@SkySkimmer SkySkimmer SkySkimmer left review comments

At least 1 approving review is required to merge this pull request.

Assignees

@ppedrot ppedrot

@SkySkimmer SkySkimmer

Labels

kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. needs: changelog entry This should be documented in doc/changelog. needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. part: rewrite rules

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

Conversion incompleteness with Definitional UIP

4 participants

@yannl35133 @SkySkimmer @jfehrle @ppedrot