From 54510966f4f2745eef0fdc252d648b5299327773 Mon Sep 17 00:00:00 2001 From: Gabriele Battimelli Date: Tue, 2 Jun 2026 14:59:09 +0200 Subject: [PATCH] Fix jixia path doubling by using absolute project root MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The weekly index 'jixia' step failed for every module with ENOENT. jixia_py runs the analyzer with cwd=project_root while passing the module file path (which already includes the project_root prefix). With a relative root like ./physlib, jixia resolves the file against its own cwd and looks for physlib/physlib/... — which does not exist. Resolve project_root to an absolute path so the file path survives the cwd change. Also make load_module skip modules whose jixia output is missing, consistent with load_symbol and load_declaration, so one unprocessable module can't abort the whole load. --- database/__init__.py | 4 +++- database/jixia_db.py | 10 +++++++++- 2 files changed, 12 insertions(+), 2 deletions(-) diff --git a/database/__init__.py b/database/__init__.py index 30b7d19..b3af96e 100644 --- a/database/__init__.py +++ b/database/__init__.py @@ -46,7 +46,9 @@ def main(): if args.command == "schema": create_schema(conn) elif args.command == "jixia": - project = LeanProject(args.project_root) + # jixia runs each module with cwd=project_root, so the module file + # path must be absolute — a relative root would be resolved twice. + project = LeanProject(os.path.abspath(args.project_root)) prefixes = [parse_name(p) for p in args.prefixes.split(",")] load_data(project, prefixes, conn) elif args.command == "informal": diff --git a/database/jixia_db.py b/database/jixia_db.py index 69b2b3b..1457f54 100644 --- a/database/jixia_db.py +++ b/database/jixia_db.py @@ -38,7 +38,15 @@ def _get_range(declaration: Declaration): def load_data(project: LeanProject, prefixes: list[LeanName], conn: Connection): def load_module(data: Iterable[LeanName], base_dir: Path): - values = ((Jsonb(m), project.path_of_module(m, base_dir).read_bytes(), project.load_module_info(m).docstring) for m in data) + values = [] + for m in data: + try: + content = project.path_of_module(m, base_dir).read_bytes() + docstring = project.load_module_info(m).docstring + except FileNotFoundError: + logger.warning("skipping module %s: jixia output not found", m) + continue + values.append((Jsonb(m), content, docstring)) cursor.executemany( """ INSERT INTO module (name, content, docstring) VALUES (%s, %s, %s) ON CONFLICT DO NOTHING