Repository navigation
Complete Polylean source port - #132
Conversation
Proof profile (new / modified Lean files)
This is the parallel build wall clock and is the compile-time answer for this PR. The serial per-file sums below are useful for ranking slow files, not as a build budget. Total heartbeats: 0 maxHeartbeats units across 11 files (472 added LOC). Sum of Count-heartbeats wall-clock total: 14.77 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.Polylean |
2.50 s |
LeanPool.Polylean.ConjInvLength.LengthNode |
1.90 s |
LeanPool.Polylean.Complexes |
1.60 s |
LeanPool.Polylean.UnitConjecture.Tactics |
1.60 s |
LeanPool.Polylean.UnitConjecture.Tactics.ReduceGoal |
1.50 s |
LeanPool.Polylean.Polymath |
0.98 s |
LeanPool.Polylean.ConjInvLength |
0.68 s |
LeanPool.Polylean.Complexes.Structures.Invertegory |
0.48 s |
LeanPool.Polylean.Complexes.Structures.FreeGroupoid |
0.46 s |
LeanPool.Polylean.Complexes.Structures.TwoComplex |
0.45 s |
LeanPool.Polylean.Complexes.Constructions.UniversalCover |
0.39 s |
Per-file `lean --profile` output
LeanPool/Polylean.lean
import took 2.32s
cumulative profiling times:
elaboration 0.177ms
import 2.32s
initialization 28.5ms
interpretation 219ms
linting 0.21ms
parsing 0.0361ms
real 3.28
user 1.96
sys 1.33
LeanPool/Polylean/Complexes.lean
import took 1.01s
cumulative profiling times:
elaboration 0.163ms
import 1.01s
initialization 28ms
interpretation 59.3ms
linting 0.209ms
parsing 0.0331ms
real 1.70
user 0.96
sys 0.76
LeanPool/Polylean/Complexes/Constructions/UniversalCover.lean
import took 210ms
cumulative profiling times:
elaboration 0.385ms
import 210ms
initialization 28.1ms
interpretation 3.27ms
linting 0.118ms
parsing 0.0796ms
real 0.80
user 0.41
sys 0.41
LeanPool/Polylean/Complexes/Structures/FreeGroupoid.lean
import took 207ms
cumulative profiling times:
attribute application 0.0579ms
blocked (unaccounted) 1.16ms
compilation (IR) 0.0691ms
compilation (LCNF base) 0.871ms
compilation (LCNF impure) 0.342ms
compilation (LCNF mono) 1.62ms
elaboration 20.4ms
fix level params 0.0175ms
import 207ms
initialization 28.6ms
instantiate metavars 0.00661ms
interpretation 3.26ms
let-to-have transformation 0.00754ms
linting 0.881ms
parsing 2.04ms
process pre-definitions 0.273ms
share common exprs 0.0551ms
type checking 10.6ms
typeclass inference 0.449ms
real 0.82
user 0.44
sys 0.41
LeanPool/Polylean/Complexes/Structures/Invertegory.lean
import took 214ms
cumulative profiling times:
attribute application 0.679ms
blocked (unaccounted) 0.863ms
congr simp thm 1.3ms
elaboration 23ms
import 214ms
initialization 28.8ms
interpretation 3.69ms
linting 0.779ms
parsing 1.35ms
simp 0.381ms
type checking 14.2ms
typeclass inference 3.68ms
real 0.85
user 0.47
sys 0.42
LeanPool/Polylean/Complexes/Structures/TwoComplex.lean
import took 218ms
cumulative profiling times:
attribute application 0.0274ms
blocked (unaccounted) 1.32ms
elaboration 17.7ms
import 218ms
initialization 28.3ms
interpretation 3.7ms
linting 0.74ms
parsing 1.32ms
type checking 13.1ms
typeclass inference 0.749ms
real 0.86
user 0.48
sys 0.41
LeanPool/Polylean/ConjInvLength.lean
import took 525ms
cumulative profiling times:
elaboration 0.164ms
import 525ms
initialization 28.3ms
interpretation 32.6ms
linting 0.18ms
parsing 0.0328ms
real 1.18
user 0.67
sys 0.54
LeanPool/Polylean/ConjInvLength/LengthNode.lean
import took 513ms
cumulative profiling times:
attribute application 0.661ms
blocked (unaccounted) 0.291ms
compilation (IR) 3.2ms
compilation (LCNF base) 79ms
compilation (LCNF impure) 16.1ms
compilation (LCNF mono) 29.8ms
congr simp thm 2.38ms
dsimp 0.242ms
elaboration 212ms
fix level params 0.307ms
import 513ms
initialization 28.3ms
instantiate metavars 0.493ms
interpretation 146ms
let-to-have transformation 6.33ms
linting 15.7ms
parsing 15.1ms
process pre-definitions 47.6ms
share common exprs 2.6ms
simp 39.3ms
tactic execution 105ms
type checking 86.8ms
typeclass inference 190ms
real 1.82
user 1.70
sys 0.56
LeanPool/Polylean/Polymath.lean
import took 514ms
cumulative profiling times:
attribute application 0.0131ms
compilation (IR) 0.718ms
compilation (LCNF base) 23.2ms
compilation (LCNF impure) 3.95ms
compilation (LCNF mono) 6.66ms
elaboration 41.6ms
fix level params 0.0349ms
import 514ms
initialization 28.2ms
instantiate metavars 0.0423ms
interpretation 48.4ms
let-to-have transformation 1.09ms
linting 1.91ms
parsing 3.01ms
process pre-definitions 1.86ms
share common exprs 0.292ms
type checking 1.05ms
typeclass inference 22ms
real 1.29
user 0.77
sys 0.54
LeanPool/Polylean/UnitConjecture/Tactics.lean
import took 955ms
cumulative profiling times:
elaboration 0.125ms
import 955ms
initialization 28.3ms
interpretation 20.5ms
linting 0.102ms
parsing 0.0333ms
real 1.61
user 0.89
sys 0.74
LeanPool/Polylean/UnitConjecture/Tactics/ReduceGoal.lean
import took 903ms
cumulative profiling times:
attribute application 0.316ms
blocked (unaccounted) 29.6ms
compilation (IR) 0.634ms
compilation (LCNF base) 14.6ms
compilation (LCNF impure) 2.67ms
compilation (LCNF mono) 5.59ms
elaboration 20.7ms
fix level params 0.0456ms
import 903ms
initialization 28.5ms
instantiate metavars 0.0338ms
interpretation 4.91ms
let-to-have transformation 0.101ms
linting 1.11ms
parsing 1.71ms
process pre-definitions 1.65ms
share common exprs 0.272ms
type checking 1.98ms
typeclass inference 15.4ms
real 1.61
user 0.94
sys 0.70
Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.
60c5689 to
5c8bdf0
Compare
🤖 LLM review (
|
| Aspect | Value |
|---|---|
| Fit | 🛑 not_a_fit |
| Level | graduate |
| Branch | geometric group theory |
| Mode | mixed |
| Obscure problem | no |
| Code quality | 3 / 5 |
The contribution is auxiliary infrastructure for an existing project rather than a formalization of a named mathematical result.
Findings (1)
- no-headline-result — PR-wide
The PR is not a self-contained Lean Pool project and does not add a main theorem or completed named result. To be mergeable here, this should either be tied to a concrete formalized theorem in the Polylean project or submitted as part of a larger PR whose project card states the source, status, and mathematical endpoint.
Tokens: 8,960 in / 824 out · Tier: flex · Cost: $0.0348
Automated review against .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.
|
/review |
|
Maintainer context for the LLM review: this PR is not intended as a standalone new Lean Pool project. It is a source-completeness follow-up to the already-merged Polylean import in #109, whose registered headline declarations remain The purpose here is to fix the partial-port failure mode by restoring importable upstream source files that were missed in #109. The remaining omitted upstream files are blocked by active upstream For |
There was a problem hiding this comment.
Pull request overview
This PR completes a Lean Pool–compatible port of additional upstream Polylean modules by adding import indices and new modules for the Unit Conjecture tactics, conjugacy-invariant length computations (including proof-node caching/expansion), and a set of foundational “Complexes” structures (free groupoids, two-complexes, etc.), plus a small IO demonstration entry point.
Changes:
- Add new Polylean modules:
UnitConjecture/Tactics/ReduceGoal,ConjInvLength/LengthNode(+ConjInvLength.leanindex),Complexesstructure/construction stubs, andPolymath.lean. - Wire the new modules into existing import aggregators (
LeanPool/Polylean.lean,LeanPool.lean, andUnitConjecture/Tactics.lean). - Replace upstream
partial def-style behavior in the proof expansion code with fuel-bounded traversals.
Fit: good_fit
Level: research
Branch: group theory / topology-adjacent infrastructure
Mode: mixed
Obscure problem: false
Code quality: 3/5
Significance: Brings the Polylean port closer to source completeness and makes more of the upstream development importable in Lean Pool.
Verdict: request_changes
Specific findings:
Invertegory.invInvis currently ill-typed (unboundX Y) and will not compile.powerLengthallowsn = 0leading to division-by-zero floats and cache corruption.reduce_goalshould report unknown transparency modes via tactic errors, notpanic!.
Reviewed changes
Copilot reviewed 12 out of 12 changed files in this pull request and generated 4 comments.
Show a summary per file
| File | Description |
|---|---|
| LeanPool/Polylean/UnitConjecture/Tactics/ReduceGoal.lean | Adds a goal-reduction tactic parameterized by transparency mode. |
| LeanPool/Polylean/UnitConjecture/Tactics.lean | Imports the new ReduceGoal tactic module. |
| LeanPool/Polylean/Polymath.lean | Adds an IO demo entry point for conjugacy-invariant length computations. |
| LeanPool/Polylean/ConjInvLength/LengthNode.lean | Adds float-bound caching plus proof-node tracking and fuel-bounded proof expansion. |
| LeanPool/Polylean/ConjInvLength.lean | New import index for the conjugacy-invariant length subproject. |
| LeanPool/Polylean/Complexes/Structures/TwoComplex.lean | Introduces a TwoComplex class with a lifting principle. |
| LeanPool/Polylean/Complexes/Structures/Invertegory.lean | Introduces an intermediate “category with formal inverses” structure. |
| LeanPool/Polylean/Complexes/Structures/FreeGroupoid.lean | Adds free-groupoid universal property interfaces and inclusion prefuctor. |
| LeanPool/Polylean/Complexes/Constructions/UniversalCover.lean | Adds an importable stub module for universal cover constructions. |
| LeanPool/Polylean/Complexes.lean | New import index for the importable “Complexes” modules. |
| LeanPool/Polylean.lean | Wires new Polylean modules into the Polylean umbrella import. |
| LeanPool.lean | Wires new Polylean modules into the repository umbrella import. |
| class Invertegory (Obj : Sort _) extends Category Obj where | ||
| /-- Formal inverse of a morphism. -/ | ||
| inv : {X Y : Obj} → (X ⟶ Y) → (Y ⟶ X) | ||
| invInv : ∀ e : X ⟶ Y, inv (inv e) = e |
| | `default => .default | ||
| | `reducible => .reducible | ||
| | `instances => .instances | ||
| | _ => panic! "Unknown transparency mode" |
|
|
||
| /-- Improve a word-length bound using a power of the word. -/ | ||
| def powerLength : Wrd → Nat → IO Float | ||
| | w, n => do |
| | gen l => s!"l({l}) = 1 (normalization)" | ||
| | triang w₁ w₂ => s!"l({w₁ ++ w₂}) ≤ l({w₁}) + l({w₂}) (triangle inequality)" | ||
| | conj l w => s!"l({w}^{l}) = l({w}) (conjugacy invariance)" | ||
| | power n w => s!"l(w) ≤ l({w^n})/{n} (homogeneity)" |
|
/review |
Summary
ConjInvLength,UnitConjecture/Tactics/ReduceGoal,Complexes, and the Polymath executable module.partial defhelpers inConjInvLength/LengthNode.leanwith total/fuel-bounded Lean Pool-compatible definitions.Source-completeness note
After this branch, the only upstream Polylean files still not represented are
Complexes/Structures/SerreGraph.lean,Complexes/Structures/CombinatorialTwoComplex.lean, andComplexes/Constructions/FundamentalGroupoid.lean.SerreGraph.leanhas active upstreamsorrys, and the other two import it, so they are not Lean Pool importable yet.Validation
lake build LeanPool.Polyleanlake build LeanPoollake exe mk_all --checklake exe runLinter LeanPool.Polyleanlake exe lint-style ...on touched Polylean filescd python && uv run python -m lean_pool.quality --repo ..