Fix the two failures blocking PhyslibAlpha and QuantumInfo

.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'

database/jixia_db.py

@@ -4,14 +4,27 @@
 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
 
 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