Skip to content

Handle new Rocq 9.2 warnings#235

Merged
proux01 merged 3 commits intorocq-prover:masterfrom
proux01:warning-92
Feb 14, 2026
Merged

Handle new Rocq 9.2 warnings#235
proux01 merged 3 commits intorocq-prover:masterfrom
proux01:warning-92

Conversation

@proux01
Copy link
Contributor

@proux01 proux01 commented Feb 13, 2026

  • Added changelog.
  • Added / updated documentation.
  • Opened overlay pull requests.

@proux01 proux01 force-pushed the warning-92 branch 2 times, most recently from 428d7b6 to 684d1d1 Compare February 13, 2026 13:14
@SkySkimmer
Copy link
Contributor

BTW in the log you will see a few warnings like

File "./btauto/Algebra.v", line 394, characters 0-54:
Warning:
Autogenerated "rew" scheme for null.
Use "Scheme Rewriting for null" to explicitly generate it.
This will become an error in the future.
[missing-scheme,deprecated-since-9.2,deprecated,default]

case_decide; simpl; try_rewrite; [ring_simplify|ring].

This is from a try_rewrite, and the rewrite does nothing so if the warning is turned into an error the proof still succeeds (but silently).

@proux01
Copy link
Contributor Author

proux01 commented Feb 13, 2026

Thanks for pointing it but why does neither Set Warnings "+default" nor Set Warnings "+missing-scheme". turn it as error? (it seems to silence the warning here, that effect being seamingly specific to that warning)
[my bad, thanks for the explanation]

@proux01 proux01 force-pushed the warning-92 branch 3 times, most recently from cf1583e to 1826a67 Compare February 13, 2026 14:02
@proux01
Copy link
Contributor Author

proux01 commented Feb 13, 2026

Noted missing-scheme as requiring handling when requiring Rocq >= 9.2 (so that it can now be turned as error by default).

@SkySkimmer
Copy link
Contributor

It does turn it as error, but try ignores the error.

@proux01
Copy link
Contributor Author

proux01 commented Feb 13, 2026

Yes, sorry, took me some time to understand (apparently, I need a break)

@proux01 proux01 added this to the 9.2 milestone Feb 14, 2026
@proux01 proux01 marked this pull request as ready for review February 14, 2026 13:23
@proux01 proux01 merged commit acfcd7e into rocq-prover:master Feb 14, 2026
582 of 583 checks passed
@proux01 proux01 deleted the warning-92 branch February 14, 2026 13:23
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.

2 participants

Comments