chore: sync rm_set_option with mathlib, fix it on Windows, remove 29 respectTransparency options

Physlib/Electromagnetism/Distributional/Dynamics/IsExtrema.lean

@@ -219,7 +219,6 @@ A natural consequence of this is that the speed of light is the same in all iner
 
 -/
 
-set_option backward.isDefEq.respectTransparency false in
 lemma isExterma_equivariant {𝓕 : FreeSpace}
     (A : DistElectromagneticPotential d)
     (J : DistLorentzCurrentDensity d) (Λ : LorentzGroup d) :

Physlib/Electromagnetism/Distributional/FieldStrength.lean

@@ -283,7 +283,6 @@ lemma fieldStrength_antisymmetric_basis {d} (A : DistElectromagneticPotential d)
 
 -/
 
-set_option backward.isDefEq.respectTransparency false in
 lemma fieldStrength_equivariant {d} (A : DistElectromagneticPotential d)
     (Λ : LorentzGroup d) :
     (Λ • A).fieldStrength = Λ • A.fieldStrength := by

Physlib/Relativity/LorentzGroup/Boosts/Generalized.lean

@@ -215,7 +215,6 @@ def generalizedBoost (u v : Velocity d) : LorentzGroup d :=
       genBoostAux₁_add_genBoostAux₂_minkowskiProduct]
   ring⟩
 
-set_option backward.isDefEq.respectTransparency false in
 lemma generalizedBoost_apply (u v : Velocity d) (x : Vector d) :
     generalizedBoost u v • x = x + genBoostAux₁ u v x + genBoostAux₂ u v x:= by
   rw [smul_eq_mulVec]

Physlib/Relativity/LorentzGroup/Rotations.lean

@@ -19,7 +19,6 @@ noncomputable section
 
 namespace LorentzGroup
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The subgroup of rotations of the Lorentz group. -/
 def Rotations (d) : Subgroup (LorentzGroup d) where
   carrier Λ := Λ.1 (Sum.inl 0) (Sum.inl 0) = 1 ∧ IsProper Λ

Physlib/Relativity/PauliMatrices/ToTensor.lean

@@ -178,7 +178,6 @@ def pauliContrDownComponent (mu : Fin 4) (a b : Fin 2) : GaussianInt :=
   if mu.val = 3 ∧ a.val = 0 ∧ b.val = 0 then ⟨-1, 0⟩ else
   if mu.val = 3 ∧ a.val = 1 ∧ b.val = 1 then ⟨1, 0⟩ else 0
 
-set_option backward.isDefEq.respectTransparency false in
 lemma toTensor_eq_ofGaussianInt : σ^^^ = ofGaussianInt (fun b =>
     pauliContrComponent (b 0) (b 1) (b 2)) := by
   apply (Tensor.basis _).repr.injective
@@ -195,7 +194,6 @@ lemma toTensor_eq_ofGaussianInt : σ^^^ = ofGaussianInt (fun b =>
   revert b
   decide +kernel
 
-set_option backward.isDefEq.respectTransparency false in
 /-- Gaussian integer components of `σ^^^` after dualizing its left-handed Weyl index. -/
 lemma toTensor_dualLeft_eq_ofGaussianInt :
     {σ^^^ | μ τ(α) β}ᵀ =
@@ -216,7 +214,6 @@ lemma toTensor_dualLeft_eq_ofGaussianInt :
   refine congrArg ofGaussianInt (funext fun b => ?_)
   decide +revert +kernel
 
-set_option backward.isDefEq.respectTransparency false in
 /-- Gaussian integer components of `σ^^^` after dualizing both Weyl indices. -/
 lemma toTensor_dualWeyl_eq_ofGaussianInt :
     {σ^^^ | μ τ(α) τ(β)}ᵀ =
@@ -236,7 +233,6 @@ lemma toTensor_dualWeyl_eq_ofGaussianInt :
   funext b
   decide +revert +kernel
 
-set_option backward.isDefEq.respectTransparency false in
 /-- Gaussian integer components of `σ^^^` after dualizing its Lorentz index. -/
 lemma toTensor_dualLorentz_eq_ofGaussianInt :
     {σ^^^ | τ(μ) α β}ᵀ =
@@ -254,7 +250,6 @@ lemma toTensor_dualLorentz_eq_ofGaussianInt :
   funext b
   decide +revert +kernel
 
-set_option backward.isDefEq.respectTransparency false in
 /-- Gaussian integer components of `σ^^^` after dualizing its Lorentz and left-handed Weyl
 indices. -/
 lemma toTensor_dualLorentzLeft_eq_ofGaussianInt :
@@ -276,7 +271,6 @@ lemma toTensor_dualLorentzLeft_eq_ofGaussianInt :
   refine congrArg ofGaussianInt (funext fun b => ?_)
   decide +revert +kernel
 
-set_option backward.isDefEq.respectTransparency false in
 /-- Gaussian integer components of `σ^^^` after dualizing all three indices. -/
 lemma toTensor_dualAll_eq_ofGaussianInt :
     {σ^^^ | τ(μ) τ(α) τ(β)}ᵀ =
@@ -295,13 +289,11 @@ lemma toTensor_dualAll_eq_ofGaussianInt :
   funext b
   decide +revert +kernel
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 lemma smul_eq_self (Λ : SL(2,ℂ)) : Λ • pauliMatrix = pauliMatrix := by
   rw [smul_eq, toTensor_eq_asConsTensor, actionT_fromConstTriple, ← toTensor_eq_asConsTensor]
   simp
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 lemma toTensor_smul_eq_self (Λ : SL(2,ℂ)) : Λ • σ^^^ = σ^^^ := by
   rw [toTensor_eq_asConsTensor]
@@ -340,7 +332,6 @@ scoped[PauliMatrix] notation "σ^__" => PauliMatrix.pauliContrDown
 -/
 open Lorentz
 
-set_option backward.isDefEq.respectTransparency false in
 lemma pauliCo_eq_ofGaussianInt : pauliCo = ofGaussianInt (fun b =>
     pauliContrDownComponent (b 0) (b 1) (b 2)) := by
   apply (Tensor.basis _).repr.injective
@@ -361,7 +352,6 @@ lemma pauliCo_eq_ofGaussianInt : pauliCo = ofGaussianInt (fun b =>
   revert b
   decide +kernel
 
-set_option backward.isDefEq.respectTransparency false in
 lemma pauliCoDown_eq_ofGaussianInt : pauliCoDown = ofGaussianInt (fun b =>
     pauliContrComponent (b 0) (b 1) (b 2)) := by
   apply (Tensor.basis _).repr.injective
@@ -394,7 +384,6 @@ lemma pauliCoDown_eq_ofGaussianInt : pauliCoDown = ofGaussianInt (fun b =>
   revert b
   decide +kernel
 
-set_option backward.isDefEq.respectTransparency false in
 lemma pauliContrDown_ofGaussianInt : pauliContrDown = ofGaussianInt (fun b =>
     pauliContrDownComponent (b 0) (b 1) (b 2)) := by
   apply (Tensor.basis _).repr.injective
@@ -447,7 +436,6 @@ lemma toTensor_dualAll_eq_pauliCoDown :
   rw [pauliCoDown_eq_ofGaussianInt, permT_ofGaussianInt]
   congr
 
-set_option backward.isDefEq.respectTransparency false in
 /-- Lowering the Lorentz index of `σ^^^` with `τ` gives `σ_^^`. -/
 lemma pauliDual_eq_pauliCo :
     ({σ^^^ | τ(μ) α β = σ_^^ | μ α β}ᵀ : Prop) := by
@@ -499,21 +487,18 @@ lemma pauliContrDownDual_eq_pauliCoDown :
 
 -/
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The tensor `pauliCo` is invariant under the action of `SL(2,ℂ)`. -/
 lemma smul_pauliCo (g : SL(2,ℂ)) : g • pauliCo = pauliCo := by
   rw [← permT_equivariant, ← contrT_equivariant, ← prodT_equivariant]
   rw [toTensor_smul_eq_self, actionT_coMetric]
 
-set_option backward.isDefEq.respectTransparency false in
 set_option maxRecDepth 2000 in
 /-- The tensor `pauliCoDown` is invariant under the action of `SL(2,ℂ)`. -/
 lemma smul_pauliCoDown (g : SL(2,ℂ)) : g • pauliCoDown = pauliCoDown := by
   rw [← permT_equivariant, ← contrT_equivariant, ← prodT_equivariant,
     ← contrT_equivariant, ← prodT_equivariant]
   rw [smul_pauliCo, actionT_dualLeftMetric, actionT_dualRightMetric]
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The tensor `pauliContrDown` is invariant under the action of `SL(2,ℂ)`. -/
 lemma smul_pauliContrDown (g : SL(2,ℂ)) : g • pauliContrDown = pauliContrDown := by
   rw [← permT_equivariant, ← contrT_equivariant, ← prodT_equivariant,

Physlib/Relativity/Special/TwinParadox/Basic.lean

@@ -137,7 +137,6 @@ lemma ageGap_nonneg : 0 ≤ T.ageGap := by
 
 -/
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The twin paradox in which:
 - Twin A starts at `0` and travels at constant
   speed to `[15, 0, 0, 0]`.
@@ -179,12 +178,10 @@ def example1 : InstantaneousTwinParadox where
     simp [Fin.sum_univ_three]
     norm_num
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 lemma example1_properTimeTwinA : example1.properTimeTwinA = 15 := by
   simp [properTimeTwinA, example1, properTime, minkowskiProduct_toCoord]
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 lemma example1_properTimeTwinB : example1.properTimeTwinB = 9 := by
   simp [properTimeTwinB, properTime, example1, minkowskiProduct_toCoord, Fin.sum_univ_three]

Physlib/SpaceAndTime/SpaceTime/Basic.lean

@@ -313,13 +313,11 @@ lemma toTimeAndSpace_symm_apply_time_space {d : ℕ} {c : SpeedOfLight} (x : Spa
     (toTimeAndSpace c).symm (x.time c, x.space) = x :=
   (toTimeAndSpace c).left_inv x
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 lemma space_toTimeAndSpace_symm {d : ℕ} {c : SpeedOfLight} (t : Time) (s : Space d) :
     ((toTimeAndSpace c).symm (t, s)).space = s := by
   simp [space, toTimeAndSpace]
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 lemma time_toTimeAndSpace_symm {d : ℕ} {c : SpeedOfLight} (t : Time) (s : Space d) :
     ((toTimeAndSpace c).symm (t, s)).time c = t := by
@@ -375,7 +373,6 @@ lemma toTimeAndSpace_basis_inr {d : ℕ} {c : SpeedOfLight} (i : Fin d) :
 
 -/
 
-set_option backward.isDefEq.respectTransparency false in
 lemma toTimeAndSpace_basis_inl {d : ℕ} {c : SpeedOfLight} :
     toTimeAndSpace (d := d) c (Lorentz.Vector.basis (Sum.inl 0)) = (⟨1/c.val⟩, 0) := by
   refine Prod.ext ?_ ?_
@@ -428,7 +425,6 @@ lemma timeSpaceBasis_apply_inr {d : ℕ} (c : SpeedOfLight) (i : Fin d) :
 
 -/
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The equivalence on of `SpaceTime` taking `(1, 0, 0, ...)` to
 of `(c, 0, 0, ....)` and keeping all other components the same. -/
 def timeSpaceBasisEquiv {d : ℕ} (c : SpeedOfLight) :
@@ -499,7 +495,6 @@ def timeSpaceBasisEquiv {d : ℕ} (c : SpeedOfLight) :
 
 -/
 
-set_option backward.isDefEq.respectTransparency false in
 lemma det_timeSpaceBasisEquiv {d : ℕ} (c : SpeedOfLight) :
     (timeSpaceBasisEquiv (d := d) c).det = c.val := by
   rw [@LinearEquiv.coe_det]
@@ -519,7 +514,6 @@ lemma det_timeSpaceBasisEquiv {d : ℕ} (c : SpeedOfLight) :
 
 -/
 
-set_option backward.isDefEq.respectTransparency false in
 lemma timeSpaceBasis_eq_map_basis {d : ℕ} (c : SpeedOfLight) :
     timeSpaceBasis (d := d) c =
     Module.Basis.map (Lorentz.Vector.basis (d := d)) (timeSpaceBasisEquiv c).toLinearEquiv := by

QuantumInfo/Entropy/VonNeumann.lean

@@ -109,7 +109,6 @@ theorem Sᵥₙ_of_pure_zero (ψ : Ket d) : Sᵥₙ (MState.pure ψ) = 0 := by
   obtain ⟨i, hi⟩ := MState.spectrum_pure_eq_constant ψ
   rw [Sᵥₙ, hi, Hₛ_constant_eq_zero]
 
-set_option backward.isDefEq.respectTransparency false in
 theorem Sᵥₙ_eq_neg_trace_log (ρ : MState d) : Sᵥₙ ρ = -⟪ρ.M.log, ρ.M⟫ := by
   open HermitianMat in
   rw [log, inner_eq_re_trace]

scripts/dag_traversal.py

@@ -46,6 +46,15 @@
 SHOW_CURSOR = "\033[?25h"
 
 
+
+def _kill_tree(proc: subprocess.Popen) -> None:
+    """Kill a build and all its children (`os.killpg` does not exist on Windows)."""
+    if hasattr(os, "killpg"):
+        os.killpg(proc.pid, signal.SIGKILL)
+    else:
+        subprocess.run(["taskkill", "/F", "/T", "/PID", str(proc.pid)],
+                       capture_output=True)
+
 class ShutdownError(Exception):
     """Raised when a shutdown has been requested (e.g. Ctrl-C)."""
 
@@ -98,7 +107,7 @@ def _kill_builds(self):
         with self._active_builds_lock:
             for proc in self._active_builds:
                 try:
-                    os.killpg(proc.pid, signal.SIGKILL)
+                    _kill_tree(proc)
                 except (ProcessLookupError, PermissionError):
                     try:
                         proc.kill()
@@ -160,7 +169,7 @@ def lake_build(
                 self._active_builds.discard(proc)
             if proc.poll() is None:
                 try:
-                    os.killpg(proc.pid, signal.SIGKILL)
+                    _kill_tree(proc)
                 except (ProcessLookupError, PermissionError):
                     proc.kill()
                 proc.wait()

scripts/rm_set_option.py

@@ -29,6 +29,7 @@
         DEFAULT_OPTIONS,
         PROJECT_DIR,
         commented_pattern,
+        is_annotated,
         lake_build_with_progress,
         lakefile_pattern,
         removable_pattern,
@@ -198,6 +199,8 @@ def scan_files(dag: DAG, options: list[str], value: str = "false") -> dict[str,
         for i, line in enumerate(lines):
             if any(p.match(line) for p in commented_pats):
                 continue
+            if is_annotated(lines, i):
+                continue
             if any(p.match(line) for p in removable_pats):
                 removable.append(i)
         if removable:
@@ -206,12 +209,16 @@ def scan_files(dag: DAG, options: list[str], value: str = "false") -> dict[str,
 
 
 def count_skipped(filepath: Path, options: list[str], value: str = "false") -> int:
-    """Count set_option lines with trailing comments."""
+    """Count set_option lines with trailing/preceding comments."""
     commented_pats = [commented_pattern(opt, value) for opt in options]
+    removable_pats = [removable_pattern(opt, value) for opt in options]
+    lines = filepath.read_text().splitlines()
     count = 0
-    for line in filepath.read_text().splitlines():
+    for i, line in enumerate(lines):
         if any(p.match(line) for p in commented_pats):
             count += 1
+        elif any(p.match(line) for p in removable_pats) and is_annotated(lines, i):
+            count += 1
     return count
 
 

scripts/set_option_utils.py

@@ -9,6 +9,7 @@
 
 DEFAULT_OPTIONS = [
     "backward.isDefEq.respectTransparency",
+    "backward.isDefEq.respectTransparency.types",
     "backward.whnf.reducibleClassField",
     "backward.inferInstanceAs.wrap",
 ]
@@ -33,6 +34,20 @@ def commented_pattern(option: str, value: str = "false") -> re.Pattern:
     return re.compile(rf"^\s*set_option {escaped} {escaped_val} in\s+--")
 
 
+def is_annotated(lines: list[str], idx: int) -> bool:
+    """Check whether line `idx` is immediately preceded by a `--` comment
+    or by a (possibly multi-line) `/-- ... -/` doc comment or `/- ... -/` block comment.
+    """
+    if idx == 0:
+        return False
+    prev = lines[idx - 1]
+    if re.search(r"^\s*--", prev):
+        return True
+    if re.search(r"-/\s*$", prev):
+        return True
+    return False
+
+
 def lakefile_pattern(option: str, value: str = "false") -> re.Pattern:
     """Match lakefile entries for an option."""
     escaped = re.escape(option)