continuous integration

fix: adapt to lean4#3084 #62317

Sign in to view logs

Triggered via push December 22, 2023 22:15

digama0

lean-pr-testing-3084

Status Failure

Total duration 47m 59s

Artifacts –

This run and associated checks have been archived and are scheduled for deletion. Learn more about checks retention

build.yml

on: push

Check all files imported

Cancel Previous Runs (CI)

check workflows

Annotations

1 error and 10 warnings

Process completed with exit code 1.

Build: Mathlib/Order/Estimator.lean#L182

unused variable `h₁` [linter.unusedVariables]

Build: Mathlib/Data/List/MinMax.lean#L348

unused variable `h` [linter.unusedVariables]

Build: Mathlib/Order/InitialSeg.lean#L516

unused variable `h` [linter.unusedVariables]

Build: Mathlib/Logic/Encodable/Basic.lean#L647

unused variable `h` [linter.unusedVariables]

Build: Mathlib/Data/PFunctor/Univariate/M.lean#L132

unused variable `h` [linter.unusedVariables]

Build: Mathlib/Data/PFunctor/Univariate/M.lean#L581

unused variable `h` [linter.unusedVariables]

Build: Mathlib/Data/FP/Basic.lean#L150

unused variable `h₁` [linter.unusedVariables]

Build: Mathlib/Data/FP/Basic.lean#L153

unused variable `h₂` [linter.unusedVariables]

Build: Mathlib/Data/QPF/Univariate/Basic.lean#L544

unused variable `h` [linter.unusedVariables]

Build: Mathlib/SetTheory/Ordinal/Notation.lean#L518

unused variable `mn` [linter.unusedVariables]