Description
On a minimal Lake package pinned to leanprover/lean4:v4.28.0, leanprover/lean-action@v1.5.0 reaches nanoda successfully but nanoda rejects the generated export stream with:
Detected module name: LogicZigOracle
Exporting LogicZigOracle...
Running nanoda type checker...
Error: invalid digit found in string
The same package builds successfully and passes the bundled leanchecker. It contains no sorry, admit, custom axioms, or unsafe declarations.
Reproduction
- uses: leanprover/lean-action@v1.5.0
with:
lake-package-directory: lean
build: true
test: false
nanoda: true
nanoda-allow-sorry: falsewith lean/lean-toolchain:
Notes
The current nanoda_lib debug branch head predates Lean 4.28. The exporter builds against 4.28 and emits the file, so this appears to be an export-format/parser compatibility problem rather than module discovery or a Lean elaboration failure.
A useful short-term outcome would be either a supported-version guard with a clear diagnostic or a compatible nanoda/exporter pin. The current generic parse error makes the gate difficult to diagnose.
Description
On a minimal Lake package pinned to
leanprover/lean4:v4.28.0,leanprover/lean-action@v1.5.0reaches nanoda successfully but nanoda rejects the generated export stream with:The same package builds successfully and passes the bundled
leanchecker. It contains nosorry,admit, custom axioms, or unsafe declarations.Reproduction
with
lean/lean-toolchain:Notes
The current
nanoda_libdebug branch head predates Lean 4.28. The exporter builds against 4.28 and emits the file, so this appears to be an export-format/parser compatibility problem rather than module discovery or a Lean elaboration failure.A useful short-term outcome would be either a supported-version guard with a clear diagnostic or a compatible nanoda/exporter pin. The current generic parse error makes the gate difficult to diagnose.