Repository navigation
Import demazureoperatorslean formalization - #89
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: 3,742 maxHeartbeats units across 5 files (1,149 added LOC). Sum of Count-heartbeats wall-clock total: 20.68 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.DemazureOperatorsLean.DemazureAuxRelations |
6.80 s |
LeanPool.DemazureOperatorsLean.Demazure |
4.10 s |
LeanPool.DemazureOperatorsLean.DemazureAux |
3.30 s |
LeanPool.DemazureOperatorsLean.DemazureRelations |
2.50 s |
LeanPool.DemazureOperatorsLean |
2.00 s |
Per-file `lean --profile` output
LeanPool/DemazureOperatorsLean.lean
import took 1.88s
cumulative profiling times:
elaboration 0.159ms
import 1.88s
initialization 27ms
interpretation 202ms
linting 0.279ms
parsing 0.0309ms
real 2.74
user 1.65
sys 1.11
LeanPool/DemazureOperatorsLean/Demazure.lean
import took 1.92s
simp took 289ms
cumulative profiling times:
attribute application 4.35ms
blocked (unaccounted) 60.2ms
compilation (IR) 0.261ms
compilation (LCNF base) 3.97ms
compilation (LCNF impure) 1.58ms
compilation (LCNF mono) 4.28ms
congr simp thm 10.3ms
dsimp 2.54ms
elaboration 243ms
fix level params 2.2ms
import 1.92s
initialization 27ms
instantiate metavars 5.95ms
interpretation 678ms
let-to-have transformation 6.51ms
linting 30.7ms
norm_num 2.44ms
parsing 29.1ms
process pre-definitions 22.8ms
ring 18.1ms
share common exprs 17.9ms
simp 924ms
tactic execution 479ms
type checking 240ms
typeclass inference 2.75s
real 4.41
user 6.85
sys 1.20
LeanPool/DemazureOperatorsLean/DemazureAux.lean
import took 1.83s
Try this:
[apply] ring_nf
The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
Try this:
[apply] ring_nf
The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
Try this:
[apply] ring_nf
The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
Try this:
[apply] ring_nf
The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
Try this:
[apply] ring_nf
The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
cumulative profiling times:
attribute application 4.84ms
blocked (unaccounted) 0.392ms
compilation (IR) 0.084ms
compilation (LCNF base) 1.21ms
compilation (LCNF impure) 0.438ms
compilation (LCNF mono) 1.36ms
congr simp thm 29.2ms
elaboration 225ms
fix level params 2.3ms
import 1.83s
initialization 26.7ms
instantiate metavars 10.7ms
interpretation 799ms
let-to-have transformation 0.458ms
linting 30ms
norm_num 5.29ms
parsing 28.8ms
process pre-definitions 29.7ms
ring 139ms
share common exprs 28.7ms
simp 388ms
tactic execution 615ms
type checking 173ms
typeclass inference 1.1s
real 3.69
user 5.01
sys 1.12
LeanPool/DemazureOperatorsLean/DemazureAuxRelations.lean
import took 1.82s
ring took 614ms
instantiate metavars took 135ms
share common exprs took 765ms
process pre-definitions took 208ms
elaboration took 604ms
type checking took 946ms
cumulative profiling times:
attribute application 0.336ms
compilation (IR) 0.263ms
compilation (LCNF base) 3.77ms
compilation (LCNF impure) 1.41ms
compilation (LCNF mono) 4.08ms
congr simp thm 4.75ms
dsimp 41.3ms
elaboration 777ms
fix level params 28.2ms
import 1.82s
initialization 27ms
instantiate metavars 145ms
interpretation 485ms
let-to-have transformation 0.365ms
linting 40.8ms
norm_num 4.96ms
parsing 14.4ms
process pre-definitions 221ms
ring 731ms
share common exprs 795ms
simp 809ms
tactic execution 135ms
type checking 1.09s
typeclass inference 779ms
real 7.08
user 7.43
sys 1.14
LeanPool/DemazureOperatorsLean/DemazureRelations.lean
import took 1.83s
cumulative profiling times:
attribute application 0.07ms
congr simp thm 0.326ms
dsimp 138ms
elaboration 55.1ms
fix level params 0.292ms
import 1.83s
initialization 26.8ms
instantiate metavars 0.638ms
interpretation 299ms
let-to-have transformation 0.203ms
linting 7.24ms
parsing 5.53ms
process pre-definitions 3.63ms
share common exprs 1.78ms
simp 1.66ms
tactic execution 73.4ms
type checking 26.8ms
typeclass inference 275ms
real 3.02
user 2.24
sys 1.12
Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.
🤖 LLM review (
|
| Aspect | Value |
|---|---|
| Fit | ✅ good_fit |
| Level | graduate |
| Branch | algebraic combinatorics |
| Mode | theory_building |
| Obscure problem | no |
| Code quality | 3 / 5 |
The contribution is a formal development of Demazure divided-difference operators and their Coxeter-type relations, with supporting formal Coxeter theory.
Tokens: 37,390 in / 747 out · Tier: standard · Cost: $0.2094
Automated review against .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.
|
/profile |
1 similar comment
|
/profile |
|
Deterministic partial-port audit flags this PR as incomplete against the registered upstream source. Compared with The imported Demazure-operator core is meaningful, but the PR currently drops a large part of the upstream development around symmetric-group words, strong exchange, and Matsumoto. Treating this as request-changes until those files are ported, or the project card/source scope is explicitly narrowed so the PR is reviewed as the smaller core development it actually imports. This is the failure mode automated in #110. |
|
Follow-up on the partial-port audit: I tried vendoring the omitted upstream |
|
/profile |
|
Restored the omitted Coxeter-theory layer in this import. The current head adds |
|
/review |
|
LLM review skipped: Lean Action CI conclusion was |
|
Updated #89 with current Local checks on the merged branch:
This should now be ready for CI and the LLM reviewer on the current head. |
|
Follow-up on the partial-port/CI repair for DemazureOperatorsLean: current head |
|
/review |
|
LLM review skipped: Lean Action CI conclusion was |
|
/review |
|
Addressed the reviewer metadata finding on head |
|
/review |
|
LLM review skipped: Lean Action CI conclusion was |
|
/review |
|
Pushed Local checks passed:
I will rerun |
|
/review |
|
/review |
1 similar comment
|
/review |
|
Follow-up audit for the partial-port flag: this one was already handled in the merged PR history and PR description. The current import includes The remaining upstream files not represented are So I do not see a new porting-agent failure here: the flagged files are either already present ( |
Imported from https://github.com/bolito2/DemazureOperatorsLean.
Slug:
demazureoperatorsleanToolchain target:
leanprover/lean4:v4.30.0-rc2Branch:
import/demazureoperatorsleanImport notes
This branch imports the completed Demazure-operator core plus the repaired Coxeter support layer:
DemazureOperators/Demazure.leanDemazureOperators/DemazureAux.leanDemazureOperators/DemazureRelations.leanDemazureOperators/DemazureAuxRelations.leanDemazureOperators/StrongExchange.leanDemazureOperators/Matsumoto.leanThe remaining upstream files are not imported because they are not Lean-Pool admissible as upstream currently stands:
DemazureOperators/SymmetricGroup.leancontains an unresolvedsorryin the proof that the map from the abstract type-A Coxeter presentation toEquiv.Perm (Fin (n + 1))is injective.DemazureOperators/DemazureWords.leandepends on that concrete symmetric-group Coxeter system and also uses forbiddenset_option quotPrecheck false.The project card therefore treats the Demazure relations and unconditional strong exchange as the headline results. The Matsumoto development is retained as conditional auxiliary Coxeter infrastructure because
CoxeterSystem.matsumoto_reducedassumes the extraMatsumotoConditionhypothesis.Current local checks on head
a38d9f2:lake build LeanPool.DemazureOperatorsLeanlake exe lint-style LeanPool/DemazureOperatorsLean.lean LeanPool/DemazureOperatorsLean/DemazureAux.leanuv run python -m lean_pool.partial_port_audit --repo .. --base-ref origin/main --head-ref HEADuv run python -m lean_pool.quality --repo ..git diff --check