This repository has been archived by the owner on Jul 24, 2024. It is now read-only.
Merge branch 'master' into YK-cont-alternating #121026
urkud
This run and associated checks have been archived and are scheduled for deletion.
Learn more about checks retention
build.yml
on: push
Build mathlib
1h 43m
Lint style
57s
Cancel Previous Runs (CI)
5s
Post-CI job
0s
Annotations
6 errors and 1 warning
|
Lint style:
src/topology/vector_bundle/alternating.lean#L162
ERR_LIN: Line has more than 100 characters
|
|
Lint style:
src/analysis/normed_space/alternating.lean#L463
ERR_LIN: Line has more than 100 characters
|
|
Lint style:
src/analysis/normed_space/alternating.lean#L464
ERR_LIN: Line has more than 100 characters
|
|
Lint style
Process completed with exit code 123.
|
|
Build mathlib:
src/topology/vector_bundle/alternating.lean#L99
/home/lean/actions-runner/_work/mathlib/mathlib/src/topology/vector_bundle/alternating.lean:99:22:
type mismatch at application
total_space E₁
term
E₁
has type
B → Type u_5 : Type (max u_3 (u_5+1))
but is expected to have type
Type ? : Type (?+1)
Additional information:
/home/lean/actions-runner/_work/mathlib/mathlib/src/topology/vector_bundle/alternating.lean:99:22: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
type mismatch, term
total_space ?m_2
has type
(?m_1 → Type ?) → Type (max ? ?) : Type (max (max ? (?+1)) (?+1) (?+1))
but is expected to have type
Type ? : Type (?+1)
|
|
Build mathlib
Process completed with exit code 1.
|
|
Build mathlib
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/upload-artifact@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
|
Artifacts
Produced during runtime
| Name | Size | |
|---|---|---|
|
precompiled-mathlib-3.51.1-2851eea
Expired
|
498 MB |
|