Hacktoberfest 2026：维护者为十月标记出来的 issue，仍然开放、适合新手。 浏览 Hacktoberfest issue

perf: refactor rejectDuplicates in Parser.lean to avoid redundant sort and O(n²) insertion

未关闭
#18 0 条评论 0 个 reaction 已指派 0 人 在 GitHub 查看

还没有人认领这个 Issue。

评估

难度
4/5
预计耗时
3-5 天
新手友好度
45/100
Issue 类型
重构
描述清晰度
基本清楚
活跃度
停滞
领域
compilers, performance

调研方向

先在 Lck/Json/Parser.lean 中阅读 SortedKVs.ofListWithPolicy、hasDuplicateKeysList、ofList 和 ofListLastWins。然后检查 Syntax.lean 中现有的结构以及 Proofs.lean 中相关的证明。当 fromSortedList helper 能够让 rejectDuplicates、firstWins 和 lastWins 共用一次 mergeSort，同时保留相应的证明和 O(n log n) 行为时，即算完成。

由索引模型根据 Issue 内容生成。

描述

Problem

SortedKVs.ofListWithPolicy .rejectDuplicates in Lck/Json/Parser.lean does two passes:

  1. hasDuplicateKeysList: sorts the list (mergeSort, O(n log n)) then scans adjacent pairs
  2. SortedKVs.ofList: builds the sorted structure via repeated insert (O(n) each → O(n²) total)

Total cost is O(n log n) + O(n²) = O(n²) with a hidden constant from sorting twice.

Suggested Fix

Add a SortedKVs.fromSortedList helper that builds the sorted structure from a pre-sorted list in O(n), then combine the duplicate check and structure construction into a single pass over the mergeSort output. This would bring the rejectDuplicates path to O(n log n) overall.

The same refactor would help firstWins and lastWins paths in ofList/ofListLastWins.

Complexity

Moderate: requires a new Syntax.lean helper and corresponding proof in Proofs.lean.

主要语言
Lean
星标
2
派生
1
30 天内没有已合并 PR

贡献指南

这个仓库没有索引到贡献指南

从这里开始

  1. 先读完整个 Issue，再读项目的贡献指南。
  2. 在 Issue 下留言说明你要接手 —— 这能避免两个人做同样的事。
  3. Fork 仓库，在一个分支上完成修改。
  4. 提交 Pull Request，并在描述里引用这个 Issue 编号。

lambdaclass/lambda_compiler_kit 的其他 Issue

查看 lambdaclass/lambda_compiler_kit 的全部 Issue

相似的 Issue

更多 Compilers Issue

把新 issue 发到你的邮箱

精选适合新手参与的 GitHub issue 摘要。