Verification run

Run 34

AlexKontorovich/PrimeNumberTheoremAnd branch main triggered via poller

failed commit 2a8fd8079ac7 toolchain lean-v4-30-0 prover lean queued 5w ago

deferred after semantic cache checkpoint; PNT cache rows preserved while IUT runs

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 884 ms · created 6/11/2026, 6:05:48 PM

git clone --depth 1 --branch main --single-branch https://github.com/AlexKontorovich/PrimeNumberTheoremAnd.git /var/lib/apodeixis/repos/job-428-source

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

git_checkout exit 0 duration 22 ms · created 6/11/2026, 6:05:48 PM

git checkout 2a8fd8079ac71c1d38991b0f17be4f7e89be20a5

Note: switching to '2a8fd8079ac71c1d38991b0f17be4f7e89be20a5'.

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 2a8fd80   BKLNW: elementary lemmas for the eta, mu and Bessel I0 layer (#1525)

lake_cache exit 137 duration 26s · created 6/11/2026, 6:05:48 PM

lake exe cache get

info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git

lean_checker exit 1 duration 721 ms · created 6/11/2026, 6:05:48 PM

lake build

info: stderr:
fatal: unable to access 'https://github.com/leanprover-community/mathlib4.git/': Could not resolve host: github.com
error: external command 'git' exited with code 128

blueprint_build exit 1 duration 1s · created 6/11/2026, 6:05:48 PM

lake build :blueprint

info: mathlib: checking out revision 'c5ea00351c28e24afc9f0f84379aa41082b1188f'
info: stderr:
fatal: Unable to create '/apx/source/.lake/packages/mathlib/.git/index.lock': File exists.

Another git process seems to be running in this repository, e.g.
an editor opened by 'git commit'. Please make sure all processes
are terminated then try again. If it still fails, a git process
may have crashed in this repository earlier:
remove the file manually to continue.
error: external command 'git' exited with code 128