Skip to content

Fix jixia path doubling (absolute project root)#12

Merged
Gabrielebattimelli merged 1 commit into
mainfrom
add-agent-skill
Jun 2, 2026
Merged

Fix jixia path doubling (absolute project root)#12
Gabrielebattimelli merged 1 commit into
mainfrom
add-agent-skill

Conversation

@Gabrielebattimelli
Copy link
Copy Markdown
Member

Why

After the schema fix (#11), the Weekly Index reached the Load jixia data into PostgreSQL step, where all 445 modules failed with:

ERROR:jixia.run:error while processing (...): uncaught exception: no such file or directory
  file: physlib/Physlib/Optics/Polarization/Basic.lean

then crashed in Python with FileNotFoundError: '.../Physlib.Thermodynamics.Temperature.Basic.mod.json'.

Root cause

jixia_py.run_jixia launches the analyzer with subprocess.run(args, cwd=root) and passes the module file from path_of_module(m, base_dir), which already includes the project-root prefix. The workflow runs python3 -m database jixia ./physlib with a relative root, so jixia (cwd=physlib) resolves the file physlib/Physlib/.../Basic.lean against its own cwd → physlib/physlib/... → ENOENT, for every module. No .mod.json is produced, so the loader then crashes.

(Note: LEAN_SYSROOT is a red herring — jixia_py never reads it, and the lean-core pass is filtered out by MODULE_NAMES=Physlib.)

What

  • Resolve project_root to an absolute path in database/__init__.py so the file path survives jixia's cwd change.
  • Make load_module skip modules with missing jixia output (matching load_symbol/load_declaration), so a single unprocessable module can't abort the whole load.

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.
Copilot AI review requested due to automatic review settings June 2, 2026 12:59
@Gabrielebattimelli Gabrielebattimelli merged commit 4d2fb51 into main Jun 2, 2026
2 checks passed
Copy link
Copy Markdown

Copilot AI left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Pull request overview

This PR fixes path resolution issues when running the jixia analyzer with a relative project root, which previously caused module paths to be resolved relative to cwd twice and resulted in widespread ENOENT failures during indexing. It also makes the module loader resilient to missing per-module jixia outputs so a single failed module won’t abort the whole load.

Changes:

  • Resolve project_root to an absolute path before constructing LeanProject, preventing “project root doubling” when jixia changes cwd.
  • Update load_module to skip modules when required files (module content and/or jixia output) are missing, logging a warning instead of raising.

Reviewed changes

Copilot reviewed 2 out of 2 changed files in this pull request and generated 1 comment.

File Description
database/__init__.py Converts project_root to an absolute path before running jixia to prevent incorrect path resolution under cwd changes.
database/jixia_db.py Makes module loading tolerant to missing files by skipping problematic modules instead of failing the entire load.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Comment thread database/jixia_db.py
Comment on lines +41 to +49
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))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants