feat(scripts): add a script to update port comments (#17600)

Also updates all existing port comments


Currently this relies on an unreleased mathlibtools, which can be installed with `pip install git+https://github.com/leanprover-community/mathlib-tools`

scripts/add_port_comments.py

@@ -0,0 +1,75 @@
+from mathlibtools.file_status import PortStatus
+from pathlib import Path
+
+import re
+from dataclasses import asdict, dataclass
+from typing import Any, Dict, Optional, Union
+import textwrap
+
+import requests
+import yaml
+
+status = PortStatus.deserialize_old()
+
+src_path = Path(__file__).parent.parent / 'src'
+
+def make_comment(fstatus):
+    return textwrap.dedent(f"""\
+    > THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+    > https://github.com/leanprover-community/mathlib4/pull/{fstatus.mathlib4_pr}
+    > Any changes to this file require a corresponding PR to mathlib4.""")
+
+def replace_range(src, pos, end_pos, new):
+    return src[:pos] + new + src[end_pos:]
+
+
+def add_port_status(fcontent, fstatus):
+    module_comment = re.search('/-!\s*(.*?)-/', fcontent, re.MULTILINE | re.DOTALL)
+    assert module_comment
+    module_comment_start = module_comment.start(1)
+    module_comment_end = module_comment.end(1)
+
+    comment_re = re.compile(
+        r"^((?:> )?)THIS FILE IS SYNCHRONIZED WITH MATHLIB4\."
+        r"(?:\n\1[^\n]+)*\n*",
+        re.MULTILINE
+    )
+    header_re = re.compile('^#[^\n]*\n?', re.MULTILINE)
+
+    existing_label = comment_re.search(fcontent, module_comment_start, module_comment_end)
+    existing_header = header_re.search(fcontent, module_comment_start, module_comment_end)
+
+    if not existing_label:
+        rest = fcontent[existing_header.end():module_comment_end]
+        trailing_whitespace = "\n" if rest.strip() else ""
+        fcontent = replace_range(fcontent, existing_header.end(), existing_header.end(),
+            "\n" + make_comment(f_status) + trailing_whitespace)
+    else:
+        if existing_label.end() <= existing_header.start():
+            rest = fcontent[existing_header.end():module_comment_end]
+            trailing_whitespace = "\n" if rest.strip() else ""
+            fcontent = replace_range(fcontent, existing_header.end(), existing_header.end(),
+                "\n" + make_comment(f_status) + trailing_whitespace)
+            fcontent = replace_range(fcontent, existing_label.start(), existing_label.end(), "")
+        elif existing_header.end() <= existing_label.start():
+            rest = fcontent[existing_label.end():module_comment_end]
+            trailing_whitespace = "\n" if rest.strip() else ""
+            fcontent = replace_range(fcontent, existing_label.start(), existing_label.end(), "")
+            fcontent = replace_range(fcontent, existing_header.end(), existing_header.end(),
+                "\n" + make_comment(f_status) + trailing_whitespace)
+        else:
+            assert False
+    return fcontent
+
+def fname_for(import_path):
+    return src_path / Path(*import_path.split('.')).with_suffix('.lean')
+
+
+for iname, f_status in status.file_statuses.items():
+    if f_status.ported:
+        fname = fname_for(iname)
+        with open(fname) as f:
+            fcontent = f.read()
+        fcontent = add_port_status(fcontent, f_status)
+        with open(fname, 'w') as f:
+            f.write(fcontent)

src/algebra/homology/complex_shape.lean

@@ -9,6 +9,10 @@ import logic.relation
 /-!
 # Shapes of homological complexes
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/635
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define a structure `complex_shape ι` for describing the shapes of homological complexes
 indexed by a type `ι`.
 This is intended to capture chain complexes and cochain complexes, indexed by either `ℕ` or `ℤ`,

src/data/bool/basic.lean

@@ -5,12 +5,12 @@ Authors: Leonardo de Moura, Jeremy Avigad
 -/
 
 /-!
-THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
-https://github.com/leanprover-community/mathlib4/pull/534
-Any changes to this file require a corresponding PR to mathlib4.
-
 # booleans
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/534
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file proves various trivial lemmas about booleans and their
 relation to decidable propositions.
 

src/data/bracket.lean

@@ -5,12 +5,12 @@ Authors: Patrick Lutz, Oliver Nash
 -/
 
 /-!
-THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
-https://github.com/leanprover-community/mathlib4/pull/480
-Any changes to this file require a corresponding PR to mathlib4.
-
 # Bracket Notation
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/480
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file provides notation which can be used for the Lie bracket, for the commutator of two
 subgroups, and for other similar operations.
 

src/data/option/basic.lean

@@ -8,12 +8,12 @@ import control.traversable.basic
 import tactic.basic
 
 /-!
-THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
-https://github.com/leanprover-community/mathlib4/pull/493
-Any changes to this file require a corresponding PR to mathlib4.
-
 # Option of a type
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/493
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file develops the basic theory of option types.
 
 If `α` is a type, then `option α` can be understood as the type with one more element than `α`.

src/data/option/defs.lean

@@ -5,12 +5,12 @@ Authors: Mario Carneiro
 -/
 
 /-!
-THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
-https://github.com/leanprover-community/mathlib4/pull/504
-Any changes to this file require a corresponding PR to mathlib4.
-
 # Extra definitions on `option`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/504
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines more operations involving `option α`. Lemmas about them are located in other
 files under `data.option.`.
 Other basic operations on `option` are defined in the core library.

src/data/prod/basic.lean

@@ -7,12 +7,12 @@ import tactic.basic
 import logic.function.basic
 
 /-!
-THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
-https://github.com/leanprover-community/mathlib4/pull/545
-Any changes to this file require a corresponding PR to mathlib4.
-
 # Extra facts about `prod`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/545
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines `prod.swap : α × β → β × α` and proves various simple lemmas about `prod`.
 -/
 

src/data/sigma/basic.lean

@@ -9,12 +9,12 @@ import tactic.ext
 import logic.function.basic
 
 /-!
-THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
-https://github.com/leanprover-community/mathlib4/pull/449
-Any changes to this file require a corresponding PR to mathlib4.
-
 # Sigma types
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/479
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file proves basic results about sigma types.
 
 A sigma type is a dependent pair type. Like `α × β` but where the type of the second component

src/data/subtype.lean

@@ -8,12 +8,12 @@ import tactic.ext
 import tactic.simps
 
 /-!
-THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
-https://github.com/leanprover-community/mathlib4/pull/546
-Any changes to this file require a corresponding PR to mathlib4.
-
 # Subtypes
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/546
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file provides basic API for subtypes, which are defined in core.
 
 A subtype is a type made from restricting another type, say `α`, to its elements that satisfy some

src/logic/function/conjugate.lean

@@ -6,12 +6,12 @@ Authors: Yury Kudryashov
 import logic.function.basic
 
 /-!
-THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
-https://github.com/leanprover-community/mathlib4/pull/533
-Any changes to this file require a corresponding PR to mathlib4.
-
 # Semiconjugate and commuting maps
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/533
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define the following predicates:
 
 * `function.semiconj`: `f : α → β` semiconjugates `ga : α → α` to `gb : β → β` if `f ∘ ga = gb ∘ f`;

src/logic/relation.lean

@@ -7,12 +7,12 @@ import tactic.basic
 import logic.relator
 
 /-!
-THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
-https://github.com/leanprover-community/mathlib4/pull/565
-Any changes to this file require a corresponding PR to mathlib4.
-
 # Relation closures
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/565
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines the reflexive, transitive, and reflexive transitive closures of relations.
 It also proves some basic results on definitions in core, such as `eqv_gen`.
 

src/logic/relator.lean

@@ -12,7 +12,6 @@ import logic.basic
 > THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
 > https://github.com/leanprover-community/mathlib4/pull/385
 > Any changes to this file require a corresponding PR to mathlib4.
-
 -/
 
 namespace relator

src/order/monotone.lean

@@ -10,6 +10,10 @@ import order.rel_classes
 /-!
 # Monotonicity
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/591
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines (strictly) monotone/antitone functions. Contrary to standard mathematical usage,
 "monotone"/"mono" here means "increasing", not "increasing or decreasing". We use "antitone"/"anti"
 to mean "decreasing".