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