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

@@ -15,16 +15,22 @@
 from collections import defaultdict
 from contextlib import contextmanager
 from pathlib import Path
+from typing import TYPE_CHECKING
 
 from codewiki.src.be.dependency_analyzer.models.core import CallRelationship, Node
 from codewiki.src.be.dependency_analyzer.utils.external_symbols import (
     CPP_STANDARD_HEADERS,
     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
 
+if TYPE_CHECKING:
+    from codewiki.src.be.dependency_analyzer.analyzers.lean import LeanFile, LeanScope
+    from codewiki.src.be.dependency_analyzer.analyzers.lean_resolution import LeanNameResolver
+
 logger = logging.getLogger(__name__)
 
 
@@ -75,6 +81,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 +103,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 +114,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 +300,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 +677,59 @@ 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:
+        self._lean_files: dict[str, LeanFile] = {}
+        self._lean_scopes: dict[str, LeanScope] = {}
+        self._lean_aliases: dict[str, list[str]] = defaultdict(list)
+        self._lean_private: set[str] = set()
+        self._lean_protected: set[str] = set()
+        self._lean_resolver: LeanNameResolver | None = None
+
+    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_files[analyzer.relative_path] = analyzer.scan
+            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)
+            self._lean_protected.update(analyzer.protected_ids)
+        except Exception:
+            logger.exception(f"Failed to analyze Lean file {file_path}")
+
+    def _resolve_lean_callee(self, callee: str, caller: Node) -> str | None:
+        from codewiki.src.be.dependency_analyzer.analyzers.lean_resolution import LeanNameResolver
+
+        if self._lean_resolver is None:
+            self._lean_resolver = LeanNameResolver(
+                self.functions,
+                self._lean_files,
+                self._lean_scopes,
+                self._lean_aliases,
+                self._lean_private,
+                self._lean_protected,
+            )
+        return self._lean_resolver.resolve(callee, caller)
+
     def _analyze_go_file(self, file_path: str, content: str, repo_dir: str):
         """
         Analyze Go file using tree-sitter based analyzer.
@@ -856,11 +922,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 +1069,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 +1217,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:]

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: