Import crdt-lean#231
Open
Vilin97 wants to merge 1 commit into
Open
Conversation
Contributor
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: 1,206 maxHeartbeats units across 7 files (764 added LOC). Sum of Count-heartbeats wall-clock total: 11.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.CrdtLean.Crdt.Defs |
2.30 s |
LeanPool.CrdtLean.Crdt.Sequence |
1.90 s |
LeanPool.CrdtLean.Crdt.Instances |
1.80 s |
LeanPool.CrdtLean.Crdt.ORSet |
1.80 s |
LeanPool.CrdtLean.Crdt.Convergence |
1.10 s |
LeanPool.CrdtLean.Crdt.Liveness |
1.10 s |
LeanPool.CrdtLean |
1.00 s |
Per-file `lean --profile` output
LeanPool/CrdtLean.lean
import took 830ms
cumulative profiling times:
elaboration 0.198ms
import 830ms
initialization 41.6ms
interpretation 114ms
linting 0.368ms
module linting 0.00117ms
overlappingInstancesLinter 0.498ms
parsing 0.0555ms
tacticAnalysis 1.25ms
real 1.62
user 0.92
sys 0.68
LeanPool/CrdtLean/Crdt/Convergence.lean
import took 795ms
cumulative profiling times:
attribute application 0.0864ms
congr simp thm 0.496ms
elaboration 24.7ms
fix level params 0.302ms
import 795ms
initialization 29.4ms
instantiate metavars 0.152ms
interpretation 141ms
let-to-have transformation 0.121ms
linting 4.78ms
module linting 0.00129ms
overlappingInstancesLinter 3.93ms
parsing 4.24ms
process pre-definitions 1.28ms
share common exprs 0.658ms
simp 2.97ms
tactic execution 9.29ms
tacticAnalysis 10.7ms
type checking 3.88ms
typeclass inference 55.1ms
real 1.58
user 1.02
sys 0.66
LeanPool/CrdtLean/Crdt/Defs.lean
import took 807ms
cumulative profiling times:
attribute application 1.01ms
compilation (IR) 0.115ms
compilation (LCNF base) 0.95ms
compilation (LCNF impure) 0.501ms
compilation (LCNF mono) 0.87ms
congr simp thm 0.989ms
elaboration 20.6ms
fix level params 0.196ms
import 807ms
initialization 30ms
instantiate metavars 0.0855ms
interpretation 158ms
let-to-have transformation 0.128ms
linting 4.26ms
module linting 0.00136ms
overlappingInstancesLinter 8.74ms
parsing 4ms
process pre-definitions 1.52ms
share common exprs 0.363ms
simp 28.1ms
tactic execution 2.34ms
tacticAnalysis 11.3ms
type checking 2.6ms
typeclass inference 40.3ms
real 1.61
user 1.04
sys 0.68
LeanPool/CrdtLean/Crdt/Instances.lean
import took 841ms
cumulative profiling times:
attribute application 0.3ms
compilation (IR) 0.612ms
compilation (LCNF base) 5.22ms
compilation (LCNF impure) 3.04ms
compilation (LCNF mono) 5.24ms
elaboration 58ms
fix level params 0.577ms
import 841ms
initialization 29.5ms
instantiate metavars 0.3ms
interpretation 215ms
let-to-have transformation 0.653ms
linting 10.1ms
module linting 0.00123ms
overlappingInstancesLinter 10.5ms
parsing 9.75ms
process pre-definitions 3.59ms
share common exprs 1.18ms
tactic execution 9.43ms
tacticAnalysis 24.3ms
type checking 9.97ms
typeclass inference 109ms
real 1.69
user 1.23
sys 0.71
LeanPool/CrdtLean/Crdt/Liveness.lean
import took 798ms
cumulative profiling times:
attribute application 0.0639ms
blocked (unaccounted) 1.16ms
compilation (IR) 0.0806ms
compilation (LCNF base) 0.387ms
compilation (LCNF impure) 0.305ms
compilation (LCNF mono) 0.71ms
congr simp thm 3.05ms
elaboration 36.8ms
fix level params 0.313ms
import 798ms
initialization 29.7ms
instantiate metavars 0.4ms
interpretation 162ms
let-to-have transformation 0.0687ms
linting 5.4ms
module linting 0.00139ms
overlappingInstancesLinter 4.66ms
parsing 5.29ms
process pre-definitions 1.72ms
share common exprs 0.716ms
simp 1.56ms
tactic execution 28.7ms
tacticAnalysis 13.6ms
type checking 14.8ms
typeclass inference 40.8ms
real 1.61
user 1.09
sys 0.66
LeanPool/CrdtLean/Crdt/ORSet.lean
import took 798ms
cumulative profiling times:
attribute application 0.206ms
blocked (unaccounted) 0.477ms
compilation (IR) 0.531ms
compilation (LCNF base) 3.92ms
compilation (LCNF impure) 2.45ms
compilation (LCNF mono) 5.13ms
congr simp thm 2.57ms
elaboration 54.6ms
fix level params 1.09ms
import 798ms
initialization 29.6ms
instantiate metavars 0.678ms
interpretation 195ms
let-to-have transformation 0.409ms
linting 11.7ms
module linting 0.0013ms
overlappingInstancesLinter 7.71ms
parsing 7.89ms
process pre-definitions 4.65ms
share common exprs 2.05ms
simp 16.7ms
tactic execution 52.7ms
tacticAnalysis 21ms
type checking 17.3ms
typeclass inference 118ms
real 1.65
user 1.27
sys 0.68
LeanPool/CrdtLean/Crdt/Sequence.lean
import took 811ms
cumulative profiling times:
attribute application 0.229ms
compilation (IR) 0.562ms
compilation (LCNF base) 4.99ms
compilation (LCNF impure) 3.04ms
compilation (LCNF mono) 9.01ms
congr simp thm 0.927ms
elaboration 58.6ms
fix level params 1.16ms
import 811ms
initialization 29.5ms
instantiate metavars 0.621ms
interpretation 197ms
let-to-have transformation 0.387ms
linting 10.4ms
module linting 0.00138ms
overlappingInstancesLinter 8.34ms
parsing 8.62ms
process pre-definitions 5.69ms
share common exprs 2.4ms
simp 8.16ms
tactic execution 47.7ms
tacticAnalysis 24ms
type checking 16ms
typeclass inference 144ms
real 1.68
user 1.31
sys 0.68
Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.
Owner
Author
Project metadata advisoryThis advisory summarizes source-project metadata for project entries added or changed by this PR.
License is read from GitHub SPDX metadata when available, and the last commit and Lean version are read from the source repository's default branch. |
Contributor
🤖 LLM review (
|
| Aspect | Value |
|---|---|
| Fit | 🟡 borderline |
| Level | graduate |
| Branch | theoretical computer science |
| Mode | theory_building |
| Obscure problem | no |
| Code quality | 3 / 5 |
The contribution is a lightweight Lean formalization of state-based CRDT strong eventual consistency, but the headline theorem is close to an immediate semilattice-fold fact and the PR does not yet anchor the development to a published CRDT source.
Findings (2)
- source-anchor —
LeanPool/CrdtLean.lean:15
The project card cites only the upstream GitHub repository as source; for Lean Pool this should point to a paper, textbook, or named published CRDT reference, e.g. the Shapiro–Preguiça–Baquero–Zawirski state-based CRDT paper/specification that these conditions and SEC theorem come from. - statement-mismatch —
LeanPool/CrdtLean/Crdt/Sequence.lean:40
The file presents this as an RGA/Logoot/Treedoc-family sequence CRDT, but the formal model only sorts live position identifiers and abstracts away allocation, causality, parent links, and element lookup in the read value. Either narrow the claimed result to convergence of a sorted live-position read, or add the missing model assumptions/results needed for the RGA-style claim.
Tokens: 13,847 in / 986 out · Tier: flex · Cost: $0.0494
Automated review against .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Verification
Notes