Recover from a HALTED latch

Find out why native calls stopped, read the ledger and the faulted call's records, and clear what the runtime checks.

When the supervision of a native call goes wrong, the runtime writes a latch file and refuses every later native call until you resolve it. The checks are in crates/lema-check/src/lib.rs.

Before you start

• Access, as the operator, to the runtime configuration and the paths it names. Below, OUT is the configuration’s output, LOCK its shared_lock, and $CONFIG the configuration file.

Steps

1. Find which latch is set:

   cat "$OUT/HALTED" "$LOCK.HALTED"

   Latch	Written when	Stops native calls of
   OUT/HALTED	a call’s supervision fails, for example a timeout, a log over 16 MiB, incomplete output capture, a process that could not be cleaned up, or the distribution changing during the call	every configuration with this output
   LOCK.HALTED	a call’s systemd scope could not be confirmed gone after it ended	every configuration with this shared_lock

   Each latch holds one line, <call name>: <fault>. Refused calls fail with native calls halted; see …/HALTED or native calls halted host-wide; see ….HALTED. A failed proof is not a fault: Lean exiting with an error is reported and sets no latch.

   While a latch is set, lema serve still answers requests that make no native call, such as info, find, show and alias. Anything that needs a native call is refused, and lema check-runtime exits 1.

2. Read the ledger. OUT/ledger.jsonl has one JSON line per event: reserve before each call (name, unit, config_sha256, at, host) and complete after it (name, fault, exit_code, wall_seconds, at). List the faulted calls:

   grep '"event":"complete"' "$OUT/ledger.jsonl" | grep -v '"fault":null'

   A reserve with no later complete for the same name is an unresolved call, for example after lema serve was killed during a call. It stops later calls too, without a latch: unresolved native calls in the ledger: […].

3. Read the faulted call’s records in OUT:

   • <name>-reserved.json: the command line, working directory, time limit and start time;
   • <name>-result.json: the same, plus the process ID, exit code, wall time, fault, log size and end time;
   • <name>.log: the call’s output;
   • work/<name>/: its work directory.

4. For a host-wide latch, make sure the scope is gone. The latch text names the unit (native scope cleanup incomplete: lema-native-….scope …). Every native call also refuses while such a scope is live (a native scope is still present). This is the listing the runtime checks, and units shown as inactive or failed do not count:

   systemctl --user list-units --all --no-legend --plain 'lema-native-*'

5. Resolve the latch.

   For a latch in OUT, the simplest way is a fresh output. Write a configuration with a new output (Write a runtime configuration), restart lema serve with it, and keep the latched output as the record of the fault. The new output starts with an empty module cache.

   To keep using the same output, two things must be true. Neither latch file may exist. Every faulted or unresolved call in the ledger must have a later line {"event":"resolved","name":"<call name>"}. No lema command writes that line or removes a latch: both are left to you. Every ledger line must be a reserve, complete or resolved event. Any other line makes every later native call fail, and info too (ledger entry …).

   For a host-wide latch, a fresh output does not help: every configuration that shares the lock is stopped until LOCK.HALTED is gone.

6. Confirm that native calls run again:

   lema check-runtime --runtime $CONFIG

   It makes one small native call in that configuration’s output. It exits 0 when the call ran, 75 when the lock is busy or the host is loaded, and 1 for any other refusal.