From 93e4cdb8ec1a66c7254d6fdc531cf8e8e294dcd7 Mon Sep 17 00:00:00 2001 From: Fabio Anza Date: Thu, 16 Apr 2026 10:20:53 -0400 Subject: [PATCH 1/2] chore: remove unused imports flagged by ruff F401 Co-Authored-By: Claude Opus 4.6 (1M context) --- database/jixia_db.py | 2 +- engine.py | 1 - server.py | 4 +--- 3 files changed, 2 insertions(+), 5 deletions(-) diff --git a/database/jixia_db.py b/database/jixia_db.py index bc33095..8229bbf 100644 --- a/database/jixia_db.py +++ b/database/jixia_db.py @@ -4,7 +4,7 @@ from pathlib import Path from jixia import LeanProject -from jixia.structs import LeanName, Symbol, Declaration, is_internal, StringRange +from jixia.structs import LeanName, Symbol, Declaration, is_internal from psycopg import Connection from psycopg.types.json import Jsonb from psycopg.types.range import Range diff --git a/engine.py b/engine.py index 1e07c16..bedd876 100644 --- a/engine.py +++ b/engine.py @@ -1,4 +1,3 @@ -import os from collections.abc import Iterable import chromadb diff --git a/server.py b/server.py index 2380206..033fa2d 100644 --- a/server.py +++ b/server.py @@ -4,11 +4,9 @@ from typing import Annotated import dotenv -import psycopg from fastapi import FastAPI, Body, Response, Cookie from jixia.structs import LeanName -from psycopg import Connection -from psycopg.rows import scalar_row, class_row, dict_row +from psycopg.rows import scalar_row, class_row from psycopg.types.json import Jsonb from psycopg_pool import ConnectionPool from pydantic import BaseModel From 167d24bbb6652c203467352f4a6f1bbec46b9cfc Mon Sep 17 00:00:00 2001 From: Fabio Anza Date: Thu, 16 Apr 2026 10:25:20 -0400 Subject: [PATCH 2/2] chore: apply ruff format Co-Authored-By: Claude Opus 4.6 (1M context) --- database/create_schema.py | 4 +--- database/informalize.py | 4 +--- database/jixia_db.py | 30 +++++++++++++++----------- prefix.py | 18 ++++++++++------ query_expansion.py | 2 +- server.py | 44 +++++++++++++++++++++------------------ 6 files changed, 57 insertions(+), 45 deletions(-) diff --git a/database/create_schema.py b/database/create_schema.py index fd51dba..3dee38a 100644 --- a/database/create_schema.py +++ b/database/create_schema.py @@ -90,11 +90,9 @@ def create_schema(conn: Connection): INNER JOIN informal i ON d.name = i.symbol_name INNER JOIN symbol s ON d.name = s.name """, - """ CREATE SCHEMA physlibsearch """, - """ CREATE TABLE physlibsearch.query ( id UUID PRIMARY KEY, @@ -108,7 +106,7 @@ def create_schema(conn: Connection): declaration_name JSONB REFERENCES declaration(name) NOT NULL, action TEXT NOT NULL, PRIMARY KEY (query_id, declaration_name) - )""" + )""", ] with conn.cursor() as cursor: diff --git a/database/informalize.py b/database/informalize.py index 4f2ad83..afc1214 100644 --- a/database/informalize.py +++ b/database/informalize.py @@ -54,9 +54,7 @@ def generate_informal(conn: Connection, batch_size: int = 50, limit_level: int | max_level = limit_level with conn.cursor(row_factory=scalar_row) as cnt_cursor: - total_remaining = cnt_cursor.execute( - "SELECT COUNT(*) FROM symbol s WHERE NOT EXISTS(SELECT 1 FROM informal i WHERE i.symbol_name = s.name)" - ).fetchone() or 0 + total_remaining = cnt_cursor.execute("SELECT COUNT(*) FROM symbol s WHERE NOT EXISTS(SELECT 1 FROM informal i WHERE i.symbol_name = s.name)").fetchone() or 0 done = 0 logger.warning("starting informalization: %d declarations remaining", total_remaining) diff --git a/database/jixia_db.py b/database/jixia_db.py index 8229bbf..69b2b3b 100644 --- a/database/jixia_db.py +++ b/database/jixia_db.py @@ -11,13 +11,15 @@ logger = logging.getLogger(__name__) + def _get_signature(declaration: Declaration, module_content): if declaration.signature.pp is not None: return declaration.signature.pp elif declaration.signature.range is not None: return module_content[declaration.signature.range.as_slice()].decode() else: - return '' + return "" + def _get_value(declaration: Declaration, module_content): if declaration.value is not None and declaration.value.range is not None: @@ -25,6 +27,7 @@ def _get_value(declaration: Declaration, module_content): else: return None + def _get_range(declaration: Declaration): r = declaration.ref.range if r is not None: @@ -32,6 +35,7 @@ def _get_range(declaration: Declaration): else: return None + 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) @@ -115,17 +119,19 @@ def load_declaration(module_name: LeanName): for index, decl in enumerate(declarations): if is_internal(decl.name) or decl.kind == "proofWanted": continue - db_declarations.append({ - "module_name": Jsonb(module_name), - "index" : index, - "name" : Jsonb(decl.name) if decl.kind != "example" else None, - "visible" : decl.modifiers.visibility != "private" and decl.kind != "example", - "docstring" : decl.modifiers.docstring, - "kind" : decl.kind, - "signature" : _get_signature(decl, module_content), - "value" : _get_value(decl, module_content), - "range" : _get_range(decl), - }) + db_declarations.append( + { + "module_name": Jsonb(module_name), + "index": index, + "name": Jsonb(decl.name) if decl.kind != "example" else None, + "visible": decl.modifiers.visibility != "private" and decl.kind != "example", + "docstring": decl.modifiers.docstring, + "kind": decl.kind, + "signature": _get_signature(decl, module_content), + "value": _get_value(decl, module_content), + "range": _get_range(decl), + } + ) cursor.executemany( """ INSERT INTO declaration (module_name, index, name, visible, docstring, kind, signature, value) diff --git a/prefix.py b/prefix.py index e60eda2..0ff011c 100644 --- a/prefix.py +++ b/prefix.py @@ -5,17 +5,20 @@ from jixia import LeanProject from jixia.structs import parse_name, is_prefix_of, LeanName + def format(lean_name: LeanName, with_indent: bool = False) -> str: - formatted = '.'.join(str(x) for x in lean_name) - indent = ' ' * (len(lean_name) - 1) if with_indent else '' + formatted = ".".join(str(x) for x in lean_name) + indent = " " * (len(lean_name) - 1) if with_indent else "" return f"{indent}{formatted}" + def sort(lean_names: list[LeanName]) -> list[LeanName]: return sorted(lean_names, key=format) + def main(project_root: str, prefixes: str | None) -> None: project = LeanProject(project_root) - all_module_names : list[LeanName] = project.find_modules() + all_module_names: list[LeanName] = project.find_modules() print("____________ALL MODULES_____________") for module_name in sort(all_module_names): @@ -23,19 +26,22 @@ def main(project_root: str, prefixes: str | None) -> None: if prefixes is not None: print("__________MODULES THAT MATCH YOUR PREFIX___________") - prefix_names : list[LeanName] = [parse_name(p) for p in prefixes.split(",")] + prefix_names: list[LeanName] = [parse_name(p) for p in prefixes.split(",")] matching_names = [n for n in all_module_names if any(is_prefix_of(p, n) for p in prefix_names)] for module_name in sort(matching_names): print(format(module_name)) + if __name__ == "__main__": dotenv.load_dotenv() path_to_lean = path_to_lean = Path(os.environ["LEAN_SYSROOT"]) / "src" / "lean" - parser = ArgumentParser(description=f""" + parser = ArgumentParser( + description=f""" Helper command that helps you understand what files are available for indexing. For example, you can run it with: python -m prefix --project_root "{path_to_lean}" --prefixes Init.Grind,Init.Control.Lawful - """) + """ + ) parser.add_argument("--project_root", help="Path to the project you want to index", required=False) parser.add_argument("--prefixes", help="Comma-separated list of module prefixes to be included in the index; e.g., Init.Grind,Init.Control.Lawful", required=False) args = parser.parse_args() diff --git a/query_expansion.py b/query_expansion.py index e79dad0..3329f0c 100644 --- a/query_expansion.py +++ b/query_expansion.py @@ -23,7 +23,7 @@ def __init__(self, model: str): ) self.model = model # Matches everything after "Hypothetical: " — the full hypothetical declaration - self.pattern = re.compile(r'Hypothetical:\s*(.*)', re.DOTALL) + self.pattern = re.compile(r"Hypothetical:\s*(.*)", re.DOTALL) async def expand(self, user_input: str) -> str | None: """ diff --git a/server.py b/server.py index 033fa2d..e1a24ca 100644 --- a/server.py +++ b/server.py @@ -26,9 +26,9 @@ async def lifespan(app: FastAPI): dotenv.load_dotenv() with ConnectionPool( - os.environ["CONNECTION_STRING"], - kwargs={"autocommit": True}, - check=ConnectionPool.check_connection, + os.environ["CONNECTION_STRING"], + kwargs={"autocommit": True}, + check=ConnectionPool.check_connection, ) as pool: app.expander = QueryExpander(os.environ["GEMINI_FAST_MODEL"]) app.retriever = PhyslibSearchEngine(os.environ["CHROMA_PATH"], None) @@ -61,25 +61,31 @@ async def set_connection(request: Request, call_next): @app.post("/search") def search( - response: Response, - query: list[str], - num_results: Annotated[int, Body(gt=0, le=150)] = 10, + response: Response, + query: list[str], + num_results: Annotated[int, Body(gt=0, le=150)] = 10, ) -> list[list[QueryResult]]: if len(query) == 1: with app.retriever.conn.cursor(row_factory=scalar_row) as cursor: - cursor.execute(""" + cursor.execute( + """ INSERT INTO physlibsearch.query(id, query, time) VALUES (GEN_RANDOM_UUID(), %s, NOW()) RETURNING id - """, (query[0],)) + """, + (query[0],), + ) session_id = cursor.fetchone() response.set_cookie("session", str(session_id)) else: with app.retriever.conn.cursor() as cursor: - cursor.executemany(""" + cursor.executemany( + """ INSERT INTO physlibsearch.query(id, query, time) VALUES (GEN_RANDOM_UUID(), %s, NOW()) - """, [(q,) for q in query]) + """, + [(q,) for q in query], + ) return app.retriever.find_declarations(query, num_results) @@ -136,13 +142,16 @@ def list_modules(request: Request) -> list[ModuleInfo]: def module_declarations(request: Request, module_name: LeanName) -> list[Record]: with app.pool.connection() as conn: with conn.cursor(row_factory=class_row(Record)) as cursor: - cursor.execute(""" + cursor.execute( + """ SELECT r.* FROM record r INNER JOIN declaration d ON r.name = d.name WHERE r.module_name = %s AND d.visible = TRUE ORDER BY d.index - """, (Jsonb(module_name),)) + """, + (Jsonb(module_name),), + ) return cursor.fetchall() @@ -151,6 +160,7 @@ def module_declarations(request: Request, module_name: LeanName) -> list[Record] async def user_feedback(request: Request, body: UserFeedback): if not (1 <= body.rating <= 5): from fastapi import HTTPException + raise HTTPException(status_code=422, detail="Rating must be between 1 and 5") with app.pool.connection() as conn: with conn.cursor() as cursor: @@ -169,13 +179,7 @@ async def feedback(session: Annotated[str, Cookie()], body: Feedback): query_id = uuid.UUID(session) if body.cancel: with app.retriever.conn.cursor() as cursor: - cursor.execute( - "DELETE FROM physlibsearch.feedback WHERE query_id = %s AND declaration_name = %s", - (query_id, Jsonb(body.declaration)) - ) + cursor.execute("DELETE FROM physlibsearch.feedback WHERE query_id = %s AND declaration_name = %s", (query_id, Jsonb(body.declaration))) else: with app.retriever.conn.cursor() as cursor: - cursor.execute( - "INSERT INTO physlibsearch.feedback(query_id, declaration_name, action) VALUES (%s, %s, %s)", - (query_id, Jsonb(body.declaration), body.action) - ) + cursor.execute("INSERT INTO physlibsearch.feedback(query_id, declaration_name, action) VALUES (%s, %s, %s)", (query_id, Jsonb(body.declaration), body.action))