Skip to content
continuous integration

chore: bump to nightly-2025-12-12 #5632

Sign in to view logs

chore: bump to nightly-2025-12-12

chore: bump to nightly-2025-12-12 #5632

Triggered via push December 12, 2025 09:21
@leanprover-community-bot-assistantleanprover-community-bot-assistant
pushed 862da6f
nightly-testing
Status Failure
Total duration 3m 26s
Artifacts –

build.yml

on: push
Build
3m 24s
Build
Lint style
2m 12s
Lint style
Post-Build Step
Post-Build Step
Post-CI job
0s
Post-CI job
Fit to window
Zoom out
Zoom in

Annotations

19 errors
Build
Process completed with exit code 1.
Build
import Batteries.Lean.NameMapAttribute failed, environment already contains 'Lean.NameMapExtension' from Lean.IdentifierSuggestion
Build
import Batteries.Lean.NameMapAttribute failed, environment already contains 'Lean.NameMapExtension' from Lean.IdentifierSuggestion
Build
`EStateM.run_throw` has already been declared
Build
`EStateM.run_modifyGet` has already been declared
Build
`EStateM.run_modify` has already been declared
Build
`EStateM.run_set` has already been declared
Build
`EStateM.run_get` has already been declared
Build
`EStateM.run_pure` has already been declared
Build
Process completed with exit code 1.
Build
`EStateM.run_throw` has already been declared
Build
`EStateM.run_modifyGet` has already been declared
Build
`EStateM.run_modify` has already been declared
Build
`EStateM.run_set` has already been declared
Build
`EStateM.run_get` has already been declared
Build
`EStateM.run_pure` has already been declared
Build
import Batteries.Lean.NameMapAttribute failed, environment already contains 'Lean.NameMapExtension' from Lean.IdentifierSuggestion
Build
import Batteries.Lean.NameMapAttribute failed, environment already contains 'Lean.NameMapExtension' from Lean.IdentifierSuggestion
Build
Process completed with exit code 3.