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