From 76cffb3fd4202a1c14f1e3549206d2d105d8f968 Mon Sep 17 00:00:00 2001 From: Gabriele Battimelli Date: Wed, 26 Aug 2026 13:09:54 -0400 Subject: [PATCH] Fix the two failures blocking PhyslibAlpha and QuantumInfo The forced run built PhyslibAlpha fine but failed the load for two reasons. QuantumInfo had no .olean files. The lake cache restored from physlib-lake-, a build made when only Physlib was compiled, and lake then considered the tree up to date, so QuantumInfo was never built and jixia failed 33 times with "object file does not exist". My previous attempt at this put the workflow hash in the key but left a bare physlib-lake- restore-key, which matched that older cache anyway. Namespace the key by the workflow hash first and keep the restore-key inside that namespace. An anonymous declaration aborted the whole load with IndexError: jixia's is_internal indexes name[-1] without checking for an empty name. Wrap it once so every call site is covered rather than guarding the one that happened to crash, and treat nameless entries as internal since they cannot be stored or searched for anyway. --- .github/workflows/weekly-index.yml | 13 +++++++------ database/jixia_db.py | 15 ++++++++++++++- 2 files changed, 21 insertions(+), 7 deletions(-) diff --git a/.github/workflows/weekly-index.yml b/.github/workflows/weekly-index.yml index 1a72288..4a5cf3b 100644 --- a/.github/workflows/weekly-index.yml +++ b/.github/workflows/weekly-index.yml @@ -120,13 +120,14 @@ jobs: uses: actions/cache@v4 with: path: physlib/.lake/build - # Keyed on MODULE_NAMES as well: which libraries were compiled is part - # of what this cache holds, so a Physlib-only build must not be reused - # verbatim once more libraries are indexed. - key: physlib-lake-${{ steps.check.outputs.current_sha }}-${{ hashFiles('.github/workflows/weekly-index.yml') }} + # Namespaced by MODULE_NAMES: which libraries this holds is part of the + # cache's identity. The restore-key must stay inside that namespace -- + # a broader fallback silently restores a build missing whole libraries, + # and lake then treats them as up to date, so their .olean files never + # appear and jixia fails per-module with "object file does not exist". + key: physlib-lake-${{ hashFiles('.github/workflows/weekly-index.yml') }}-${{ steps.check.outputs.current_sha }} restore-keys: | - physlib-lake-${{ steps.check.outputs.current_sha }}- - physlib-lake- + physlib-lake-${{ hashFiles('.github/workflows/weekly-index.yml') }}- - name: Install elan if: steps.check.outputs.has_changes == 'true' diff --git a/database/jixia_db.py b/database/jixia_db.py index 188aa7a..612901e 100644 --- a/database/jixia_db.py +++ b/database/jixia_db.py @@ -4,7 +4,8 @@ from pathlib import Path from jixia import LeanProject -from jixia.structs import LeanName, Modifiers, RootModel, Symbol, Declaration, is_internal +from jixia.structs import LeanName, Modifiers, RootModel, Symbol, Declaration +from jixia.structs import is_internal as _jixia_is_internal from psycopg import Connection from psycopg.types.json import Jsonb from psycopg.types.range import Range @@ -12,6 +13,18 @@ logger = logging.getLogger(__name__) +def is_internal(name: LeanName) -> bool: + """Treat anonymous declarations as internal. + + jixia's is_internal indexes name[-1], so an empty name raises IndexError and + aborts the whole load. Nameless entries cannot be stored or searched for + anyway, so classify them as internal and let the callers skip them. + """ + if not name: + return True + return _jixia_is_internal(name) + + # jixia's model types docString as Lean's older [text, bool] pair, but Lean 4.33 # emits a bare string, so every declaration carrying a docstring fails to # validate. Widening Modifiers' annotation does not fix this: Declaration and