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