Remove obsolete v1 translation artifacts#20
Merged
lihaokun merged 2 commits intoMay 19, 2026
Conversation
lihaokun
added a commit
that referenced
this pull request
May 18, 2026
) PR #20 删 cpp2lean/ v1 时会带走 survey_ast.py（生成 v2 测试用的 _ast_cache）。 本 commit 先发，迁移到 cpp2lean_v2/scripts/ 让 PR #20 可平滑 merge。 改动： 1. **proof/cpp2lean_v2/scripts/survey_ast.py**（new） - 复制自 cpp2lean/scripts/survey_ast.py（556 行 → 556 行 +/- 路径常量） - 路径常量同步 PR #20 layout: * AST_CACHE_DIR: cpp2lean/_ast_cache → cpp2lean_v2/tests/ast_cache * INSTANTIATE_CC: cpp2lean/instantiate.cc → cpp2lean_v2/tests/fixtures/instantiate.cc * cwd: HERE → V2_ROOT - 本地实测：dump 66/66 函数成功，cache 22M， diff vs v1 cache：仅 'id' 字段（runtime mem addrs）差异，语义等价 2. **proof/cpp2lean_v2/tests/fixtures/instantiate.cc**（new） - 复制自 cpp2lean/instantiate.cc（与 PR #20 的 rename 目标重叠 → 合并时 git 应识别为相同内容，无冲突） 3. **proof/cpp2lean_v2/.gitignore**（new） - 排除 tests/ast_cache/（22M 数据，CI 重生）+ pycache + pytest_cache 4. **.github/workflows/cpp2lean-v2.yml**（new） - clang + libgmp + boost 安装 - make CLPoly（头文件解析依赖） - survey_ast.py 生成 cache（~5-10 min） - 跑 Pass 1-7 单元 + smoke（66 functions × 7 passes） - Pass 4 单元已知 4 处 pre-existing failure（filter recognition），暂跑 smoke only - 触发：push/PR to master 或 feature/formal-proofs 5. **.github/workflows/lean-proofs.yml**（new） - elan + Lean toolchain（从 lean-toolchain 文件读） - Mathlib cache（actions/cache）+ lake exe cache get - lake build 全量（含 Phase 2A.4c+d 的 1021 行） - lake build B2B targets - sorry 检查（Experiment/ 外不允许） - 触发：proof/lean/** 改动时 本地验证： - v2 survey_ast.py: 66/66 functions OK - v2 smoke Pass 1-7: all green（68 OK / 0 FAIL per pass） - Lake build (Lean 4.29.0): 3304 jobs 全过 0 sorry Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
lihaokun
added a commit
that referenced
this pull request
May 18, 2026
PR #20 修这 18 个文件，但未合并。我们这里先做（PR 20 合时会无冲突， git 识别相同内容更改）。 改动： - V2_ROOT.parent / "cpp2lean" / "_ast_cache" → V2_ROOT / "tests" / "ast_cache" - V2_ROOT.parent / "cpp2lean" / "instantiate.cc" → V2_ROOT / "tests" / "fixtures" / "instantiate.cc" - comments 中的 proof/cpp2lean/_ast_cache/ → proof/cpp2lean_v2/tests/ast_cache/ 18 文件批量 sed 替换。 Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…tantiate.cc（CI 验证过的修复版） # Conflicts: # proof/cpp2lean_v2/tests/fixtures/instantiate.cc
lihaokun
merged commit 334acca
into
lihaokun:feature/formal-proofs
2 of 3 checks passed
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
2 participants
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
This PR removes the obsolete v1 C++→Lean translation artifacts and the unused hand-written L1 Lean prototypes.
The current translation path is
proof/cpp2lean_v2/, with generated Lean code targetingCLPoly.Model. The oldproof/cpp2lean/implementation and unused L1 prototype files were no longer part of the active build or B2B path.Changes
proof/cpp2lean/translator implementation.instantiate.ccinto the v2 test fixtures:proof/cpp2lean_v2/tests/fixtures/instantiate.ccproof/cpp2lean_v2/tests/ast_cacheinstantiate.ccCLPoly/Impl/Types.leanCLPoly/Impl/SquarefreeZp.leanCLPoly/Experiment/L1Barrett.leanCLPoly/Generated/MakeZp.leanValidation
cd proof/lean && lake buildcd proof/lean && lake build b2b_test_typespython3 -m compileall -q proof/cpp2lean_v2