leanprover-community
diff --git a/‎scripts/README.md‎
Lines changed: 40 additions & 0 deletions b/‎scripts/README.md‎
Lines changed: 40 additions & 0 deletions
diff --git a/‎scripts/add_module_set_option.py‎
Lines changed: 236 additions & 0 deletions b/‎scripts/add_module_set_option.py‎
Lines changed: 236 additions & 0 deletions
@@ -106,6 +106,21 @@ file used by the library's own linters.
 These scripts help with testing Lean PRs that change backward-compatibility option
 behaviour. They share a common DAG traversal library that parallelises work in import-graph order.
 
+***Using these scripts in a downstream project.***  Each script depends on sibling
+files in the same directory.  Minimally:
+
+1. Copy the script you want plus `dag_traversal.py` and `set_option_utils.py` into
+   a `scripts/` directory in your project.  `fix_nonlocal_set_option.py` additionally
+   requires `add_module_set_option.py` and `rm_module_set_option.py`.
+2. From the project root, run e.g. `python3 scripts/rm_set_option.py --dry-run --option <name>`.
+3. If you see "warning: no .lean files found", pass `--directories <your-source-dir>`
+   (e.g. `--directories FLT`).
+4. If you have a `lakefile.toml` and have configured the option in `leanOptions`,
+   remove the entry manually — these scripts only edit `lakefile.lean`.
+
+Module-name derivation assumes a Mathlib-style layout where `Foo/Bar.lean` corresponds
+to module `Foo.Bar` (no `srcDir` indirection).
+
 - `dag_traversal.py`
   Reusable parallel DAG traversal for Lean import graphs. Parses the import DAG from `.lean`
   source files and parallelises an action over a forward or backward traversal. Each module is
@@ -146,6 +161,31 @@ behaviour. They share a common DAG traversal library that parallelises work in i
   falls back to one-at-a-time removal.
   Usage: `python3 scripts/rm_set_option.py [--option NAME] [--dry-run] [--max-workers N] [--files FILE ...] [--resume]`
 
+- `add_module_set_option.py`, `rm_module_set_option.py`
+  File-level variants of `add_set_option.py` / `rm_set_option.py`: they insert or remove a
+  `set_option ...` at the top of the file rather than scoped to individual declarations.
+  Both accept `--directories <root>` for downstream projects whose source files aren't
+  directly under the project root.
+
+- `fix_nonlocal_set_option.py`
+  Helper that bisects the import DAG to find the upstream file whose missing
+  `set_option ...` is causing a downstream failure — useful when the direct fix is in a
+  different module than the one reporting the error.  Accepts `--directories <root>` for
+  downstream projects.
+
+- `fix_unused_simp_args.py`
+  Parses `lake build` warnings of the form `This simp argument is unused: X` and removes `X`
+  from the corresponding `simp`/`simp only` call. For `← X` arguments it rewrites to `- X`
+  instead, because the `←` form has side effects on the simp set even when the rewrite itself
+  is unused.
+  Usage: `lake build 2>&1 | scripts/fix_unused_simp_args.py`
+
+- `fix_long_lines.py`
+  Breaks a too-long line at the last comma before column 100 and indents the continuation.
+  Takes `path:line` pairs as arguments; intended as a follow-up to scripts that rewrite simp
+  lists (which occasionally leave lines over the 100-char limit).
+  Usage: `scripts/fix_long_lines.py path:line ...`
+
 **CI workflow**
 - `lake-build-with-retry.sh`
   Runs `lake build` on a target until `lake build --no-build` succeeds. Used in the main build workflows.
 
@@ -0,0 +1,236 @@
+#!/usr/bin/env python3
+"""
+Add module-level `set_option` lines to every Lean file in the project.
+
+Inserts `set_option <option> false` (module-scoped, no `in`) after the last
+import line in each .lean file in the project.  Also removes the corresponding
+entry from lakefile.lean if present.
+
+To use outside mathlib, copy `add_module_set_option.py`, `dag_traversal.py` and
+`set_option_utils.py` to a subdirectory of your project named `scripts/` and
+then run from the project root with `scripts/add_module_set_option.py`.  Pass
+`--directories <root>` if your source files aren't directly under the project
+root.
+
+Usage:
+    python3 scripts/add_module_set_option.py [--option NAME] [--dry-run]
+"""
+
+import argparse
+import re
+import sys
+from pathlib import Path
+
+try:
+    from set_option_utils import PROJECT_DIR, lakefile_pattern
+    from dag_traversal import DAG
+except ImportError as _e:
+    raise SystemExit(
+        f"error: {_e}\n\n"
+        f"  This script depends on sibling Python files in {Path(__file__).parent}:\n"
+        "    - dag_traversal.py\n"
+        "    - set_option_utils.py\n"
+        "  These are mathlib scripts, not pip packages.  Copy them into your\n"
+        "  `scripts/` directory alongside this script."
+    )
+
+DEFAULT_OPTION = "backward.defeq.atInstanceTransparency"
+
+
+def find_insert_point(lines: list[str]) -> int:
+    """Find the line index after imports and module docstring.
+
+    Inserts after the module docstring (/-! ... -/) if present right after
+    imports, otherwise after the last import. The linter requires the module
+    docstring to be the first command after imports, so set_option must come
+    after it.
+
+    Falls back to after `module` if no imports, or line 0.
+    """
+    import_re = re.compile(r"^(?:public\s+)?(?:meta\s+)?import\s")
+    last_import = -1
+    module_line = -1
+    in_block_comment = False
+    for i, line in enumerate(lines):
+        stripped = line.strip()
+        # Track block comments
+        if in_block_comment:
+            if "-/" in stripped:
+                in_block_comment = False
+            continue
+        if stripped.startswith("/-"):
+            if "-/" not in stripped[2:]:
+                in_block_comment = True
+            continue
+        # Track module line
+        if stripped == "module" or stripped.startswith("module ") or stripped.startswith("module\t"):
+            module_line = i
+            continue
+        # Skip blank lines and line comments
+        if stripped == "" or stripped.startswith("--"):
+            continue
+        # Check for import
+        if import_re.match(stripped):
+            last_import = i
+            continue
+        # Any other content after we've seen imports means header is done
+        if last_import >= 0:
+            break
+    if last_import < 0:
+        if module_line >= 0:
+            return module_line + 1
+        return 0
+    # We have the last import at last_import. Now look for a module docstring
+    # (/-! ... -/) immediately following (possibly separated by blank lines).
+    idx = last_import + 1
+    # Skip blank lines
+    while idx < len(lines) and lines[idx].strip() == "":
+        idx += 1
+    # Check for module docstring
+    if idx < len(lines) and lines[idx].strip().startswith("/-!"):
+        # Find the end of this block comment
+        if "-/" in lines[idx].strip()[3:]:
+            # Single-line module docstring
+            return idx + 1
+        # Multi-line: scan for closing -/
+        idx += 1
+        while idx < len(lines):
+            if "-/" in lines[idx]:
+                return idx + 1
+            idx += 1
+    # No module docstring, insert after imports
+    return last_import + 1
+
+
+def add_to_file(filepath: Path, option: str, value: str, dry_run: bool) -> bool:
+    """Add module-level set_option to a file. Returns True if modified."""
+    text = filepath.read_text()
+    line = f"set_option {option} {value}"
+
+    # Skip if already present as a module-level option (not `set_option ... in`)
+    if re.search(rf"^{re.escape(line)}$", text, re.MULTILINE):
+        return False
+
+    lines = text.splitlines(keepends=True)
+    idx = find_insert_point(lines)
+
+    # Insert a blank line + the set_option + blank line
+    insert = f"\n{line}\n"
+    # If there's already a blank line after imports, don't double-blank
+    if idx < len(lines) and lines[idx].strip() == "":
+        insert = f"{line}\n"
+
+    new_lines = lines[:idx] + [insert] + lines[idx:]
+
+    if not dry_run:
+        filepath.write_text("".join(new_lines))
+    return True
+
+
+def main():
+    parser = argparse.ArgumentParser(
+        description="Add module-level set_option to every Lean file in the project."
+    )
+    parser.add_argument(
+        "--option",
+        default=DEFAULT_OPTION,
+        help=f"Option name (default: {DEFAULT_OPTION})",
+    )
+    parser.add_argument(
+        "--value",
+        default="false",
+        help="Value of the option (default: false)",
+    )
+    parser.add_argument(
+        "--dry-run",
+        action="store_true",
+        help="Report without modifying files",
+    )
+    parser.add_argument(
+        "--directories",
+        nargs="+",
+        default=None,
+        help="Directories to scan for .lean files (default: '.')",
+    )
+    parser.add_argument(
+        "--deps-of",
+        nargs="*",
+        metavar="MODULE",
+        help="Only add to transitive dependencies of these modules "
+             "(module names like Mathlib.Foo.Bar)",
+    )
+    parser.add_argument(
+        "--no-lakefile",
+        action="store_true",
+        help="Skip removing the option from lakefile.lean",
+    )
+    args = parser.parse_args()
+
+    option = args.option
+
+    # Step 1: remove from lakefile
+    if not args.no_lakefile:
+        lakefile = PROJECT_DIR / "lakefile.lean"
+        if lakefile.exists():
+            content = lakefile.read_text()
+            pat = lakefile_pattern(option, args.value)
+            new_content = pat.sub("", content)
+            if new_content != content:
+                if not args.dry_run:
+                    lakefile.write_text(new_content)
+                print(f"Removed {option} from lakefile.lean")
+        elif (PROJECT_DIR / "lakefile.toml").exists():
+            print(
+                f"Note: lakefile.toml detected.  If {option} is set in `leanOptions`\n"
+                "  there, you'll need to remove the entry manually — this script only\n"
+                "  edits lakefile.lean."
+            )
+
+    # Step 2: determine which files to process via the import DAG
+    dag = DAG.from_directories(PROJECT_DIR, args.directories)
+
+    if args.deps_of:
+        deps_set: set[str] = set()
+        for mod in args.deps_of:
+            # Collect transitive dependencies
+            frontier = {mod}
+            visited: set[str] = set()
+            while frontier:
+                next_frontier: set[str] = set()
+                for m in frontier:
+                    info = dag.modules.get(m)
+                    if info is None:
+                        continue
+                    for imp in info.imports:
+                        if imp not in visited and imp != mod:
+                            visited.add(imp)
+                            next_frontier.add(imp)
+                frontier = next_frontier
+            deps_set |= visited
+        files = []
+        for name in sorted(deps_set):
+            info = dag.modules.get(name)
+            if info:
+                fp = dag.project_root / info.filepath
+                if fp.exists():
+                    files.append(fp)
+        print(f"  {len(files)} dependencies of {', '.join(args.deps_of)}")
+    else:
+        files = []
+        for name in sorted(dag.modules):
+            info = dag.modules[name]
+            fp = dag.project_root / info.filepath
+            if fp.exists():
+                files.append(fp)
+
+    modified = 0
+    for filepath in files:
+        if add_to_file(filepath, option, args.value, args.dry_run):
+            modified += 1
+
+    action = "Would modify" if args.dry_run else "Modified"
+    print(f"{action} {modified}/{len(files)} files")
+
+
+if __name__ == "__main__":
+    main()