Automation

Automation commands by role

lev verify publishes a fixed verification gate. lev check adds repository-specific tasks and policy. The other commands cover maintenance and multi-project workflows without changing the underlying Lake commands.

Command	Role
`lev verify`	Fixed gate for CI, issue reports, and release checks.
`lev check`	Repository tasks, import policy, and trust policy.
`lev deps upgrade --check`	Build and test a dependency proposal in an isolated workspace.
`lev workspace`	Run ordered operations across independent Lake roots.
`lev project bundle`	Archive the locked source tree and omit generated state.
`lev watch`	Rerun a command in the selected environment after source changes.

lev verify --offline --test --lint

Publish one gate that means the same thing everywhere

Now bug reports, pull requests, and CI can all point at the same fixed sequence instead of a different shell alias on every machine.

lev check --task test --task lint --imports

Layer local repository policy on top

Once the project wants import drift checks, named tasks, or trust policy, keep that in versioned config instead of hidden job definitions.

lev deps upgrade --check --test

Rehearse upgrades away from the working tree

The upgrade transaction is more reviewable when the proposal builds somewhere else before you apply it for real.

lev workspace build --keep-going

Add workspace operations when one repository holds several Lake roots

Each member keeps its own lock and failure boundary, which matters for mixed library, examples, and benchmark repos.

Two verification commands

A typical release check verifies the lock, dependency selections, checkout, toolchain, build, tests, lint, and imports. lev provides two related commands for that sequence.

`lev verify`

Fixed published phase order.
Optional --test and --lint Lake drivers.
Best when you want a stable public gate and the lev.cli.verify/v1 contract.

`lev check`

Configurable repository tasks from lev.toml.
Import policy and trust policy phases.
Best when the project wants a stricter local gate and the lev.cli.check/v1 contract.

These built-in phases run first. Tasks and policy checks only happen after the build succeeds.

Configurationparse project files

Lockcompare recorded state

Dependenciesexplain selected revisions

Auditverify integrity

Toolchaincheck availability

Builddelegate to Lake

Gate commands

lev check
lev check --clean --offline --strict --imports
lev check MyLibrary --task test --task lint
lev check --json > check.json

lev verify --offline --test --lint
lev verify --json > verify.json

Example verification report

Build completed successfully.
PASS  configuration     0.182 ms  parsed lakefile.toml and lev.toml
PASS  lock              0.321 ms  lev.lock matches project configuration
PASS  dependencies      0.060 ms  0 stale, 0 conflicts, 0 root overrides, 0 unknown
PASS  audit             0.208 ms  3 passed, 0 warnings, 0 errors
PASS  toolchain       144.053 ms  leanprover/lean4:v4.18.0 is available
PASS  build           300.273 ms  lake build

Each row names the phase, duration, and evidence behind the result.

Both commands stop at the first failed phase and preserve delegated exit status. If the build fails, later tasks and policy checks are absent on purpose because lev never pretends those phases ran.

Review upgrades before they touch the checkout

Plain lev deps update remains the direct Lake update path. The upgrade workflow checks which direct dependency changes are available, whether they match the selected Lean version, and whether the proposal builds before changing the checkout.

lev deps outdated

See compatible releases first

Use --check in scheduled CI if you want status 1 whenever a compatible update exists.

lev deps upgrade --dry-run

Preview the transaction

Review the exact proposal before the source checkout changes. This is where you decide whether the update is even worth rehearsing.

lev deps upgrade --check --test

Build the proposal in an isolated workspace

lev copies the project into a cache-local workspace keyed by the proposal, applies the change there, verifies the resulting manifest commits, and runs the requested build or test gate.

lev deps upgrade mathlib

Apply only after the rehearsal makes sense

The transaction edits project state deliberately. Source compatibility still belongs to the follow-up build and repository checks.

Upgrade commands

lev deps outdated
lev deps outdated --check
lev deps upgrade --dry-run
lev deps upgrade mathlib --dry-run
lev deps upgrade --check --test
lev deps upgrade mathlib
lev check --task test --task lint

Operate on several Lake roots without merging their failure boundaries

A lev workspace is an ordered set of independent Lake projects declared in the nearest ancestor lev.toml. Each member keeps its own toolchain, manifest, lock, and source transaction.

lev.toml

[workspace]
members = [
  "library",
  "examples",
  "benchmarks",
]

Workspace commands

lev workspace list
lev workspace lock --check
lev workspace sync --frozen
lev workspace build --offline --keep-going
lev workspace run --keep-going -- lake test

list, lock, sync, build, and run process members in deterministic path order. Without --keep-going, the first failure stops the operation. With it, lev runs the remaining members and returns the first failure code.

lev workspace shake applies one import policy across the members while preserving a separate source transaction and report for each project.

Workspace shake examples

lev workspace shake --check --keep-public --keep-implied --keep-going
lev workspace shake --fix --isolate --keep-public --keep-implied --keep-going
lev workspace shake --check --json > workspace-shake.json
lev workspace shake --check --sarif workspace-shake.sarif

During lev workspace sync, the aggregate lev-workspace.lock is published only after every member succeeds. During lev workspace lock, lev refreshes each member lock first, then writes and verifies the aggregate lock. In both cases the aggregate file never claims success for a partial run.

Bundle for handoff, watch for iteration

`lev project bundle`

Create a deterministic Zstandard-compressed tar archive of locked project sources. Generated trees and transient lev outputs are excluded.

lev check --offlinelev project bundle--output artifacts/project.lev.tar.zst

`lev watch`

Keep the selected environment attached to the command you rerun all day. The watcher is event-driven, debounced, and ignores generated trees such as .git, .lake, build, and lock outputs written by the run itself.

lev watch--debounce-ms 400--max-runs 5

Bundle output

lev: bundled 21 files (11237 source bytes)
into /tmp/lev-doc-bundle.lev.tar.zst

One-run watch session

lev: watching /tmp/project and running `lake build`
lev: watch run: lake build
Build completed successfully.

The bundle count provides a quick archive check. Watch reports the command it reruns and the delegated output.

Keep project tasks in versioned config

Tasks give repeated project commands a name without hiding the underlying process. They are a good fit when a repository has a stable set of tests, lints, docs builds, or smoke passes that everyone should run the same way.

lev.toml

[tasks]
docs = ["lake", "build", "Documentation"]
smoke = ["lake", "test", "--", "smoke"]
test = ["lake", "test"]
lint = ["lake", "lint"]

[check]
tasks = ["test", "lint"]
imports = true
deny-axioms = ["sorryAx"]

Terminal

lev task
lev task docs
lev task smoke -- --seed 42
lev check
lev check --task smoke

[tasks] defines commands. [check].tasks chooses which of those belong to every project check. lev check --task NAME adds one more for the current run without changing the config file. For a single Lean file outside a package, lev script builds a cached inline environment from metadata in the file itself.