From 657bfe990eaa82866f871a71f82c4d43031a61f7 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Thu, 15 Oct 2026 22:24:41 -0700 Subject: [PATCH] Preserve compact proof budgets and validate import builds with Lake --- lean/README.md | 4 +++ lean/SourceProfiler.lean | 13 ++++++-- package.json | 2 +- scripts/capture-whole-pool.cjs | 12 ++------ test/build-recovery.integration.cjs | 30 +++++++++++++++++++ test/heartbeat.integration.cjs | 46 +++++++++++++++++++++++++++++ 6 files changed, 95 insertions(+), 12 deletions(-) create mode 100644 test/build-recovery.integration.cjs create mode 100644 test/heartbeat.integration.cjs diff --git a/lean/README.md b/lean/README.md index 5e3cb5c66..5b37366d1 100644 --- a/lean/README.md +++ b/lean/README.md @@ -86,6 +86,10 @@ duration must not be presented as the exclusive cost of unfolding that declarati native CPU stacks, heap allocations, or peak RSS. - Trace collection adds overhead. Use uninstrumented compiler wall time for final benchmark numbers, and compare recordings captured with the same settings. +- Compact source scopes remove internal `trace.*` options while running the elaborator. + Merely setting profiling to false still activates Lean's internal trace checks and can + spend a typeclass search's heartbeat budget on instrumentation. Source timers and outer + command/async scopes are retained; proof limits and all other native options are preserved. - Formatting happens after the timed frontend interval. Large traces can take substantially longer to format/export than the proof took to elaborate. - Pretty printing is bounded to 500 steps/depth 12, details to 4,096 characters, and ordinary diff --git a/lean/SourceProfiler.lean b/lean/SourceProfiler.lean index 98f591dc4..23f40eff0 100644 --- a/lean/SourceProfiler.lean +++ b/lean/SourceProfiler.lean @@ -40,6 +40,16 @@ def ClockMapping.at (clock : ClockMapping) (time : Float) : Float := initialize registerTraceClass `Source.tactic initialize registerTraceClass `Source.term +/-- Source timers collect their own traces. Leaving disabled `trace.*` options in scope +still activates Lean's per-call tracing checks, charging proof heartbeat budgets for +instrumentation inside typeclass search. Retain every non-trace proof option. -/ +def sourceOptions (opts : Options) : Options := Id.run do + let mut result := Options.empty + for (name, value) in opts do + unless (`trace).isPrefixOf name do + result := result.insert name value + return result + /-- Source timers avoid constructing diagnostic contexts and timing every internal Meta call. The exception instance matches Lean's trace builder, so failed elaborator alternatives restore their parent trace state before rethrowing. -/ @@ -51,8 +61,7 @@ def withSourceTrace {m : Type → Type} {α : Type} [Monad m] [MonadTrace m] let _ := always.except if trace.profiler.useHeartbeats.get opts then throw <| Exception.error stx "Source profiler requires wall-clock traces." - let action := if trace.profiler.get opts then - withOptions (·.setBool `trace.profiler false) action else action + let action := withOptions sourceOptions action -- Generated, unlocated syntax is covered by its enclosing source timer. if stx.getRange? (canonicalOnly := true) |>.isNone then return ← action let oldTraces ← getTraces diff --git a/package.json b/package.json index a810f1124..43370bc05 100644 --- a/package.json +++ b/package.json @@ -209,7 +209,7 @@ "test": "npm run build && node --test test/*.test.cjs", "test:extension": "node test/run-extension.cjs", "test:accuracy": "npm run build && node test/capture.integration.cjs", - "test:source-focused": "npm run build && node test/compact.integration.cjs && node test/setup.integration.cjs && node test/raw-clock.integration.cjs", + "test:source-focused": "npm run build && node test/compact.integration.cjs && node test/setup.integration.cjs && node test/heartbeat.integration.cjs && node test/build-recovery.integration.cjs && node test/raw-clock.integration.cjs", "package": "node scripts/package-release.mjs --vsix-only", "vscode:prepublish": "npm run build", "release": "node scripts/package-release.mjs" diff --git a/scripts/capture-whole-pool.cjs b/scripts/capture-whole-pool.cjs index a11c96b48..069a89742 100644 --- a/scripts/capture-whole-pool.cjs +++ b/scripts/capture-whole-pool.cjs @@ -78,14 +78,8 @@ async function initialize(repository, output, signal) { async function buildProject(repository, output, project, lake, signal) { const marker = path.join(output, 'builds', project.name + '.json'); - try { - const built = await readJson(marker); - for (const entry of project.files) { - await fs.access(path.join(repository, '.lake/build/lib/lean', entry.path.replace(/\.lean$/, '.olean'))); - if (built[entry.path] !== await fileDigest(setupPath(repository, entry))) throw new Error('Native module setup changed.'); - } - return; - } catch (error) { if (signal.aborted) throw error; } + // Only Lake can validate the transitive artifact graph. A saved source setup and + // root olean can remain unchanged after an imported artifact has disappeared. for (let index = 0; index < project.files.length; index += 128) { const targets = project.files.slice(index, index + 128).map(entry => '+' + entry.path.replace(/\.lean$/, '').replaceAll('/', '.') + ':olean'); await run(lake, ['build', ...targets], repository, signal); @@ -191,5 +185,5 @@ async function main() { await capturePool(path.resolve(args[0]), path.resolve(args[1]), process.env.LAKE || 'lake', controller.signal); } -module.exports = { inventory, capturePool, audit, completed }; +module.exports = { inventory, capturePool, audit, completed, buildProject }; if (require.main === module) main().catch(error => { console.error(error.message); process.exitCode ||= 1; }); diff --git a/test/build-recovery.integration.cjs b/test/build-recovery.integration.cjs new file mode 100644 index 000000000..b7b192865 --- /dev/null +++ b/test/build-recovery.integration.cjs @@ -0,0 +1,30 @@ +#!/usr/bin/env node +// A warm profiler checkpoint must not conceal a deleted transitive dependency. +const assert = require('node:assert/strict'); +const fs = require('node:fs/promises'); +const os = require('node:os'); +const path = require('node:path'); +const { buildProject } = require('../scripts/capture-whole-pool.cjs'); +(async () => { + const repository = await fs.mkdtemp(path.join(os.tmpdir(), 'lean-build-recovery-')); + try { + await fs.writeFile(path.join(repository, 'lean-toolchain'), 'leanprover/lean4:v4.34.0-rc2\n'); + await fs.writeFile(path.join(repository, 'lakefile.toml'), + 'name = "build-recovery-fixture"\n[[lean_lib]]\nname = "LeanPool"\n'); + await fs.mkdir(path.join(repository, 'LeanPool')); + await fs.writeFile(path.join(repository, 'LeanPool/Dependency.lean'), 'def dependencyValue : Nat := 7\n'); + await fs.writeFile(path.join(repository, 'LeanPool/Example.lean'), + 'import LeanPool.Dependency\nexample : dependencyValue = 7 := rfl\n'); + const project = { name: 'Example', files: [{ path: 'LeanPool/Example.lean' }] }; + const output = path.join(repository, 'recording'); + const dependency = path.join(repository, '.lake/build/lib/lean/LeanPool/Dependency.olean'); + const root = path.join(repository, '.lake/build/lib/lean/LeanPool/Example.olean'); + await buildProject(repository, output, project, 'lake'); + const rootBytes = await fs.readFile(root); + await fs.unlink(dependency); + await buildProject(repository, output, project, 'lake'); + assert((await fs.stat(dependency)).isFile(), 'Lake repairs imports behind a warm profiler checkpoint'); + assert.deepEqual(await fs.readFile(root), rootBytes, 'the source module remains unchanged'); + console.log('PASS build recovery: a retained root artifact and setup cannot hide a missing dependency.'); + } finally { await fs.rm(repository, { recursive: true, force: true }); } +})().catch(error => { console.error(error); process.exitCode = 1; }); diff --git a/test/heartbeat.integration.cjs b/test/heartbeat.integration.cjs new file mode 100644 index 000000000..c97aa6d87 --- /dev/null +++ b/test/heartbeat.integration.cjs @@ -0,0 +1,46 @@ +#!/usr/bin/env node +// Compact source timers must leave Lean's internal tracing fast path and proof budgets intact. +const assert = require('node:assert/strict'); +const fs = require('node:fs/promises'); +const os = require('node:os'); +const path = require('node:path'); +const { capture, prepareBackend, runProcess } = require('../out/capture.js'); +const extensionRoot = path.resolve(__dirname, '..'); +(async () => { + const project = await fs.mkdtemp(path.join(os.tmpdir(), 'lean-heartbeat-contract-')); + try { + await fs.writeFile(path.join(project, 'lean-toolchain'), 'leanprover/lean4:v4.34.0-rc2\n'); + await fs.writeFile(path.join(project, 'lakefile.toml'), 'name = "heartbeat-fixture"\n'); + const file = path.join(project, 'Heartbeat.lean'), output = path.join(project, 'capture.json'); + const source = `import Lean +open Lean Elab Tactic +class Chain (n : Nat) : Prop where + holds : True +instance : Chain 0 := ⟨trivial⟩ +instance [Chain n] : Chain (n + 1) := ⟨trivial⟩ +elab "check_native_budget" : tactic => do + let opts ← getOptions + if opts.hasTrace then throwError "Internal tracing would charge the proof budget." + unless opts.get "synthInstance.maxHeartbeats".toName (0 : Nat) == 100 do + throwError "The native typeclass budget changed." +set_option synthInstance.maxHeartbeats 100 +example : Chain 80 := by + check_native_budget + infer_instance +`; + await fs.writeFile(file, source); + const backend = await prepareBackend(project, 'lake', extensionRoot); + const native = () => runProcess(backend.leanExecutable, [file], project, + undefined, undefined, backend.env); + await native(); + const profile = await capture({ file, extensionRoot, output }); + assert(profile.nodes.some(n => n.category === 'Source.tactic'), 'source timers remain active'); + const previous = await fs.readFile(output); + await fs.writeFile(file, source.replace('maxHeartbeats 100', 'maxHeartbeats 1') + .replace(' check_native_budget\n', '')); + await assert.rejects(native(), /maximum number of heartbeats/); + await assert.rejects(capture({ file, extensionRoot, output }), /maximum number of heartbeats/); + assert.deepEqual(await fs.readFile(output), previous, 'failed capture cannot replace a valid one'); + console.log('PASS heartbeat: compact source timers preserve native internal-tracing fast path and typeclass limits.'); + } finally { await fs.rm(project, { recursive: true, force: true }); } +})().catch(error => { console.error(error); process.exitCode = 1; });