Merge pull request #13 from Kernel-Science/add-agent-skill

Build jixia with PhysLib's toolchain + tolerant decode

Author: Gabrielebattimelli

.github/workflows/weekly-index.yml

@@ -116,12 +116,18 @@ jobs:
         uses: actions/cache@v4
         with:
           path: jixia/.lake/build
-          key: jixia-${{ hashFiles('physlib/lean-toolchain') }}-${{ hashFiles('jixia/lakefile.lean', 'jixia/lakefile.toml') }}
-          restore-keys: jixia-${{ hashFiles('physlib/lean-toolchain') }}-
+          # v2: rebuilt against PhysLib's toolchain (see Build jixia below)
+          key: jixia-v2-${{ hashFiles('physlib/lean-toolchain') }}-${{ hashFiles('jixia/lakefile.lean', 'jixia/lakefile.toml') }}
+          restore-keys: jixia-v2-${{ hashFiles('physlib/lean-toolchain') }}-
 
       - name: Build jixia
         if: steps.check.outputs.has_changes == 'true'
-        run: cd jixia && lake build
+        # jixia reads PhysLib's compiled .olean files, which are version-locked
+        # to PhysLib's Lean toolchain. Build jixia with the same toolchain so the
+        # olean headers are compatible (otherwise: "incompatible header").
+        run: |
+          cp physlib/lean-toolchain jixia/lean-toolchain
+          cd jixia && lake build
         timeout-minutes: 30
 
       - name: Set JIXIA_PATH and LEAN_SYSROOT

database/jixia_db.py

@@ -16,14 +16,15 @@ 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()
+        # A range may not land on a UTF-8 boundary; don't let it abort the load.
+        return module_content[declaration.signature.range.as_slice()].decode(errors="replace")
     else:
         return ""
 
 
 def _get_value(declaration: Declaration, module_content):
     if declaration.value is not None and declaration.value.range is not None:
-        return module_content[declaration.value.range.as_slice()].decode()
+        return module_content[declaration.value.range.as_slice()].decode(errors="replace")
     else:
         return None