From efc6ce96d5072539e64334a94b49c08f527089c5 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 23 Sep 2026 12:46:00 +1000 Subject: [PATCH 1/3] feat: use the bundled nanoda, and deprecate the `nanoda` input `nanoda: true` currently installs a Rust toolchain, clones and builds `lean4export`, then clones and builds `nanoda_lib` from a branch rather than a release, on every run. Recent release toolchains ship `leanexport` and `nanoda_bin` already, matched to each other and to the compiler that produced the oleans, so prefer those when they are present. Older toolchains keep the source-build path unchanged. The axioms permitted are the same either way, so this changes what the step costs and not what it accepts. Also deprecates `nanoda` and `nanoda-allow-sorry` in favour of `lake-check: paranoid`, which runs nanoda alongside every other bundled checker. The warning and the documentation are explicit that one case has no migration: `lake check` permits only the standard axioms and cannot be told to tolerate `sorryAx`, so a project that relies on `nanoda-allow-sorry: true` should stay on this input for now. The functional test asserts both that the check still passes on a toolchain that bundles the binaries and that no source build happened, since the saving is the point of the change. --- .../nanoda_bundled/action.yml | 54 +++++++++++++ .github/workflows/functional_tests.yml | 11 +++ CHANGELOG.md | 8 ++ README.md | 5 +- action.yml | 8 +- scripts/run_nanoda.sh | 77 ++++++++++++------- 6 files changed, 133 insertions(+), 30 deletions(-) create mode 100644 .github/functional_tests/nanoda_bundled/action.yml diff --git a/.github/functional_tests/nanoda_bundled/action.yml b/.github/functional_tests/nanoda_bundled/action.yml new file mode 100644 index 0000000..a94df23 --- /dev/null +++ b/.github/functional_tests/nanoda_bundled/action.yml @@ -0,0 +1,54 @@ +name: 'nanoda bundled binaries test' +description: 'Verify `nanoda: true` succeeds using the leanexport and nanoda_bin bundled with a recent toolchain, without building either from source.' +inputs: + toolchain: + description: 'Toolchain to use for the test. Must bundle `leanexport` and `nanoda_bin`.' + required: true +runs: + using: 'composite' + steps: + # TODO: once `lean-action` supports just setup, use it here + - name: install elan + run: | + set -o pipefail + curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain ${{ inputs.toolchain }} + echo "$HOME/.elan/bin" >> "$GITHUB_PATH" + shell: bash + + - name: confirm the toolchain really does bundle both binaries + run: | + elan which leanexport + elan which nanoda_bin + shell: bash + + - name: create a clean lake library + run: | + lake init foo lib + lake update + shell: bash + + - name: "run `lean-action` with `nanoda: true`" + id: lean-action-nanoda + uses: ./ + with: + use-github-cache: false + nanoda: true + + - name: verify nanoda accepted the clean package + env: + OUTPUT_NAME: "nanoda-status" + EXPECTED_VALUE: "SUCCESS" + ACTUAL_VALUE: ${{ steps.lean-action-nanoda.outputs.nanoda-status }} + run: .github/functional_tests/test_helpers/verify_action_output.sh + shell: bash + + # The point of the change is that no Rust toolchain and no source builds are needed when the + # toolchain ships the binaries, so assert the source-build path did not run. + - name: verify nothing was built from source + run: | + if [ -d _lean4export ] || [ -d _nanoda_lib ]; then + echo "::error::the source-build fallback ran even though the toolchain bundles leanexport and nanoda_bin" + exit 1 + fi + echo "no source builds, as expected" + shell: bash diff --git a/.github/workflows/functional_tests.yml b/.github/workflows/functional_tests.yml index 30c937b..3cf98a2 100644 --- a/.github/workflows/functional_tests.yml +++ b/.github/workflows/functional_tests.yml @@ -28,6 +28,9 @@ env: # Toolchain without the bundled `leanchecker` binary, # used to cover the external `lean4checker` fallback path legacy_toolchain: leanprover/lean4:v4.26.0 + # Bundles `leanexport` and `nanoda_bin`, which the `nanoda` step now prefers over building + # lean4export and nanoda_lib from source. + bundled_nanoda_toolchain: leanprover/lean4:v4.35.0-rc2 jobs: # The default toolchain is pinned in `.github/functional_test_toolchain` @@ -243,6 +246,14 @@ jobs: # axiom-audit builds with the project's toolchain, so use a recent one. toolchain: ${{ needs.resolve-toolchain.outputs.toolchain }} + nanoda-bundled: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v7 + - uses: ./.github/functional_tests/nanoda_bundled + with: + toolchain: ${{ env.bundled_nanoda_toolchain }} + macos-runner: needs: resolve-toolchain runs-on: macos-latest diff --git a/CHANGELOG.md b/CHANGELOG.md index 28e88ee..9b69afe 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,6 +7,14 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ## Unreleased +### Changed + +- `nanoda` now uses the `leanexport` and `nanoda_bin` bundled with the toolchain when it ships them, instead of installing a Rust toolchain and building lean4export and nanoda_lib from source on every run. Older toolchains keep the source-build path, and the axioms permitted are unchanged either way + +### Deprecated + +- `nanoda` and `nanoda-allow-sorry`, in favour of `lake-check: paranoid`. Note that `lake check` permits only the standard axioms, so there is no equivalent of `nanoda-allow-sorry: true`; projects carrying a `sorry` should stay on `nanoda` for now + ## v1.6.0 - 2026-08-22 ### Added diff --git a/README.md b/README.md index 9f6004f..a045851 100644 --- a/README.md +++ b/README.md @@ -226,9 +226,12 @@ To be certain `lean-action` runs a step, specify the desire feature with a featu # Deprecated alias for `leanchecker`. lean4checker: "" + # Deprecated: use `lake-check: paranoid`, except when `nanoda-allow-sorry: true` is + # needed; `lake check` permits only the standard axioms and cannot tolerate a `sorry`. # Check environment with nanoda external type checker. # nanoda is an independent Lean 4 type checker written in Rust. - # Requires Rust toolchain (will be installed automatically if not present). + # Uses the `leanexport` and `nanoda_bin` bundled with the toolchain when available, + # otherwise builds lean4export and nanoda_lib from source (installing Rust if needed). # Allowed values: "true" | "false". # Default: "false" nanoda: "" diff --git a/action.yml b/action.yml index 27638db..7d00461 100644 --- a/action.yml +++ b/action.yml @@ -120,9 +120,15 @@ inputs: default: "false" nanoda: description: | + Deprecated: use `lake-check: paranoid`, which runs nanoda among every other checker + bundled with the toolchain. There is no migration for `nanoda-allow-sorry: true`, because + `lake check` permits only the standard axioms, so a project that needs `sorry` tolerated + should stay on this input for now. Check environment with nanoda external type checker. nanoda is an independent Lean 4 type checker written in Rust. - Requires Rust toolchain (will be installed automatically if not present). + Uses the `leanexport` and `nanoda_bin` bundled with the toolchain when it ships them, + and otherwise builds lean4export and nanoda_lib from source, which needs a Rust toolchain + (installed automatically if not present). Allowed values: "true" | "false". required: false default: "false" diff --git a/scripts/run_nanoda.sh b/scripts/run_nanoda.sh index 6675345..e7fd812 100755 --- a/scripts/run_nanoda.sh +++ b/scripts/run_nanoda.sh @@ -5,6 +5,8 @@ set -e echo "::group::nanoda Output" echo "Checking environment with nanoda external type checker" +echo "::warning::\`nanoda\` is deprecated; use \`lake-check: paranoid\` instead, which runs nanoda together with every other checker bundled with the toolchain. It has no equivalent of \`nanoda-allow-sorry: true\`, because \`lake check\` permits only the standard axioms, so projects that carry a \`sorry\` should stay on this input for now." + # handle_exit function to capture exit status and cleanup handle_exit() { exit_status=$? @@ -32,38 +34,57 @@ if [ -d "_lean4export" ] || [ -d "_nanoda_lib" ]; then exit 1 fi -# Step 1: Install Rust if not present -echo "Checking for Rust installation..." -if ! command -v cargo &> /dev/null; then - echo "Installing Rust toolchain..." - curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --default-toolchain stable --profile minimal - # shellcheck source=/dev/null - source "$HOME/.cargo/env" +# Recent release toolchains ship both the exporter and nanoda, matched to each other and to the +# compiler that produced the oleans. When they are there, use them: cloning and building +# `lean4export` and `nanoda_lib` costs a Rust toolchain and two source builds on every run, and +# pins `nanoda_lib` to a branch rather than a release. +BUNDLED_EXPORTER="$(elan which leanexport 2>/dev/null || true)" +BUNDLED_NANODA="$(elan which nanoda_bin 2>/dev/null || true)" + +if [ -n "$BUNDLED_EXPORTER" ] && [ -x "$BUNDLED_EXPORTER" ] \ + && [ -n "$BUNDLED_NANODA" ] && [ -x "$BUNDLED_NANODA" ]; then + echo "Using the leanexport and nanoda_bin bundled with this toolchain" + EXPORTER="$BUNDLED_EXPORTER" + NANODA="$BUNDLED_NANODA" else - echo "Rust already installed: $(cargo --version)" -fi + echo "This toolchain bundles no nanoda; building it and lean4export from source" + + # Step 1: Install Rust if not present + echo "Checking for Rust installation..." + if ! command -v cargo &> /dev/null; then + echo "Installing Rust toolchain..." + curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --default-toolchain stable --profile minimal + # shellcheck source=/dev/null + source "$HOME/.cargo/env" + else + echo "Rust already installed: $(cargo --version)" + fi + + # Step 2: Clone and build lean4export + echo "Cloning and building lean4export..." + git clone --depth 1 https://github.com/leanprover/lean4export.git _lean4export -# Step 2: Clone and build lean4export -echo "Cloning and building lean4export..." -git clone --depth 1 https://github.com/leanprover/lean4export.git _lean4export + # Copy lean-toolchain to lean4export so it uses matching Lean version + cp lean-toolchain _lean4export/ -# Copy lean-toolchain to lean4export so it uses matching Lean version -cp lean-toolchain _lean4export/ + ( + cd _lean4export + lake build + ) -( - cd _lean4export - lake build -) + # Step 3: Clone and build nanoda_lib + echo "Cloning and building nanoda_lib..." + # Using debug branch which has fixes for recent Lean kernel changes + git clone --depth 1 --branch debug https://github.com/ammkrn/nanoda_lib.git _nanoda_lib -# Step 3: Clone and build nanoda_lib -echo "Cloning and building nanoda_lib..." -# Using debug branch which has fixes for recent Lean kernel changes -git clone --depth 1 --branch debug https://github.com/ammkrn/nanoda_lib.git _nanoda_lib + ( + cd _nanoda_lib + cargo build --release + ) -( - cd _nanoda_lib - cargo build --release -) + EXPORTER="_lean4export/.lake/build/bin/lean4export" + NANODA="_nanoda_lib/target/release/nanoda_bin" +fi # Step 4: Detect module name from lakefile echo "Detecting module name..." @@ -91,7 +112,7 @@ echo "Detected module name: $MODULE_NAME" # Step 5: Export the project echo "Exporting $MODULE_NAME..." EXPORT_FILE="_nanoda_export.txt" -lake env _lean4export/.lake/build/bin/lean4export "$MODULE_NAME" > "$EXPORT_FILE" +lake env "$EXPORTER" "$MODULE_NAME" > "$EXPORT_FILE" echo "Export file size: $(wc -c < "$EXPORT_FILE") bytes" echo "Export file lines: $(wc -l < "$EXPORT_FILE") lines" @@ -126,6 +147,6 @@ cat "$CONFIG_FILE" # Step 7: Run nanoda echo "" echo "Running nanoda type checker..." -_nanoda_lib/target/release/nanoda_bin "$CONFIG_FILE" +"$NANODA" "$CONFIG_FILE" echo "nanoda check completed successfully" From ee1dfb33a9b916693ea9cae928fdefcca2f60062 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 23 Sep 2026 12:47:45 +1000 Subject: [PATCH 2/3] test: check for the bundled binaries after the toolchain is downloaded `elan` sets the default toolchain without downloading it, so the precondition step ran 40ms after `elan-init` and found no toolchain directory at all. Move it after `lake update`, which is the first thing that actually uses the toolchain. --- .github/functional_tests/nanoda_bundled/action.yml | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/.github/functional_tests/nanoda_bundled/action.yml b/.github/functional_tests/nanoda_bundled/action.yml index a94df23..e2161d9 100644 --- a/.github/functional_tests/nanoda_bundled/action.yml +++ b/.github/functional_tests/nanoda_bundled/action.yml @@ -15,18 +15,20 @@ runs: echo "$HOME/.elan/bin" >> "$GITHUB_PATH" shell: bash - - name: confirm the toolchain really does bundle both binaries - run: | - elan which leanexport - elan which nanoda_bin - shell: bash - - name: create a clean lake library run: | lake init foo lib lake update shell: bash + # `elan` sets the default toolchain without downloading it, so this can only run once + # something has actually used it: `lake update` above is the first thing that does. + - name: confirm the toolchain really does bundle both binaries + run: | + elan which leanexport + elan which nanoda_bin + shell: bash + - name: "run `lean-action` with `nanoda: true`" id: lean-action-nanoda uses: ./ From 209c085c3370c2fbae9e8bdfc87955f0c49a1082 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 23 Sep 2026 13:05:18 +1000 Subject: [PATCH 3/3] fix: detect the module to export from the default targets `lake init foo lib` on a current toolchain writes `name = "foo"` at the top level of `lakefile.toml`, with no `[package]` section and a library called `Foo`. Looking only for a package name therefore found nothing, and `nanoda` failed with "Could not detect module name from lakefile.toml or lakefile.lean" before it checked anything. Prefer `defaultTargets`, then the first `lean_lib`, then the `[package]` name. The first two name a module to export; a package name need not be one. --- CHANGELOG.md | 4 ++++ scripts/run_nanoda.sh | 17 ++++++++++++++--- 2 files changed, 18 insertions(+), 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 9b69afe..b4779d9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -11,6 +11,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 - `nanoda` now uses the `leanexport` and `nanoda_bin` bundled with the toolchain when it ships them, instead of installing a Rust toolchain and building lean4export and nanoda_lib from source on every run. Older toolchains keep the source-build path, and the axioms permitted are unchanged either way +### Fixed + +- detect the module to export for `nanoda` from `defaultTargets` or the first `lean_lib`, rather than only from a `[package]` section. A current `lake init` writes no `[package]` section, so `nanoda: true` failed outright with "Could not detect module name" + ### Deprecated - `nanoda` and `nanoda-allow-sorry`, in favour of `lake-check: paranoid`. Note that `lake check` permits only the standard axioms, so there is no equivalent of `nanoda-allow-sorry: true`; projects carrying a `sorry` should stay on `nanoda` for now diff --git a/scripts/run_nanoda.sh b/scripts/run_nanoda.sh index e7fd812..f62943d 100755 --- a/scripts/run_nanoda.sh +++ b/scripts/run_nanoda.sh @@ -90,10 +90,21 @@ fi echo "Detecting module name..." MODULE_NAME="" -# Try lakefile.toml first +# Try lakefile.toml first. Prefer `defaultTargets`, then the first `lean_lib`: those name the +# module to export, where the package name need not be a module at all. `lake init foo lib` on a +# current toolchain writes `name = "foo"` at the top level with no `[package]` section and a +# library called `Foo`, so looking only for a package name finds nothing to export. if [ -f "lakefile.toml" ]; then - # Extract name from [package] section - MODULE_NAME=$(grep -A5 '^\[package\]' lakefile.toml | grep '^name' | head -1 | sed 's/.*= *"\([^"]*\)".*/\1/' || true) + MODULE_NAME=$(grep -m1 '^defaultTargets' lakefile.toml | sed -n 's/.*\[[^"]*"\([^"]*\)".*/\1/p' || true) + + if [ -z "$MODULE_NAME" ]; then + MODULE_NAME=$(grep -A3 '^\[\[lean_lib\]\]' lakefile.toml | grep -m1 '^name' | sed 's/.*= *"\([^"]*\)".*/\1/' || true) + fi + + # Older lakefiles put the package name in a `[package]` section. + if [ -z "$MODULE_NAME" ]; then + MODULE_NAME=$(grep -A5 '^\[package\]' lakefile.toml | grep '^name' | head -1 | sed 's/.*= *"\([^"]*\)".*/\1/' || true) + fi fi # Fallback to lakefile.lean