[Merged by Bors] - chore: robustifying for debug.byAsSorry #14993
Conversation
PR summary 77fd010eb8Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diff
You can run this locally as follows## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit> |
|
|
||
| /-- Transferring from `IsField` to `Field`. -/ | ||
| noncomputable def IsField.toField {R : Type u} [Ring R] (h : IsField R) : Field R := | ||
| { ‹Ring R›, IsField.toSemifield h with qsmul := _ } | ||
| { ‹Ring R›, IsField.toSemifield h with |
There was a problem hiding this comment.
Just flagging for the other reviewers: I don't have an opinion on these - I trust you these are necessary later.
There was a problem hiding this comment.
This change is harmless, but I don't understand why it is needed.
Clearly the _ is being populated by elaborating the rfl proof, but why is this impacted by whether the rfl proof is inlined or inserted automatically behind the scenes?
There was a problem hiding this comment.
Under byAsSorry, rfl will never even run.
There was a problem hiding this comment.
Oh, is the difference here by rfl vs rfl?
|
🚀 Pull request has been placed on the maintainer queue by grunweg. |
|
✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with |
|
Can you explain in the PR description what |
Co-authored-by: grunweg <[email protected]>
|
bors merge |
These are some minor changes, which are think are positive or neutral in any case, that help Mathlib compile under `set_option debug.byAsSorry true` (an option that [arrived](leanprover/lean4#4576) in v4.10 that turns all `by` blocks into sorries
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
Followup to #14993. Hopefully these are all independently positive or neutral. These help get Mathlib compiling under `set_option debug.byAsSorry true`.
These are some minor changes, which are think are positive or neutral in any case, that help Mathlib compile under
set_option debug.byAsSorry true(an option that arrived in v4.10 that turns allbyblocks into sorries --- Mathlib is very much broken, although perhaps less than one might expect).