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

Updated normal correspondence code to Lean 4 #121024

Sign in to view logs

Updated normal correspondence code to Lean 4

Updated normal correspondence code to Lean 4 #121024

Triggered via push November 27, 2023 16:49
@ChimiSeanGaChimiSeanGa
pushed 6e16239
normal_correspondence
Status Failure
Total duration 1h 47m 42s
Artifacts 1

build.yml

on: push
Build mathlib
8m 20s
Build mathlib
Lint style
30s
Lint style
Cancel Previous Runs (CI)
7s
Cancel Previous Runs (CI)
Lint mathlib
58m 49s
Lint mathlib
Run tests
19m 51s
Run tests
Post-CI job
0s
Post-CI job
Fit to window
Zoom out
Zoom in

Annotations

10 errors and 17 warnings
Lint style: src/field_theory/normal_correspondence.lean#L1
ERR_COP: Malformed or missing copyright header
Lint style: src/field_theory/normal_correspondence.lean#L2
ERR_COP: Malformed or missing copyright header
Lint style: src/field_theory/normal_correspondence.lean#L1
ERR_COP: Malformed or missing copyright header
Lint style: src/field_theory/normal_correspondence.lean#L4
ERR_COP: Malformed or missing copyright header
Lint style: src/field_theory/normal_correspondence.lean#L4
ERR_MOD: Module docstring missing, or too late
Lint style
Process completed with exit code 123.
Warning from unused_arguments linter: src/field_theory/normal_correspondence.lean#L38
stabilizing_iff_res_stabilizing - argument 7: [_inst_5 : finite_dimensional F L]
Warning from unused_arguments linter: src/field_theory/normal_correspondence.lean#L59
res_stabilizing_iff_normal_closure_contained - argument 6: [_inst_4 : is_galois F L], argument 7: [_inst_5 : finite_dimensional F L]
Warning from unused_arguments linter: src/field_theory/normal_correspondence.lean#L71
normal_closure_contained_iff_normal - argument 7: [_inst_5 : finite_dimensional F L]
Lint mathlib
Process completed with exit code 1.
Cancel Previous Runs (CI)
The following actions uses node12 which is deprecated and will be forced to run on node16: styfle/[email protected]. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
Lint style
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2, actions/setup-python@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
Lint style: src/field_theory/normal_correspondence.lean#L10
WRN_BRC: Probable misformatting of curly braces
Lint style: src/field_theory/normal_correspondence.lean#L19
WRN_BRC: Probable misformatting of curly braces
Lint style: src/field_theory/normal_correspondence.lean#L23
WRN_BRC: Probable misformatting of curly braces
Lint style: src/field_theory/normal_correspondence.lean#L26
WRN_BRC: Probable misformatting of curly braces
Lint style: src/field_theory/normal_correspondence.lean#L27
WRN_BRC: Probable misformatting of curly braces
Lint style: src/field_theory/normal_correspondence.lean#L35
WRN_BRC: Probable misformatting of curly braces
Lint style: src/field_theory/normal_correspondence.lean#L44
WRN_BRC: Probable misformatting of curly braces
Lint style: src/field_theory/normal_correspondence.lean#L51
WRN_BRC: Probable misformatting of curly braces
Lint style: src/field_theory/normal_correspondence.lean#L52
WRN_BRC: Probable misformatting of curly braces
Lint style: src/field_theory/normal_correspondence.lean#L56
WRN_BRC: Probable misformatting of curly braces
Build mathlib
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2, 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/
Build mathlib
The `set-output` command is deprecated and will be disabled soon. Please upgrade to using Environment Files. For more information see: https://github.blog/changelog/2022-10-11-github-actions-deprecating-save-state-and-set-output-commands/
Build mathlib
The `set-output` command is deprecated and will be disabled soon. Please upgrade to using Environment Files. For more information see: https://github.blog/changelog/2022-10-11-github-actions-deprecating-save-state-and-set-output-commands/
Run tests
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/download-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/
Lint mathlib
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/download-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.50.3-6e16239 Expired
481 MB