Ejecuta cualquier Skill en Manus
con un clic

Ejecuta cualquier Skill en Manus con un clic

sync-isabelle-afp-distribution

Estrellas5

Forks0

Actualizado18 de junio de 2026 a las 13:05

How to repackage/upload and download/unpack the Isabelle + paired AFP distribution, published together as contrib/Isabelle2025-2_and_afp-2026-05-13.tar.zst on the Hugging Face Hub (via manage_data.py update/get). Use when publishing a rebuilt Isabelle+AFP tarball (after isabelle scala_build, patches, etc.) or installing/refreshing the distribution on another machine.

Instalación

Instalar con Codex o Claude Copia este prompt, pégalo en Codex, Claude u otro asistente, y deja que revise la página de la skill y la instale por ti.

Ejecutar en Manus

Fuente

xqyww123

xqyww123/MLML

Abrir repositorio de GitHub Ver repositorios del creador

Descarga

Ejecutar en Manus

Ocupaciones relacionadasSOC

Basado en la clasificación ocupacional SOC

Administradores de redes y sistemas informáticosOcupaciones informáticas y matemáticas·SOC 15-1244

SKILL.md

readonly

name	sync-isabelle-afp-distribution
description	How to repackage/upload and download/unpack the Isabelle + paired AFP distribution, published together as contrib/Isabelle2025-2_and_afp-2026-05-13.tar.zst on the Hugging Face Hub (via manage_data.py update/get). Use when publishing a rebuilt Isabelle+AFP tarball (after isabelle scala_build, patches, etc.) or installing/refreshing the distribution on another machine.

Packaging and syncing the Isabelle + AFP distribution

Isabelle + its paired AFP snapshot are published together as contrib/Isabelle2025-2_and_afp-2026-05-13.tar.zst on the Hugging Face Hub.

Repackage and upload (after rebuilding the shared jar with isabelle scala_build, applying patches, etc.). -y skips the [y/N] confirmation (required for non-interactive / detached runs — else update blocks on the prompt and dies with EOFError); update regenerates data/manifest.json, so commit and push it:

cd contrib
tar --zstd -cvf Isabelle2025-2_and_afp-2026-05-13.tar.zst Isabelle2025-2 afp-2026-05-13
cd .. && ./manage_data.py update -y contrib/Isabelle2025-2_and_afp-2026-05-13.tar.zst
git add data/manifest.json
git commit -m "data: bump Isabelle+AFP tarball size"
git push

Download and unpack on another machine — mirror of the above:

./manage_data.py get -y contrib/Isabelle2025-2_and_afp-2026-05-13.tar.zst
cd contrib
tar --zstd -xf Isabelle2025-2_and_afp-2026-05-13.tar.zst   # overwrites Isabelle2025-2/ + afp-2026-05-13/

Más de este repositorio

mismo repositorio

missing-lemma-loop

xqyww123/MLML

Operational pipeline to start, monitor, STOP, and recover the MathBench missing-lemma loop running in multi-node fleet mode on the MBZUAI cluster (watcher + slurmx fleet REPLs + login-node RPC host + serial adjudication + phase-2 import reconciliation). Use when launching/resuming the fleet run, stopping it cleanly, recovering after a crash, or applying the hard-won operational rules (correct kill sequence, git safety on the shared checkout, shell/conda/timeout fixes, re-collection prerequisite). For the single-machine AoA×PutnamBench eval use `aoa-putnam-eval` instead; for the design rationale of the loop see `MISSING_LEMMA_LOOP.md`.

2026-07-205

sync-semantic-embedding-db

xqyww123/MLML

How to refresh the local semantic embedding database (~1.5 GB of LMDB at ~/.cache/Isabelle_Semantic_Embedding). The development channel is the Hugging Face Hub tarball via manage_data.py (get/update). End users instead pull it anonymously from Cloudflare R2 with `semantics_manage.py pull`. Use when setting up or refreshing the semantic DB on a machine, or when deformalizations / vector stores are stale or missing. Do NOT run R2 `push` — it overwrites the shared remote and is a human-only action.

2026-07-105

isabelle-intro-elim-rules

xqyww123/MLML

How to read Isabelle introduction and elimination rules

2026-06-115

mathbench-import-reconcile

xqyww123/MLML

Playbook for adding a new import to MathBench_ProverBase and reconciling any syntax conflicts (constant/type short-name resolution and notation) so that PutnamBench problems still parse to identical goal terms. Use when adding/changing imports of the MathBench_Prover session, or when investigating MathBench-vs-PutnamBench environment divergences.

2026-06-105

isabelle-datatype

xqyww123/MLML

How to read constants and theorems generated by Isabelle datatype and codatatype definitions

2026-06-045

isabelle-ml

xqyww123/MLML

Essential reference for all Isabelle/ML development — system library, data structures, exception handling, and coding patterns. Load this skill whenever writing or modifying Isabelle/ML code.

2026-06-045

name	sync-isabelle-afp-distribution
description	How to repackage/upload and download/unpack the Isabelle + paired AFP distribution, published together as contrib/Isabelle2025-2_and_afp-2026-05-13.tar.zst on the Hugging Face Hub (via manage_data.py update/get). Use when publishing a rebuilt Isabelle+AFP tarball (after isabelle scala_build, patches, etc.) or installing/refreshing the distribution on another machine.

Packaging and syncing the Isabelle + AFP distribution

Isabelle + its paired AFP snapshot are published together as contrib/Isabelle2025-2_and_afp-2026-05-13.tar.zst on the Hugging Face Hub.

cd contrib
tar --zstd -cvf Isabelle2025-2_and_afp-2026-05-13.tar.zst Isabelle2025-2 afp-2026-05-13
cd .. && ./manage_data.py update -y contrib/Isabelle2025-2_and_afp-2026-05-13.tar.zst
git add data/manifest.json
git commit -m "data: bump Isabelle+AFP tarball size"
git push

Download and unpack on another machine — mirror of the above:

./manage_data.py get -y contrib/Isabelle2025-2_and_afp-2026-05-13.tar.zst
cd contrib
tar --zstd -xf Isabelle2025-2_and_afp-2026-05-13.tar.zst   # overwrites Isabelle2025-2/ + afp-2026-05-13/