[release] 9.3 backports#22247
Draft
gares wants to merge 33 commits into
Draft
Conversation
(cherry picked from commit 65769ad)
(cherry picked from commit a9434da)
Fixing an unfortunate variable overlap from rocq-prover#21564 (cherry picked from commit e964f5c)
coqbot-app
Bot
added
the
needs: full CI
Member
Author
|
@coqbot run full ci |
coqbot-app
Bot
removed
the
needs: full CI
This makes it easier to track what values we store for each object kind. (cherry picked from commit 9f730cc)
(cherry picked from commit 4a7a653)
(cherry picked from commit bb20170)
(cherry picked from commit af80298)
(cherry picked from commit f93ea0f)
(cherry picked from commit 36040ea)
(cherry picked from commit 02a9f7a)
This makes sure to avoid conflicts with SUB which works only whenever there are two consecutive underscores. But in return things like `setoid_rewrite` will be seen as a single token (as it should). (cherry picked from commit 2a6c43f)
(cherry picked from commit debc670)
(cherry picked from commit a511e40)
…schemes
The scheme builders in tactics/eqschemes.ml (Scheme Rewriting and the
congr scheme) substituted the default template levels (e.g. eq.u0) into
the contexts copied from the inductive declaration, so the types of
eq_sym, eq_sym_involutive and eq_rew_r_dep mentioned Type@{eq.u0}.
Using these constants at any fresh universe would then constrain the
global template universe, which is flagged by bad-template-constraint;
with Set Warnings "+bad-template-constraint", even eta-expanding
eq_sym failed:
Check (fun x => @eq_sym x).
(* Error: Adding constraints involving global template univs:
test.22 <= eq.u0 *)
Instead, instantiate the template context with fresh levels declared as
universes of the scheme: eq_sym now gets its own eq_sym.u0, consistent
with eq_ind/eq_rect (whose generation already goes through the standard
case-analysis machinery) and with what a manually stated lemma gets.
Since the schemes of a family no longer share their universes,
hand-computed context sets would miss cross-scheme constraints (the
l2r rewriting scheme applies sym at the fresh universes, requiring
fresh <= sym.u0). Rather than computing those by hand, type-check the
built terms once with Typing.type_of and declare the resulting ustate.
Without this, the kernel rejection was silently swallowed by the
ignore_error in declare_rewriting_schemes, making eq_rew_r_dep vanish.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019ttctspSoVoquHLQtbPVZw
(cherry picked from commit 2829830)
Address review: instead of re-typechecking the hand-built schemes with Typing.type_of to recover the universe constraints missing from the hand-computed context sets, compute them explicitly. Since the schemes of an inductive type no longer share the universes standing for its template universes, the builders that apply a previously declared scheme (sym_involutive and l2r_rew, via const_of_scheme) must enforce the sorts of the parameters of the scheme being built to fit in the sorts of the corresponding binders of the applied constant, e.g. eq_rew_r_dep.u0 <= eq_sym.u0. These constraints were previously invisible because all schemes shared the default template levels (eq.u0 <= eq.u0). The other builders' context sets are self-contained: in particular, applications of template inductives (the inductive itself, and eq) need no constraints since the kernel instantiates them at application time; bugs/bug_22220.v now also tests this with a Type-sorted equality. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019ttctspSoVoquHLQtbPVZw (cherry picked from commit c93c0b4)
…schemes their own universes instead of the template defaults
(cherry picked from commit 2eac902)
The "_pos" fields are accurate even when running with positions disabled. (cherry picked from commit 970c226)
This requires rereading the file to get line number counts. (cherry picked from commit 9ae0258)
Fix rocq-prover#10815 (cherry picked from commit a25317a)
It's not fully ideal as we print `if _ is $ctor` with the ctor name instead of any notation and without any needed hole arguments but better than nothing IMO. (cherry picked from commit 68ff0a7)
…ame in warning message
coqbot-app
Bot
added
the
needs: full CI
Member
Author
|
@coqbot run full ci |
coqbot-app
Bot
removed
the
needs: full CI
Member
Author
|
@coqbot run full ci |
cf ocaml/dune#15458 (comment) (the `%{pkg` suggestion can't be used until we depend on 3.24) (cherry picked from commit 84bf942)
(cherry picked from commit 9412aba)
… Default Proof Using if relevant
It seems this was more used than expected. (cherry picked from commit 9dd02ea)
coqbot-app
Bot
added
the
needs: full CI
Member
Author
|
@coqbot run full ci |
coqbot-app
Bot
removed
the
needs: full CI
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
5 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.