Preserve native proof budgets and repair stale capture dependencies

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

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

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"

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; });

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; });

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; });