Login

Verification run

Run 29

promachina/iut-lean branch master triggered via manual
failed commit 7dc5aeb267bc toolchain lean-v4-30-0 prover lean took 1m 17s · finished 6w 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_checkout exit 0 duration 4 ms · created 
git remote set-url origin [clone-url]
git_checkout exit 0 duration 483 ms · created 
git fetch --prune --depth 1 origin master
From https://github.com/promachina/iut-lean
 * branch            master     -> FETCH_HEAD
git_checkout exit 0 duration 12 ms · created 
git checkout -B master FETCH_HEAD
Your branch is up to date with 'origin/master'.

Switched to and reset branch 'master'
git_checkout exit 0 duration 5 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_cache exit 125 duration 58 ms · created 
lake exe cache get
Error: lstat data/repos/.cache/lean-workspaces/semantic-runner: no such file or directory
lean_checker exit 125 duration 52 ms · created 
lake build
Error: lstat data/repos/.cache/lean-workspaces/semantic-runner: no such file or directory
blueprint_build exit 125 duration 62 ms · created 
lake build :blueprint
Error: lstat data/repos/.cache/lean-workspaces/semantic-runner: no such file or directory
semantic_extract exit 125 duration 73 ms · created 
./.apodeixis/tools/lean-semantic-extract.sh
Error: lstat data/repos/.cache/lean-workspaces/semantic-runner: no such file or directory

Keyboard shortcuts