[Merged by Bors] - fix (RingTheory.Kaehler): short cut instances to remove timeouts#6149
[Merged by Bors] - fix (RingTheory.Kaehler): short cut instances to remove timeouts#6149mattrobball wants to merge 35 commits intomasterfrom
Conversation
…' into mrb/kaehler_speedup
The optional fields to the algebra typeclasses are a trap; if you forget to provide them then you get diamonds.
|
Can you please fix the conflicts? Thanks! |
Modulo the Rust errors (lol), it should build fine now though maybe not lint. I am still working on removing the hacky instances. If I don't succeed by early tomorrow, I will clean this up and mark it |
|
!bench |
|
Run cancelled. This is the only instances now. |
Mathlib/RingTheory/Kaehler.lean
Outdated
| theorem isScalarTower_S_right : IsScalarTower S (S ⊗[R] S ⧸ KaehlerDifferential.ideal R S ^ 2) | ||
| (S ⊗[R] S ⧸ KaehlerDifferential.ideal R S ^ 2) := IsScalarTower.right | ||
|
|
||
| attribute [local instance] isScalarTower_S_right |
There was a problem hiding this comment.
Why a theorem and not local instance?
There was a problem hiding this comment.
defLemma complained. Is there a better fix?
There was a problem hiding this comment.
That sounds like a bug in local instance that we should report somewhere. I think a minimal repro is
local instance : Fact True := sorryThere was a problem hiding this comment.
It isn't making that easy for me. But local is definitely the trigger. I am going to try to minimize in a bit. This has occurred for me before with Fact deep into the library. Maybe the import is messing things up? We'll see.
There was a problem hiding this comment.
I think the problem is that instance is just always a def
There was a problem hiding this comment.
This seems like a mwe:
namespace OhNo
local instance : Fact True := sorry
end OhNo
#lint
There was a problem hiding this comment.
It is a def with or without the local. Should this
if (← isAutoDecl declName) || isGlobalInstance (← getEnv) declName thenbe
if (← isAutoDecl declName) || (← isInstance declName) then?
There was a problem hiding this comment.
Hmm. Probably out of scope regardless
There was a problem hiding this comment.
I didn't figure out how to read local instances in the scope that #lint works in. For now, it seems better just to nolint and bring the issue up on Zulip.
|
!bench |
|
Here are the benchmark results for commit 066a706. |
|
!bench |
|
Here are the benchmark results for commit ea8b9af. Benchmark Metric Change
===================================================
+ ~Mathlib.RingTheory.Kaehler instructions -33.4% |
|
Great work! Thanks 🎉 bors merge |
This obviates the need for bumping timeout limits in `RingTheory.Kaehler` at the expense of explicit instances that Lean should easily be finding. Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
This obviates the need for bumping timeout limits in `RingTheory.Kaehler` at the expense of explicit instances that Lean should easily be finding. Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
This obviates the need for bumping timeout limits in
RingTheory.Kaehlerat the expense of explicit instances that Lean should easily be finding.