nit: several low-priority polish items in JSON parser (decimal rendering, ordering invariant, docstrings)

未关闭

#23 创建于 2026年2月26日 0 条评论 0 个 reaction 已指派 0 人在 GitHub 查看

还没有人认领这个 Issue。

评估

难度: 5/5
预计耗时: 一周以上
新手友好度: 25/100

Issue 类型: 重构
描述清晰度: 基本清楚
活跃度: 停滞
领域: compilers

调研方向

先阅读列出的三个区域：cli/LckJsonFmt.lean:30、Lck/Json/Syntax.lean:444-450 和 Lck/Json/Parser.lean。在决定范围之前，先将精度、顺序不变性和文档方面的提案分开；要完成这项工作，需要为列出的每一项达成一致的解决方案，包括 convOfPolicy 的 API 可见性问题。

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

描述

Items

These are low-priority nits flagged by AI code review on PR #8. Grouping them into a single issue to keep the tracker clean.

1. Decimal rendering precision (`cli/LckJsonFmt.lean:30`)

The renderNumber function may truncate fractional digits beyond 20 decimal places, losing round-trip fidelity for numbers with high precision.

2. Dependent types for ordering invariant (`Lck/Json/Syntax.lean:444-450`)

SortedKVs currently enforces its key-sorted ordering invariant by convention. Using dependent types (a sigma type or a subtype with a Sorted proof) would make the invariant enforcement compile-time rather than runtime.

3. Missing docstrings (`Lck/Json/Parser.lean`)

convOfPolicy: no docstring explaining what it does or why it exists
SortedKVs.ofList: no documentation of the byte-lexicographic key ordering behavior
Consider making convOfPolicy private to reduce public API surface

References

Flagged by AI code review on PR #8

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

贡献指南

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

从这里开始

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

lambdaclass/lambda_compiler_kit 的其他 Issue

refactor: remove unnecessary import of Parser.lean from Semantics.lean 未关闭

难度 1/5 1 小时以内新手友好度 72/100

lambdaclass/lambda_compiler_kit#31 · 2026年2月26日创建
nit: fix misleading traversal-order comments in Syntax.lean and Parser.lean 未关闭

难度 1/5 1 小时以内新手友好度 68/100

lambdaclass/lambda_compiler_kit#26 · 2026年2月26日创建
bug: CLI readAll stops reading at first empty line instead of reading to EOF 未关闭

难度 2/5 1-3 小时新手友好度 68/100

lambdaclass/lambda_compiler_kit#22 · 2026年2月26日创建
Enable --wfail axiom-guard gate once warnings are clean 未关闭

enhancement

难度 4/5 3-5 天新手友好度 48/100

lambdaclass/lambda_compiler_kit#38 · 2026年6月9日创建
feat: add --version flag to lck-grep CLI 未关闭

难度 2/5 1-3 小时新手友好度 50/100

lambdaclass/lambda_compiler_kit#36 · 2026年2月26日创建

查看 lambdaclass/lambda_compiler_kit 的全部 Issue

相似的 Issue

self-host checker: `write` with the wrong argument count is not E004 未关闭

难度 2/5 1-3 小时新手友好度 75/100

JakeChampion/lang#10213 · 2026年9月24日创建
Add fixed-width integer peeks for byte readers 未关闭

enhancement good first issue needs testing

难度 2/5 1-3 小时新手友好度 75/100

wavefnd/Wave#717 · 2026年9月24日创建
Dotfiles such as ._main.plum are compiled as source, with no file or position in the error 未关闭

bug

难度 2/5 1-3 小时新手友好度 75/100

bradcypert/plum#58 · 2026年9月24日创建
[flang][cuda] CUFPredefinedVarToGPU crashes on a fir.copy whose destination is the predefined-variable declare 未关闭

flang:fir-hlfir

难度 2/5 1-3 小时新手友好度 70/100

llvm/llvm-project#225935 · 2026年9月23日创建
Hand Tail: Brass Herald 未关闭

area:cards hand-tail ready-for-agent

难度 2/5 1-3 小时新手友好度 65/100

fil-donadoni/tolaria#4446 · 2026年9月23日创建

更多 Compilers Issue