Jeden Skill in Manus ausführen
mit einem Klick

Jeden Skill in Manus mit einem Klick ausführen

sync-isabelle-afp-distribution

Sterne5

Forks0

Aktualisiert18. Juni 2026 um 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.

Installation

Mit Codex oder Claude installieren Kopieren Sie diesen Prompt, fügen Sie ihn in Codex, Claude oder einen anderen Assistant ein und lassen Sie die Skill-Seite prüfen und installieren.

In Manus ausführen

Quelle

xqyww123

xqyww123/MLML

GitHub-Repository öffnen Creator-Repositorys ansehen

Download

In Manus ausführen

Verwandte BerufeSOC

Basierend auf der SOC-Berufsklassifikation

Netzwerk- und ComputersystemadministratorenInformatik- und Mathematikberufe·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/

Mehr aus diesem Repository

gleiches Repository

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/