Bug: multi-library projects get 0 declarations when Aeneas code is not in defaultTargets

[astefano]

Summary

probe-lean fails to extract declarations from Lean projects that define multiple libraries in lakefile.toml when the Aeneas-generated code lives in a library that is not the default build target.

Discovered when running probe-aeneas extract on SparsePostQuantumRatchet with its Aeneas translation project spqr_aeneas.

Root cause

Two compounding problems:

1. lake build only builds defaultTargets

In ProbeLean/Extract.lean (line 72), probe-lean runs:

let (buildStdout, buildStderr, buildExit) ← runCmd "lake" #["build"] (some config.projectPath)

With no library argument, lake build builds only defaultTargets. For spqr_aeneas, the lakefile is:

name = "Spqr"
defaultTargets = ["Spqr"]

[[lean_lib]]
name = "Extraction"

[[lean_lib]]
name = "Spqr"

So only the Spqr module gets built. The Extraction library (where all the Aeneas-generated code lives) is never compiled.

2. Module discovery depends on .olean files

In ProbeLean/Environment.lean (lines 101-130), getProjectModules scans .lake/build/lib/lean/ for .olean files. Since Extraction was never built, no Extraction.*.olean files exist. The resulting module list contains only Spqr, so zero Extraction declarations are found.

Reproducer

Given a project spqr_aeneas with:

• lakefile.toml as shown above
• Spqr.lean is empty (does not import Extraction)
• Extraction/Funs.lean, Extraction/Types.lean, etc. contain Aeneas-generated Lean code

Running probe-lean produces:

Building project at /path/to/spqr_aeneas...
Extracting declarations...
Found 0 declarations
Found 0 atoms

Why curve25519-dalek works

For comparison, curve25519-dalek-lean-verify works because it uses a single library where the package name, library name, and directory all match (Curve25519Dalek). There is no multi-library split, so lake build builds everything.

Suggested fixes

• Option A: Build all libraries. Parse lakefile.toml to discover all [[lean_lib]] entries and pass them to lake build (e.g. lake build Extraction Spqr).
• Option B: Source-file fallback. If getProjectModules returns an empty or minimal list, fall back to scanning .lean source files on disk to infer module names.
• Option C: --library CLI flag. Accept a --library flag so users can specify which library to build and extract from.

Options A and C are probably the most robust. Option A makes multi-library projects work out of the box; Option C gives users explicit control.