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

old WIP trying to replace fractional_ideal by submodule in class_group: to be ported #7381

Sign in to view logs

old WIP trying to replace fractional_ideal by submodule in class_group: to be ported

old WIP trying to replace fractional_ideal by submodule in class_group: to be ported #7381

Triggered via pull request June 28, 2024 02:36
@alreadydonealreadydone
reopened #19245
alreadydone:class_group_without_fractional
Status Success
Total duration 29s
Artifacts –

add_ported_warnings.yml

on: pull_request
Check for modifications to ported files
22s
Check for modifications to ported files
Fit to window
Zoom out
Zoom in

Annotations

8 warnings
Check for modifications to ported files
Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v3, actions/setup-python@v4, Ana06/[email protected], 8BitJonny/[email protected]. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.
Check for modifications to ported files: src/algebra/algebra/operations.lean#L1
Changes to this file will need to be ported to mathlib 4! Please consider retracting the changes to this file unless you are willing to immediately forward-port them.
Check for modifications to ported files: src/algebra/module/equiv.lean#L1
Changes to this file will need to be ported to mathlib 4! Please consider retracting the changes to this file unless you are willing to immediately forward-port them.
Check for modifications to ported files: src/algebra/module/submodule/pointwise.lean#L1
Changes to this file will need to be ported to mathlib 4! Please consider retracting the changes to this file unless you are willing to immediately forward-port them.
Check for modifications to ported files: src/linear_algebra/basic.lean#L1
Changes to this file will need to be ported to mathlib 4! Please consider retracting the changes to this file unless you are willing to immediately forward-port them.
Check for modifications to ported files: src/ring_theory/class_group.lean#L1
Changes to this file will need to be ported to mathlib 4! Please consider retracting the changes to this file unless you are willing to immediately forward-port them.
Check for modifications to ported files: src/ring_theory/fractional_ideal.lean#L1
Changes to this file will need to be ported to mathlib 4! Please consider retracting the changes to this file unless you are willing to immediately forward-port them.
Check for modifications to ported files: src/ring_theory/localization/submodule.lean#L1
Changes to this file will need to be ported to mathlib 4! Please consider retracting the changes to this file unless you are willing to immediately forward-port them.