feat(ci): add build timing reporting

[quangvdao]

Summary

• replace the implicit PR CI path with a single explicit workflow that measures clean builds, warm rebuilds, and a repo-local test module
• upload timing artifacts, compare PR runs against a prior successful baseline, and publish the report in both the step summary and a sticky PR comment
• port CompPoly's timing helper and adapt the slow-file path mapping for VCVio, Examples, ToMathlib, LibSodium, VCVioWidgets, and Test

Test plan

• bash -n scripts/build_timing_report.sh
• lake build
• lake env lean Test.lean
• local end-to-end timing run rendering the markdown report

Made with Cursor

[github-actions]

🤖 Gemini PR Summary

Infrastructure & CI

• Consolidates PR CI into a single explicit workflow in .github/workflows/build.yml using lean-action.
• Implements build performance tracking via scripts/build_timing_report.sh to measure clean builds, warm rebuilds, and specific test module durations.
• Automates performance comparisons against a prior successful baseline, publishing results to GitHub step summaries and sticky PR comments.
• Adapts slow-file path mapping for the following directories: VCVio, Examples, ToMathlib, LibSodium, VCVioWidgets, and Test.

Formal Library Refinement

Note: The following changes were identified in the code but are not explicitly detailed in the PR body description.

• Proof Modularity: Modularizes the ElGamal IND-CPA security proof by extracting inductive cases from stepDDH_simulation_deferred into private lemmas.
• Tactic Validation: Refines tactic examples and introduces #guard_msgs to formally verify the output suggestions of the qvcgen_step tactic.

---

Note on Proof Completeness: No new sorry or admit placeholders were introduced; all modified proofs remain complete.

---

Statistics

Metric	Count
📝 Files Changed	5
✅ Lines Added	862
❌ Lines Removed	187

---

Lean Declarations

• No declarations were added, removed, or affected.

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📄 **Per-File Summaries**

• .github/workflows/build.yml: This update introduces a comprehensive build performance tracking and reporting system to the CI pipeline. It measures build durations across various scenarios, compares them against historical baselines, and automatically posts the results as a comment on pull requests. Additionally, the workflow migrates to the lean-action for environment setup and implements more robust caching for Lake build artifacts.
• .github/workflows/ci.yml: This change removes the project's continuous integration (CI) workflow, disabling the automated build and proof verification process previously triggered by pushes and pull requests. Consequently, Lean code changes will no longer be automatically validated using lean-action in this pipeline.
• scripts/build_timing_report.sh: This script introduces a utility to measure and report build performance by capturing timing data for clean builds, warm rebuilds, and specific test paths. It includes functionality to render these metrics into a Markdown report that compares current results against a baseline, identifies incremental rebuild efficiency, and lists the slowest individual source files.
• VCVio/ProgramLogic/Tactics/Examples.lean: This file refines the collection of tactic examples by removing several redundant test cases for the qvcgen_step? and rvcgen_step? tactics. It also adds a #guard_msgs block to formally verify the suggestion output of the qvcgen_step tactic. No new definitions, theorems, or sorry placeholders are introduced.
• Examples/ElGamal.lean: This refactors the proof of stepDDH_simulation_deferred by extracting its inductive cases into several new private lemmas and introducing the StepDDHSimulationEq abbreviation to represent simulation equality. These changes improve the modularity and maintainability of the ElGamal IND-CPA security formalization without introducing any sorry placeholders.

---

Last updated: 2026-03-12 22:31 UTC.

[github-actions]

🤖 Initial AI review without external context

🤖 AI Review

Reviewed Revision

• Commit: 3c67af9c47e01551e8ef3f696d5547499d84342a
• Commit message:

perf: reduce Lean build hotspots

Trim redundant planner example coverage and split ElGamal's deferred DDH simulation into smaller helpers so the default build keeps the same proof surface with much lower elaboration cost.

Made-with: Cursor

Overall Summary:

Pull Request Synthesis Report

TL;DR:
This PR is in excellent shape. The formalizations in both the ElGamal examples and the program logic tactics are clean, mathematically sound, and ready to be merged without any necessary modifications.

Checklist Coverage:
No explicit specification checklist was provided for this PR. However, a thorough review of the newly introduced definitions and proofs confirms they are complete and robust.

Overall Verdict: Approved

(Excellent work! Thank you for the clean and well-structured contributions.)

---

📄 **Review for `Examples/ElGamal.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `VCVio/ProgramLogic/Tactics/Examples.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

[github-actions]

Build Timing Report

• Commit: 3a0b618
• Message: Merge 3c67af9 into c6f78b4
• Ref: quang/add-build-timing-ci
• Comparison baseline: b009941 from the previous successful PR update.
• Measured on ubuntu-latest with /usr/bin/time -p.
• Commands: clean build rm -rf .lake/build && lake build; warm rebuild lake build; test module lake env lean Test.lean.

Measurement	Baseline (s)	Current (s)	Delta (s)	Status
Clean build	299.31	297.24	-2.07	ok
Warm rebuild	1.66	1.48	-0.18	ok
Test module	3.10	2.97	-0.13	ok

Incremental Rebuild Signal

• Warm rebuild saved 295.76s vs clean (200.84x faster).

This compares a clean project build against an incremental rebuild in the same CI job; it is a lightweight variability signal, not a full cross-run benchmark.

Slowest Current Clean-Build Files

Showing 20 slowest current targets, with comparison against the selected baseline when available.

Current (s)	Baseline (s)	Delta (s)	Path
83.00	89.00	-6.00	VCVio/ProgramLogic/Tactics/Examples.lean
31.00	33.00	-2.00	Examples/ElGamal.lean
18.00	18.00	+0.00	ToMathlib/General.lean
14.00	14.00	+0.00	VCVio/OracleComp/QueryTracking/SeededOracle.lean
13.00	13.00	+0.00	VCVio/CryptoFoundations/Fork.lean
12.00	13.00	-1.00	VCVio/EvalDist/Defs/Basic.lean
12.00	12.00	+0.00	VCVio/ProgramLogic/Relational/Quantitative.lean
11.00	9.80	+1.20	VCVio/OracleComp/Coercions/Add.lean
10.00	9.00	+1.00	VCVio/OracleComp/SimSemantics/PreservesInv.lean
9.60	9.60	+0.00	VCVio/ProgramLogic/Relational/Basic.lean
9.40	9.70	-0.30	VCVio/OracleComp/Constructions/GenerateSeed.lean
9.00	8.60	+0.40	VCVio/CryptoFoundations/AsymmEncAlg/IND_CPA.lean
8.80	8.70	+0.10	VCVio/CryptoFoundations/SymmEncAlg.lean
8.80	6.30	+2.50	Examples/Schnorr.lean
8.60	8.30	+0.30	VCVio/OracleComp/QueryTracking/CountingOracle.lean
8.50	8.20	+0.30	VCVio/EvalDist/Monad/Basic.lean
8.40	8.90	-0.50	VCVio/OracleComp/Constructions/SampleableType.lean
8.20	8.10	+0.10	VCVio/CryptoFoundations/SecExp.lean
8.10	8.20	-0.10	ToMathlib/ProbabilityTheory/OptimalCoupling.lean
7.60	7.50	+0.10	VCVio/OracleComp/ProbComp.lean

[quangvdao]

Test comment for disclosure policy.

Posted by Cursor assistant (model: GPT-5.4) on behalf of the user with approval.

This comment intentionally verifies the new rule requiring explicit disclosure and exact model identification for online posts.