chore: test fast_instance% everywhere by riccardobrasca · Pull Request #39780 · leanprover-community/mathlib4

riccardobrasca · 2026-05-24T15:52:49Z

github-actions · 2026-05-24T15:54:08Z

PR summary 3eb8c21d31

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Logic.Equiv.Defs	117	118	+1 (+0.85%)
Mathlib.Algebra.Group.ULift	134	135	+1 (+0.75%)
Mathlib.Algebra.GroupWithZero.ULift	141	142	+1 (+0.71%)
Mathlib.Data.ULift	145	146	+1 (+0.69%)
Mathlib.Logic.Embedding.Basic	149	150	+1 (+0.67%)
Mathlib.SetTheory.Cardinal.Defs	149	150	+1 (+0.67%)
Mathlib.Control.ULiftable	295	296	+1 (+0.34%)

Import changes for all files

Files	Import difference
145 files `Mathlib.Algebra.AddTorsor.Defs` `Mathlib.Algebra.Divisibility.Prod` `Mathlib.Algebra.Field.Equiv` `Mathlib.Algebra.FreeMonoid.Basic` `Mathlib.Algebra.FreeMonoid.Count` `Mathlib.Algebra.Free` `Mathlib.Algebra.Group.Action.Basic` `Mathlib.Algebra.Group.Action.Defs` `Mathlib.Algebra.Group.Action.Faithful` `Mathlib.Algebra.Group.Action.Hom` `Mathlib.Algebra.Group.Action.Opposite` `Mathlib.Algebra.Group.Action.Option` `Mathlib.Algebra.Group.Action.Pretransitive` `Mathlib.Algebra.Group.Action.Prod` `Mathlib.Algebra.Group.Action.Sigma` `Mathlib.Algebra.Group.Action.Sum` `Mathlib.Algebra.Group.Action.TypeTags` `Mathlib.Algebra.Group.Action.Units` `Mathlib.Algebra.Group.Embedding` `Mathlib.Algebra.Group.Equiv.Basic` `Mathlib.Algebra.Group.Equiv.Defs` `Mathlib.Algebra.Group.Equiv.Opposite` `Mathlib.Algebra.Group.Equiv.TypeTags` `Mathlib.Algebra.Group.Even` `Mathlib.Algebra.Group.Int.Even` `Mathlib.Algebra.Group.Int.TypeTags` `Mathlib.Algebra.Group.Invertible.Basic` `Mathlib.Algebra.Group.Irreducible.Lemmas` `Mathlib.Algebra.Group.Nat.Even` `Mathlib.Algebra.Group.Nat.Hom` `Mathlib.Algebra.Group.Nat.TypeTags` `Mathlib.Algebra.Group.Opposite` `Mathlib.Algebra.Group.Pi.Units` `Mathlib.Algebra.Group.Prod` `Mathlib.Algebra.Group.TypeTags.Basic` `Mathlib.Algebra.Group.TypeTags.Hom` `Mathlib.Algebra.Group.ULift` `Mathlib.Algebra.Group.Units.Equiv` `Mathlib.Algebra.Group.Units.Hom` `Mathlib.Algebra.Group.Units.Opposite` `Mathlib.Algebra.Group.WithOne.Basic` `Mathlib.Algebra.GroupWithZero.Action.Defs` `Mathlib.Algebra.GroupWithZero.Action.End` `Mathlib.Algebra.GroupWithZero.Action.Faithful` `Mathlib.Algebra.GroupWithZero.Action.Opposite` `Mathlib.Algebra.GroupWithZero.Action.Prod` `Mathlib.Algebra.GroupWithZero.Action.Units` `Mathlib.Algebra.GroupWithZero.Equiv` `Mathlib.Algebra.GroupWithZero.Invertible` `Mathlib.Algebra.GroupWithZero.Opposite` `Mathlib.Algebra.GroupWithZero.ProdHom` `Mathlib.Algebra.GroupWithZero.Prod` `Mathlib.Algebra.GroupWithZero.ULift` `Mathlib.Algebra.GroupWithZero.Units.Equiv` `Mathlib.Algebra.GroupWithZero.Units.Lemmas` `Mathlib.Algebra.GroupWithZero.WithZero` `Mathlib.Algebra.Module.Defs` `Mathlib.Algebra.Module.MinimalAxioms` `Mathlib.Algebra.Module.Prod` `Mathlib.Algebra.Opposites` `Mathlib.Algebra.Regular.Opposite` `Mathlib.Algebra.Regular.Pi` `Mathlib.Algebra.Regular.Prod` `Mathlib.Algebra.Regular.SMul` `Mathlib.Algebra.Regular.ULift` `Mathlib.Algebra.Ring.Action.Rat` `Mathlib.Algebra.Ring.Divisibility.Basic` `Mathlib.Algebra.Ring.InjSurj` `Mathlib.Algebra.Ring.Invertible` `Mathlib.Algebra.Ring.WithZero` `Mathlib.CategoryTheory.Bicategory.Adjunction.Basic` `Mathlib.CategoryTheory.Bicategory.Adjunction.Mate` `Mathlib.CategoryTheory.Bicategory.Basic` `Mathlib.CategoryTheory.Category.Basic` `Mathlib.CategoryTheory.Category.KleisliCat` `Mathlib.CategoryTheory.Functor.Basic` `Mathlib.CategoryTheory.Functor.Category` `Mathlib.CategoryTheory.Functor.FullyFaithful` `Mathlib.CategoryTheory.Functor.Functorial` `Mathlib.CategoryTheory.Functor.ReflectsIso.Basic` `Mathlib.CategoryTheory.Functor.Trifunctor` `Mathlib.CategoryTheory.HomCongr` `Mathlib.CategoryTheory.InducedCategory` `Mathlib.CategoryTheory.Iso` `Mathlib.CategoryTheory.NatIso` `Mathlib.CategoryTheory.NatTrans` `Mathlib.CategoryTheory.Sigma.Basic` `Mathlib.CategoryTheory.Thin` `Mathlib.CategoryTheory.Whiskering` `Mathlib.Combinatorics.Quiver.Basic` `Mathlib.Combinatorics.Quiver.Cast` `Mathlib.Combinatorics.Quiver.ConnectedComponent` `Mathlib.Combinatorics.Quiver.Covering` `Mathlib.Combinatorics.Quiver.Path` `Mathlib.Combinatorics.Quiver.Prefunctor` `Mathlib.Combinatorics.Quiver.Push` `Mathlib.Combinatorics.Quiver.Schreier` `Mathlib.Combinatorics.Quiver.SingleObj` `Mathlib.Combinatorics.Quiver.Subquiver` `Mathlib.Combinatorics.Quiver.Symmetric` `Mathlib.Control.EquivFunctor` `Mathlib.Control.Monad.Basic` `Mathlib.Control.Monad.Cont` `Mathlib.Control.Monad.Writer` `Mathlib.Control.Traversable.Equiv` `Mathlib.Control.ULiftable` `Mathlib.Data.Countable.Defs` `Mathlib.Data.Erased` `Mathlib.Data.Finite.Defs` `Mathlib.Data.Int.Cast.Prod` `Mathlib.Data.Nat.Cast.Prod` `Mathlib.Data.Opposite` `Mathlib.Data.Set.Opposite` `Mathlib.Data.ULift` `Mathlib.GroupTheory.GroupAction.IterateAct` `Mathlib.GroupTheory.GroupAction.Ring` `Mathlib.LinearAlgebra.AffineSpace.Defs` `Mathlib.Logic.Embedding.Basic` `Mathlib.Logic.Equiv.Basic` `Mathlib.Logic.Equiv.Bool` `Mathlib.Logic.Equiv.Defs` `Mathlib.Logic.Equiv.Functor` `Mathlib.Logic.Equiv.Option` `Mathlib.Logic.Equiv.Prod` `Mathlib.Logic.Equiv.Sum` `Mathlib.Logic.Small.Defs` `Mathlib.Logic.UnivLE` `Mathlib.SetTheory.Cardinal.Defs` `Mathlib.Tactic.CategoryTheory.BicategoricalComp` `Mathlib.Tactic.CategoryTheory.Bicategory.Basic` `Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes` `Mathlib.Tactic.CategoryTheory.Bicategory.Normalize` `Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence` `Mathlib.Tactic.CategoryTheory.CancelIso` `Mathlib.Tactic.CategoryTheory.CheckCompositions` `Mathlib.Tactic.CategoryTheory.Coherence.Basic` `Mathlib.Tactic.CategoryTheory.IsoReassoc` `Mathlib.Tactic.CategoryTheory.Reassoc` `Mathlib.Tactic.DeriveFintype` `Mathlib.Tactic.NormNum.Core` `Mathlib.Tactic.NormNum.Parity` `Mathlib.Tactic.NormNum.Result` `Mathlib.Tactic.ProdAssoc` `Mathlib.Tactic.ProxyType` `Mathlib.Tactic.Widget.CommDiag`	1

Declarations diff

+ _find_body(text:
+ _skip_comment(text:
+ _worker(args):
+ add_fast_instance_import(text:
+ apply_edits(text:
+ build(file:
+ candidate_edits(text:
+ edit_ok(file:
+ find_files(roots:
+ instance : Algebra R (FiniteAdeleRing R K) := fast_instance% Algebra.compHom _ (algebraMap R K)
+ instance : Bornology α := fast_instance% Bornology.induced (f : α → β)
+ instance : Inhabited (ValueGroup A K) := fast_instance% ⟨Quotient.mk'' 0⟩
+ instance : MulAction (α ≃o α) (Flag α) := fast_instance% SetLike.coe_injective.mulAction _ coe_smul
+ instance : MulAction Mᵈᵐᵃ (A →* B) := fast_instance%
+ instance : One (ValueGroup A K) := fast_instance% ⟨Quotient.mk'' 1⟩
+ instance : PartialOrder (DiffeologicalSpace X) := fast_instance%
+ instance : PartialOrder (IdealSheafData X) := fast_instance%
+ instance : Preorder X.N := fast_instance% Preorder.lift toS
+ instance : Preorder X.S := fast_instance% Preorder.lift subcomplex
+ instance : PseudoEMetricSpace (ULift α) := fast_instance% PseudoEMetricSpace.induced ULift.down ‹_›
+ instance : Zero (ValueGroup A K) := fast_instance% ⟨Quotient.mk'' 0⟩
+ instance [Bornology E] : Bornology C⋆ᵐᵒᵈ(A, E) := fast_instance% Bornology.induced <| equiv A E
+ main():
+ sweep(file:
- instance : Algebra R (FiniteAdeleRing R K) := Algebra.compHom _ (algebraMap R K)
- instance : Bornology α := Bornology.induced (f : α → β)
- instance : Inhabited (ValueGroup A K) := ⟨Quotient.mk'' 0⟩
- instance : MulAction (α ≃o α) (Flag α) := SetLike.coe_injective.mulAction _ coe_smul
- instance : MulAction Mᵈᵐᵃ (A →* B) := DFunLike.coe_injective.mulAction (⇑) fun _ _ ↦ rfl
- instance : One (ValueGroup A K) := ⟨Quotient.mk'' 1⟩
- instance : PartialOrder (DiffeologicalSpace X) := PartialOrder.lift _ injective_toPlots
- instance : PartialOrder (IdealSheafData X) := PartialOrder.lift ideal fun _ _ ↦ IdealSheafData.ext
- instance : Preorder X.N := Preorder.lift toS
- instance : Preorder X.S := Preorder.lift subcomplex
- instance : PseudoEMetricSpace (ULift α) := PseudoEMetricSpace.induced ULift.down ‹_›
- instance : Zero (ValueGroup A K) := ⟨Quotient.mk'' 0⟩
- instance [Bornology E] : Bornology C⋆ᵐᵒᵈ(A, E) := Bornology.induced <| equiv A E

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to strong technical debt.

No changes to weak technical debt.

⚠️ Scripts folder reminder

This PR adds files under scripts/.
Please consider whether each added script belongs in this repository or in leanprover-community/mathlib-ci.

A script belongs in mathlib-ci if it is a CI automation script that interacts with GitHub (e.g. managing labels, posting comments, triggering bots), runs from a trusted external checkout in CI, or requires access to secrets.

A script belongs in this repository (scripts/) if it is a developer or maintainer tool to be run locally, a code maintenance or analysis utility, a style linting tool, or a data file used by the library's own linters.

See the mathlib-ci README for more details.

Added scripts files:

scripts/sweep_fast_instance.py

github-actions · 2026-05-24T15:54:14Z

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

kbuzzard · 2026-05-24T20:08:40Z


 instance monoidalCategory : MonoidalCategory (ModuleCat.{u} R) :=
-  Monoidal.induced equivalenceSemimoduleCat.functor
+  fast_instance% Monoidal.induced equivalenceSemimoduleCat.functor


If you revert this then the error in Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric goes away (and in fact mathlib builds)

Oh -- I can push to this fork for some reason! Fixes coming up.

Maintainers can push to all forks by default (users can change this on their github, but if they just fork mathlib this is the status quo).

kbuzzard · 2026-05-24T20:26:50Z

!radar

leanprover-radar · 2026-05-24T20:27:03Z

Benchmark results for cac073f against 383a355 are in. No significant results found. @kbuzzard

✅ build//instructions: -21.5G (-0.01%)

Medium changes (2✅, 1🟥)

✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Bounds//instructions: -3.3G (-3.56%)
🟥 build/module/Mathlib.Data.UInt//instructions: +1.9G (+15.68%)
✅ build/module/Mathlib.Topology.Algebra.Valued.WithVal//instructions: -11.8G (-12.65%)

Small changes (3✅, 3🟥)

✅ build/module/Mathlib.Algebra.Group.ULift//instructions: -250.4M (-3.56%)
✅ build/module/Mathlib.Algebra.Module.Submodule.Invariant//instructions: -230.8M (-1.72%)
🟥 build/module/Mathlib.Algebra.Order.CauSeq.Basic//instructions: +1.5G (+2.78%)
✅ build/module/Mathlib.Algebra.Ring.ULift//instructions: -683.8M (-5.75%) (reduced significance based on absolute threshold)
🟥 build/module/Mathlib.Algebra.Star.Module//instructions: +591.5M (+3.21%)
🟥 build/module/Mathlib.Algebra.Star.SelfAdjoint//instructions: +2.4G (+8.91%)

kbuzzard · 2026-05-24T20:31:42Z

+  Wraps `instance` bodies whose RHS uses a known smart constructor with `fast_instance%`,
+  then rebuilds the file and reverts the edit if it breaks the build or triggers the
+  `linter.fast_instance_existing` warning. Supports parallel sweeps over a subtree.
+  Usage: `python3 scripts/sweep_fast_instance.py [-j N] [--dry-run] <path>`


(this is just for the linter, I am unclear about whether the plan is to PR the script but I'm just worried about linter failures making radar fail)

I just wanted to test it, I didn't realize I staged also the script. Anyway thanks for fixing the linter!

…nstance # Conflicts: # Mathlib/Algebra/Ring/Subsemiring/Basic.lean

riccardobrasca · 2026-05-24T22:49:23Z

!radar

leanprover-radar · 2026-05-24T22:49:36Z

Benchmark results for dd22ac0 against 383a355 are in. There are significant results. @riccardobrasca

🟥 main exited with code 1

No significant changes detected.

kbuzzard · 2026-05-25T08:17:54Z

!radar

leanprover-radar · 2026-05-25T08:18:15Z

Benchmark results for a11dfb5 against 383a355 are in. There are significant results. @kbuzzard

🟥 main exited with code 1

No significant changes detected.

riccardobrasca · 2026-05-25T09:10:26Z

!radar

leanprover-radar · 2026-05-25T09:10:51Z

Benchmark results for 9849b61 against 383a355 are in. There are significant results. @riccardobrasca

🟥 main exited with code 1

No significant changes detected.

riccardobrasca · 2026-05-25T09:54:57Z

!radar

leanprover-radar · 2026-05-25T09:55:13Z

Benchmark results for 13c8ec5 against 383a355 are in. There are significant results. @riccardobrasca

🟥 main exited with code 1

No significant changes detected.

riccardobrasca · 2026-05-25T10:40:19Z

!radar

leanprover-radar · 2026-05-25T10:40:34Z

Benchmark results for dde7887 against 383a355 are in. There are significant results. @riccardobrasca

✅ build//instructions: -3.7G (-0.00%)

Large changes (1✅)

✅ build/module/Mathlib.LinearAlgebra.PiTensorProduct.DirectSum//instructions: -8.1G (-21.86%)

Medium changes (4✅, 2🟥)

✅ build/module/Mathlib.Algebra.Category.Grp.Colimits//instructions: -10.6G (-24.00%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Bounds//instructions: -7.0G (-7.55%)
🟥 build/module/Mathlib.Data.UInt//instructions: +1.9G (+16.05%)
✅ build/module/Mathlib.LinearAlgebra.Multilinear.DirectSum//instructions: -7.3G (-27.45%)
🟥 build/module/Mathlib.NumberTheory.ModularForms.Basic//instructions: +4.6G (+10.78%)
✅ build/module/Mathlib.Topology.Algebra.Valued.WithVal//instructions: -11.7G (-12.61%)

Small changes (7✅, 8🟥)

🟥 build/module/Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric//instructions: +7.7G (+50.60%) (reduced significance based on *//lines)
✅ build/module/Mathlib.Algebra.DirectSum.Module//instructions: -2.6G (-5.67%)
✅ build/module/Mathlib.Algebra.Group.ULift//instructions: -266.6M (-3.79%)
✅ build/module/Mathlib.Algebra.Module.Submodule.Invariant//instructions: -228.7M (-1.70%)
🟥 build/module/Mathlib.Algebra.Order.CauSeq.Basic//instructions: +1.5G (+2.82%)
✅ build/module/Mathlib.Algebra.Ring.ULift//instructions: -678.9M (-5.71%) (reduced significance based on absolute threshold)
🟥 build/module/Mathlib.Algebra.Star.Module//instructions: +597.9M (+3.24%)
🟥 build/module/Mathlib.Algebra.Star.SelfAdjoint//instructions: +2.5G (+9.44%)
✅ build/module/Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation//instructions: -2.5G (-2.70%)
🟥 build/module/Mathlib.NumberTheory.KummerDedekind//instructions: +3.6G (+9.78%)
✅ build/module/Mathlib.RingTheory.ClassGroup//instructions: -1.7G (-2.53%)
🟥 build/module/Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing//instructions: +1.6G (+3.48%)
🟥 build/module/Mathlib.RingTheory.Extension.Presentation.Core//instructions: +3.5G (+6.68%)
🟥 build/module/Mathlib.RingTheory.Ideal.CotangentBaseChange//instructions: +12.7G (+30.48%) (reduced significance based on *//lines)
✅ build/module/Mathlib.Topology.Category.Profinite.Nobeling.Successor//instructions: -1.9G (-5.20%)

riccardobrasca · 2026-05-28T17:52:06Z

!radar

leanprover-radar · 2026-05-28T17:52:25Z

Benchmark results for 3eb8c21 against 84c838c are in. There are significant results. @riccardobrasca

🟥 build//instructions: +7.4G (+0.00%)

Large changes (1✅)

✅ build/module/Mathlib.LinearAlgebra.PiTensorProduct.DirectSum//instructions: -8.1G (-22.07%)

Medium changes (3✅, 2🟥)

✅ build/module/Mathlib.Algebra.Category.Grp.Colimits//instructions: -10.8G (-24.63%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Bounds//instructions: -7.1G (-7.59%)
🟥 build/module/Mathlib.Data.UInt//instructions: +1.9G (+15.99%)
✅ build/module/Mathlib.LinearAlgebra.Multilinear.DirectSum//instructions: -7.5G (-28.38%)
🟥 build/module/Mathlib.NumberTheory.ModularForms.Basic//instructions: +4.6G (+10.98%)

Small changes (5✅, 9🟥)

🟥 build/module/Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric//instructions: +7.8G (+52.22%) (reduced significance based on *//lines)
✅ build/module/Mathlib.Algebra.DirectSum.Module//instructions: -2.6G (-5.57%)
✅ build/module/Mathlib.Algebra.Group.ULift//instructions: -251.7M (-3.74%)
🟥 build/module/Mathlib.Algebra.Order.CauSeq.Basic//instructions: +1.6G (+2.95%)
✅ build/module/Mathlib.Algebra.Ring.ULift//instructions: -681.9M (-6.11%)
🟥 build/module/Mathlib.Algebra.Star.Module//instructions: +568.0M (+3.10%)
🟥 build/module/Mathlib.Algebra.Star.SelfAdjoint//instructions: +2.4G (+8.91%)
✅ build/module/Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation//instructions: -2.6G (-2.75%)
🟥 build/module/Mathlib.GroupTheory.Torsion//instructions: +851.6M (+4.41%)
🟥 build/module/Mathlib.NumberTheory.KummerDedekind//instructions: +3.7G (+10.23%)
🟥 build/module/Mathlib.Order.CompleteSublattice//instructions: +645.2M (+5.16%)
🟥 build/module/Mathlib.RingTheory.Extension.Presentation.Core//instructions: +3.6G (+6.81%)
🟥 build/module/Mathlib.RingTheory.Ideal.CotangentBaseChange//instructions: +12.7G (+30.85%) (reduced significance based on *//lines)
✅ build/module/Mathlib.Topology.Category.Profinite.Nobeling.Successor//instructions: -2.0G (-5.25%)

riccardobrasca added 2 commits May 24, 2026 17:52

test

3bc1a54

more files

43f37f0

riccardobrasca added the WIP Work in progress label May 24, 2026

more

b301914

kbuzzard reviewed May 24, 2026

View reviewed changes

kbuzzard added 3 commits May 24, 2026 21:11

fix build

7a49924

fix line-length lints and drop fast_instance% from proof-instances

6fcab5d

document sweep_fast_instance.py in scripts/README.md

cac073f

kbuzzard reviewed May 24, 2026

View reviewed changes

Comment thread Mathlib/CategoryTheory/Abelian/Basic.lean

kbuzzard reviewed May 24, 2026

View reviewed changes

riccardobrasca added 4 commits May 25, 2026 00:12

more files

fc4c3e8

Merge remote-tracking branch 'origin/RB/fast_instance' into RB/fast_i…

7a3601f

…nstance # Conflicts: # Mathlib/Algebra/Ring/Subsemiring/Basic.lean

long line

abe410a

fix remaining long lines from fast_instance% sweep

dd22ac0

riccardobrasca added 6 commits May 25, 2026 01:22

fix

d857bd4

fix

340edf5

fix

ad71a43

another one

76c759b

fix

f6a6609

another one

b39823b

kbuzzard mentioned this pull request May 24, 2026

[Merged by Bors] - perf: fast_instance% in Mathlib.Order.Basic #39795

Closed

riccardobrasca added 3 commits May 25, 2026 01:48

again

833f251

fix

f28ec51

another one

2129ff6

riccardobrasca added 5 commits May 25, 2026 02:19

also this

a761a30

Let's fix the errors rather than avoiding

7b7ce40

linter

ff8d73f

fix

54b8387

this is done

a11dfb5

riccardobrasca changed the title ~~test~~ chore: test fast_instance% everywhere May 25, 2026

riccardobrasca added 5 commits May 25, 2026 10:40

fix

c8805a9

another one

44493bd

ops

98333c7

two more

61fd75e

fix

9849b61

linter

13c8ec5

Fix proofs broken by simplification changes

dde7887

Merge remote-tracking branch 'upstream/master' into RB/fast_instance

3eb8c21

riccardobrasca closed this May 28, 2026

riccardobrasca deleted the RB/fast_instance branch May 28, 2026 19:24

Uh oh!

Conversation

riccardobrasca commented May 24, 2026

Uh oh!

github-actions Bot commented May 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 3eb8c21d31

Import changes for modified files

Declarations diff

⚠️ Scripts folder reminder

Uh oh!

github-actions Bot commented May 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

✅ PR Title Formatted Correctly

Uh oh!

kbuzzard May 24, 2026

Choose a reason for hiding this comment

Uh oh!

kbuzzard May 24, 2026

Choose a reason for hiding this comment

Uh oh!

riccardobrasca May 24, 2026

Choose a reason for hiding this comment

Uh oh!

kbuzzard commented May 24, 2026

Uh oh!

leanprover-radar commented May 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

kbuzzard May 24, 2026

Choose a reason for hiding this comment

Uh oh!

riccardobrasca May 24, 2026

Choose a reason for hiding this comment

Uh oh!

riccardobrasca commented May 24, 2026

Uh oh!

leanprover-radar commented May 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

kbuzzard commented May 25, 2026

Uh oh!

leanprover-radar commented May 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

riccardobrasca commented May 25, 2026

Uh oh!

leanprover-radar commented May 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

riccardobrasca commented May 25, 2026

Uh oh!

leanprover-radar commented May 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

riccardobrasca commented May 25, 2026

Uh oh!

leanprover-radar commented May 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

riccardobrasca commented May 28, 2026

Uh oh!

leanprover-radar commented May 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

github-actions Bot commented May 24, 2026 •

edited

Loading

github-actions Bot commented May 24, 2026 •

edited

Loading

leanprover-radar commented May 24, 2026 •

edited

Loading

leanprover-radar commented May 24, 2026 •

edited

Loading

leanprover-radar commented May 25, 2026 •

edited

Loading

leanprover-radar commented May 25, 2026 •

edited

Loading

leanprover-radar commented May 25, 2026 •

edited

Loading

leanprover-radar commented May 25, 2026 •

edited

Loading

leanprover-radar commented May 28, 2026 •

edited

Loading