feat: Lean 4 analyzer, with header-scanner structure and exact-name resolution

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<T>(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
 

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

codewiki/cli/utils/repo_validator.py

@@ -37,6 +37,7 @@
     ".dart",  # Dart
     ".go",  # Go
     ".zig",  # Zig
+    ".lean",  # Lean 4
     ".vue",  # Vue single-file components
 }
 

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"],
     }
 

codewiki/mcp/tools/analysis.py

@@ -232,6 +232,7 @@ def _detect_via_mtime(
         ".dart",
         ".go",
         ".zig",
+        ".lean",
         ".vue",
     }
 

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",
         ]
 

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")
 

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:

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<T>(x)` / `foo<T>(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:]