diff --git a/scripts/add_port_comments.py b/scripts/add_port_comments.py new file mode 100644 index 0000000000000..e4605e94254b7 --- /dev/null +++ b/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) diff --git a/src/algebra/homology/complex_shape.lean b/src/algebra/homology/complex_shape.lean index 640e7ce12ade7..bffbd9a898316 100644 --- a/src/algebra/homology/complex_shape.lean +++ b/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 `ℤ`, diff --git a/src/data/bool/basic.lean b/src/data/bool/basic.lean index c6030986ca704..bc94fe07905be 100644 --- a/src/data/bool/basic.lean +++ b/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. diff --git a/src/data/bracket.lean b/src/data/bracket.lean index d2d4801a42eeb..f081f02f9187e 100644 --- a/src/data/bracket.lean +++ b/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. diff --git a/src/data/option/basic.lean b/src/data/option/basic.lean index c91cafbdee8ee..2a3b9fbd78561 100644 --- a/src/data/option/basic.lean +++ b/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 `α`. diff --git a/src/data/option/defs.lean b/src/data/option/defs.lean index 0eb349d34446f..ecc410e921e6e 100644 --- a/src/data/option/defs.lean +++ b/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. diff --git a/src/data/prod/basic.lean b/src/data/prod/basic.lean index 97854127ba0d0..226e5aacd1726 100644 --- a/src/data/prod/basic.lean +++ b/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`. -/ diff --git a/src/data/sigma/basic.lean b/src/data/sigma/basic.lean index c5b06f97f6aca..f937ce7989648 100644 --- a/src/data/sigma/basic.lean +++ b/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 diff --git a/src/data/subtype.lean b/src/data/subtype.lean index 2346a3f39f64f..ac204394899cf 100644 --- a/src/data/subtype.lean +++ b/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 diff --git a/src/logic/function/conjugate.lean b/src/logic/function/conjugate.lean index f1e65a091dcd2..8275b8fbb1fd2 100644 --- a/src/logic/function/conjugate.lean +++ b/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`; diff --git a/src/logic/relation.lean b/src/logic/relation.lean index bf3861a1a2ba2..a30950cd28fd3 100644 --- a/src/logic/relation.lean +++ b/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`. diff --git a/src/logic/relator.lean b/src/logic/relator.lean index de2d4441d0fa5..013d5ded9cf00 100644 --- a/src/logic/relator.lean +++ b/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 diff --git a/src/order/monotone.lean b/src/order/monotone.lean index 451958f237553..686c3519a6646 100644 --- a/src/order/monotone.lean +++ b/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".