Description
In ProbeLean/Loader.lean, loadFilteredAtoms has a hardcoded filter:
atom.codePath.endsWith "Funs.lean"
This is specific to Aeneas-transpiled projects where functions live in *Funs.lean files. For any non-Aeneas Lean project, the stubify command will produce zero stubs because no atoms match.
Suggested Fix
Either:
- Make the filter conditional on whether the project is an Aeneas project (e.g., check for presence of Aeneas config or rust-source fields)
- Remove the filter and let stubify work on all relevant atoms
- Document stubify as an Aeneas-only feature
Description
In
ProbeLean/Loader.lean,loadFilteredAtomshas a hardcoded filter:atom.codePath.endsWith "Funs.lean"This is specific to Aeneas-transpiled projects where functions live in
*Funs.leanfiles. For any non-Aeneas Lean project, the stubify command will produce zero stubs because no atoms match.Suggested Fix
Either: