Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

higher derivatives of a mutlilinear map #81630

higher derivatives of a mutlilinear map

higher derivatives of a mutlilinear map #81630

Triggered via push December 20, 2023 08:51
Status Failure
Total duration 1h 24m 20s
Artifacts

build_fork.yml

on: push
Lint style (fork)
20s
Lint style (fork)
Check all files imported (fork)
11s
Check all files imported (fork)
Build (fork)
1h 24m
Build (fork)
Cancel Previous Runs (CI)
0s
Cancel Previous Runs (CI)
check workflows (fork)
6s
check workflows (fork)
Post-CI job (fork)
0s
Post-CI job (fork)
Fit to window
Zoom out
Zoom in

Annotations

5 errors
Lint style (fork): Mathlib/LinearAlgebra/Multilinear/Basic.lean#L810
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L810: ERR_LIN: Line has more than 100 characters
Lint style (fork): Mathlib/LinearAlgebra/Multilinear/Basic.lean#L946
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L946: ERR_LIN: Line has more than 100 characters
Lint style (fork)
Process completed with exit code 123.
Build (fork): Mathlib/LinearAlgebra/Multilinear/Basic.lean#L780
MultilinearMap.toMultilinearMap_set.{uR, uι, v₁, v₂} definition missing documentation string
Build (fork)
The process '/usr/bin/env' failed with exit code 1