another mathlib3 bump #1069
Annotations
1 error and 7 warnings
|
push release to azure
Process completed with exit code 1.
|
|
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/setup-python@v1, 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/
|
|
setup precompiled zip file
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/
|
|
leanpkg build
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/
|
|
leanpkg build:
src/unused/resultant/basic.lean#L80
/home/runner/work/flt-regular/flt-regular/src/unused/resultant/basic.lean:80:0:
declaration 'discriminant'_mul_X_pow_add_C_mul_X_add_C' uses sorry
|
|
leanpkg build:
src/number_theory/kummers_lemma.lean#L17
/home/runner/work/flt-regular/flt-regular/src/number_theory/kummers_lemma.lean:17:0:
declaration 'eq_pow_prime_of_unit_of_congruent' uses sorry
|
|
leanpkg build:
src/caseII/statement.lean#L11
/home/runner/work/flt-regular/flt-regular/src/caseII/statement.lean:11:0:
declaration 'flt_regular.caseII' uses sorry
|
|
leanpkg build:
src/flt_regular.lean#L2
/home/runner/work/flt-regular/flt-regular/src/flt_regular.lean:2:0:
imported file '/home/runner/work/flt-regular/flt-regular/src/caseII/statement.lean' uses sorry
|
The logs for this run have expired and are no longer available.
Loading