chore(*): add mathlib3 synchronization labels (#17314)

Co-authored-by: Scott Morrison <[email protected]>
leanprover-community · Nov 7, 2022 · d82d6e2 · d82d6e2
1 parent 2901424
commit d82d6e2
Show file tree

Hide file tree

Showing 11 changed files with 43 additions and 1 deletion.
diff --git a/scripts/port_status.py b/scripts/port_status.py
@@ -110,7 +110,7 @@ def stripPrefix(tag : str) -> str:
 print('# The following files are marked as ported, but do not have a SYNCHRONIZED WITH MATHLIB4 label.')
 for node in graph.nodes:
     if data[node].startswith('Yes') and not node in synchronized:
-        print(node)
+        print(node + "     -- " + data[node][4:])
 
 print()
 print('# The following files are marked as ported, but have not been verified against a commit hash from mathlib.')

diff --git a/src/algebra/group_power/identities.lean b/src/algebra/group_power/identities.lean
@@ -4,9 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bryan Gin-ge Chen, Kevin Lacker
 -/
 import tactic.ring
+
 /-!
 # Identities
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/531
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file contains some "named" commutative ring identities.
 -/
 

diff --git a/src/category_theory/concrete_category/bundled.lean b/src/category_theory/concrete_category/bundled.lean
@@ -8,6 +8,10 @@ import tactic.lint
 /-!
 # Bundled types
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/514
+> Any changes to this file require a corresponding PR to mathlib4.
+
 `bundled c` provides a uniform structure for bundling a type equipped with a type class.
 
 We provide `category` instances for these in `category_theory/unbundled_hom.lean`

diff --git a/src/data/fin/fin2.lean b/src/data/fin/fin2.lean
@@ -7,6 +7,10 @@ Authors: Mario Carneiro
 /-!
 # Inductive type variant of `fin`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/478
+> Any changes to this file require a corresponding PR to mathlib4.
+
 `fin` is defined as a subtype of `ℕ`. This file defines an equivalent type, `fin2`, which is
 defined inductively. This is useful for its induction principle and different definitional
 equalities.

diff --git a/src/data/prod/pprod.lean b/src/data/prod/pprod.lean
@@ -7,6 +7,10 @@ import logic.basic
 
 /-!
 # Extra facts about `pprod`
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/496
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 open function

diff --git a/src/data/sum/basic.lean b/src/data/sum/basic.lean
@@ -8,6 +8,10 @@ import data.option.basic
 /-!
 # Disjoint union of types
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/497
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file proves basic results about the sum type `α ⊕ β`.
 
 `α ⊕ β` is the type made of a copy of `α` and a copy of `β`. It is also called *disjoint union*.

diff --git a/src/logic/basic.lean b/src/logic/basic.lean
@@ -9,6 +9,10 @@ import tactic.reserved_notation
 /-!
 # Basic logic properties
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/484
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file is one of the earliest imports in mathlib.
 
 ## Implementation notes

diff --git a/src/logic/function/basic.lean b/src/logic/function/basic.lean
@@ -9,6 +9,10 @@ import tactic.cache
 
 /-!
 # Miscellaneous function constructions and lemmas
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/511
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 universes u v w

diff --git a/src/logic/is_empty.lean b/src/logic/is_empty.lean
@@ -5,9 +5,14 @@ Authors: Floris van Doorn
 -/
 import logic.function.basic
 import tactic.protected
+
 /-!
 # Types that are empty
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/486
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define a typeclass `is_empty`, which expresses that a type has no elements.
 
 ## Main declaration

diff --git a/src/logic/nonempty.lean b/src/logic/nonempty.lean
@@ -8,6 +8,10 @@ import logic.basic
 /-!
 # Nonempty types
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/487
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file proves a few extra facts about `nonempty`, which is defined in core Lean.
 
 ## Main declarations

diff --git a/src/logic/unique.lean b/src/logic/unique.lean
@@ -9,6 +9,10 @@ import logic.is_empty
 /-!
 # Types with a unique term
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/512
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define a typeclass `unique`,
 which expresses that a type has a unique term.
 In other words, a type that is `inhabited` and a `subsingleton`.