Discovering Commands🔗

The dispatcher provides grouped help and a machine-readable list:

# Compare grouped help with the flat list used by scripts.
scripts/lake.sh exe torchlean --help
scripts/lake.sh exe torchlean --list

--help explains the command groups and gives a starting path. --list prints exactly one registered command name per line, which is what you want in a script. Running scripts/lake.sh exe torchlean with no arguments prints the same help and exits with status 1, so a bare invocation in a Makefile fails rather than silently doing nothing.

Use the generated help for the current groups and command descriptions; they come directly from the runner's registry rather than a second catalogue maintained in this chapter.

--list prints the registered command names with no grouping and no descriptions:

quickstart_tensors
quickstart_autograd
quickstart_mlp
mlp
...
torch_ir_pytorch

An unknown name is refused before anything runs, and the help follows so the correct spelling is on screen:

# An unknown name exercises dispatch before any model is
# constructed.
scripts/lake.sh exe torchlean nosuchthing

Unknown example: nosuchthing

TorchLean runnable examples
...

The exit status is 1.

Command Implementation🔗

The MLP quickstart shows how the shared parser connects to a trainer. Its main first handles help and arguments, then constructs the training configuration:

-- Dispatch selects the registered command; that command
-- parses its remaining arguments.
def main (args : List String) : IO Unit := do
  let args := CLI.dropDashDash args
  if CLI.hasHelp args then
    IO.println usage
    return
  let (seed, args) ← CLI.orThrow exeName <| CLI.takeSeed args
  let (steps, args) ← CLI.orThrow exeName <|
    CLI.takePositiveNatFlag args exeName "steps" 200
  let runtime ← CLI.Trainer.parseCommandLine exeName args

  let trainer := Trainer.new model
    { runtime with
        objective := mse
        optimizer := optim.adam { lr := 0.03 }
        seed := seed }
  ...

The command drops a leading --, answers --help if present, and parses the remaining arguments before constructing the trainer. The full file is SimpleMlpTrain.lean. Each binding of args contains only the arguments left by the previous parser. After consuming --seed and --steps, CLI.Trainer.parseCommandLine handles runtime flags and checks for anything left over. The shared functions in NN/API/CLI.lean expose this remainder in their return types:

CLI.takeFlagValue? : List String → String → Except String (Option String × List String)

CLI.takeNatFlag? : List String → String → Except String (Option ℕ × List String)

CLI.takePathFlag? : List String → String → Except String (Option System.FilePath × List String)

CLI.takeBoolValueFlag? : List String → String → Except String (Option Bool × List String)

CLI.checkNoArgs : List String → Except String Unit

The four take... functions return the parsed optional value together with the remaining arguments. Each can also return an error message. checkNoArgs returns only Unit on success, and succeeds only for an empty list. Calling it on the final remainder rejects flags that no parser consumed.

If you know Python's argparse, parse_args also rejects unknown arguments by default, while parse_known_args returns them to its caller. Here we can see that choice in the call to checkNoArgs.

The Except and Option in these signatures answer separate questions. Except.error means that the supplied command line cannot be used. Inside Except.ok, none means that this particular flag was absent, while some value means it was present and parsed. This distinction lets a command supply a default without silently replacing a misspelled number. The second component is just as important: it records the arguments that another parser still has to account for. A successful individual parser does not establish that the whole command line is valid.

Parser Results🔗

The parsers can be evaluated directly. This call consumes --steps 20 and leaves the unrelated path flag in the remainder:

Except.ok (some 20, ["--x", "a.npy"])

The 20 came out, and --x a.npy was handed back untouched. The --key=value spelling is accepted as the same thing:

Except.ok (some 20, [])

A repeated flag produces an error:

Except.error "--steps: duplicate flag"

A shell script that appends options from several variables can supply conflicting values for the same flag. Rejecting duplicates requires the caller to resolve that conflict before running.

An absent flag is not an error, because callers supply defaults:

Except.ok (none, ["--x", "a.npy"])

A present flag with an unusable value is:

Except.error "--steps: expected a natural number, got `two`"

The final check reports arguments left unconsumed:

Except.error "unexpected arguments: [--rollout, 8]"

Except.ok ()

Paths and Booleans go through typed variants, so a path becomes a System.FilePath at the boundary rather than being carried around as a string:

Except.ok (some (FilePath.mk "/tmp/trainlog.json"), [])

Except.ok (some false, [])

The two remaining helpers handle the shape of the command line rather than its contents. A leading separator is dropped for the benefit of wrappers that insist on one:

["quickstart_mlp", "--steps", "20"]

true

hasHelp is checked before the other parsers, so help remains available even if another argument on the command line is invalid.

The path and Boolean outputs above describe parsing, not the effects of running the command. FilePath.mk does not check whether a file exists, whether its contents have the required shape, or whether its directory is writable. Those checks belong to the reader or writer that uses the path. Similarly, successfully parsing false says which Boolean was requested; the command must still use that value when it constructs its configuration. Following the parsed value into the configuration is the useful next step when a flag appears to have no effect.

Command Grammar🔗

The normal form is:

# Runtime and command-specific flags share the argument list
# after the command.
scripts/lake.sh exe torchlean <subcommand> [runtime flags] [command flags]

For example:

# Select CPU execution while setting the training length and
# initialization seed.
scripts/lake.sh exe torchlean quickstart_mlp \
  --device cpu --steps 20 --seed 2026

Runtime flags may also precede the subcommand:

# The dispatcher also accepts the runtime selection before
# the command name.
scripts/lake.sh exe torchlean --device cpu quickstart_mlp \
  --steps 20 --seed 2026

The runner collects prefix flags, finds the command, and forwards those flags together with the arguments after it. The selected command parses both. I put the command first in these examples so we can read what will run before its options. A leading separator is accepted for wrappers that require one:

# The separator is removed before the command parses its
# remaining flags.
scripts/lake.sh exe torchlean -- quickstart_mlp --device cpu --steps 20

Strict Parsing🔗

The GridWorld command has a fixed source-level horizon and does not accept --rollout:

# GridWorld does not accept this spelling of the rollout
# option.
scripts/lake.sh exe torchlean ppo_gridworld \
  --device cpu --updates 1 --rollout 8

[TorchLean] device: cpu
ppo_gridworld: PPO on Lean-native GridWorld (4x4, horizon=64) (device=cpu)
  env: pure Lean dynamics + boundary contract check + formal MDP validity proof available
error: ppo_gridworld: unexpected arguments: [--rollout, 8]

The command exits with status 1 before training or writing artifacts. Its runtime selection and description appear first because it prints them before the final checkNoArgs. The runner's TorchLean.CLI.exitOnError catches the error and adds the error: prefix. Scripts should test the exit status rather than infer success from a banner or require an error message to start with the command name.

The same rule catches flags borrowed from a neighbouring command. The FNO application takes --x and --y for its training arrays, so the plausible-looking --train-x fails:

# A dataset option from another command is rejected by the
# Burgers example.
scripts/lake.sh exe torchlean fno1d_burgers --train-x a.npy

fno1d_burgers: native FNO1D Burgers (device=cpu)
error: fno1d_burgers: unexpected arguments: [--train-x, a.npy]

The leftover-argument check makes independently written parsers compose. A training parser can consume --steps, then hand the remainder to the runtime parser without knowing every device option itself. The final checkNoArgs closes that process: an unrecognized flag cannot quietly survive the chain. This is why the errors above show the original unused arguments. When adding a new option, both consuming it and placing its value in the eventual configuration matter.

Runtime Flags🔗

The common runtime parser recognizes:

Per-command help narrows this shared list. The convolutional classifier, for instance, advertises only native arithmetic:

# Read the CNN-specific defaults before preparing image
# batches.
scripts/lake.sh exe torchlean cnn --help

Usage: scripts/lake.sh exe torchlean cnn [options]

Data:
  --x PATH           feature/image NPY file
  --y PATH           class-label NPY file
  --n-total N        rows to load

Training:
  --steps N          optimizer updates
  --batch-size N     dataset items accumulated per update (default: 1)
  --lr X             learning rate
  --log PATH|false   write a TrainLog JSON, or disable logging
  --cuda-mem-watch N sample CUDA allocator state every N updates

Runtime:
  --device auto|cpu|gpu|cuda|rocm|metal|wasm|tpu|trainium|custom|external
  --arithmetic native
  --seed N           runtime seed (default: 0)
  --show-backend     print backend capsules as they execute

Read the Runtime: block as this command's contract, not as a copy of the global list.

# A known device name can still lack an implementation for
# this command.
scripts/lake.sh exe torchlean quickstart_mlp --device rocm --steps 1

error: quickstart_mlp: device `rocm` has no maintained
runtime profile; use a programmatic backend profile

# An unknown device name fails during parsing rather than
# backend execution.
scripts/lake.sh exe torchlean quickstart_mlp --device banana --steps 1

error: quickstart_mlp: unknown device banana (known targets:
cpu | cuda | rocm | metal | wasm | tpu | trainium | custom | external)

CPU And CUDA Builds🔗

CPU execution uses the ordinary build:

# Build the CPU configuration before asking the executable
# to use CPU storage.
scripts/lake.sh build
scripts/lake.sh exe torchlean quickstart_mlp --device cpu --steps 20

CUDA execution requires a CUDA-enabled LibTorch SDK and the Lake option:

# Set this to the installed SDK before linking the CUDA configuration.
export TORCHLEAN_LIBTORCH_HOME=/path/to/libtorch
scripts/lake.sh -R -K cuda=true build
scripts/lake.sh -R -K cuda=true exe torchlean chargpt --device cuda \
  --tiny-shakespeare --preset smoke

The wrapper isolates CPU and CUDA build profiles; pass -Kcuda=true on each CUDA invocation. -R forces Lake to reconfigure the package. Without cuda=true, the CUDA symbols fail with a message to rebuild. The SDK, CUDA toolkit, and compiler must be compatible; GPU And CUDA describes the native build.

Add --show-backend to inspect what was selected:

# Inspect the contracts selected by this runtime profile.
scripts/lake.sh exe torchlean quickstart_mlp --steps 1 --show-backend

The report names, for each operation, its provider, trust level, VJP source, and reduction order, then four evidence lines. Wrapped to fit this page, the matrix-multiply entry reads:

  matmul: reference.matmul provider=reference trust=checked
      vjp=torchlean-tape reduction=fixed-left
    shape: shape safety for matmul; guarded at runtime by
      portable runtime shape checks
    layout: canonical-tensor layout compatibility for matmul;
      guarded at runtime by typed tensor layout
    value: matmul forward refines its TorchLean semantics;
      covered by test suite NN.Tests.Runtime.Floats.Suite
    vjp: matmul torchlean-tape VJP refines its TorchLean
      semantics; covered by test suite NN.Tests.Runtime.Floats.Suite

For that one-step run the report covers seven operations: reshape, permute, matmul, broadcast, add, relu, and mse_loss. reduction=fixed-left records a specific summation order, which matters when reproducing floating-point results (Goldberg, 1991). The trust=checked entry points to runtime guards and tests; the two value/VJP lines name the test suite that supports those claims. They do not identify a kernel-checked refinement proof.

Capsule lines may interleave with the application's output. Redirect to a file and search for provider= to find the report. Backend Selection explains what the fields mean and where they come from.

The device identifies where operations run. The capsule identifies the implementation selected for each operation on that device.

A build flag and a runtime flag act at different stages. -Kcuda=true changes the build configuration and linked backend support. --device cuda asks an already built executable to select that backend. Recording only the latter leaves out whether the executable could satisfy the request. Capsule reporting describes selection before handler lookup and execution; a report can therefore precede a missing-handler error. A successful native call requires the linked implementation and a usable device as well as an admissible capsule.

Arithmetic🔗

Most model commands use native Float32. The arithmetic-polymorphic quickstarts and numerical workflows also accept --arithmetic ieee, which selects FloatLib's executable binary32:

# Keep the model configuration fixed while changing the
# arithmetic implementation.
scripts/lake.sh exe torchlean quickstart_mlp --device cpu --steps 1 --seed 2026
scripts/lake.sh exe torchlean quickstart_mlp --device cpu --steps 1 --seed 2026 --arithmetic ieee

Native arithmetic executes hardware floating-point operations; --arithmetic ieee selects ExecFloat.Binary 8 23, with binary32 rounding defined in FloatLib. Compare the reported losses and held-out prediction. Running both can expose a disagreement between the executable reference and the runtime, but matching decimal output alone does not compare every bit or cover other inputs. The proof statements and their assumptions are in Float32 Soundness; Floating-Point Semantics describes the scalar types (Boldo and Melquiond, 2011).

A command that cannot implement the requested semantics says so instead of approximating:

# Complex arithmetic is not an available training mode for
# this command.
scripts/lake.sh exe torchlean quickstart_mlp --steps 1 --arithmetic complex

error: quickstart_mlp: TorchLean.Trainer: supervised training
supports native or IEEE arithmetic; complex arithmetic requires an explicit
complex-valued training API

The shared parser recognizes names across commands. Each selected command still checks whether it supports the requested arithmetic and device.

For complex training, the explicit-state example has its own command:

scripts/lake.sh exe torchlean complex_regression 50 /tmp/complex-regression.state

It minimizes a real squared-residual loss over complex binary32 weights and bias, then prints a held-out complex prediction. The optional checkpoint is reloaded and checked without discarding either component. Its coordinate-forward gradient is intended for small models, not as a native complex GPU training benchmark.

Device and arithmetic describe two choices: where tensor operations run and how scalar arithmetic is implemented. They are useful to record separately even when only some combinations are implemented. The two commands above make a deliberately small comparison with the same training arguments. Reading a numerical difference as an arithmetic effect requires keeping the initialization, data, optimizer settings, and number of updates fixed as well. A completed command establishes that its selected path ran; the printed loss describes that run's objective.

The Interactive Device Chooser🔗

Use --choose when running a command by hand and you do not want to remember the device flag:

# Choose the device interactively for the selected
# quickstart command.
scripts/lake.sh exe torchlean --choose quickstart_mlp --steps 1

TorchLean runtime chooser
Runtime device:
  1) CPU    portable default
  2) CUDA   GPU runtime, requires `scripts/lake.sh -K cuda=true exe ...`
Select device [1]:

Pressing Enter selects CPU and the run proceeds. The chooser is opt-in so shell scripts, tests, and continuous integration never block waiting for input, and it offers only the two implemented runtimes rather than the whole device registry.

The command registry records which examples accept device selection. The chooser prompts only for those examples; fixed-runtime commands run directly, and help, unknown commands, and incomplete invocations are handled without prompting. For example:

# A command with a fixed runtime can bypass the device
# chooser.
scripts/lake.sh exe torchlean --choose quickstart_tensors

This runs the tensor quickstart directly. An explicit --device is preserved and suppresses the prompt; its value is still validated by the selected command.

Command-Specific Flags🔗

Ask the subcommand:

# Inspect the text model dimensions, data path, and
# evaluation options together.
scripts/lake.sh exe torchlean chargpt --help

torchlean chargpt: character-level GPT training

Usage:
  scripts/lake.sh -R -K cuda=true exe torchlean chargpt --device cuda --tiny-shakespeare \
    --preset PRESET [flags]

Presets:
  smoke       two-update end-to-end CUDA check
  karpathy    full Tiny Shakespeare lecture experiment

Architecture:
  --width N       embedding width
  --heads N       attention heads; must divide width
  --layers N      Transformer blocks
  --dropout P     dropout probability in [0, 1)
  --batch-size N  training windows per update
  --seq-len N     context length
  --steps N       optimizer updates
  --lr FLOAT      AdamW learning rate
  --eval-every N  validation cadence; 0 disables intermediate evaluation
  --eval-iters N  batches averaged at each validation point
  --load-checkpoint P restore model state before training
  --save-checkpoint P save final model state

Notes:
  - Training and validation use disjoint 90/10 corpus splits.
  - CPU and CUDA runs both use native Float32 arithmetic.

The help lists presets, architecture and training options, and checkpoint paths. It also gives constraints such as the requirement that --heads divide --width. The batch flag is --batch-size; --batch is rejected.

Not every application has equally detailed command-specific help yet. If a generic runtime page is printed, read the module documentation or the parser next to that application; the source links in the preceding chapters point at the maintained definitions.

The text-model help groups dimensions with training controls because they constrain each other. Context length determines how many token positions participate in an example; batch size determines how many such examples are processed together. An evaluation batch count controls how many losses are averaged, so changing it changes the measurement even when the model parameters are fixed. When reproducing a reported result, keep these values alongside the seed and step count. A command name alone does not identify the experiment.

Preparing Data🔗

Synthetic examples need no dataset download. Real-data examples have separate preparation steps; check the command because some text workflows can download their corpus. The dataset script prepares several public datasets:

# Prepare the input datasets before running the examples
# that consume them.
python3 scripts/datasets/download_example_data.py \
  --auto-mpg --tiny-shakespeare --tinystories-valid --cifar10

It writes under data/real/, and --cifar10-limit-train -1 opts into all 50000 training images instead of the small default subset. Forecasting and the Burgers operator use dedicated preparation:

# Convert the source data into the formats expected by the
# sequence and operator examples.
python3 scripts/datasets/download_example_data.py \
  --household-power --household-power-windows 512

python3 NN/Examples/Data/prepare_fno1d_burgers.py \
  --download --grid 32 --ntrain 128 --ntest 32

Convert a local labeled image folder with:

# Match the converted image dimensions and labels to the
# image training command.
python3 scripts/datasets/torchlean_data_convert.py image-folder \
  --input /path/to/images \
  --x-output data/real/imagenet64/imagenet64_train_X.npy \
  --y-output data/real/imagenet64/imagenet64_train_y.npy \
  --height 64 --width 64 \
  --labels-from-dirs --limit 2000

These Python tools download and preprocess data, including image decoding and array conversion. The Lean loaders then check file existence, array metadata, dimensions, finiteness where required, and conversion to typed tensors. These checks do not establish that the downloaded labels or the preprocessing script are semantically correct. Datasets And Loaders describes the loader contracts.

Data preparation determines the interface that the trainer will see. Resizing an image changes its spatial dimensions, choosing a label column changes the target, and converting a sequence fixes the ordering in which observations are presented. These choices should agree with the model configuration before training begins. A limit on input rows is also different from a minibatch size: one limits the available dataset, while the other controls how examples are grouped for an update. The conversion and training commands expose different parts of that contract.

Artifact Paths🔗

Pass explicit paths when an output will be inspected later:

# Save the autoencoder training log at an explicit path.
scripts/lake.sh exe torchlean autoencoder --device cpu \
  --n-total 1 --steps 1 \
  --log /tmp/autoencoder-trainlog.json

# Keep the policy checkpoint, rollout record, and training
# log as separate artifacts.
scripts/lake.sh exe torchlean ppo_gridworld --device cpu \
  --updates 1 --eval-every 1 \
  --log /tmp/ppo-trainlog.json \
  --policy /tmp/ppo-policy.json \
  --path /tmp/ppo-path.json

# Write the sampled image to the requested PPM file.
scripts/lake.sh -R -K cuda=true exe torchlean diffusion --device cuda \
  --dataset cifar10 --n-total 8 --steps 20 --T 20 \
  --sample-ppm /tmp/diffusion-sample.ppm

--log PATH|false appears in most training commands, and passing false turns logging off rather than writing to a file named false. The path is part of the experiment: it tells a widget, plotting script, or checker which exact object it is reading. Interactive Widgets consumes these files.

An artifact path gives a run a destination, but it does not by itself describe the artifact's provenance. Keep the command, configuration, and input identity with a checkpoint or log if it will be compared with another run later. Explicit paths are particularly useful when invoking the same example repeatedly: a default filename otherwise refers to whichever run wrote it most recently. The three PPO outputs serve different purposes, so preserving a log does not replace preserving the policy parameters or the recorded rollout.

Verification Commands🔗

List the registry, then choose one workflow:

# Discover the checker names, then run the in-memory IBP
# workflow explicitly.
scripts/lake.sh exe verify -- list
scripts/lake.sh exe verify -- torchlean-ibp

Each row below is one Tool record in NN/Verification/CLI.lean, and the last column is its includeInAll field:

The lirpa-* names refer to interval bound propagation (Gowal et al., 2018) and the LiRPA framework (Xu et al., 2020). The other names refer to α,β-CROWN (Wang et al., 2021) for abcrown-leaf, physics-informed residuals (Raissi et al., 2019) for the PINN tools, and neural Lyapunov functions (Chang et al., 2019) for the two-stage workflows.

The table includes both in-memory computations and readers of external artifacts. An in-memory workflow such as torchlean-ibp builds a model, lowers it to IR, and runs a bound algorithm inside the current process:

# This workflow builds and lowers its model inside the
# current process.
scripts/lake.sh exe verify -- torchlean-ibp

=== TorchLean → IR → IBP (small MLP) workflow ===
[TorchLean] arithmetic: native binary32
lowered IR nodes: 18
output box lo: [1.904000]
output box hi: [2.256001]

The workflow computes this box from its built-in model. An artifact checker such as pinn-cert or abcrown-leaf parses a file produced elsewhere and applies its declared checks. These differ: the α,β-CROWN leaf reader checks that the leaves cover the root and clear their thresholds without recomputing the bounds, while a semantic certificate checker must also establish the claimed bounds. This distinction matters for proof-carrying code (Necula, 1997): the producer may be untrusted as long as the consumer can check the evidence. A checker accepts only its declared schema and semantic fragment, and it does not retroactively verify the process that produced the artifact.

# Run the registry entries whose includeInAll field is
# enabled.
scripts/lake.sh exe verify -- all

== lirpa-mlp ==
IBP certificate verified: serialized bounds enclose Lean recomputation.

== lirpa-cnn ==
IBP certificate verified: serialized bounds enclose Lean recomputation.
...
== abcrown-leaf ==
[artifact] Checked 1 leaves: ok=1, bad=0
[artifact] consistent: the leaves cover the root and every leaf clears its threshold.
[artifact] The lower bounds are the producer's claims; TorchLean did not recompute them.

== margin-report ==
[margin report] examples=360
[margin report] nominal_ok=349 (requires 'pred' in examples)
[margin report] positive_margin=318

Validation Sequence🔗

After a fresh clone or a substantial local change, run these commands in order:

# Check elaboration, small executions, training, and
# verification in sequence.
scripts/lake.sh build
scripts/lake.sh build NNExamples
scripts/lake.sh exe torchlean quickstart_tensors
scripts/lake.sh exe torchlean quickstart_autograd
scripts/lake.sh exe torchlean quickstart_mlp --device cpu --steps 20 --seed 2026
scripts/lake.sh exe torchlean numerical_certificate
scripts/lake.sh exe verify -- torchlean-ibp

They answer different questions:

The numerical-certificate command includes a negative control alongside successful certificate and replay cases:

TorchLean numerical runtime certificate
  ok  base certificate
  ok  base IEEE replay
  ok  tampered range rejected
  ok  two-layer MLP certificate
  ok  two-layer MLP IEEE replay
All numerical certificate checks passed.

The negative control changes an addition range and confirms rejection. The remaining rows check successful generation and replay of the small graph and the MLP. For the broader native numerical checks, use the curated suite; this example keeps the artifact workflow visible.

For CUDA changes, follow with CUDA-specific builds and runtime checks. For external tools, prepare their dependencies separately. Their dependencies and acceptance conditions differ from the CPU checks above.

Building The Website🔗

The guide, API reference, and application pages are built by:

# Regenerate the blueprint before serving the website that
# includes it.
scripts/docs/build_site.sh

For a local Jekyll preview after the generated site exists:

# Serve the generated site from the website directory.
cd home_page
bundle _2.3.14_ exec jekyll serve \
  --config _config.yml,_config_dev.yml \
  --host 127.0.0.1 --port 4001

Then open:

http://127.0.0.1:4001/
http://127.0.0.1:4001/blueprint/
http://127.0.0.1:4001/examples/
http://127.0.0.1:4001/docs/

If the source changed but the browser did not, rebuild the generated site before restarting Jekyll. The blueprint build checks the document's executable pieces and regenerates the guide; Jekyll serves the resulting files. Restarting the server against an older generated tree will still show the older examples. After rebuilding, read the edited prose beside its output blocks in the served page: elaboration checks the executable pieces, while this reading checks whether the explanation still makes sense with them.

Command Exercises🔗

1. Run scripts/lake.sh exe torchlean --list | wc -l and account for the commands across the groups shown by --help.

2. Pick any training command and pass a flag from a different one. Read the message and identify which parser rejected it.

3. Run one command twice with --seed 1 and --seed 2, then twice with the same seed, and confirm which pairs agree exactly.

4. Run quickstart_mlp --steps 1 with --arithmetic native and --arithmetic ieee and diff the two outputs. Then try --steps 200 and compare the losses and predictions again.

5. Redirect --show-backend output to a file and count the distinct provider= values.

6. Run scripts/lake.sh exe verify -- all, then run each torchlean-* tool by hand, and note how much of the registry a green all left untouched.

7. Write a --log under a new directory and inspect the created parent directories. Then try a path whose parent is a regular file and inspect the reported write failure.

Command Results🔗

A successful process, a backend selection report, and an accepted certificate answer different questions. When recording a result, keep the command, selected implementation, and the tool's actual acceptance condition together. Verification Overview describes the claims that the verification commands check.