diff --git a/CHANGELOG.md b/CHANGELOG.md index 47d174ca..77adf74a 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -65,6 +65,25 @@ uses [Semantic Versioning](https://semver.org/). `addModule`; `std`, `builtin`, and third-party packages are dropped. `test` blocks and `zig-cache/`, `.zig-cache/`, `zig-out/` are skipped, `build.zig` is also a build artifact, and `build.zig.zon` is a manifest. +- **Lean 4 analyzer** ([#154](https://github.com/FSoft-AI4Code/CodeWiki/issues/154)). + `def`, `theorem`/`lemma`, `abbrev`, `instance`, `structure`, `class`, + `inductive`, `axiom` and `opaque` declarations become components, keyed by + their fully qualified name (`Geo.Point.add`). A header scanner reads the + structure from the source with comments and strings masked: declarations, + the `namespace`/`section`/`mutual`/`end` stack, `open` (also `open X in`), + `import`, spans and `/-- -/` docstrings. So a region that the tree-sitter + grammar cannot parse does not hide a declaration. References come from the + tree-sitter identifiers, without binders, `let`/`have`/`fun`/`intro` names + and match patterns. A reference resolves only to an exact name in the + declaration's namespaces, the root or the open namespaces, in a file that + the caller imports (transitively); `private` names stay in their file, and + a reference with no match or more than one is dropped. Constructor and + field names (`Point.mk`, `Point.x`, `Shape.dot`) link to their structure or + inductive, and `origin.x` links to `origin`. `structure` is a `struct`, + `class` an `interface`, `inductive` a `class`, and the rest are functions. + `.lake/` and `lake-packages/` are skipped, `lakefile.lean` and + `lakefile.toml` are build artifacts, and `lake-manifest.json` and + `lean-toolchain` are manifests. - **Vue single-file components.** Each `.vue` file becomes a component (`ArticleList.vue::ArticleList`), and its options-API members (`methods`, `computed`, `watch`, lifecycle hooks such as `mounted` or `setup`) become @@ -93,6 +112,17 @@ uses [Semantic Versioning](https://semver.org/). `--update` keeps it, so existing flat docs stay flat. The GitHub Pages viewer, the web app and the MCP tools (`doc_path` in `processing_order.json`) follow the layout. +- **tree-sitter-language-pack 1.x.** The pin moves from `>=0.8.0,<0.9.0` to + `>=1.23.1,<2.0.0`, which brings grammars 0.8 does not ship (Lean, among + others). 1.x downloads a grammar on first use and caches it under + `tree_sitter_language_pack.cache_dir()`, so the first run of the Dart, Go, + JavaScript/TypeScript-in-Vue, Vue and Zig analyzers needs network access; + the Docker image fetches them at build time. Without network access and + without a cached grammar, the analysis stops before the first file with one + error that names the grammar, the cache folder and the `t.download([...])` + command, instead of a traceback per file. The 1.x Dart grammar parses + `Foo(x)` as a call instead of a relational expression, and the Dart + analyzer now takes the type-argument edges from that call too. ## [2.0.0] - 2026-09-18 diff --git a/README.md b/README.md index 594eeb31..bab8597e 100644 --- a/README.md +++ b/README.md @@ -120,8 +120,8 @@ Full list in the [CHANGELOG](./CHANGELOG.md). ## Features **Languages.** Python, Java, JavaScript, TypeScript, C, C++, C#, Kotlin, -PHP, Ruby, Scala, Rust, Dart (Flutter-aware), Go, Zig, Vue (single-file -components). +PHP, Ruby, Scala, Rust, Dart (Flutter-aware), Go, Zig, Lean 4, Vue +(single-file components). **Hierarchical decomposition.** The dependency graph is clustered into a module tree, recursively, so a 1.4M-line repository gets the same treatment diff --git a/codewiki/cli/utils/repo_validator.py b/codewiki/cli/utils/repo_validator.py index 3a56587a..ebd93f3f 100644 --- a/codewiki/cli/utils/repo_validator.py +++ b/codewiki/cli/utils/repo_validator.py @@ -37,6 +37,7 @@ ".dart", # Dart ".go", # Go ".zig", # Zig + ".lean", # Lean 4 ".vue", # Vue single-file components } diff --git a/codewiki/cli/utils/validation.py b/codewiki/cli/utils/validation.py index d5bddfd0..82f77b6b 100644 --- a/codewiki/cli/utils/validation.py +++ b/codewiki/cli/utils/validation.py @@ -171,6 +171,7 @@ def detect_supported_languages(directory: Path) -> list[tuple[str, int]]: "Dart": [".dart"], "Go": [".go"], "Zig": [".zig"], + "Lean": [".lean"], "Vue": [".vue"], } diff --git a/codewiki/mcp/tools/analysis.py b/codewiki/mcp/tools/analysis.py index 0d05040d..1a1e7859 100644 --- a/codewiki/mcp/tools/analysis.py +++ b/codewiki/mcp/tools/analysis.py @@ -232,6 +232,7 @@ def _detect_via_mtime( ".dart", ".go", ".zig", + ".lean", ".vue", } diff --git a/codewiki/src/be/dependency_analyzer/analysis/analysis_service.py b/codewiki/src/be/dependency_analyzer/analysis/analysis_service.py index 0be19e62..7b41b7fb 100644 --- a/codewiki/src/be/dependency_analyzer/analysis/analysis_service.py +++ b/codewiki/src/be/dependency_analyzer/analysis/analysis_service.py @@ -365,6 +365,7 @@ def _filter_supported_languages(self, code_files: list[dict]) -> list[dict]: "scala", "dart", "zig", + "lean", "vue", } @@ -392,6 +393,7 @@ def _get_supported_languages(self) -> list[str]: "dart", "go", "zig", + "lean", "vue", ] diff --git a/codewiki/src/be/dependency_analyzer/analysis/call_graph_analyzer.py b/codewiki/src/be/dependency_analyzer/analysis/call_graph_analyzer.py index c52d090f..213720da 100644 --- a/codewiki/src/be/dependency_analyzer/analysis/call_graph_analyzer.py +++ b/codewiki/src/be/dependency_analyzer/analysis/call_graph_analyzer.py @@ -22,11 +22,15 @@ is_external_symbol, is_macro_name, ) +from codewiki.src.be.dependency_analyzer.utils.grammars import ensure_pack_grammars from codewiki.src.be.dependency_analyzer.utils.patterns import CODE_EXTENSIONS from codewiki.src.be.dependency_analyzer.utils.security import safe_open_text logger = logging.getLogger(__name__) +# `_resolve_lean_name` result: no declaration has this name (try a shorter one). +_LEAN_NO_MATCH = object() + class TimeoutError(BaseException): """Raised when file parsing exceeds timeout. @@ -75,6 +79,7 @@ def __init__(self): self._dart_unscoped = False self._go_visible: dict[str, set[str]] = {} self._go_index = None + self._reset_lean_state() self.call_relationships: list[CallRelationship] = [] self._python_project_modules: set = set() self._python_external_import_roots: set = set() @@ -96,6 +101,9 @@ def analyze_code_files(self, code_files: list[dict], base_dir: str) -> dict: self.functions = {} self.call_relationships = [] code_files = self._route_contextual_headers(code_files, base_dir) + # Fail once, with a clear message, when a pack grammar cannot be + # downloaded, instead of once per file inside the per-file handlers. + ensure_pack_grammars(f["language"] for f in code_files) self._python_project_modules = self._collect_python_modules(code_files) self._python_external_import_roots = set() self._dart_directives = {} @@ -104,6 +112,7 @@ def analyze_code_files(self, code_files: list[dict], base_dir: str) -> dict: self._dart_unscoped = False self._go_visible = {} self._go_index = None + self._reset_lean_state() files_analyzed = 0 files_failed = 0 @@ -289,6 +298,8 @@ def _analyze_code_file(self, repo_dir: str, file_info: dict): self._analyze_go_file(file_path, content, repo_dir) elif language == "zig": self._analyze_zig_file(file_path, content, repo_dir) + elif language == "lean": + self._analyze_lean_file(file_path, content, repo_dir) elif language == "vue": self._analyze_vue_file(file_path, content, repo_dir) # else: @@ -664,6 +675,145 @@ def _analyze_vue_file(self, file_path: str, content: str, repo_dir: str): except Exception: logger.exception(f"Failed to analyze Vue file {file_path}") + def _reset_lean_state(self) -> None: + # Relative path -> imported module names, per Lean file. + self._lean_imports: dict[str, list[str]] = {} + # Node id -> (namespace prefixes innermost first, open namespaces). + self._lean_scopes: dict[str, tuple[list[str], list[str]]] = {} + # Constructor/field FQN -> ids of the structures or inductives it names. + self._lean_aliases: dict[str, list[str]] = defaultdict(list) + self._lean_private: set[str] = set() + self._lean_index: dict[str, list[str]] | None = None + self._lean_modules: dict[str, set[str]] = {} + self._lean_visible: dict[str, frozenset[str]] = {} + + def _analyze_lean_file(self, file_path: str, content: str, repo_dir: str): + """ + Analyze a Lean 4 file. + + Besides components and references, records the file's imports, each + declaration's namespaces and open namespaces, and the constructor and + field names of its structures, for Lean resolution by exact name. + + Args: + file_path: Path to the Lean file + content: File content string + repo_dir: Repository base directory + """ + from codewiki.src.be.dependency_analyzer.analyzers.lean import TreeSitterLeanAnalyzer + + try: + analyzer = TreeSitterLeanAnalyzer(str(file_path), content, repo_path=repo_dir) + + for func in analyzer.nodes: + self.functions[func.id] = func + + self.call_relationships.extend(analyzer.call_relationships) + self._lean_imports[analyzer.relative_path] = analyzer.imports + self._lean_scopes.update(analyzer.scopes) + for alias, node_id in analyzer.aliases.items(): + self._lean_aliases[alias].append(node_id) + self._lean_private.update(analyzer.private_ids) + except Exception: + logger.exception(f"Failed to analyze Lean file {file_path}") + + def _build_lean_index(self) -> dict[str, list[str]]: + """FQN -> Lean node ids, and module name -> files. A module name maps + to every file whose path ends with it (`Geo.Point` -> `src/Geo/Point.lean`), + because the Lake source folder is not known.""" + if self._lean_index is None: + index: dict[str, list[str]] = defaultdict(list) + for func_id, func in self.functions.items(): + if func.language == "lean" and func.qualified_name: + index[func.qualified_name].append(func_id) + for alias, node_ids in self._lean_aliases.items(): + for node_id in node_ids: + if node_id not in index[alias]: + index[alias].append(node_id) + modules: dict[str, set[str]] = defaultdict(set) + for rel in self._lean_imports: + parts = rel[: -len(".lean")].split("/") + for k in range(len(parts)): + modules[".".join(parts[k:])].add(rel) + self._lean_index = index + self._lean_modules = modules + return self._lean_index + + def _lean_visible_files(self, rel: str) -> frozenset[str]: + """The file itself and every repository file it imports, transitively.""" + if rel not in self._lean_visible: + self._build_lean_index() + seen = {rel} + queue = [rel] + while queue: + current = queue.pop() + for module in self._lean_imports.get(current, []): + for target in self._lean_modules.get(module, ()): + if target not in seen: + seen.add(target) + queue.append(target) + self._lean_visible[rel] = frozenset(seen) + return self._lean_visible[rel] + + def _resolve_lean_callee(self, callee: str, caller: Node) -> str | None: + """Resolve a Lean reference to one declaration by exact FQN, in Lean's + order: the caller's namespaces (innermost first), the root, then the + open namespaces. No match, or more than one, drops the reference. + + When the whole dotted name matches nothing, its longest prefix that + matches is the constant and the rest are projections, as in Lean + (`origin.x` is `origin` then the field `x`).""" + parts = callee.split(".") + for end in range(len(parts), 0, -1): + found = self._resolve_lean_name(".".join(parts[:end]), caller) + if found is not _LEAN_NO_MATCH: + return found + return None + + def _resolve_lean_name(self, callee: str, caller: Node): + """One exact name: a node id, None (ambiguous or recursion: stop), or + _LEAN_NO_MATCH (try a shorter prefix).""" + index = self._build_lean_index() + visible = self._lean_visible_files(caller.relative_path) + namespaces, opens = self._lean_scopes.get(caller.id, ([], [])) + + def qualify(prefix: str, name: str) -> str: + return f"{prefix}.{name}" if prefix else name + + def matches(fqn: str) -> list[str]: + return [ + node_id + for node_id in index.get(fqn, []) + if self.functions[node_id].relative_path in visible + and ( + node_id not in self._lean_private + or self.functions[node_id].relative_path == caller.relative_path + ) + ] + + def unique(found) -> str | None: + # A reference to the caller itself is recursion, not an edge. + found = list(found) + return found[0] if len(found) == 1 and found[0] != caller.id else None + + if callee.startswith("_root_."): + found = matches(callee[len("_root_.") :]) + return unique(found) if found else _LEAN_NO_MATCH + + prefixes = [*namespaces, ""] + for prefix in prefixes: + found = matches(qualify(prefix, callee)) + if found: + return unique(found) # the innermost match shadows the outer ones + + opened = { + node_id + for name in opens + for prefix in prefixes + for node_id in matches(qualify(qualify(prefix, name), callee)) + } + return unique(opened) if opened else _LEAN_NO_MATCH + def _analyze_go_file(self, file_path: str, content: str, repo_dir: str): """ Analyze Go file using tree-sitter based analyzer. @@ -856,11 +1006,11 @@ def _resolve_call_relationships(self): self.call_relationships.extend(link_go_interfaces(self.functions)) def _has_authoritative_resolution(self, relationship: CallRelationship) -> bool: - """A Dart or Go caller's callee that the language's scoped resolution + """A Dart, Go or Lean caller's callee that the language's scoped resolution rejected is external or invisible; drop it so ast_parser's name-only fallback cannot bind it to an unrelated component.""" caller = self.functions.get(relationship.caller) - return caller is not None and caller.language in ("dart", "go") + return caller is not None and caller.language in ("dart", "go", "lean") def _dotted_project_packages(self) -> dict[str, set]: """Project packages/namespaces, partitioned by language. Java and C# @@ -1003,6 +1153,9 @@ def _resolve_callee( if caller_language == "go" and caller is not None: # So is Go's: a name resolves only in the package it names. return self._resolve_go_callee(relationship.callee, caller) + if caller_language == "lean" and caller is not None: + # And Lean's: only an exact FQN in a visible file. + return self._resolve_lean_callee(relationship.callee, caller) if lang_indexes: match = self._resolve_callee_in( relationship, lang_indexes["exact"], lang_indexes["simple"] @@ -1148,6 +1301,8 @@ def _generate_visualization_data(self) -> dict: node_classes.append("lang-go") elif file_ext == ".zig": node_classes.append("lang-zig") + elif file_ext == ".lean": + node_classes.append("lang-lean") elif file_ext == ".vue": node_classes.append("lang-vue") diff --git a/codewiki/src/be/dependency_analyzer/analyzers/artifact.py b/codewiki/src/be/dependency_analyzer/analyzers/artifact.py index d7be67a9..e87d4d8b 100644 --- a/codewiki/src/be/dependency_analyzer/analyzers/artifact.py +++ b/codewiki/src/be/dependency_analyzer/analyzers/artifact.py @@ -244,6 +244,8 @@ def is_artifact_file_node(node: Any) -> bool: "build.sbt", "Package.swift", "build.zig.zon", + "lake-manifest.json", + "lean-toolchain", "pubspec.yaml", "Pipfile", "environment.yml", @@ -296,6 +298,8 @@ def is_artifact_file_node(node: Any) -> bool: "Gruntfile.js", "Herebyfile.mjs", "build.zig", + "lakefile.lean", + "lakefile.toml", # Autotools inputs; the generated configure, Makefile.in and aclocal.m4 # are not build sources. "configure.ac", @@ -451,6 +455,7 @@ def classify_artifact( ".scala", ".sc", ".zig", + ".lean", ".vue", }: if name in _TEST_INFRA_NAMES: diff --git a/codewiki/src/be/dependency_analyzer/analyzers/dart.py b/codewiki/src/be/dependency_analyzer/analyzers/dart.py index c773265d..6af1b0c9 100644 --- a/codewiki/src/be/dependency_analyzer/analyzers/dart.py +++ b/codewiki/src/be/dependency_analyzer/analyzers/dart.py @@ -36,7 +36,7 @@ from functools import lru_cache from pathlib import Path -from tree_sitter_language_pack import get_parser +from codewiki.src.be.dependency_analyzer.utils.grammars import get_pack_parser from codewiki.src.be.dependency_analyzer.analyzers.dart_flutter import ( COMPOSITION_METHOD_RE, @@ -212,7 +212,7 @@ def _local_declared_types(*roots) -> dict[str, str]: @lru_cache(maxsize=1) def _dart_parser(): - return get_parser("dart") + return get_pack_parser("dart") def _text(node) -> str: @@ -762,6 +762,17 @@ def _process_chain(self, target, head, selectors, local_types, lift_to): return caller, owner = target.caller, target.owner line = head.start_point[0] + 1 + # `Foo(x)` / `foo(x)`: the type arguments sit in the call's + # argument_part (grammars that misparse it as a relational expression + # are handled by _handle_generic_invocation). + for token_kind, _, token_node in tokens: + if token_kind != "call": + continue + type_args = _first_child(token_node, "type_arguments") + if type_args is not None: + for ref in _descendants(type_args): + if ref.type == "type_identifier": + self._add_type_edge(caller, _text(ref), line) name = _text(head) if head.type == "identifier" and name in self.import_prefixes and tokens[0][0] == "member": name, tokens = tokens[0][1] or "", tokens[1:] diff --git a/codewiki/src/be/dependency_analyzer/analyzers/go.py b/codewiki/src/be/dependency_analyzer/analyzers/go.py index 7a241812..8c0042fa 100644 --- a/codewiki/src/be/dependency_analyzer/analyzers/go.py +++ b/codewiki/src/be/dependency_analyzer/analyzers/go.py @@ -48,7 +48,7 @@ from functools import lru_cache from pathlib import Path -from tree_sitter_language_pack import get_parser +from codewiki.src.be.dependency_analyzer.utils.grammars import get_pack_parser from codewiki.src.be.dependency_analyzer.models.core import CallRelationship, Node from codewiki.src.be.dependency_analyzer.utils.file_selection import is_skipped_go_file @@ -326,7 +326,7 @@ def _default_import_names(import_path: str) -> set[str]: @lru_cache(maxsize=1) def _go_parser(): - return get_parser("go") + return get_pack_parser("go") class TreeSitterGoAnalyzer: diff --git a/codewiki/src/be/dependency_analyzer/analyzers/lean.py b/codewiki/src/be/dependency_analyzer/analyzers/lean.py new file mode 100644 index 00000000..0bbec7f1 --- /dev/null +++ b/codewiki/src/be/dependency_analyzer/analyzers/lean.py @@ -0,0 +1,703 @@ +"""Lean 4 analyzer: a header scanner for structure, tree-sitter for references. + +The tree-sitter Lean grammar (``lean`` in tree-sitter-language-pack) parses +most declarations, but it fails on many commands and notations (``#eval``, +``¬``, ``←``, ``do`` blocks, user notation), and it gives ``end`` as a flat +node, so the tree does not show namespace nesting. This analyzer therefore +uses two layers: + +1. **Structure, from a header scanner.** Comments and strings are masked, + and the Lean commands are read line by line: declarations (``def``, + ``theorem``/``lemma``, ``abbrev``, ``instance``, ``structure``, ``class``, + ``inductive``, ``axiom``, ``opaque``), the ``namespace``/``section``/ + ``mutual``/``end`` stack, ``open`` (also ``open X in``), ``import``, + ``/-- -/`` docstrings and spans. The scanner does not depend on the + parse tree, so an ``ERROR`` region does not hide a declaration. +2. **References, from tree-sitter.** Every ``identifier`` node in a + declaration's lines is a reference candidate, also inside ``ERROR`` + nodes. Text that an ``ERROR`` node does not cover with child nodes is + tokenized from the masked source. Local names (binders, ``let``, + ``have``, ``fun``, ``intro``, match patterns) are removed, and so is a + dotted name whose first part is local (``p.x``). + +Each declaration is keyed by its fully qualified name (FQN). Structures and +classes also answer to their constructor and field names (``Point.mk``, +``Point.x``), and inductives to their constructors (``Tree.node``). The +analyzer emits each reference as written. ``CallGraphAnalyzer`` resolves it +to an exact FQN only, in Lean's order: the namespaces of the declaration +(innermost first), the root namespace, then the open namespaces. Only the +file itself and the files it imports (transitively) are visible, and a +``private`` name is visible only in its own file. A reference that matches +no declaration, or more than one, is dropped. A bare name is never guessed. + +Known limitations: +- Generalized field notation (``v.norm`` for ``Vec.norm``) needs type + information, so it does not resolve. +- References made through user ``notation``/``macro`` are lost. +- The scanner assumes that each command starts a line, which is the usual + Lean style. A declaration ends at the next command at the same or a + smaller indentation. +- An anonymous ``instance`` gets the synthetic name ``instance_L``, + not the name that Lean generates. ``example`` makes no component. +- Local names are removed by name for the whole declaration, so a global + with the same simple name as a local of that declaration is not linked. +""" + +import bisect +import logging +import os +import re +from dataclasses import dataclass, field +from functools import lru_cache +from pathlib import Path + +from codewiki.src.be.dependency_analyzer.models.core import CallRelationship, Node +from codewiki.src.be.dependency_analyzer.utils.file_selection import is_skipped_lean_file +from codewiki.src.be.dependency_analyzer.utils.grammars import get_pack_parser + +logger = logging.getLogger(__name__) + +# `component_type` per declaration keyword; `node_type` keeps the keyword. +COMPONENT_TYPES = { + "structure": "struct", + "class": "interface", + "inductive": "class", + "class inductive": "class", +} + +_IDENT_PART = r"(?:«[^»\n]*»|[^\W\d][\w'!?₀-₉ₐ-ₜ]*)" +IDENT = rf"{_IDENT_PART}(?:\.(?:{_IDENT_PART}|\d+))*" +_IDENT_RE = re.compile(IDENT) + +_MODIFIERS = r"(?:private|protected|noncomputable|partial|unsafe|nonrec|scoped|local|public|meta)" +_ATTRS = r"(?:@\[[^\]\n]*\]\s*)*" +_DECL_RE = re.compile( + rf"^(?P\s*){_ATTRS}(?P(?:{_MODIFIERS}\s+)*)" + r"(?Pclass\s+inductive|def|theorem|lemma|abbrev|instance|structure|class|inductive" + r"|axiom|opaque|example)\b(?P.*)$" +) +_ATTR_ONLY_RE = re.compile(r"^\s*@\[[^\]\n]*\]\s*$") +_IMPORT_RE = re.compile(r"^\s*(?:(?:public|meta|private)\s+)*import\s+(?P.+)$") +_NAMESPACE_RE = re.compile(rf"^\s*namespace\s+(?P{IDENT})") +_SECTION_RE = re.compile(rf"^\s*(?:noncomputable\s+)?section\b\s*(?P{IDENT})?") +_MUTUAL_RE = re.compile(r"^\s*mutual\b") +_END_RE = re.compile(rf"^\s*end\b\s*(?P{IDENT})?\s*$") +_OPEN_RE = re.compile(r"^\s*(?:(?:public|scoped|local)\s+)*(?:open|export)\s+(?P.*)$") +# Commands that end the span of the declaration before them. +_COMMAND_RE = re.compile( + r"^\s*(?:@\[|#|(?:" + r"import|namespace|section|end|open|export|mutual|attribute|variable|universe|set_option" + r"|notation|infix|infixl|infixr|prefix|postfix|macro|macro_rules|syntax|elab|elab_rules" + r"|deriving|initialize|builtin_initialize|declare_syntax_cat|add_decl_doc|omit|include" + r"|run_cmd" + r")\b)" +) +_NAME_AFTER_KIND_RE = re.compile(rf"^\s*(?P{IDENT})") +_INSTANCE_NAME_RE = re.compile(rf"^\s*(?:\(\s*priority\s*:=[^)]*\)\s*)?(?P{IDENT})?\s*") +_EXTENDS_RE = re.compile(r"\bextends\s+(?P[^:=]*?)(?:\bwhere\b|:=|:|$)") +_STRUCT_CTOR_RE = re.compile(rf"^\s*(?P{IDENT})\s*::\s*$") +_FIELD_RE = re.compile(rf"^\s*\(?\s*(?P{IDENT}(?:\s+{IDENT})*)\s*(?::(?!=)|:=)") + +# Local names introduced in a declaration's text. Tree rules cover the parsed +# parts; these also cover `ERROR` regions and tactic blocks. +_LOCAL_RES = [ + re.compile(r"\bfun\s+(?P[^=]*?)=>"), + re.compile(r"(?:∀|∃|∃!|Σ|Π|λ)\s*(?P[^,]*?),"), + re.compile(rf"\blet\s+(?:mut\s+|rec\s+)?(?P{IDENT})"), + re.compile(rf"\bhave\s+(?P{IDENT})\s*:"), + re.compile(rf"\bfor\s+(?P{IDENT})\s+in\b"), + re.compile(rf"[({{⦃\[]\s*(?P{IDENT}(?:\s+{IDENT})*)\s*:(?!=)"), + re.compile(rf"\(\s*(?P{IDENT})\s*:="), + re.compile( + r"\b(?:intro|intros|rintro|rename_i|next|case|obtain|rcases|cases'|induction')\s+(?P[^\n:=]*)" + ), + re.compile(rf"(?P{IDENT})\s*←"), +] + +_KEYWORDS = { + "fun", "let", "have", "show", "from", "by", "do", "then", "else", "if", "match", "with", + "at", "in", "for", "return", "where", "deriving", "mut", "rec", "Type", "Sort", "Prop", + "true", "false", "True", "False", "this", "_", "sorry", "calc", "suffices", "using", +} # fmt: skip + +_LOCAL_BINDER_PARENTS = {"binders"} +_BINDER_TYPES = { + "explicit_binder", + "implicit_binder", + "inst_binder", + "strict_implicit_binder", +} +_INTRO_TACTICS = {"intro", "intros", "rintro", "obtain", "rcases", "rename_i", "next", "case"} + + +@lru_cache(maxsize=1) +def _lean_parser(): + return get_pack_parser("lean") + + +# ---------------------------------------------------------------------- +# Masking +# ---------------------------------------------------------------------- + + +@dataclass +class _Masked: + text: str # same lines and the same UTF-8 byte offsets as the source + docstrings: list = field(default_factory=list) # (end line index, text) + + +_RAW_STRING_RE = re.compile(r'r(#*)"') +_MASK_START_RE = re.compile(r"--|/-|r#*\"|\"|'") +_BLOCK_TOKEN_RE = re.compile(r"/-|-/") +_NOT_NEWLINE_RE = re.compile(rb"[^\n]") +_CHAR_RE = re.compile(r"'(?:\\[^']*|[^\\'\n])'") + + +def _blank(text: str) -> str: + return _NOT_NEWLINE_RE.sub(b" ", text.encode("utf8")).decode("ascii") + + +def mask_source(source: str) -> _Masked: + """Blank comments, strings and char literals with spaces of the same + UTF-8 length, so lines and byte offsets do not move. Docstrings + (``/-- -/``) are kept aside with the line on which they end.""" + out: list[str] = [] + docstrings = [] + i, n = 0, len(source) + line, counted = 0, 0 # newlines before `counted`, so line numbers stay linear + + while i < n: + m = _MASK_START_RE.search(source, i) + if m is None: + out.append(source[i:]) + break + start, token = m.start(), m.group(0) + out.append(source[i:start]) + if token == "--": + j = source.find("\n", start) + j = n if j < 0 else j + elif token == "/-": + depth, j = 1, start + 2 + while depth: + b = _BLOCK_TOKEN_RE.search(source, j) + if b is None: + j = n + break + depth += 1 if b.group(0) == "/-" else -1 + j = b.end() + if source.startswith("/--", start): + line += source.count("\n", counted, j) + counted = j + docstrings.append((line, _clean_docstring(source[start:j]))) + elif token != '"' and _ident_before(source, start): + # `add_comm'` or `r"` after a name: not a literal. + out.append(source[start]) + i = start + 1 + continue + elif token == "'": + c = _CHAR_RE.match(source, start) + if c is None: + out.append(token) + i = start + 1 + continue + j = c.end() + else: + j = _string_end(source, start) + out.append(_blank(source[start:j])) + i = j + return _Masked("".join(out), docstrings) + + +def _ident_before(source: str, i: int) -> bool: + return i > 0 and (source[i - 1].isalnum() or source[i - 1] in "_'!?»") + + +def _string_end(source: str, i: int) -> int: + n = len(source) + if source[i] == "r": + hashes = len(_RAW_STRING_RE.match(source, i).group(1)) + close = '"' + "#" * hashes + j = source.find(close, i + 2 + hashes) + return n if j < 0 else j + len(close) + j = i + 1 + while j < n: + if source[j] == "\\": + j += 2 + elif source[j] == '"': + return j + 1 + else: + j += 1 + return n + + +def _clean_docstring(block: str) -> str: + body = block[3:-2] if block.endswith("-/") else block[3:] + return "\n".join(line.strip() for line in body.strip().splitlines()).strip() + + +# ---------------------------------------------------------------------- +# Header scanner +# ---------------------------------------------------------------------- + + +@dataclass +class LeanDecl: + fqn: str + kind: str + start: int # 0-based line of the first attribute or keyword line + keyword_line: int + end: int # 0-based, inclusive + indent: int + private: bool + namespaces: list[str] # the declaration's namespace prefixes, innermost first + opens: list[str] + docstring: str = "" + aliases: list[str] = field(default_factory=list) # constructor and field FQNs + bases: list[str] = field(default_factory=list) + + +@dataclass +class _Scope: + kind: str # "namespace", "section" or "mutual" + name: str + opens: list[str] = field(default_factory=list) + + +def _qualify(prefix: str, name: str) -> str: + return f"{prefix}.{name}" if prefix else name + + +def _strip_guillemets(name: str) -> str: + return name.replace("«", "").replace("»", "") + + +def _parse_open_names(body: str) -> list[str]: + """`open A B (x y) hiding z renaming p → q` -> ["A", "B"].""" + body = re.split(r"\b(?:hiding|renaming)\b", body)[0] + body = re.sub(r"\([^)]*\)", " ", body) + return [_strip_guillemets(m.group(0)) for m in _IDENT_RE.finditer(body)] + + +def scan_headers(masked: _Masked) -> tuple[list[LeanDecl], list[str]]: + """Return the declarations and the imported module names of a file.""" + lines = masked.text.split("\n") + docs = {end: text for end, text in masked.docstrings} + decls: list[LeanDecl] = [] + imports: list[str] = [] + stack: list[_Scope] = [] + file_opens: list[str] = [] + pending_open_in: list[str] = [] + attr_start: int | None = None + + def namespace() -> str: + return ".".join(s.name for s in stack if s.kind == "namespace") + + def active_opens() -> list[str]: + return file_opens + [o for s in stack for o in s.opens] + + def close_previous(line_idx: int, indent: int) -> None: + if decls and decls[-1].end < 0 and indent <= decls[-1].indent: + end = line_idx - 1 + while end > decls[-1].keyword_line and not lines[end].strip(): + end -= 1 + decls[-1].end = end + + for idx, line in enumerate(lines): + if not line.strip(): + continue + indent = len(line) - len(line.lstrip()) + if decls and decls[-1].end < 0 and indent > decls[-1].indent: + continue # a body line of the open declaration, even if it looks like a command + decl_m = _DECL_RE.match(line) + if decl_m is None and not _COMMAND_RE.match(line): + continue # a continuation line at the declaration's indentation + close_previous(idx, indent) + + if _ATTR_ONLY_RE.match(line): + if attr_start is None: + attr_start = idx + continue + start = attr_start if attr_start is not None else idx + attr_start = None + + if decl_m is not None: + decl = _decl_from_match(decl_m, idx, start, namespace(), pending_open_in) + pending_open_in = [] + if decl is None: + continue + decl.opens = active_opens() + decl.opens + decl.docstring = _docstring_before(docs, lines, start) + decls.append(decl) + continue + + # `open X in` covers only the next command, whatever it is. + pending_open_in = [] + if m := _IMPORT_RE.match(line): + imports.extend( + _strip_guillemets(x.group(0)) for x in _IDENT_RE.finditer(m.group("mods")) + ) + elif m := _NAMESPACE_RE.match(line): + stack.append(_Scope("namespace", _strip_guillemets(m.group("name")))) + elif _MUTUAL_RE.match(line): + stack.append(_Scope("mutual", "")) + elif m := _END_RE.match(line): + if stack: + stack.pop() + elif m := _SECTION_RE.match(line): + stack.append(_Scope("section", m.group("name") or "")) + elif m := _OPEN_RE.match(line): + body = m.group("body") + parts = re.split(r"\bin\b", body, maxsplit=1) + names = _parse_open_names(parts[0]) + if len(parts) == 2: + pending_open_in = names + rest = parts[1] + if rest.strip() and (inner := _DECL_RE.match(" " * indent + rest.strip())): + decl = _decl_from_match(inner, idx, start, namespace(), pending_open_in) + pending_open_in = [] + if decl is not None: + decl.opens = active_opens() + decl.opens + decl.docstring = _docstring_before(docs, lines, start) + decls.append(decl) + elif stack: + stack[-1].opens.extend(names) + else: + file_opens.extend(names) + + if decls and decls[-1].end < 0: + end = len(lines) - 1 + while end > decls[-1].keyword_line and not lines[end].strip(): + end -= 1 + decls[-1].end = end + for decl in decls: + if decl.kind in ("structure", "class", "inductive", "class inductive"): + decl.aliases = _member_aliases(decl, lines) + return decls, imports + + +def _decl_from_match(m, idx, start, ns, open_in) -> LeanDecl | None: + kind = re.sub(r"\s+", " ", m.group("kind")) + rest = m.group("rest") + if kind == "example": + name = None + elif kind == "instance": + nm = _INSTANCE_NAME_RE.match(rest) + name = nm.group("name") if nm else None + if name in _KEYWORDS: + name = None + if name is None: + name = f"instance_L{idx + 1}" + else: + nm = _NAME_AFTER_KIND_RE.match(rest) + name = nm.group("name") if nm else None + if not name: + # `example` and unnamed forms still end the previous declaration. + return None + name = _strip_guillemets(name) + if name.startswith("_root_."): + fqn = name[len("_root_.") :] + else: + fqn = _qualify(ns, name) + parts = fqn.split(".") + namespaces = [".".join(parts[:k]) for k in range(len(parts) - 1, 0, -1)] + bases = [] + if kind in ("structure", "class") and (em := _EXTENDS_RE.search(rest)): + bases = [_strip_guillemets(b.group(0)) for b in _IDENT_RE.finditer(em.group("bases"))] + return LeanDecl( + fqn=fqn, + kind=kind, + start=start, + keyword_line=idx, + end=-1, + indent=len(m.group("indent")), + private="private" in m.group("mods").split(), + namespaces=namespaces, + opens=list(open_in), + bases=bases, + ) + + +def _docstring_before(docs: dict, lines: list[str], start: int) -> str: + line = start - 1 + while line >= 0 and not lines[line].strip(): + if line in docs: + return docs[line] + line -= 1 + return docs.get(line, "") if line >= 0 else "" + + +def _member_aliases(decl: LeanDecl, lines: list[str]) -> list[str]: + aliases: list[str] = [] + body = lines[decl.keyword_line + 1 : decl.end + 1] + header = lines[decl.keyword_line] + if decl.kind in ("inductive", "class inductive"): + for line in [header.split(" where", 1)[-1], *body]: + for chunk in line.split("|")[1:]: + if m := _IDENT_RE.match(chunk.strip()): + aliases.append(_qualify(decl.fqn, _strip_guillemets(m.group(0)))) + return aliases + ctor = "mk" + if " where" in header or header.rstrip().endswith("where"): + for line in body: + if line.strip().startswith("deriving"): + break + if m := _STRUCT_CTOR_RE.match(line): + ctor = _strip_guillemets(m.group("name")) + elif m := _FIELD_RE.match(line): + for name in m.group("names").split(): + aliases.append(_qualify(decl.fqn, _strip_guillemets(name))) + aliases.append(_qualify(decl.fqn, ctor)) + return aliases + + +# ---------------------------------------------------------------------- +# References +# ---------------------------------------------------------------------- + + +def _node_text(node) -> str: + return node.text.decode("utf8", errors="replace") + + +def _collect_tree_names(root, masked_bytes: bytes): + """Return (references, locals): references as (line, name); locals as + (line, simple name).""" + refs: list[tuple[int, str]] = [] + locals_: list[tuple[int, str]] = [] + line_starts = [0] + [m.end() for m in re.finditer(rb"\n", masked_bytes)] + skip: set[int] = set() # ids of identifier nodes that are not references + + def mark_local(node) -> None: + for ident in _identifiers(node): + skip.add(ident.id) + text = _node_text(ident) + if "." not in text: + locals_.append((ident.start_point[0], text)) + + stack = [root] + while stack: + node = stack.pop() + t = node.type + children = node.children + if t in _LOCAL_BINDER_PARENTS: + for child in children: + if child.type == "identifier": + mark_local(child) + elif t in _BINDER_TYPES: + for child in children: + if child.type == ":": + break + if child.type == "identifier": + mark_local(child) + elif t in ("let", "have"): + for child in children[1:]: + if child.type == "identifier": + mark_local(child) + break + if child.type in (":=", ":", "←"): + break + elif t == "match_alt": + for child in children: + if child.type == "=>": + break + for ident in _identifiers(child): + if "." not in _node_text(ident): + mark_local(ident) + elif t in ("struct_field", "field"): + for child in children: + if child.type in (":=", ":"): + break + if child.type == "identifier": + skip.add(child.id) + elif t == "app" and children and children[0].type == "identifier": + if _node_text(children[0]) in _INTRO_TACTICS: + for child in children[1:]: + mark_local(child) + elif t == "ERROR": + covered = 0 + for child in children: + if child.start_byte > covered: + _tokens_in( + masked_bytes, + line_starts, + max(covered, node.start_byte), + child.start_byte, + refs, + ) + covered = max(covered, child.end_byte) + if covered < node.end_byte: + _tokens_in( + masked_bytes, line_starts, max(covered, node.start_byte), node.end_byte, refs + ) + if t == "identifier" and node.id not in skip: + refs.append((node.start_point[0], _node_text(node))) + stack.extend(reversed(children)) + return refs, locals_ + + +def _identifiers(node): + if node.type == "identifier": + yield node + return + for child in node.children: + yield from _identifiers(child) + + +def _tokens_in( + masked_bytes: bytes, line_starts: list[int], start: int, end: int, out: list +) -> None: + if end <= start: + return + chunk = masked_bytes[start:end].decode("utf8", errors="replace") + base_line = bisect.bisect_right(line_starts, start) - 1 + for m in _IDENT_RE.finditer(chunk): + out.append((base_line + chunk.count("\n", 0, m.start()), m.group(0))) + + +def _text_locals(text: str) -> set[str]: + names: set[str] = set() + for regex in _LOCAL_RES: + for m in regex.finditer(text): + for ident in _IDENT_RE.finditer(m.group("names")): + if "." not in ident.group(0): + names.add(ident.group(0)) + return names - _KEYWORDS + + +def normalize_reference(name: str) -> str | None: + """Strip `@`, guillemets and numeric projections; drop `.foo` and keywords.""" + name = name.lstrip("@") + if not name or name.startswith("."): + return None + parts = [p for p in _strip_guillemets(name).split(".") if p] + while parts and parts[-1].isdigit(): + parts.pop() + if not parts or parts[0] in _KEYWORDS: + return None + return ".".join(parts) + + +# ---------------------------------------------------------------------- +# Analyzer +# ---------------------------------------------------------------------- + + +class TreeSitterLeanAnalyzer: + def __init__(self, file_path: str, content: str, repo_path: str | None = None): + self.file_path = Path(file_path) + self.content = content + self.repo_path = repo_path or "" + self.nodes: list[Node] = [] + self.call_relationships: list[CallRelationship] = [] + self.imports: list[str] = [] + # node id -> (namespace prefixes innermost first, open namespaces) + self.scopes: dict[str, tuple[list[str], list[str]]] = {} + # constructor/field FQN -> node id of the structure or inductive + self.aliases: dict[str, str] = {} + self.private_ids: set[str] = set() + self.relative_path = Path(self._relative_path()).as_posix() + if is_skipped_lean_file(self.relative_path): + return + try: + self._analyze() + except Exception as e: # noqa: BLE001 — a broken file must not abort the sweep + logger.error(f"Error parsing Lean file {self.file_path}: {e}") + + def _relative_path(self) -> str: + if self.repo_path: + try: + return os.path.relpath(str(self.file_path), self.repo_path) + except ValueError: + return str(self.file_path) + return str(self.file_path) + + def _component_id(self, fqn: str) -> str: + return f"{self.relative_path}::{fqn}" + + def _analyze(self) -> None: + masked = mask_source(self.content) + decls, self.imports = scan_headers(masked) + source_lines = self.content.split("\n") + by_fqn: dict[str, Node] = {} + owners: list[tuple[LeanDecl, Node]] = [] + for decl in decls: + if decl.fqn in by_fqn: + continue + node = self._add_node(decl, source_lines) + by_fqn[decl.fqn] = node + owners.append((decl, node)) + for alias in decl.aliases: + self.aliases.setdefault(alias, node.id) + if not owners: + return + + tree = _lean_parser().parse(self.content.encode("utf8")) + masked_bytes = masked.text.encode("utf8") + refs, tree_locals = _collect_tree_names(tree.root_node, masked_bytes) + line_owner: dict[int, tuple[LeanDecl, Node]] = {} + for decl, node in owners: + for line in range(decl.keyword_line, decl.end + 1): + line_owner.setdefault(line, (decl, node)) + + locals_by_decl: dict[str, set[str]] = {} + masked_lines = masked.text.split("\n") + for decl, node in owners: + text = "\n".join(masked_lines[decl.keyword_line : decl.end + 1]) + locals_by_decl[node.id] = _text_locals(text) + for line, name in tree_locals: + if line in line_owner: + locals_by_decl[line_owner[line][1].id].add(name) + + seen: set[tuple[str, str]] = set() + for line, raw in refs: + owner = line_owner.get(line) + if owner is None: + continue + decl, node = owner + name = normalize_reference(raw) + if name is None or name.split(".")[0] in locals_by_decl[node.id]: + continue + if line == decl.keyword_line and name == decl.fqn.split(".")[-1]: + continue # the declaration's own name + key = (node.id, name) + if key in seen: + continue + seen.add(key) + self.call_relationships.append( + CallRelationship(caller=node.id, callee=name, call_line=line + 1) + ) + + def _add_node(self, decl: LeanDecl, source_lines: list[str]) -> Node: + component_id = self._component_id(decl.fqn) + component_type = COMPONENT_TYPES.get(decl.kind, "function") + node_type = "theorem" if decl.kind == "lemma" else decl.kind + node = Node( + id=component_id, + name=decl.fqn, + component_type=component_type, + file_path=str(self.file_path), + relative_path=self.relative_path, + source_code="\n".join(source_lines[decl.start : decl.end + 1]), + start_line=decl.start + 1, + end_line=decl.end + 1, + has_docstring=bool(decl.docstring), + docstring=decl.docstring, + node_type=node_type, + base_classes=decl.bases or None, + display_name=f"{node_type} {decl.fqn}", + component_id=component_id, + language="lean", + qualified_name=decl.fqn, + ) + self.nodes.append(node) + self.scopes[component_id] = (decl.namespaces, decl.opens) + if decl.private: + self.private_ids.add(component_id) + return node + + +def analyze_lean_file( + file_path: str, content: str, repo_path: str | None = None +) -> tuple[list[Node], list[CallRelationship]]: + analyzer = TreeSitterLeanAnalyzer(file_path, content, repo_path) + return analyzer.nodes, analyzer.call_relationships diff --git a/codewiki/src/be/dependency_analyzer/analyzers/vue.py b/codewiki/src/be/dependency_analyzer/analyzers/vue.py index 1a17f1ab..4934f72c 100644 --- a/codewiki/src/be/dependency_analyzer/analyzers/vue.py +++ b/codewiki/src/be/dependency_analyzer/analyzers/vue.py @@ -37,7 +37,7 @@ from functools import lru_cache from pathlib import Path -from tree_sitter_language_pack import get_parser +from codewiki.src.be.dependency_analyzer.utils.grammars import get_pack_parser from codewiki.src.be.dependency_analyzer.models.core import CallRelationship, Node @@ -107,7 +107,7 @@ @lru_cache(maxsize=None) def _parser(language: str): - return get_parser(language) + return get_pack_parser(language) def _is_sfc(target: str) -> bool: diff --git a/codewiki/src/be/dependency_analyzer/analyzers/zig.py b/codewiki/src/be/dependency_analyzer/analyzers/zig.py index cd5f1b7c..feb60e2e 100644 --- a/codewiki/src/be/dependency_analyzer/analyzers/zig.py +++ b/codewiki/src/be/dependency_analyzer/analyzers/zig.py @@ -47,7 +47,7 @@ from functools import lru_cache from pathlib import Path -from tree_sitter_language_pack import get_parser +from codewiki.src.be.dependency_analyzer.utils.grammars import get_pack_parser from codewiki.src.be.dependency_analyzer.models.core import CallRelationship, Node from codewiki.src.be.dependency_analyzer.utils.file_selection import is_skipped_zig_file @@ -107,7 +107,7 @@ def _build_zig_modules(repo_path: str) -> dict[str, str]: def _zig_parser(): - return get_parser("zig") + return get_pack_parser("zig") def _alias_chain(var_decl) -> tuple[tuple[str, str], tuple[str, ...]] | None: diff --git a/codewiki/src/be/dependency_analyzer/ast_parser.py b/codewiki/src/be/dependency_analyzer/ast_parser.py index e5f67c40..8e626112 100644 --- a/codewiki/src/be/dependency_analyzer/ast_parser.py +++ b/codewiki/src/be/dependency_analyzer/ast_parser.py @@ -230,6 +230,7 @@ def _file_to_module_path(self, file_path: str) -> str: ".dart", ".go", ".zig", + ".lean", ".vue", ] for ext in extensions: diff --git a/codewiki/src/be/dependency_analyzer/utils/file_selection.py b/codewiki/src/be/dependency_analyzer/utils/file_selection.py index 02fa5942..6793a970 100644 --- a/codewiki/src/be/dependency_analyzer/utils/file_selection.py +++ b/codewiki/src/be/dependency_analyzer/utils/file_selection.py @@ -5,6 +5,7 @@ PHP_TEMPLATE_PATTERNS = {".blade.php", ".phtml", ".twig.php"} PHP_TEMPLATE_DIRECTORIES = {"views", "templates", "resources/views"} ZIG_SKIPPED_DIRS = {"zig-cache", ".zig-cache", "zig-out"} +LEAN_SKIPPED_DIRS = {".lake", "lake-packages"} def is_skipped_go_file(relative_path: str) -> bool: @@ -17,6 +18,11 @@ def is_skipped_zig_file(relative_path: str) -> bool: return any(part in ZIG_SKIPPED_DIRS for part in Path(relative_path).parts[:-1]) +def is_skipped_lean_file(relative_path: str) -> bool: + """Lake's build folder and its package checkouts are not project code.""" + return any(part in LEAN_SKIPPED_DIRS for part in Path(relative_path).parts[:-1]) + + def is_php_template_file(file_path: str) -> bool: file_str = str(file_path) return any(file_str.endswith(pattern) for pattern in PHP_TEMPLATE_PATTERNS) or any( @@ -32,6 +38,8 @@ def is_skipped_source_file(file_info: dict, base_dir: str) -> bool: return is_skipped_go_file(file_info["path"]) if language == "zig": return is_skipped_zig_file(file_info["path"]) + if language == "lean": + return is_skipped_lean_file(file_info["path"]) if language == "php": return is_php_template_file(str(Path(base_dir) / file_info["path"])) return False diff --git a/codewiki/src/be/dependency_analyzer/utils/grammars.py b/codewiki/src/be/dependency_analyzer/utils/grammars.py new file mode 100644 index 00000000..bdbae313 --- /dev/null +++ b/codewiki/src/be/dependency_analyzer/utils/grammars.py @@ -0,0 +1,64 @@ +"""Parsers from ``tree-sitter-language-pack``. + +Pack 1.x does not ship its grammars in the wheel. It downloads each grammar +the first time it is loaded and caches it under ``cache_dir()``. Without +network access that first load fails with a ``DownloadError`` that names a +URL but not the cause or the fix. The per-file ``except`` blocks of the +analyzers would also swallow it, and the language would silently drop out of +the graph. So the analysis checks the grammars it needs once, before it +parses any file, and stops with one clear message. +""" + +from functools import lru_cache + +import tree_sitter_language_pack as tslp + +# Pack grammars each analyzed language loads. ``docker/Dockerfile`` downloads +# the same set at build time (``tests/test_pack_grammars.py`` checks this). +PACK_GRAMMARS_BY_LANGUAGE: dict[str, tuple[str, ...]] = { + "dart": ("dart",), + "go": ("go",), + "lean": ("lean",), + "vue": ("vue", "javascript", "typescript"), + "zig": ("zig",), +} + +PACK_GRAMMARS: tuple[str, ...] = tuple( + sorted({g for grammars in PACK_GRAMMARS_BY_LANGUAGE.values() for g in grammars}) +) + + +class GrammarUnavailableError(RuntimeError): + """A pack grammar is not cached and could not be downloaded.""" + + def __init__(self, grammar: str, cause: Exception): + try: + cache = tslp.cache_dir() + except Exception: # noqa: BLE001 — the path only improves the message + cache = "the tree-sitter-language-pack cache" + names = ", ".join(repr(g) for g in PACK_GRAMMARS) + super().__init__( + f"The tree-sitter grammar '{grammar}' is not in {cache} and could not be " + f"downloaded ({cause}). tree-sitter-language-pack downloads each grammar on " + "first use, so the first analysis of these files needs network access. " + "To prepare a machine without network access, run this once on a machine " + "with access and copy the cache folder: " + f'python -c "import tree_sitter_language_pack as t; t.download([{names}])"' + ) + self.grammar = grammar + + +@lru_cache(maxsize=None) +def get_pack_parser(grammar: str): + """Return the pack parser for ``grammar``, with a clear error when it is unavailable.""" + try: + return tslp.get_parser(grammar) + except tslp.DownloadError as e: + raise GrammarUnavailableError(grammar, e) from e + + +def ensure_pack_grammars(languages) -> None: + """Load every pack grammar that ``languages`` need, or raise ``GrammarUnavailableError``.""" + for language in sorted(set(languages)): + for grammar in PACK_GRAMMARS_BY_LANGUAGE.get(language, ()): + get_pack_parser(grammar) diff --git a/codewiki/src/be/dependency_analyzer/utils/patterns.py b/codewiki/src/be/dependency_analyzer/utils/patterns.py index 6692df36..84c4ffe2 100644 --- a/codewiki/src/be/dependency_analyzer/utils/patterns.py +++ b/codewiki/src/be/dependency_analyzer/utils/patterns.py @@ -70,6 +70,11 @@ "zig-cache/", "zig-out", "zig-out/", + # Lean: Lake build folder and package checkouts + ".lake", + ".lake/", + "lake-packages", + "lake-packages/", # IDEs and editors / Java ".project", # C/C++ @@ -184,6 +189,7 @@ "*.sc", "*.dart", "*.zig", + "*.lean", "*.vue", "*.clj", "*.hs", @@ -250,6 +256,9 @@ "Procfile", "go.mod", "build.zig.zon", + "lakefile.toml", + "lake-manifest.json", + "lean-toolchain", ".editorconfig", ".pre-commit-config.yaml", ".eslintrc*", @@ -321,6 +330,7 @@ ".dart": "dart", ".cs": "csharp", ".zig": "zig", + ".lean": "lean", ".vue": "vue", } @@ -556,6 +566,15 @@ "const {name} = enum", "const {name} = union", ], + "lean": [ + "def {name}", + "theorem {name}", + "lemma {name}", + "abbrev {name}", + "structure {name}", + "class {name}", + "inductive {name}", + ], "c": ["void {name}", "int {name}", "{name}("], "cpp": ["void {name}", "int {name}", "{name}("], "php": [ diff --git a/codewiki/src/be/prompt_template.py b/codewiki/src/be/prompt_template.py index db16a55d..f649cead 100644 --- a/codewiki/src/be/prompt_template.py +++ b/codewiki/src/be/prompt_template.py @@ -400,6 +400,7 @@ ".dart": "dart", ".go": "go", ".zig": "zig", + ".lean": "lean", ".vue": "vue", ".php": "php", ".phtml": "php", diff --git a/docker/Dockerfile b/docker/Dockerfile index d0a70d16..38fca3c2 100644 --- a/docker/Dockerfile +++ b/docker/Dockerfile @@ -18,6 +18,10 @@ COPY requirements.txt . # Install Python dependencies RUN pip install --no-cache-dir -r requirements.txt +# tree-sitter-language-pack 1.x downloads each grammar on first use. Fetch the +# ones the analyzers load at build time, so the image runs offline. +RUN python -c "import tree_sitter_language_pack as t; t.download(['dart', 'go', 'javascript', 'lean', 'typescript', 'vue', 'zig'])" + # Copy application code COPY codewiki ./codewiki COPY img ./img diff --git a/guides/artifact-aware-generation.md b/guides/artifact-aware-generation.md index 90db8486..17d7212b 100644 --- a/guides/artifact-aware-generation.md +++ b/guides/artifact-aware-generation.md @@ -20,8 +20,8 @@ Files are classified by name, extension, and directory. Nine classes: | Class | Examples | | --- | --- | -| `manifest` | `package.json`, `pyproject.toml`, `setup.py`, `setup.cfg`, `Cargo.toml`, `go.mod`, `build.zig.zon`, `Gemfile`, `pnpm-workspace.yaml` | -| `build` | `Makefile`, `CMakeLists.txt`, `configure.ac`, `Makefile.am`, `m4/*.m4`, `build.zig`, `*.gradle`, `BUILD.gn`, `*.gni`, `DEPS`, `Rakefile`, `rakelib/*.rake`, `build/` | +| `manifest` | `package.json`, `pyproject.toml`, `setup.py`, `setup.cfg`, `Cargo.toml`, `go.mod`, `build.zig.zon`, `lake-manifest.json`, `lean-toolchain`, `Gemfile`, `pnpm-workspace.yaml` | +| `build` | `Makefile`, `CMakeLists.txt`, `configure.ac`, `Makefile.am`, `m4/*.m4`, `build.zig`, `lakefile.lean`, `lakefile.toml`, `*.gradle`, `BUILD.gn`, `*.gni`, `DEPS`, `Rakefile`, `rakelib/*.rake`, `build/` | | `container` | `Dockerfile*`, `Containerfile`, `docker-compose*.yml`, files under `docker/` | | `ci` | `.github/workflows/*.yml`, `.github/actions/*/action.yml`, `.gitlab-ci.yml`, `Jenkinsfile`, `ci/`, `.circleci/` | | `packaging` | `debian/`, `rpm/`, `pkg/`, `packages/`, `*.spec`, `*.service`, install and lifecycle scripts | diff --git a/guides/development.md b/guides/development.md index 4c88fb32..73a1bcd5 100644 --- a/guides/development.md +++ b/guides/development.md @@ -122,7 +122,12 @@ Analyzers are standalone classes, one file per language. Follow 1. **Grammar.** Add the `tree-sitter-` package to `pyproject.toml` and `requirements.txt`, or take the grammar from `tree-sitter-language-pack` (already a dependency) with - `get_parser("")`, as `analyzers/dart.py` and `analyzers/go.py` do. + `get_pack_parser("")` from `utils/grammars.py`, as + `analyzers/dart.py` and `analyzers/go.py` do. Add the language and its + grammars to `PACK_GRAMMARS_BY_LANGUAGE` in the same file. The pack (1.x) downloads a grammar on first + use, so also add the name to the `t.download([...])` list in + `docker/Dockerfile`. `tests/test_pack_grammars.py` checks that the two + lists match. 2. **Analyzer.** Create `analyzers/.py` with a `TreeSitterAnalyzer` class that extracts components and relationships, plus a module-level `analyze__file(...)` function. @@ -138,8 +143,8 @@ Analyzers are standalone classes, one file per language. Follow snippets that check component and edge extraction. See `tests/test_scala_analyzer.py`, `tests/test_ruby_analyzer.py`, `tests/test_rust_analyzer.py`, `tests/test_dart_analyzer.py`, - `tests/test_go_analyzer.py`, `tests/test_zig_analyzer.py`, and - `tests/test_vue_analyzer.py`. + `tests/test_go_analyzer.py`, `tests/test_zig_analyzer.py`, + `tests/test_lean_analyzer.py`, and `tests/test_vue_analyzer.py`. 6. **Docs.** Add the language to the README list. ## Tests and lint diff --git a/pyproject.toml b/pyproject.toml index a407109a..a96d9216 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -29,7 +29,7 @@ dependencies = [ "GitPython>=3.1.40", "Jinja2>=3.1.6", "tree-sitter>=0.25", - "tree-sitter-language-pack>=0.8.0,<0.9.0", + "tree-sitter-language-pack>=1.23.1,<2.0.0", "tree-sitter-python>=0.23.6", "tree-sitter-java>=0.23.5", "tree-sitter-javascript>=0.21.4", diff --git a/requirements.txt b/requirements.txt index 7551bf8a..1d764c05 100644 --- a/requirements.txt +++ b/requirements.txt @@ -148,7 +148,7 @@ tree-sitter-embedded-template==0.23.2 tree-sitter-java==0.23.5 tree-sitter-javascript==0.21.4 tree-sitter-kotlin==1.1.0 -tree-sitter-language-pack==0.8.0 +tree-sitter-language-pack==1.23.1 tree-sitter-python==0.23.6 tree-sitter-ruby==0.23.1 tree-sitter-rust==0.23.2 diff --git a/tests/test_artifact_analyzer.py b/tests/test_artifact_analyzer.py index 6ba521a2..8c73e8bf 100644 --- a/tests/test_artifact_analyzer.py +++ b/tests/test_artifact_analyzer.py @@ -130,6 +130,11 @@ def _artifact_nodes(components: dict[str, Node]) -> dict[str, Node]: ("build.zig", "build"), ("build.zig.zon", "manifest"), ("src/main.zig", None), + ("lakefile.lean", "build"), + ("lakefile.toml", "build"), + ("lake-manifest.json", "manifest"), + ("lean-toolchain", "manifest"), + ("Geo/Point.lean", None), ("src/App.vue", None), ("pytest.ini", "test_infra"), ("conftest.py", "test_infra"), diff --git a/tests/test_lean_analyzer.py b/tests/test_lean_analyzer.py new file mode 100644 index 00000000..6fbba270 --- /dev/null +++ b/tests/test_lean_analyzer.py @@ -0,0 +1,274 @@ +"""Tests for the Lean 4 analyzer: header-scanner structure, tree-sitter +references, and exact-name resolution in CallGraphAnalyzer.""" + +from pathlib import Path + +import pytest + +pytest.importorskip("tree_sitter_language_pack") + +from codewiki.src.be.dependency_analyzer.analysis.call_graph_analyzer import ( + CallGraphAnalyzer, +) +from codewiki.src.be.dependency_analyzer.analyzers.lean import ( + analyze_lean_file, + mask_source, + normalize_reference, + scan_headers, +) +from codewiki.src.be.dependency_analyzer.utils.file_selection import is_skipped_lean_file + +POINT = """\ +/-! Geometry primitives. -/ +namespace Geo + +/-- A point in the plane. +Coordinates are naturals. -/ +structure Point where + x : Nat + y : Nat + deriving Repr + +def Point.add (p q : Point) : Point := + let s := p.x + q.x + { x := s, y := p.y + q.y } + +@[simp] +theorem Point.add_zero (p : Point) : Point.add p ⟨0, 0⟩ = p := by + cases p + simp [Point.add, Nat.add_zero] + +inductive Shape where + | dot (p : Point) + | segment (a b : Point) + +def Shape.start : Shape → Point + | .dot p => p + | .segment a _ => a + +private def secret : Nat := 1 + +instance : Add Point := ⟨Point.add⟩ + +section Ops +open Point in +def double (p : Point) : Point := add p p +end Ops + +end Geo +""" + +USE = """\ +import Geo.Point + +open Geo + +def origin : Point := Point.mk 0 0 + +def first (s : Shape) : Point := Shape.start s + +def shapes : List Shape := [Shape.dot origin, .segment origin origin] + +def leak : Nat := secret + +lemma origin_x : origin.x = 0 := rfl + +def report : IO Unit := do + let p ← pure origin + IO.println s!"{p.x}" + #eval first (Shape.dot p) + +def after : Point := double origin + +def external := Nat.add_comm 1 2 +""" + +ISLAND = """\ +def lonely : Nat := Geo.secret + +def notImported := Geo.Point.add +""" + + +def _write(root: Path, rel: str, text: str) -> str: + path = root / rel + path.parent.mkdir(parents=True, exist_ok=True) + path.write_text(text, encoding="utf-8") + return rel + + +@pytest.fixture +def lean_repo(tmp_path: Path): + files = [ + _write(tmp_path, "src/Geo/Point.lean", POINT), + _write(tmp_path, "src/Geo/Use.lean", USE), + _write(tmp_path, "src/Island.lean", ISLAND), + _write(tmp_path, ".lake/packages/dep/Dep.lean", "def dep := 1\n"), + ] + analyzer = CallGraphAnalyzer() + analyzer.analyze_code_files([{"path": f, "language": "lean"} for f in files], str(tmp_path)) + edges = {(r.caller, r.callee) for r in analyzer.call_relationships} + return analyzer.functions, edges + + +P = "src/Geo/Point.lean::" +U = "src/Geo/Use.lean::" +I = "src/Island.lean::" # noqa: E741 + + +def test_declarations_namespaces_and_types(lean_repo) -> None: + functions, _ = lean_repo + kinds = {f.qualified_name: (f.component_type, f.node_type) for f in functions.values()} + assert kinds["Geo.Point"] == ("struct", "structure") + assert kinds["Geo.Point.add"] == ("function", "def") + assert kinds["Geo.Point.add_zero"] == ("function", "theorem") + assert kinds["Geo.Shape"] == ("class", "inductive") + assert kinds["Geo.double"] == ("function", "def") + assert kinds["origin_x"] == ("function", "theorem") # `lemma` is a theorem + assert any(name.startswith("Geo.instance_L") for name in kinds) + assert all(f.language == "lean" for f in functions.values()) + + +def test_spans_docstrings_and_attributes(lean_repo) -> None: + functions, _ = lean_repo + point = functions[P + "Geo.Point"] + assert point.docstring == "A point in the plane.\nCoordinates are naturals." + assert (point.start_line, point.end_line) == (6, 9) + theorem = functions[P + "Geo.Point.add_zero"] + assert theorem.start_line == 15 # the `@[simp]` line + assert "simp [Point.add" in (theorem.source_code or "") + assert not functions[P + "Geo.Point.add"].docstring + + +def test_lake_folders_are_skipped(lean_repo) -> None: + functions, _ = lean_repo + assert not any(".lake" in f.relative_path for f in functions.values()) + assert is_skipped_lean_file(".lake/packages/dep/Dep.lean") + assert is_skipped_lean_file("lake-packages/std/Std.lean") + assert not is_skipped_lean_file("src/Geo/Point.lean") + + +def test_same_file_references_resolve_in_the_namespace(lean_repo) -> None: + _, edges = lean_repo + assert (P + "Geo.Point.add", P + "Geo.Point") in edges + assert (P + "Geo.Point.add_zero", P + "Geo.Point.add") in edges + assert (P + "Geo.Shape", P + "Geo.Point") in edges # constructor argument types + assert (P + "Geo.Shape.start", P + "Geo.Shape") in edges + + +def test_open_in_applies_to_the_next_declaration(lean_repo) -> None: + functions, edges = lean_repo + assert (P + "Geo.double", P + "Geo.Point.add") in edges # `add` through `open Point in` + instance = next(i for i in functions if i.startswith(P + "Geo.instance_L")) + assert (instance, P + "Geo.Point.add") in edges + + +def test_imports_open_and_member_aliases(lean_repo) -> None: + _, edges = lean_repo + assert (U + "origin", P + "Geo.Point") in edges # `Point.mk` is the structure + assert (U + "first", P + "Geo.Shape.start") in edges + assert (U + "shapes", P + "Geo.Shape") in edges # `Shape.dot` is the inductive + assert (U + "shapes", U + "origin") in edges + assert (U + "origin_x", U + "origin") in edges + assert (U + "after", P + "Geo.double") in edges + + +def test_error_regions_still_give_references(lean_repo) -> None: + _, edges = lean_repo + assert (U + "report", U + "origin") in edges + assert (U + "report", U + "first") in edges + assert (U + "report", P + "Geo.Shape") in edges + + +def test_locals_externals_and_recursion_give_no_edges(lean_repo) -> None: + functions, edges = lean_repo + callees = {callee for caller, callee in edges if caller == P + "Geo.Point.add"} + assert callees == {P + "Geo.Point"} # p, q, s, p.x are locals + assert not any(caller == U + "external" for caller, _ in edges) # Nat.add_comm + assert all(caller != callee for caller, callee in edges) + assert all(callee in functions for _, callee in edges) + + +def test_private_and_unimported_names_are_invisible(lean_repo) -> None: + _, edges = lean_repo + assert not any(caller == U + "leak" for caller, _ in edges) # private in another file + assert not any(caller.startswith(I) for caller, _ in edges) # Island imports nothing + + +def test_ambiguous_name_is_dropped(tmp_path: Path) -> None: + files = [ + _write(tmp_path, "A.lean", "namespace X\ndef f := 1\nend X\n"), + _write(tmp_path, "B.lean", "namespace Y\ndef f := 2\nend Y\n"), + _write(tmp_path, "C.lean", "import A\nimport B\nopen X Y\ndef g := f\ndef h := X.f\n"), + ] + analyzer = CallGraphAnalyzer() + analyzer.analyze_code_files([{"path": f, "language": "lean"} for f in files], str(tmp_path)) + edges = {(r.caller, r.callee) for r in analyzer.call_relationships} + assert not any(caller == "C.lean::g" for caller, _ in edges) + assert ("C.lean::h", "A.lean::X.f") in edges + + +def test_root_prefix_mutual_and_nested_namespaces(tmp_path: Path) -> None: + source = """\ +namespace A.B +def _root_.top := 1 +mutual + def even : Nat → Bool + | 0 => true + | n + 1 => odd n + def odd : Nat → Bool + | 0 => false + | n + 1 => even n +end +end A.B +def last := top +""" + nodes, _ = analyze_lean_file(str(tmp_path / "M.lean"), source, repo_path=str(tmp_path)) + names = {n.qualified_name for n in nodes} + assert names == {"top", "A.B.even", "A.B.odd", "last"} + + +def test_masking_keeps_lines_and_byte_offsets() -> None: + source = "def a := \"-- not a comment\" -- é comment\n/- block /- nested -/ -/ def b := 'x'\n" + masked = mask_source(source) + assert masked.text.count("\n") == source.count("\n") + assert len(masked.text.encode("utf8")) == len(source.encode("utf8")) + assert "not a comment" not in masked.text and "nested" not in masked.text + assert "def b" in masked.text + + +def test_interpolated_strings_and_primes_are_masked_correctly() -> None: + masked = mask_source('def c := s!"x {y} -- z"\ndef d\' := r#"q"# ++ a\'\n') + assert "-- z" not in masked.text and '"q"' not in masked.text + assert "def d' :=" in masked.text and "a'" in masked.text + + +def test_header_scanner_without_the_parse_tree() -> None: + decls, imports = scan_headers( + mask_source("import Mathlib.Data.Nat\nimport Foo\n#eval 1\ntheorem t : True := trivial\n") + ) + assert imports == ["Mathlib.Data.Nat", "Foo"] + assert [d.fqn for d in decls] == ["t"] + + +@pytest.mark.parametrize( + "raw, expected", + [ + ("Foo.bar", "Foo.bar"), + ("@Foo.bar", "Foo.bar"), + ("«weird name».x", "weird name.x"), + ("p.1", "p"), + (".dot", None), + ("fun", None), + ], +) +def test_normalize_reference(raw: str, expected: str | None) -> None: + assert normalize_reference(raw) == expected + + +def test_empty_and_broken_files(tmp_path: Path) -> None: + assert analyze_lean_file(str(tmp_path / "E.lean"), "", repo_path=str(tmp_path)) == ([], []) + nodes, _ = analyze_lean_file( + str(tmp_path / "B.lean"), "def broken (x : := ⟨\n#eval ¬¬\n", repo_path=str(tmp_path) + ) + assert [n.qualified_name for n in nodes] == ["broken"] diff --git a/tests/test_pack_grammars.py b/tests/test_pack_grammars.py new file mode 100644 index 00000000..88803fd9 --- /dev/null +++ b/tests/test_pack_grammars.py @@ -0,0 +1,80 @@ +"""Grammars from tree-sitter-language-pack: a failed download stops the +analysis once, with a clear message, and the Docker image fetches every +grammar the analyzers load.""" + +import re +from pathlib import Path + +import pytest +import tree_sitter_language_pack as tslp + +from codewiki.src.be.dependency_analyzer.analysis.call_graph_analyzer import ( + CallGraphAnalyzer, +) +from codewiki.src.be.dependency_analyzer.utils import grammars +from codewiki.src.be.dependency_analyzer.utils.grammars import ( + PACK_GRAMMARS, + GrammarUnavailableError, + ensure_pack_grammars, + get_pack_parser, +) + +DOCKERFILE = Path(__file__).resolve().parents[1] / "docker" / "Dockerfile" + + +@pytest.fixture +def offline(monkeypatch): + """Every pack grammar load fails as it does without network access.""" + calls = [] + + def fail(name): + calls.append(name) + raise tslp.DownloadError(f"Failed to fetch manifest for {name}: Connection refused") + + get_pack_parser.cache_clear() + monkeypatch.setattr(grammars.tslp, "get_parser", fail) + yield calls + get_pack_parser.cache_clear() + + +def test_download_failure_gives_a_clear_error(offline): + with pytest.raises(GrammarUnavailableError) as info: + get_pack_parser("go") + message = str(info.value) + assert info.value.grammar == "go" + assert "'go'" in message + assert "network access" in message + assert "Connection refused" in message + assert "t.download([" in message + assert isinstance(info.value.__cause__, tslp.DownloadError) + + +def test_only_the_grammars_of_present_languages_load(offline, monkeypatch): + monkeypatch.setattr(grammars.tslp, "get_parser", lambda name: offline.append(name)) + ensure_pack_grammars(["python", "vue", "java", "vue"]) + assert sorted(offline) == ["javascript", "typescript", "vue"] + + +def test_languages_without_pack_grammars_need_no_network(offline): + ensure_pack_grammars(["python", "java", "rust"]) + assert offline == [] + + +def test_analysis_stops_before_the_first_file(offline, tmp_path, monkeypatch): + (tmp_path / "main.go").write_text("package main\n\nfunc main() {}\n", encoding="utf-8") + analyzed = [] + monkeypatch.setattr( + CallGraphAnalyzer, "_analyze_code_file", lambda self, base, info: analyzed.append(info) + ) + with pytest.raises(GrammarUnavailableError, match="'go'"): + CallGraphAnalyzer().analyze_code_files( + [{"path": "main.go", "language": "go"}], str(tmp_path) + ) + assert analyzed == [] + + +def test_dockerfile_downloads_every_pack_grammar(): + match = re.search(r"t\.download\(\[([^\]]*)\]\)", DOCKERFILE.read_text(encoding="utf-8")) + assert match, "docker/Dockerfile must download the pack grammars at build time" + in_dockerfile = sorted(re.findall(r"'([^']+)'", match.group(1))) + assert in_dockerfile == list(PACK_GRAMMARS)