Login

Verification run

Run 31

promachina/iut-leanbranch mastertriggered via manual
failedcommit 7dc5aeb267bctoolchain lean-v4-30-0prover leantook 2s · finished 15w ago

lake build failed with exit code 125 (toolchain lean-v4-30-0, command: elan run leanprover/lean4:v4.30.0 -- bash -c export PATH="$(dirname "$(elan which lean)"):$PATH"; exec "$@" apx-lean-phase lake build)

Open project

Package inputs

This verification run did not include a theorem package lock. Its inputs depend only on repository, toolchain, image, and command inputs.

Trust verification

Recomputes trust checks from the recorded attestations, manifest, and command history.

(verification not run)

Manifest

Loads the published files manifest and location metadata for this job.

(manifest not loaded)

Verifier log excerpt

(no log excerpt)

Command runs

git_cloneexit 0duration 2s · created 
git clone --depth 1 --branch master --single-branch https://github.com/promachina/iut-lean.git /var/lib/apodeixis/repos/job-54-source
Cloning into '/var/lib/apodeixis/repos/job-54-source'...
git_checkoutexit 0duration 93 ms · created 
git checkout 7dc5aeb267bc377d6848d260ba7f9289232728df
Note: switching to '7dc5aeb267bc377d6848d260ba7f9289232728df'.

You are in 'detached HEAD' state. You can look around, make experimental
changes and commit them, and you can discard any commits you make in this
state without impacting any branches by switching back to a branch.

If you want to create a new branch to retain commits you create, you may
do so (now or later) by using -c with the switch command. Example:

  git switch -c <new-branch-name>

Or undo this operation with:

  git switch -

Turn off this advice by setting config variable advice.detachedHead to false

HEAD is now at 7dc5aeb Add finite source first pass route
lake_cacheexit 125duration 32 ms · created 
lake exe cache get
time="2026-06-03T12:55:08Z" level=warning msg="Failed to get rootless runtime dir for DefaultAPIAddress: lstat /run/user/996: permission denied"
time="2026-06-03T12:55:08Z" level=error msg="running `/usr/bin/newuidmap 3249790 0 996 1 1 100000 65536`: newuidmap: write to uid_map failed: Operation not permitted\n"
Error: cannot set up namespace using "/usr/bin/newuidmap": exit status 1
lean_checkerexit 125duration 30 ms · created 
lake build
time="2026-06-03T12:55:08Z" level=warning msg="Failed to get rootless runtime dir for DefaultAPIAddress: lstat /run/user/996: permission denied"
time="2026-06-03T12:55:08Z" level=error msg="running `/usr/bin/newuidmap 3249803 0 996 1 1 100000 65536`: newuidmap: write to uid_map failed: Operation not permitted\n"
Error: cannot set up namespace using "/usr/bin/newuidmap": exit status 1
blueprint_buildexit 125duration 26 ms · created 
lake build :blueprint
time="2026-06-03T12:55:08Z" level=warning msg="Failed to get rootless runtime dir for DefaultAPIAddress: lstat /run/user/996: permission denied"
time="2026-06-03T12:55:08Z" level=error msg="running `/usr/bin/newuidmap 3249815 0 996 1 1 100000 65536`: newuidmap: write to uid_map failed: Operation not permitted\n"
Error: cannot set up namespace using "/usr/bin/newuidmap": exit status 1
semantic_module_factsexit 125duration 25 ms · created 
./.apodeixis/tools/lean-semantic-extract.sh --module-facts
time="2026-06-03T12:55:08Z" level=warning msg="Failed to get rootless runtime dir for DefaultAPIAddress: lstat /run/user/996: permission denied"
time="2026-06-03T12:55:08Z" level=error msg="running `/usr/bin/newuidmap 3249826 0 996 1 1 100000 65536`: newuidmap: write to uid_map failed: Operation not permitted\n"
Error: cannot set up namespace using "/usr/bin/newuidmap": exit status 1
semantic_extractexit 125duration 33 ms · created 
./.apodeixis/tools/lean-semantic-extract.sh
time="2026-06-03T12:55:08Z" level=warning msg="Failed to get rootless runtime dir for DefaultAPIAddress: lstat /run/user/996: permission denied"
time="2026-06-03T12:55:08Z" level=error msg="running `/usr/bin/newuidmap 3249839 0 996 1 1 100000 65536`: newuidmap: write to uid_map failed: Operation not permitted\n"
Error: cannot set up namespace using "/usr/bin/newuidmap": exit status 1

Keyboard shortcuts