Verification run

Run 4

Gogopex/pfr branch master triggered via manual

failed commit manual toolchain lean-v4-28-0-rc1 prover lean took 1m 15s · finished 7w ago

lake build failed with exit code 1 (toolchain lean-v4-28-0-rc1, command: elan run leanprover/lean4:v4.28.0-rc1 -- 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_clone exit 0 duration 622 ms · created 6/1/2026, 2:28:32 PM

git clone --depth 1 --branch master --single-branch https://github.com/Gogopex/pfr.git /var/lib/apodeixis/repos/job-4-source

Cloning into '/var/lib/apodeixis/repos/job-4-source'...

lake_cache exit 1 duration 1m 3s · created 6/1/2026, 2:28:32 PM

lake exe cache get

installing leantar 0.1.16

info: downloading https://releases.lean-lang.org/lean4/v4.28.0-rc1/lean-4.28.0-rc1-linux.tar.zst
info: installing /root/.elan/toolchains/leanprover--lean4---v4.28.0-rc1
info: checkdecls: cloning https://github.com/PatrickMassot/checkdecls.git
info: checkdecls: checking out revision '3d425859e73fcfbef85b9638c2a91708ef4a22d4'
info: APAP: cloning https://github.com/YaelDillies/apap.git
info: APAP: checking out revision '13fd6dd3a47445b6dd10826f0ffc1116f4e13144'
info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git
info: mathlib: checking out revision '507f18fc9044549fc730d8d0270521e3b090360a'
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision '7311586e1a56af887b1081d05e80c11b6c41d212'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision '5ce7f0a355f522a952a3d678d696bd563bb4fd28'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision 'b5908dbac486279f1133cb937648c63c30b455af'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision '6d65c6e0a25b8a52c13c3adeb63ecde3bfbb6294'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision 'f08e838d4f9aea519f3cde06260cfb686fd4bab0'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision '23324752757bf28124a518ec284044c8db79fee5'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision '0100f1a3222df01286db33fcb6a1f98564f5439d'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '28e0856d4424863a85b18f38868c5420c55f9bae'
✔ [2/22] Built Cache.Init (397ms)
✔ [3/22] Built Cache.Lean (521ms)
✔ [4/22] Built Cache.Init:c.o (86ms)
✔ [5/22] Built Cache.Lean:c.o (110ms)
✔ [6/22] Built Cache.IO (1.4s)
✔ [7/22] Built Cache.Hashing (759ms)
✔ [8/22] Built Cache.Hashing:c.o (408ms)
✔ [9/22] Built Cache.IO:c.o (1.2s)
✔ [15/22] Built Batteries.Data.String.Basic:c.o (94ms)
✔ [16/22] Built Batteries.Data.Array.Match:c.o (208ms)
✔ [17/22] Built Batteries.Data.String.Matcher:c.o (167ms)
✔ [18/22] Built Cache.Requests (1.5s)
✔ [19/22] Built Cache.Main (715ms)
✔ [20/22] Built Cache.Main:c.o (436ms)
✔ [21/22] Built Cache.Requests:c.o (1.3s)
✔ [22/22] Built cache:exe (829ms)
  % Total    % Received % Xferd  Average Speed   Time    Time     Time  Current
                                 Dload  Upload   Total   Spent    Left  Speed

  0     0    0     0    0     0      0      0 --:--:-- --:--:-- --:--:--     0
  0     0    0     0    0     0      0      0 --:--:-- --:--:-- --:--:--     0

100 1125k  100 1125k    0     0  2995k      0 --:--:-- --:--:-- --:--:-- 2995k

uncaught exception: failure in tar #[-xf, /root/.cache/mathlib/leantar-0.1.16.tar.gz, -C, /root/.cache/mathlib, --strip-components=1]:
tar: leantar: Cannot change ownership to uid 1001, gid 1001: Operation not permitted
tar: Exiting with failure status due to previous errors

lean_checker exit 1 duration 5s · created 6/1/2026, 2:28:32 PM

lake build

error: error during download
info: caused by: [6] Could not resolve hostname (Could not resolve host: github.com)

semantic_extract exit 1 duration 5s · created 6/1/2026, 2:28:32 PM

./.apodeixis/tools/lean-semantic-extract.sh

error: error during download
info: caused by: [6] Could not resolve hostname (Could not resolve host: github.com)