Zulip Chat Archive

Stream: mathlib4

Topic: source references


Reid Barton (Dec 15 2022 at 08:09):

Dear mathlib4 porters,

mathlib3port now has notices at the top of each file recording the file's origin, such as

! This file was ported from Lean 3 source module algebra.abs
! leanprover-community/mathlib commit aba57d4d3dae35460225919dcd82fe91355162f9
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.

Please update mathlib3port before starting any new mathlib4 PRs (which I guess is a good idea in any case) so that your PR will also contain this notice. For now there is no need to take any action on existing PRs.
Thanks!


Last updated: Dec 20 2023 at 11:08 UTC