continuous integration

fixes #64642

Sign in to view logs

Triggered via push January 8, 2024 01:16

kim-em

lean-pr-testing-3124

Status Cancelled

Total duration 25m 11s

Artifacts –

build.yml

on: push

Check all files imported

Cancel Previous Runs (CI)

check workflows

Annotations

13 errors

Lint style: Mathlib/Tactic/SimpIntro.lean#L69

Mathlib/Tactic/SimpIntro.lean#L69: ERR_LIN: Line has more than 100 characters

Process completed with exit code 123.

The run was canceled by @github-actions[bot].

Build: Mathlib/Computability/PartrecCode.lean#L942

(deterministic) timeout at 'whnf', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)

Build: Mathlib/Computability/PartrecCode.lean#L1002

unknown identifier 'hlup.comp'

Build: Mathlib/Computability/PartrecCode.lean#L1009

unknown identifier 'hlup.comp'

Build: Mathlib/Computability/PartrecCode.lean#L1022

unknown identifier 'hlup.comp'

Build: Mathlib/Computability/PartrecCode.lean#L1025

unknown identifier 'hlup.comp'

Build: Mathlib/Computability/PartrecCode.lean#L1040

unknown identifier 'hlup.comp'

Build: Mathlib/Computability/PartrecCode.lean#L1046

unknown identifier 'hlup.comp'

Build: Mathlib/Computability/PartrecCode.lean#L1067

unknown identifier 'hlup.comp'

Build: Mathlib/CategoryTheory/Limits/Opposites.lean#L545

tactic 'simp' failed, nested error:

Build: Mathlib/CategoryTheory/Limits/Opposites.lean#L546

tactic 'simp' failed, nested error: