Conversation
Proof profile (new / modified Lean files)
This build covers the changed modules and their dependency cones on top of the restored cache. The serial per-file sums below are useful for ranking slow files, not as a build budget. Total heartbeats: 8,360 maxHeartbeats units across 28 files (6,929 added LOC). Sum of Count-heartbeats wall-clock total: 243.45 s. Repeated import cost inside Heartbeat values come from Mathlib's LOC counts added lines in the profiled Lean files from this PR diff.
Aggregate phase totals
Slowest changed modules (from
|
| Changed module | Lake time |
|---|---|
LeanPool.OneManifold.OneMfld.CircleBlocks |
30.00 s |
LeanPool.OneManifold.OneMfld.RealIntervals |
29.00 s |
LeanPool.OneManifold.OneMfld.TransitionMono |
28.00 s |
LeanPool.OneManifold.OneMfld.Noncompact |
28.00 s |
LeanPool.OneManifold.OneMfld.CircleGlue |
25.00 s |
LeanPool.OneManifold.OneMfld.GlueUI |
21.00 s |
LeanPool.OneManifold.OneMfld.ClassifyInterval |
12.00 s |
LeanPool.OneManifold.OneMfld.GlueBlocks |
10.00 s |
LeanPool.OneManifold.OneMfld.NiceCharts |
8.90 s |
LeanPool.OneManifold.OneMfld.LocallyConnected |
8.40 s |
LeanPool.OneManifold.OneMfld.Normalize |
8.40 s |
LeanPool.OneManifold.OneMfld.GlueNNReal |
8.30 s |
Per-file `lean --profile` output
LeanPool/OneManifold.lean
import took 3.76s
cumulative profiling times:
elaboration 0.157ms
import 3.76s
initialization 30.1ms
interpretation 313ms
linting 0.303ms
module linting 0.00122ms
overlappingInstancesLinter 0.266ms
parsing 0.0294ms
tacticAnalysis 1.27ms
real 4.95
user 2.68
sys 2.31
LeanPool/OneManifold/OneMfld.lean
import took 3.7s
cumulative profiling times:
elaboration 0.0882ms
import 3.7s
initialization 31.2ms
interpretation 296ms
linting 0.16ms
module linting 0.00119ms
overlappingInstancesLinter 0.0965ms
parsing 0.00174ms
tacticAnalysis 0.427ms
real 4.88
user 2.63
sys 2.25
LeanPool/OneManifold/OneMfld/Charts.lean
import took 3.69s
cumulative profiling times:
attribute application 0.122ms
blocked (unaccounted) 2.22ms
compilation (IR) 0.0976ms
compilation (LCNF base) 0.696ms
compilation (LCNF impure) 0.393ms
compilation (LCNF mono) 0.352ms
congr simp thm 1.89ms
dsimp 0.84ms
elaboration 58.5ms
fix level params 0.38ms
import 3.69s
initialization 39.6ms
instantiate metavars 0.415ms
interpretation 356ms
let-to-have transformation 0.0902ms
linting 8.11ms
module linting 0.00144ms
overlappingInstancesLinter 3.53ms
parsing 5.41ms
process pre-definitions 2.97ms
share common exprs 0.844ms
simp 0.838ms
tactic execution 30.7ms
tacticAnalysis 14ms
type checking 21.4ms
typeclass inference 35.1ms
real 5.03
user 2.90
sys 2.28
LeanPool/OneManifold/OneMfld/CircleBlocks.lean
import took 3.65s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 120ms
cumulative profiling times:
attribute application 0.129ms
congr simp thm 2.48ms
elaboration 67.2ms
fix level params 1.36ms
import 3.65s
initialization 37.1ms
instantiate metavars 5.17ms
interpretation 949ms
let-to-have transformation 0.181ms
linting 44.9ms
module linting 0.0013ms
norm_num 11.3ms
overlappingInstancesLinter 4.39ms
parsing 30.7ms
process pre-definitions 36.6ms
ring 41.9ms
share common exprs 17.3ms
simp 36.4ms
tactic execution 350ms
tacticAnalysis 51.2ms
type checking 154ms
typeclass inference 1.05s
real 6.25
user 5.03
sys 2.26
LeanPool/OneManifold/OneMfld/CircleGlue.lean
import took 3.64s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 294ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 681ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 855ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.05s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.25s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.05s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.34s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.37s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_linarith_1._boxed took 102ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_linarith_1._boxed took 101ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_linarith_1._boxed took 196ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_linarith_1._boxed took 194ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_linarith_1._boxed took 100ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_linarith_1._boxed took 105ms
tactic execution of Lean.Parser.Tactic.rcases took 104ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_linarith_1._boxed took 196ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_linarith_1._boxed took 197ms
tactic execution of Lean.Parser.Tactic.exact took 132ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_linarith_1._boxed took 121ms
tactic execution of Lean.Parser.Tactic.exact took 126ms
tactic execution of Lean.Parser.Tactic.refine took 145ms
tactic execution of Lean.Parser.Tactic.refine took 125ms
tactic execution of Lean.Parser.Tactic.exact took 126ms
share common exprs took 110ms
tacticAnalysis took 143ms
linting took 112ms
tactic execution of Lean.Parser.Tactic.obtain took 196ms
cumulative profiling times:
attribute application 0.144ms
blocked (unaccounted) 22.5ms
congr simp thm 30.4ms
elaboration 194ms
fix level params 14.7ms
import 3.64s
initialization 30ms
instantiate metavars 41.7ms
interpretation 14.9s
let-to-have transformation 0.314ms
linting 248ms
module linting 0.00186ms
norm_num 3.39s
overlappingInstancesLinter 13.9ms
parsing 81.8ms
process pre-definitions 139ms
ring 380ms
share common exprs 176ms
simp 893ms
tactic execution 3.78s
tacticAnalysis 233ms
type checking 219ms
typeclass inference 3.13s
real 18.88
user 29.99
sys 2.37
LeanPool/OneManifold/OneMfld/Classification.lean
import took 3.67s
cumulative profiling times:
attribute application 0.0683ms
blocked (unaccounted) 11.7ms
compilation (IR) 0.0937ms
compilation (LCNF base) 2.77ms
compilation (LCNF impure) 0.53ms
compilation (LCNF mono) 0.728ms
congr simp thm 16ms
dsimp 4.07ms
elaboration 37.3ms
fix level params 2.16ms
import 3.67s
initialization 31.7ms
instantiate metavars 2.46ms
interpretation 587ms
let-to-have transformation 58.1ms
linting 29.4ms
module linting 0.00148ms
norm_num 1.87ms
overlappingInstancesLinter 5.55ms
parsing 20.5ms
process pre-definitions 111ms
ring 9.91ms
share common exprs 5.57ms
simp 287ms
tactic execution 397ms
tacticAnalysis 49.3ms
type checking 142ms
typeclass inference 3.08s
real 8.73
user 7.14
sys 2.29
LeanPool/OneManifold/OneMfld/ClassifyInterval.lean
import took 3.61s
Try this:
[apply] rwa [proj_relu hy']
Try this:
[apply] rwa [hy'] at this
Try this:
[apply] rwa [this]
Try this:
[apply] rwa [proj_relu]
Try this:
[apply] rwa [proj_relu]
Try this:
[apply] rwa [relu_proj] at h0z'
Try this:
[apply] rwa [proj_relu] at this
Try this:
[apply] rwa [proj_relu]
interpretation of Mathlib.Tactic.Tauto._aux_Mathlib_Tactic_Tauto___elabRules_Mathlib_Tactic_Tauto_tauto_1._boxed took 112ms
interpretation of Mathlib.Tactic.Tauto._aux_Mathlib_Tactic_Tauto___elabRules_Mathlib_Tactic_Tauto_tauto_1._boxed took 124ms
interpretation of Mathlib.Tactic.Tauto._aux_Mathlib_Tactic_Tauto___elabRules_Mathlib_Tactic_Tauto_tauto_1._boxed took 106ms
Try this:
[apply] rwa [relu_zero]
Try this:
[apply] rwa [hx]
Try this:
[apply] rwa [hz0]
Try this:
[apply] rwa [relu_proj] at this'
Try this:
[apply] rwa [c] at this'
Try this:
[apply] rwa [hz]
Try this:
[apply] rwa [← ht2]
Try this:
[apply] rwa [relu_zero] at this
cumulative profiling times:
attribute application 0.469ms
blocked (unaccounted) 357ms
compilation (IR) 0.244ms
compilation (LCNF base) 11.6ms
compilation (LCNF impure) 1.52ms
compilation (LCNF mono) 2.2ms
congr simp thm 9.6ms
dsimp 20ms
elaboration 130ms
fix level params 3.25ms
import 3.61s
initialization 41.2ms
instantiate metavars 13.9ms
interpretation 2.02s
let-to-have transformation 0.376ms
linting 95.5ms
module linting 0.00174ms
norm_num 53.8ms
overlappingInstancesLinter 13.2ms
parsing 72ms
process pre-definitions 43.4ms
ring 124ms
share common exprs 32.9ms
simp 382ms
tactic execution 1.39s
tacticAnalysis 182ms
type checking 206ms
typeclass inference 1.4s
real 6.83
user 8.40
sys 2.29
LeanPool/OneManifold/OneMfld/ClassifyOverlaps.lean
import took 3.64s
LeanPool/OneManifold/OneMfld/ClassifyOverlaps.lean:48:36: warning: `dif_pos` has been deprecated: Use `dite_eq_left` instead
LeanPool/OneManifold/OneMfld/ClassifyOverlaps.lean:49:36: warning: `dif_pos` has been deprecated: Use `dite_eq_left` instead
LeanPool/OneManifold/OneMfld/ClassifyOverlaps.lean:51:15: warning: `dif_pos` has been deprecated: Use `dite_eq_left` instead
LeanPool/OneManifold/OneMfld/ClassifyOverlaps.lean:51:27: warning: `dif_pos` has been deprecated: Use `dite_eq_left` instead
LeanPool/OneManifold/OneMfld/ClassifyOverlaps.lean:55:15: warning: `dif_pos` has been deprecated: Use `dite_eq_left` instead
LeanPool/OneManifold/OneMfld/ClassifyOverlaps.lean:55:27: warning: `dif_pos` has been deprecated: Use `dite_eq_left` instead
LeanPool/OneManifold/OneMfld/ClassifyOverlaps.lean:64:50: warning: `dif_pos` has been deprecated: Use `dite_eq_left` instead
LeanPool/OneManifold/OneMfld/ClassifyOverlaps.lean:71:50: warning: `dif_pos` has been deprecated: Use `dite_eq_left` instead
cumulative profiling times:
attribute application 0.186ms
congr simp thm 2.3ms
elaboration 136ms
fix level params 5.21ms
import 3.64s
initialization 30ms
instantiate metavars 6.18ms
interpretation 535ms
let-to-have transformation 2.98ms
linting 47.6ms
module linting 0.00118ms
overlappingInstancesLinter 9.54ms
parsing 30.9ms
process pre-definitions 33ms
share common exprs 11.6ms
simp 73.2ms
tactic execution 433ms
tacticAnalysis 76.9ms
type checking 67.3ms
typeclass inference 292ms
real 5.41
user 4.05
sys 2.23
LeanPool/OneManifold/OneMfld/ClosureOverlap.lean
import took 3.64s
cumulative profiling times:
attribute application 0.0127ms
congr simp thm 0.575ms
dsimp 0.241ms
elaboration 7.56ms
fix level params 0.122ms
import 3.64s
initialization 31.1ms
instantiate metavars 0.204ms
interpretation 352ms
let-to-have transformation 0.00966ms
linting 3.76ms
module linting 0.00106ms
overlappingInstancesLinter 2.02ms
parsing 3.77ms
process pre-definitions 0.869ms
share common exprs 0.302ms
simp 5.28ms
tactic execution 28ms
tacticAnalysis 11.7ms
type checking 2.66ms
typeclass inference 9.24ms
real 4.89
user 2.70
sys 2.23
LeanPool/OneManifold/OneMfld/Compactness.lean
import took 3.68s
cumulative profiling times:
attribute application 0.0788ms
congr simp thm 0.499ms
elaboration 16.4ms
fix level params 0.267ms
import 3.68s
initialization 35.3ms
instantiate metavars 0.53ms
interpretation 368ms
let-to-have transformation 0.0631ms
linting 9.17ms
module linting 0.0012ms
overlappingInstancesLinter 3.09ms
parsing 5.66ms
process pre-definitions 1.9ms
share common exprs 0.939ms
simp 2.49ms
tactic execution 52.5ms
tacticAnalysis 16.3ms
type checking 5.22ms
typeclass inference 147ms
real 4.97
user 2.90
sys 2.28
LeanPool/OneManifold/OneMfld/FiniteIntervalCharts.lean
import took 3.65s
cumulative profiling times:
attribute application 0.065ms
blocked (unaccounted) 1.1ms
elaboration 7.72ms
fix level params 0.0519ms
import 3.65s
initialization 31.1ms
instantiate metavars 0.0646ms
interpretation 321ms
let-to-have transformation 0.022ms
linting 1.51ms
module linting 0.00135ms
overlappingInstancesLinter 1.69ms
parsing 1.45ms
process pre-definitions 1.13ms
share common exprs 0.121ms
tactic execution 4.4ms
tacticAnalysis 3.23ms
type checking 3.7ms
typeclass inference 2.54ms
real 4.85
user 2.65
sys 2.23
LeanPool/OneManifold/OneMfld/FinitelyCharted.lean
import took 3.65s
cumulative profiling times:
attribute application 0.0101ms
congr simp thm 2.77ms
dsimp 4.24ms
elaboration 4.78ms
fix level params 0.173ms
import 3.65s
initialization 37.8ms
instantiate metavars 0.213ms
interpretation 331ms
let-to-have transformation 10.4ms
linting 2.27ms
module linting 0.00167ms
overlappingInstancesLinter 1.46ms
parsing 3.51ms
process pre-definitions 12ms
share common exprs 0.544ms
simp 16.3ms
tactic execution 26ms
tacticAnalysis 5.75ms
type checking 22.9ms
typeclass inference 12.5ms
real 4.93
user 2.76
sys 2.21
LeanPool/OneManifold/OneMfld/GlueBlocks.lean
import took 3.68s
cumulative profiling times:
attribute application 0.0605ms
congr simp thm 2.86ms
elaboration 27.2ms
fix level params 0.759ms
import 3.68s
initialization 29.4ms
instantiate metavars 2.17ms
interpretation 627ms
let-to-have transformation 0.102ms
linting 20.1ms
module linting 0.00179ms
norm_num 59.1ms
overlappingInstancesLinter 2.93ms
parsing 16ms
process pre-definitions 29.2ms
ring 36.6ms
share common exprs 11ms
simp 19.6ms
tactic execution 273ms
tacticAnalysis 32.8ms
type checking 101ms
typeclass inference 605ms
real 6.01
user 4.12
sys 2.27
LeanPool/OneManifold/OneMfld/GlueCore.lean
import took 3.66s
cumulative profiling times:
attribute application 0.0492ms
blocked (unaccounted) 0.408ms
congr simp thm 0.39ms
dsimp 4.86ms
elaboration 41.5ms
fix level params 1.12ms
import 3.66s
initialization 30ms
instantiate metavars 2.04ms
interpretation 424ms
let-to-have transformation 0.0843ms
linting 28.2ms
module linting 0.00126ms
overlappingInstancesLinter 4.06ms
parsing 19.9ms
process pre-definitions 8.6ms
share common exprs 2.96ms
simp 3.14ms
tactic execution 251ms
tacticAnalysis 44.8ms
type checking 18.9ms
typeclass inference 88.3ms
real 5.10
user 3.20
sys 2.28
LeanPool/OneManifold/OneMfld/GlueNNReal.lean
import took 3.67s
cumulative profiling times:
attribute application 0.0127ms
congr simp thm 1.5ms
elaboration 16.5ms
fix level params 0.961ms
import 3.67s
initialization 34.6ms
instantiate metavars 2.59ms
interpretation 380ms
let-to-have transformation 0.0359ms
linting 15.1ms
module linting 0.00134ms
overlappingInstancesLinter 2.72ms
parsing 8.96ms
process pre-definitions 5.72ms
share common exprs 3.62ms
simp 14.3ms
tactic execution 218ms
tacticAnalysis 32.8ms
type checking 16.9ms
typeclass inference 89.9ms
real 5.34
user 3.12
sys 2.25
LeanPool/OneManifold/OneMfld/GlueUI.lean
import took 3.69s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.1s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.02s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.31s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.55s
cumulative profiling times:
attribute application 0.0169ms
congr simp thm 6.13ms
elaboration 25.7ms
fix level params 2.26ms
import 3.69s
initialization 29.9ms
instantiate metavars 5.82ms
interpretation 6.12s
let-to-have transformation 0.0383ms
linting 43.9ms
module linting 0.00131ms
norm_num 139ms
overlappingInstancesLinter 5.39ms
parsing 15ms
process pre-definitions 27.2ms
ring 52.3ms
share common exprs 20.9ms
simp 241ms
tactic execution 621ms
tacticAnalysis 91.2ms
type checking 41.1ms
typeclass inference 1.26s
real 13.27
user 11.07
sys 2.24
LeanPool/OneManifold/OneMfld/IntervalCharts.lean
import took 3.68s
cumulative profiling times:
attribute application 0.0838ms
blocked (unaccounted) 1.29ms
elaboration 16.5ms
fix level params 0.0928ms
import 3.68s
initialization 31.7ms
instantiate metavars 0.153ms
interpretation 328ms
let-to-have transformation 0.0161ms
linting 3.11ms
module linting 0.00119ms
overlappingInstancesLinter 1.76ms
parsing 2.91ms
process pre-definitions 1.52ms
share common exprs 0.284ms
tactic execution 14.7ms
tacticAnalysis 6.4ms
type checking 5.63ms
typeclass inference 13.2ms
real 4.94
user 2.76
sys 2.23
LeanPool/OneManifold/OneMfld/LocallyConnected.lean
import took 3.68s
cumulative profiling times:
attribute application 0.284ms
congr simp thm 1.5ms
dsimp 40.6ms
elaboration 13.6ms
fix level params 0.669ms
import 3.68s
initialization 41.7ms
instantiate metavars 3.36ms
interpretation 463ms
let-to-have transformation 0.00605ms
linting 6.43ms
module linting 0.00142ms
norm_num 31ms
overlappingInstancesLinter 1.27ms
parsing 7.42ms
process pre-definitions 7.6ms
ring 36ms
share common exprs 11.2ms
simp 44.5ms
tactic execution 241ms
tacticAnalysis 17.7ms
type checking 35.2ms
typeclass inference 323ms
real 5.84
user 3.65
sys 2.23
LeanPool/OneManifold/OneMfld/NiceCharts.lean
import took 3.68s
cumulative profiling times:
attribute application 0.126ms
blocked (unaccounted) 2.52ms
congr simp thm 4.77ms
dsimp 28.3ms
elaboration 48.7ms
fix level params 0.899ms
import 3.68s
initialization 31.3ms
instantiate metavars 0.975ms
interpretation 373ms
let-to-have transformation 7.51ms
linting 12.1ms
module linting 0.00175ms
overlappingInstancesLinter 3.13ms
parsing 8.43ms
process pre-definitions 12.5ms
share common exprs 2.66ms
simp 71.9ms
tactic execution 105ms
tacticAnalysis 19.4ms
type checking 44ms
typeclass inference 162ms
real 5.32
user 3.22
sys 2.27
LeanPool/OneManifold/OneMfld/Noncompact.lean
import took 3.64s
cumulative profiling times:
attribute application 0.0236ms
congr simp thm 1.19ms
elaboration 3.4ms
fix level params 0.0522ms
import 3.64s
initialization 29.6ms
instantiate metavars 0.199ms
interpretation 322ms
let-to-have transformation 0.0123ms
linting 2.95ms
module linting 0.00126ms
overlappingInstancesLinter 0.796ms
parsing 2.96ms
process pre-definitions 1.01ms
share common exprs 0.313ms
simp 24.6ms
tactic execution 33.8ms
tacticAnalysis 5.75ms
type checking 3.42ms
typeclass inference 60.6ms
real 4.91
user 2.73
sys 2.24
LeanPool/OneManifold/OneMfld/Normalize.lean
import took 3.67s
cumulative profiling times:
attribute application 2.71ms
compilation (IR) 0.0817ms
compilation (LCNF base) 1.48ms
compilation (LCNF impure) 0.364ms
compilation (LCNF mono) 0.709ms
congr simp thm 0.912ms
elaboration 41.4ms
fix level params 0.714ms
import 3.67s
initialization 35.2ms
instantiate metavars 1.06ms
interpretation 387ms
let-to-have transformation 8.86ms
linting 11ms
module linting 0.00143ms
overlappingInstancesLinter 3.58ms
parsing 10ms
process pre-definitions 23.1ms
share common exprs 2.38ms
simp 3.65ms
tactic execution 160ms
tacticAnalysis 23.5ms
type checking 47ms
typeclass inference 177ms
real 5.29
user 3.21
sys 2.25
LeanPool/OneManifold/OneMfld/Outer.lean
import took 3.64s
LeanPool/OneManifold/OneMfld/Outer.lean:118:13: warning: Variable name `hx` is not explicitly referenced.
Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
[apply] _hx
Note: This linter can be disabled with `set_option linter.unusedVariables false`
cumulative profiling times:
attribute application 0.115ms
congr simp thm 0.488ms
elaboration 60ms
fix level params 1.99ms
import 3.64s
initialization 38.5ms
instantiate metavars 3.66ms
interpretation 589ms
let-to-have transformation 0.178ms
linting 46ms
module linting 0.00115ms
overlappingInstancesLinter 7.61ms
parsing 25.8ms
process pre-definitions 15.6ms
share common exprs 5.67ms
simp 2.26ms
tactic execution 389ms
tacticAnalysis 84.6ms
type checking 30.4ms
typeclass inference 199ms
real 5.12
user 3.68
sys 2.28
LeanPool/OneManifold/OneMfld/PartialHomeomorphHelpers.lean
import took 3.66s
cumulative profiling times:
attribute application 0.0449ms
congr simp thm 0.87ms
elaboration 10.2ms
fix level params 0.263ms
import 3.66s
initialization 35.6ms
instantiate metavars 0.271ms
interpretation 331ms
let-to-have transformation 0.0357ms
linting 3.97ms
module linting 0.00129ms
overlappingInstancesLinter 2.08ms
parsing 2.75ms
process pre-definitions 1.02ms
share common exprs 0.552ms
simp 7.04ms
tactic execution 23ms
tacticAnalysis 7.83ms
type checking 3.33ms
typeclass inference 6.34ms
real 4.89
user 2.74
sys 2.21
LeanPool/OneManifold/OneMfld/RealIntervals.lean
import took 3.63s
LeanPool/OneManifold/OneMfld/RealIntervals.lean:23:49: warning: `dif_pos` has been deprecated: Use `dite_eq_left` instead
cumulative profiling times:
attribute application 7.34ms
blocked (unaccounted) 188ms
compilation (IR) 0.465ms
compilation (LCNF base) 3.95ms
compilation (LCNF impure) 2.74ms
compilation (LCNF mono) 5.36ms
congr simp thm 3.91ms
dsimp 7.86ms
elaboration 163ms
fix level params 1.15ms
import 3.63s
initialization 39.4ms
instantiate metavars 3.09ms
interpretation 751ms
let-to-have transformation 0.352ms
linting 57.9ms
module linting 0.00164ms
norm_num 0.908ms
overlappingInstancesLinter 9.3ms
parsing 29.4ms
process pre-definitions 15ms
ring 17.3ms
share common exprs 8.74ms
simp 21.2ms
tactic execution 407ms
tacticAnalysis 90.9ms
type checking 76ms
typeclass inference 300ms
real 5.33
user 4.21
sys 2.26
LeanPool/OneManifold/OneMfld/TransitionMono.lean
import took 3.7s
cumulative profiling times:
attribute application 0.0344ms
congr simp thm 0.39ms
elaboration 12.6ms
fix level params 0.0715ms
import 3.7s
initialization 29.9ms
instantiate metavars 0.151ms
interpretation 334ms
let-to-have transformation 0.0321ms
linting 4.53ms
module linting 0.00119ms
overlappingInstancesLinter 1.2ms
parsing 3.11ms
process pre-definitions 0.879ms
share common exprs 0.383ms
simp 5.29ms
tactic execution 29.4ms
tacticAnalysis 6.77ms
type checking 3.2ms
typeclass inference 33.6ms
real 4.91
user 2.78
sys 2.22
LeanPool/OneManifold/OneMfld/TwoComponents.lean
import took 3.68s
cumulative profiling times:
attribute application 0.064ms
congr simp thm 0.589ms
dsimp 7.28ms
elaboration 66.8ms
fix level params 2.89ms
import 3.68s
initialization 37.9ms
instantiate metavars 6.52ms
interpretation 536ms
let-to-have transformation 0.168ms
linting 46ms
module linting 0.00154ms
overlappingInstancesLinter 4.95ms
parsing 26.9ms
process pre-definitions 20.4ms
share common exprs 7.98ms
simp 6.39ms
tactic execution 546ms
tacticAnalysis 73ms
type checking 32.7ms
typeclass inference 209ms
real 5.25
user 3.91
sys 2.23
LeanPool/OneManifold/OneMfld/UnitInterval.lean
import took 3.67s
cumulative profiling times:
attribute application 0.763ms
elaboration 10.7ms
fix level params 0.0303ms
import 3.67s
initialization 35.7ms
instantiate metavars 0.0609ms
interpretation 318ms
let-to-have transformation 0.019ms
linting 1.31ms
module linting 0.00114ms
overlappingInstancesLinter 1.58ms
parsing 1.02ms
process pre-definitions 0.776ms
share common exprs 0.125ms
tactic execution 2.54ms
tacticAnalysis 2.9ms
type checking 1.06ms
typeclass inference 28.7ms
real 4.88
user 2.71
sys 2.21
LeanPool/OneManifold/Solution.lean
import took 3.62s
cumulative profiling times:
attribute application 0.0121ms
elaboration 3.78ms
fix level params 0.0286ms
import 3.62s
initialization 29.9ms
instantiate metavars 0.041ms
interpretation 303ms
let-to-have transformation 0.0111ms
linting 0.769ms
module linting 0.00121ms
overlappingInstancesLinter 1.66ms
parsing 0.769ms
process pre-definitions 0.174ms
share common exprs 0.0882ms
tactic execution 3.23ms
tacticAnalysis 1.92ms
type checking 0.427ms
typeclass inference 3.23ms
real 4.80
user 2.59
sys 2.23
Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.
Vilin97
changed the title
Automation disposition: needs-maintainerReviewed exact head No concrete author-actionable defect was established in this bounded review that would justify an ordinary change request. The PR is still marked draft, so protected merge is not permitted. Maintainer decision required: confirm the headline result's significance, faithfulness, novelty, source/provenance and scope, then ask the author to mark the PR ready (or give scope direction). This is a maintainer disposition, not an approval. |
Vilin97
added
the
needs-maintainer
|
/review |
|
Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict. [Low risk] Adds mathematical proofs about one-dimensional manifolds. No outstanding review finding blocks this PR, but current-head aggregate validation remains to be confirmed before merging. SummaryImports the compact connected one-manifold classification, its chart and gluing development, real-interval API, and proved solution bridge.
Reviews (17) · Last reviewed commit: "Merge remote-tracking branch 'origin/mai..." |
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
🤖 LLM review (
|
| Rubric | Verdict | Bottom line |
|---|---|---|
| Faithfulness | ✅ pass |
The Lean faithfully proves the card’s compact connected one-manifold classification without undisclosed mathematical assumptions. |
| Novelty | ✅ pass |
No declaration subsuming OneMfld.homeomorph_circle_or_unitInterval was found in pinned Mathlib v4.34.0 or the existing pool. |
| Significance | ✅ pass |
The classical classification of compact connected one-manifolds is a substantial graduate-level topology result and a good fit for the pool. |
| Sources | ✅ pass |
The pinned upstream solution states the claimed classification with identical hypotheses, and the PR credits the prior formalization and Gale’s outline. |
| Code quality (advisory) | 🤔 discuss |
Duplicated foundational proofs and parallel representations leave enough maintenance debt to warrant a human cleanup decision. |
| Aspect | Value |
|---|---|
| Proves the claim | ✅ proves_it |
| Assumed, not proved | CompactSpace M, ConnectedSpace M (including nonemptiness), T2Space M, and ChartedSpace NNReal M express the card’s hypotheses; the refined finite atlas, overlap classification, and gluing results are constructed and proved rather than assumed. |
| Matches cited source | ✅ matches |
| Fit | ✅ good_fit |
| Level | graduate |
| Branch | geometric topology |
| Mode | theory_building |
| Code quality | 2 / 5 |
Statement check: OneMfld.homeomorph_circle_or_unitInterval proves that every compact connected Hausdorff space charted on NNReal admits a homeomorphism to Mathlib’s Circle or the real subtype {x | 0 ≤ x ∧ x ≤ 1}.
OneMfld.homeomorph_circle_or_unitInterval completes the circle-or-closed-interval classification through a substantial development of chart refinement, overlap structure, gluing, and finite-atlas induction.
Code quality findings (2)
- proof-duplication —
LeanPool/OneManifold/OneMfld/NiceCharts.lean:33
improvedChart repeats the restriction construction and its membership/boundedness proofs in both branches, although Iio (y + 1) is a bounded open neighborhood of every y : NNReal. Similar substantial duplication occurs in Compactness.noncompact_ioo'/noncompact_iio' and the two Möbius reparametrizations in CircleGlue.exists_normalized_charts. These parallel proof bodies multiply the places requiring repair when underlying APIs change. Use a uniform neighborhood here, extract the common noncompact-open-set argument, and package chart reparametrization once for both charts.
Evidence: In improvedChart:by_cases h0 : y > 0selectslet interval := Set.Ioo (y-1) (y+1)orlet interval := Set.Iio (1 : NNReal); both repeatlet t := φ.target ∩ interval,let s := φ.symm '' t,let φ' := φ.restrOpen s sOpen, andrw [restrOpen_symm_image_target φ (t := t) Set.inter_subset_left] at hz'. In Compactness.lean, bothlemma noncompact_ioo'andlemma noncompact_iio'repeathave hc : IsCompact s := by exact isCompact_iff_compactSpace.mpr h',have hs : IsClosed s := by exact IsCompact.isClosed hc, and the nested contradiction beginninghave : ¬ IsCompact (Set.univ : Set NNReal) := by. CircleGlue.exists_normalized_charts likewise separately constructsset A := a₀.toOpenPartialHomeomorph.trans mA with hAdefandset B := B₁.trans mB with hBdef, repeating source, target, image, and endpoint-order proofs. - duplicate-definition —
LeanPool/OneManifold/OneMfld/ClassifyInterval.lean:327
The foundational API maintains multiple representations of the same objects. relu duplicates Real.toNNReal, already used elsewhere in this PR, and rebuilds its basic continuity/projection/order API. UnitInterval similarly duplicates Mathlib's unitInterval while LocallyConnected uses the existing unitInterval API. Within NiceCharts, the unused NiceChartAt structure duplicates the dependent subtype returned by niceChart; no added file consumes it. These alternatives create unnecessary rewriting and obscure which representation downstream code should use. Prefer the existing primitives, retaining compatibility abbreviations or thin wrappers where needed, and either use NiceChartAt as the construction's result or remove it.
Evidence: ClassifyInterval.lean definesdef relu (x : ℝ) : NNReal := NNReal.mk (max x 0) (by simp)and separately provestheorem continuous_relu : Continuous relu,lemma relu_proj {x : NNReal} : (relu x.toReal) = x, andlemma relu_mono : StrictMonoOn relu (Set.Ici 0). CircleBlocks.affineNNRealOPH already usesinvFun := fun y => Real.toNNReal ((y - d) / k)andcontinuous_real_toNNReal.comp. UnitInterval.lean definesdef UnitInterval : Set Real := { x : Real | 0 ≤ x ∧ x ≤ 1 }andlemma UnitInterval_eq_Icc : UnitInterval = Set.Icc (0 : Real) 1 := rfl. NiceCharts.niceChart returns{ ψ : OpenPartialHomeomorph M NNReal | x ∈ ψ.source ∧ Bornology.IsBounded ψ.target ∧ ConnectedSpace ψ.target }, whilestructure NiceChartAt (x : M) whererepeats the fieldschart,mem_chart_source,bounded, andconnected.
Tokens: 7,265,377 in / 26,723 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $147.3118 (Standard API equivalent; uncached input)
Each rubric is an independent review against .github/review-rubrics/ on top of .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.
# Conflicts: # LeanPool.lean
Changes requested by automated reviewReviewed exact current head The exact-head Build project check fails because Acceptance condition: repair the named defect on a new head and make all required protected checks green. Do not change repository policy or add waivers. |
Vilin97
removed
the
needs-maintainer
Changes requested by automated reviewReviewed head
Review coverage: complete changed-file inventory and full diff retained; 28 changed project files, 7,188 lines, import reachability and executable trust-token scan; advertised endpoints and supporting definitions examined with bounded implementation sampling and existing review findings reconciled. Potential reusable value: Chart transition and interval/circle classification infrastructure. Source/provenance and prior-art evidence were considered separately from CI; these findings do not assert that every proof line was manually read. Earlier automated scores are advisory and are not approval of this failing head. |
Vilin97
added
the
needs-manual-rebase
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
{
"reviewed_head": "83cb928262cc40232304be4d1c52c9a658831530",
"recommendation": "approve",
"scope": "Bounded maintenance review plus reconciliation with the prior source review; fresh aggregate CI remains pending.",
"statement": "For a compact connected Hausdorff space charted on NNReal, the public endpoint proves existence of a homeomorphism to Circle or the closed unit interval. ConnectedSpace includes nonemptiness. Its name and type are unchanged.",
"changes": [
"Project-owned declarations are contained in OneMfld; the public card bridge remains OneMfld.homeomorph_circle_or_unitInterval.",
"Removed the unused RealIntervals module after checking declaration, import, and card consumers. Pinned Mathlib supplies IsPreconnected.mem_intervals and the interval closure/interior/frontier facts. No retained proof depends on this module.",
"Removed the redundant inferred LocallyConnectedSpace Real instance; retained the NNReal proof."
],
"validation": {
"warning_free_project_modules": 27,
"declaration_linters": "all 15 pass",
"style_and_generated_index": "pass",
"public_api_probe": "original theorem type and namespaced API pass; former root names absent",
"axiom_audit_declarations": 153,
"compiled_environment_audit": "pass",
"static_headers_sizes_reachability_metadata": "pass",
"main_cards_preserved": 218,
"post_build_edit": "Trimmed one trailing blank line in the import-only index; executable tokens unchanged and git diff --check passes."
},
"source": "https://raw.githubusercontent.com/sweeneyde/1mfld/83e961ba28dd8182e7bae844756aba614eb1512e/README.md",
"maintenance_judgment": "The remaining interval wrappers and proof scaffolding are nonblocking; this patch addresses the three concrete outstanding threads without changing the classification scope.",
"findings": []
}
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Reconciled exact current head 50bc0d1f9ae1cdcda81cc83d8e5daf2121aac9d0 (restoration 66db25f6, followed by its aggregate-index update). Recommendation: approve after fresh required CI passes.
The later contributor commit explicitly restores the complete upstream real-interval results inside OneMfld. The delta from previously validated 83cb9282 is only RealIntervals.lean and its imports in the project/root indexes. After removing the enclosing OneMfld namespace, the restored module's executable tokens exactly match the previously reviewed pre-removal source. Its API is now contained in OneMfld.RealIntervals; all other project namespace fixes, the public classification bridge and removal of the duplicate Real instance remain intact.
This corrects my earlier removal disposition: the parallel interval API remains to preserve the complete source development. Its Mathlib overlap and lack of external consumers are accepted nonblocking maintenance debt, rather than a claim that the API was removed. The compact one-manifold classification statement is unchanged.
The earlier 27-module compiler/linter/axiom checks apply to 83cb9282; they did not compile this subsequently restored module. This source reconciliation is read-only. Fresh required CI must validate the full restored exact head before merge.
Vilin97
removed
the
needs-manual-rebase
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
{
"reviewed_head": "50e9f9bc72d4e6622cb63d87725646d22d43aa8d",
"recommendation": "approve after required current-head CI passes",
"scope": "Full incoming four-file source audit, carrying forward the prior substantive review at50bc0d1f and source-identical5111ee05 reconciliation.",
"findings": [],
"changes": "Consolidates chart-transition continuity/injectivity and Hausdorff endpoint-limit arguments; moves overlap_mono_on into publicly imported GlueCore and specializes overlap_mono. Shortens relu/strict-monotonicity proofs and proves continuity of the same NNReal path using standard continuous operations.",
"contracts": "All41 existing named declaration headers in the changed files are byte-identical. Both added helpers are proved; source/target membership, nonbottom-filter and Hausdorff hypotheses remain explicit, with the same endpoint and monotonicity orientations. The public compact connected one-manifold classification statement is unchanged.",
"preservation": {
"project_files_retained": 28,
"unchanged_project_files": 24,
"own_card_bytes": "unchanged",
"own_project_and_root_index_imports": "unchanged",
"restored_RealIntervals": "unchanged"
},
"validation": "Complete old/new proof contexts independently reviewed twice; declaration/inventory/import/card checks and whitespace check pass. No fresh local compilation was performed. Earlier compiler evidence remains limited to its previously recorded head; fresh required CI must validate this exact head."
}
|
/review Please reassess exact head |
Vilin97
added
the
needs-maintainer
Daily disposition: needs maintainer — protected merge operationReviewed exact head
The remaining authority boundary is operational: this repository has |
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
{
"summary": "Source approval carried forward to e63fd21. The incoming relu_interval_ioo repair rewrites the interval equality in the membership hypothesis, producing exactly the required preimage membership. Its theorem, graph-free interval construction, reverse inclusion and all other project source are unchanged. The earlier complete source assessment is retained; fresh required CI remains necessary before merge.",
"assessment": {
"scope": "focused membership proof repair",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "more_robust",
"risk": "low",
"assessment_one_sentence": "The explicit rewrite replaces an ill-typed transport without changing the mathematical statement or adding assumptions."
},
"verdict": "approve",
"findings": [],
"validation": {
"exact_incoming_head": "e63fd2175bf7da63c3d7c8634e9b2e0395e34f18",
"inventory": "All 28 project files retained; 27 byte-identical to the previously reviewed head; own card bytes/value and project root-index imports preserved.",
"exact_incoming_source_checks": "Actual target text style in pinned Lake environment, four recursive scoped source gates, whitespace, pinned mk_all --module --check, source/config/dependency/output stability checks passed.",
"compiler_scope": "A mathematically equivalent local simpa-only proof variant compiled warning-free and passed the unchanged API/allowed-axiom probe and one-module declaration linter. The importer rw-at-hy variant is preserved here and was source-reviewed, not recompiled locally. No exact-head aggregate compiler claim is made.",
"guard_qualification": "The original validator stopped at a style executable environment error before its final hash assertions. A separate finishing stage ran the real target style check with correct Lake configuration and verified its own before/after hashes; this does not retroactively claim the original final guard ran.",
"publication": "No new source commit, push, main refresh, gate change or CI queue action."
}
}
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
{
"reviewed_commit": "cc5e2fc1a0c38897b7abb88d4b3a894cb4a271d7",
"review_type": "focused_code_quality_followup",
"conclusion": "The two-proof helper refactor passes source review and scoped validation. The author’s Do not merge hold remains; fresh exact-head CI is required.",
"scope": {
"files": [
"LeanPool/OneManifold/OneMfld/CircleBlocks.lean",
"LeanPool/OneManifold/OneMfld/CircleGlue.lean"
],
"finding": "PRRT_kwDOSY3yXM6mOSSr",
"change": "Extract 12 private proof helpers for inverse, continuity, interval-image, chart orientation/composition, and common interval shrinking; reduce both long construction bodies to short compositions.",
"preservation": "All 27 existing explicit declaration headers retained; all 12 new helpers remain private; Möbius forward function, inverse lambda, source and target are definitionally unchanged. Both normalized charts retain their exact endpoint/image contracts and strict 1/4 bounds. No card/configuration/option changes."
},
"review_basis": "Focused follow-up carrying prior project assessments; root and independent peer read both complete old/new constructions and all new helper proofs. This is not a new five-axis project audit.",
"validation": {
"compilation": "All 14 modules in the changed files’ project dependency closure compiled warning-free: 12 retained from the prior bounded run and the two changed modules from the preceding successful compilation stages; the final runs reused those artifacts for API, axiom, linter, style and index checks only.",
"api": "Four rfl checks for the Möbius computational fields; checks of the original Möbius subtype contract and downstream public circle-chart theorem.",
"trust": {
"OneMfld.mobiusOPH'": [
"Classical.choice",
"Quot.sound",
"propext"
],
"OneMfld.exists_circle_chart": [
"Classical.choice",
"Quot.sound",
"propext"
]
},
"linters": "One native --no-build linter invocation covering the 14-module project closure; native style on the two changed files.",
"other_checks": "Four scoped source quality gates, git diff --check and actual pinned mk_all --module --check passed.",
"limits": "Serial Lean -j2 under 8 GiB memory/zero swap, explicit timeouts, no donor artifacts. No full-project/pool build or remote CI claim."
},
"remaining": "Preserve Do not merge instruction and require fresh exact-head required CI/branch protection before any merge."
}
This branch has not been deployed
1 participant
Imports the compact connected one-manifold classification from https://github.com/sweeneyde/1mfld at
83e961ba28dd8182e7bae844756aba614eb1512e. For a compact connected Hausdorff space charted on the half-line,OneMfld.homeomorph_circle_or_unitIntervalproves existence of a homeomorphism to a circle or closed unit interval. The chart refinement, overlap classification, gluing, finite-atlas induction, real-interval results, and proved solution bridge are retained.The Lean/Mathlib 4.34 port uses the required module system and places project-owned declarations under
OneMfld. Checkpoint50bc0d1f9preserves the namespace migration and restores the complete 511-lineRealIntervals.leanAPI with its public imports, including the generated root library index. All 28 project files remain in scope. Jim Fowler and Dennis Sweeney’s attribution, Apache-2.0 license, and mixed proof provenance are recorded. Excluded upstream files are the duplicate openChallenge.leanstatement and upstream Lake configuration.Validation at
50bc0d1f9: the earlier checkpoint pool job passes module/index generation, compilation, declaration linters, text style, and repository quality checks. Recursive local static/header/proof-size and diff checks also pass. All restored real-interval content participates in the successful aggregate build. Auxiliary documentation/metadata jobs and independent review remain separate; no checks or linter settings changed. Do not merge.Latest checkpoint
50e9f9bc7shares chart-transition continuity/injectivity and endpoint arguments, derives overlap monotonicity from that common API, and reuses elementary interval-image and path-continuity results. It retains all 37 affected theorem headers and all 28 project files, including the full real-interval API. The four-file refactor has source review and passes recursive static/header/size and diff checks; its compiler validation and fresh aggregate CI remain pending. No limits or gates changed.