تشغيل أي مهارة في Manus بنقرة واحدة

repo-tour

النجوم٢

التفرعات١

آخر تحديث٣ يوليو ٢٠٢٦ في ١٧:٢٥

Get oriented in the Factoidal repository layout. Use when starting work on a fresh clone, when asked "where does X live?", or when a doc references a path that's unfamiliar. Maps the dual nature of the project (verified F* spec is the product; everything else is plumbing or build artifacts).

التثبيت

التثبيت باستخدام Codex أو Claude انسخ هذا Prompt والصقه في Codex أو Claude أو مساعد آخر ليراجع صفحة Skill ويثبّتها لك.

تشغيل في Manus

المصدر

danbri

danbri/factoidal

فتح مستودع GitHub عرض مستودعات المنشئ

تنزيل

تشغيل في Manus

المهن ذات الصلةSOC

استنادا إلى تصنيف SOC المهني

مطوّرو البرمجياتمهن الحاسوب والرياضيات·SOC 15-1252

SKILL.md

readonly

name	repo-tour
description	Get oriented in the Factoidal repository layout. Use when starting work on a fresh clone, when asked "where does X live?", or when a doc references a path that's unfamiliar. Maps the dual nature of the project (verified F* spec is the product; everything else is plumbing or build artifacts).

Factoidal — repository tour

The product is the F* spec. Everything else is plumbing for getting the F* code into runnable form (extraction, compilation, tests) or project documentation. The directory layout makes that visible.

factoidal/
├── CLAUDE.md                     short-and-tight project rules
├── README.md                     public-facing project overview
├── formal/                       VERIFIED CORE
│   ├── fstar/                    main F* tree (the product)
│   │   ├── *.fst                 verified specs
│   │   ├── Makefile              verify target
│   │   ├── build-ocaml.sh        F* → OCaml → JS/WASM pipeline
│   │   ├── ocaml-patches.sh      applies all glue patches
│   │   ├── ocaml-output/         extracted .ml + symlinks to bin/
│   │   │   ├── *.ml              extracted F* OCaml output (tracked)
│   │   │   ├── fstar_pure_hashes.ml   allowlisted hand-written assume-val realisation
│   │   │   └── sparql_parser_stubs.ml allowlisted hand-written assume-val realisation
│   │   ├── minimal_regrettable_glue_code_each_with_an_open_issue/
│   │   │   └── <issue>_*.sh      assume-val realisations + bug fixes
│   │   ├── experimental_ocaml_glue/    Layer-2 unwind targets (rule #11 violators)
│   │   ├── krml-output/          F* → .krml output (gitignored, C-build pilot)
│   │   └── c-output/             krml → .c output (gitignored, future)
│   ├── roaring/                  Roaring bitmap F* port
│   │   ├── src/
│   │   │   ├── Spec.fst              abstract roaring set
│   │   │   ├── Bits.fst              popcount/tzcnt
│   │   │   ├── Container.{Array,Bitmap,Run}.fst
│   │   │   ├── IODemo.fst            file round-trip demo
│   │   │   ├── Test.fst              verification-only tests
│   │   │   ├── Makefile              standalone verify/extract/demo
│   │   │   └── iterate.sh            one-shot verify-all loop
│   │   ├── README.md
│   │   └── paper/roaring.{pdf,txt}   reference paper
│   └── third_party/              future home for vendored F* deps
│       └── (e.g. hacl-star/ for SHA-256 — see io-verification doc)
├── bin/                          BINARIES + CONSUMER SOURCES
│   ├── darwin-arm64/             committed binaries, macOS Apple Silicon
│   ├── linux-x86_64/             committed binaries, Linux x86-64 (static):
│   │                             factoidal, w3c_runner, owl_runner,
│   │                             rdfc10_runner, factoidal-http, …
│   ├── ci-linux-x86_64/          CI shadow builds (Fly deploy source of truth)
│   ├── ci-darwin-arm64/          CI shadow builds
│   └── <consumer>/               hand-written consumer .ml sources:
│                                 factoidal-cli/, w3c-runner/, owl-runner/,
│                                 factoidal-http/, factoidal-serve/, … (rule #11)
├── third_party/                  VENDORED CORPORA + DATA
│   ├── testing/                  W3C test fixture submodules
│   │   ├── w3c/                  rdf-tests submodule
│   │   ├── rdf-canon/            RDFC-1.0 tests
│   │   ├── csvw/                 CSVW tests
│   │   ├── rml/                  RML tests
│   │   ├── shex/                 ShEx tests
│   │   ├── vc/                   Verifiable Credentials tests
│   │   └── did/                  DID tests
│   ├── data/                     vendored datasets (e.g. Wikidata samples)
│   └── README.md
├── docs/
│   ├── claude-rules/             expanded Claude rules
│   │   ├── anti-patterns.md      full text of the 25 numbered rules
│   │   ├── current-state.md      F* inventory, assume-val table, scores
│   │   ├── performance.md        Turtle parser audit, speed plan
│   │   ├── scope.md
│   │   └── README.md             index
│   ├── designissues/             architecture decisions
│   │   ├── 2026-05-07-c-build-and-roaring-plan.md
│   │   ├── 2026-05-07-query-planning-fstar-recovery.md
│   │   ├── 2026-05-07-io-verification-and-third-party.md
│   │   ├── fstar-purity-unwind.md
│   │   ├── fstar-ocaml-boundary-audit.md
│   │   └── (many historical drift / fix design docs)
│   ├── skills/                   RETIRED (pre-pivot Rust-era; see README there)
│   ├── code-name-glossary.md     Yod6 / Tet3 / etc. — historical decoder ring
│   ├── test-results/
│   │   ├── latest.json           most recent W3C run (CI-maintained)
│   │   ├── ukparliament-bench-modern.json   perf baseline (harness-maintained)
│   │   ├── history/              timestamped snapshots
│   │   └── index.html            dashboard (deployed to gh-pages)
│   ├── web/                      landing page + demo pages
│   ├── deploy/                   Fly.io / Cloudflare tunnel notes
│   └── fstar-extracted/          js_of_ocaml + wasm bundles for browser demo
├── skills/                       SKILL FILES (agentskills.io format)
│   └── <name>/SKILL.md           listed in CLAUDE.md's ## Skills section
├── tests/                        first-party harnesses (unit, local
│                                 regressions, beyond-w3c parity, web-demos)
├── tools/                        probes + benches (jena_arq_*, bench_ukpar_*)
├── .claude/
│   ├── settings.json             permissions, hooks
│   └── settings.local.json       local overrides
├── .github/
│   ├── workflows/                CI configs
│   │   ├── check-extraction.yml
│   │   ├── check-fstar-purity.yml      (Omega3 — rule #11 gate)
│   │   ├── w3c-tests.yml
│   │   └── (...)
│   └── scripts/
├── kgx/                          SPARQL CONSTRUCT queries (future)
├── design_issues/                older design notes (e.g. roaring_fstar_plan.md)
└── junk/do_not_use/              vibe-coded artifacts (DO NOT USE)

"Where do I add a new ___?"

Adding	Goes in
F* spec module	`formal/fstar/<Module>.fst` (or `formal/roaring/src/` for roaring) — and add to ALL THREE lists in `build-ocaml.sh` (extract loop, `COMMON_MODULES`, `FSTAR_MODULES`); see the `fstar-module-style` skill for which tier it belongs to
Hand-written CLI/runner/server tool	`bin/<consumer>/` (Phase 8 relocation is done — nothing hand-written goes in `ocaml-output/` except the two allowlisted assume-val realisations)
`assume val` realisation	A patch file in `formal/fstar/minimal_regrettable_glue_code_each_with_an_open_issue/<issue>_<desc>.sh` referenced by `ocaml-patches.sh` + an open GitHub issue
Vendored 3rd-party F* code	`formal/third_party/<lib>/` (see I/O verification design doc)
Architecture decision doc	`docs/designissues/<YYYY-MM-DD>-<topic>.md`
How-to / operational guide	`skills/<topic>/SKILL.md` (agentskills.io format; add it to CLAUDE.md's `## Skills` section)
Anti-pattern war story	New numbered entry in `docs/claude-rules/anti-patterns.md`; one-line summary in `CLAUDE.md`
W3C test data	Don't add — submodules under `third_party/testing/`. Update the submodule pin if the W3C suite version changes
External (non-W3C) test suite	`tests/external/<project>/` + `THIRD_PARTY_NOTICES.md` (licence-clean only; see `test-suites` skill)

"I see X in a commit message — what's it mean?"

Yod6, Tet3, Lamed3, Mem5, Pe5, Bet7, Tav5, Heth3, Vav3, Psi3, …: see docs/code-name-glossary.md. No new short-codes. Use descriptive names for new things.
Omega3: F*-purity CI gate (.github/workflows/check-fstar-purity.yml).
Mim3, Mim2: pre-warm fallback infrastructure (mostly retired).

The recovery plan (docs/designissues/2026-05-07-query-planning-fstar-recovery.md) maps every short-code to a real name + target F* module.

What this skill does NOT do

Doesn't navigate inside files — for that, just open them.
Doesn't track every tweak to the layout — major moves are recorded in docs/designissues/ plan docs.

المزيد من هذا المستودع

نفس المستودع

test-suites

danbri/factoidal

Run and interpret every test suite in the Factoidal project — W3C conformance (SPARQL 1.1, RDF 1.1/1.2 syntax, rdf-mt, RDF canonicalization, OWL 2), local regression scripts, cross-runtime parity (native/JS/wasm), Apache Jena ARQ comparison probes, running only the suites a diff touches (`tools/affected-tests.sh`), regression-pinning discipline (write the failing test before the fix, confirm it fails for the right reason), and the policy for importing external suites. Use when the user asks to "run the tests", "check conformance", "compare against Jena", to investigate a score change, when landing a bug fix and deciding which regression to write, or before claiming any change is done. Testing (with perf measured separately — see perf-benchmarking) drives everything in this project.

2026-07-172

markdown-style

danbri/factoidal

Markdown formatting + prose register for Claude-generated text in this repository — chat replies, design docs, READMEs, PR bodies, commit messages. Two load-bearing rules. (1) Links must be unambiguously clickable — bold/italic emphasis around URLs and link syntax frequently breaks the click target. (2) No sycophantic adjectives — drop "honest", "genuine", "important", "critical", "big picture", "key insight", "headline", and similar candor-performance words. Use whenever generating user-facing markdown that may be rendered in different clients (CLI, web, mobile chat, GitHub).

2026-07-152

disk-storage-format

danbri/factoidal

How Factoidal stores RDF data on disk — the COTTAS/Parquet base file, its 11 sidecars, the durable-UPDATE delta log, the compacted-epoch marker, and the symlink-current versioning layout. Use when asked how data is stored on disk, when adding a new on-disk companion file, when a magic-number/framing question comes up (DLE1/DLB1/DLOG/CEP1/COTD/COTP/COTO/COPO/COTS), when running import/query/compact/serve against a COTTAS store, or when auditing rule

2026-07-132

subagent-prompting

danbri/factoidal

How to write subagent prompts for the Factoidal repo so the agent's work actually lands cleanly. Use whenever you dispatch a subagent with the Agent tool, especially with `isolation: "worktree"`. Two load-bearing rules. (1) Path discipline — agents must use only paths under their worktree, not absolute paths from your prompt context. (2) Post-condition checks — agent must verify its main-worktree footprint is zero before reporting back. Also carries MANDATORY brief inclusions for build-list edits (only while `.build-running` is absent), the F*/OCaml comment-nesting trap, and iron rule #11 (no hand-editing extracted `.ml`) — plus the one-agent-one-commit and ship-code-sketches rules. Pairs with workflow-gotchas-debugging (which catalogues recovery steps when these rules are violated).

2026-07-132

fstar-env

danbri/factoidal

Set up or repair the F* / opam / z3 toolchain for the Factoidal project. Use when the user asks to install or set up F*, when `fstar.exe` is missing from PATH, when z3 has the wrong version (must be 4.13.3), when `make verify` or `build-ocaml.sh` fails with toolchain errors, when starting on a fresh clone that hasn't been bootstrapped, or when an agent has been "burning time on partial builds" because the opam switch isn't activated.

2026-07-112

session-restore

danbri/factoidal

Restore a fresh or recycled VM/container/session to full working state in minutes, not hours — the cache inventory (toolchain-cache branch, .checked verification cache, pycottas venv, skill symlinks), what the bootstrap hook restores automatically vs what needs a command, the wasm_of_ocaml/binaryen ≥116 install path (proxy-blocked release binaries, conda-forge fallback), and the never-again rules from the 2026-07-03 session that burned ~90 minutes compiling F* from source twice. Use on any fresh clone, restored VM, new sandbox, when fstar.exe or test data is missing, when a wasm build fails on a missing `wasm-merge`, when a session is about to do something expensive that a previous session already did, or when adding a new cache-worthy artifact.

2026-07-112

Factoidal — repository tour

The product is the F* spec. Everything else is plumbing for getting the F* code into runnable form (extraction, compilation, tests) or project documentation. The directory layout makes that visible.

factoidal/ ├── CLAUDE.md short-and-tight project rules ├── README.md public-facing project overview ├── formal/ VERIFIED CORE │ ├── fstar/ main F* tree (the product) │ │ ├── *.fst verified specs │ │ ├── Makefile verify target │ │ ├── build-ocaml.sh F* → OCaml → JS/WASM pipeline │ │ ├── ocaml-patches.sh applies all glue patches │ │ ├── ocaml-output/ extracted .ml + symlinks to bin/ │ │ │ ├── *.ml extracted F* OCaml output (tracked) │ │ │ ├── fstar_pure_hashes.ml allowlisted hand-written assume-val realisation │ │ │ └── sparql_parser_stubs.ml allowlisted hand-written assume-val realisation │ │ ├── minimal_regrettable_glue_code_each_with_an_open_issue/ │ │ │ └── <issue>_*.sh assume-val realisations + bug fixes │ │ ├── experimental_ocaml_glue/ Layer-2 unwind targets (rule #11 violators) │ │ ├── krml-output/ F* → .krml output (gitignored, C-build pilot) │ │ └── c-output/ krml → .c output (gitignored, future) │ ├── roaring/ Roaring bitmap F* port │ │ ├── src/ │ │ │ ├── Spec.fst abstract roaring set │ │ │ ├── Bits.fst popcount/tzcnt │ │ │ ├── Container.{Array,Bitmap,Run}.fst │ │ │ ├── IODemo.fst file round-trip demo │ │ │ ├── Test.fst verification-only tests │ │ │ ├── Makefile standalone verify/extract/demo │ │ │ └── iterate.sh one-shot verify-all loop │ │ ├── README.md │ │ └── paper/roaring.{pdf,txt} reference paper │ └── third_party/ future home for vendored F* deps │ └── (e.g. hacl-star/ for SHA-256 — see io-verification doc) ├── bin/ BINARIES + CONSUMER SOURCES │ ├── darwin-arm64/ committed binaries, macOS Apple Silicon │ ├── linux-x86_64/ committed binaries, Linux x86-64 (static): │ │ factoidal, w3c_runner, owl_runner, │ │ rdfc10_runner, factoidal-http, … │ ├── ci-linux-x86_64/ CI shadow builds (Fly deploy source of truth) │ ├── ci-darwin-arm64/ CI shadow builds │ └── <consumer>/ hand-written consumer .ml sources: │ factoidal-cli/, w3c-runner/, owl-runner/, │ factoidal-http/, factoidal-serve/, … (rule #11) ├── third_party/ VENDORED CORPORA + DATA │ ├── testing/ W3C test fixture submodules │ │ ├── w3c/ rdf-tests submodule │ │ ├── rdf-canon/ RDFC-1.0 tests │ │ ├── csvw/ CSVW tests │ │ ├── rml/ RML tests │ │ ├── shex/ ShEx tests │ │ ├── vc/ Verifiable Credentials tests │ │ └── did/ DID tests │ ├── data/ vendored datasets (e.g. Wikidata samples) │ └── README.md ├── docs/ │ ├── claude-rules/ expanded Claude rules │ │ ├── anti-patterns.md full text of the 25 numbered rules │ │ ├── current-state.md F* inventory, assume-val table, scores │ │ ├── performance.md Turtle parser audit, speed plan │ │ ├── scope.md │ │ └── README.md index │ ├── designissues/ architecture decisions │ │ ├── 2026-05-07-c-build-and-roaring-plan.md │ │ ├── 2026-05-07-query-planning-fstar-recovery.md │ │ ├── 2026-05-07-io-verification-and-third-party.md │ │ ├── fstar-purity-unwind.md │ │ ├── fstar-ocaml-boundary-audit.md │ │ └── (many historical drift / fix design docs) │ ├── skills/ RETIRED (pre-pivot Rust-era; see README there) │ ├── code-name-glossary.md Yod6 / Tet3 / etc. — historical decoder ring │ ├── test-results/ │ │ ├── latest.json most recent W3C run (CI-maintained) │ │ ├── ukparliament-bench-modern.json perf baseline (harness-maintained) │ │ ├── history/ timestamped snapshots │ │ └── index.html dashboard (deployed to gh-pages) │ ├── web/ landing page + demo pages │ ├── deploy/ Fly.io / Cloudflare tunnel notes │ └── fstar-extracted/ js_of_ocaml + wasm bundles for browser demo ├── skills/ SKILL FILES (agentskills.io format) │ └── <name>/SKILL.md listed in CLAUDE.md's ## Skills section ├── tests/ first-party harnesses (unit, local │ regressions, beyond-w3c parity, web-demos) ├── tools/ probes + benches (jena_arq_*, bench_ukpar_*) ├── .claude/ │ ├── settings.json permissions, hooks │ └── settings.local.json local overrides ├── .github/ │ ├── workflows/ CI configs │ │ ├── check-extraction.yml │ │ ├── check-fstar-purity.yml (Omega3 — rule #11 gate) │ │ ├── w3c-tests.yml │ │ └── (...) │ └── scripts/ ├── kgx/ SPARQL CONSTRUCT queries (future) ├── design_issues/ older design notes (e.g. roaring_fstar_plan.md) └── junk/do_not_use/ vibe-coded artifacts (DO NOT USE)

"Where do I add a new ___?"

Adding

Goes in

F* spec module

formal/fstar/<Module>.fst (or formal/roaring/src/ for roaring) — and add to ALL THREE lists in build-ocaml.sh (extract loop, COMMON_MODULES, FSTAR_MODULES); see the fstar-module-style skill for which tier it belongs to

Hand-written CLI/runner/server tool

bin/<consumer>/ (Phase 8 relocation is done — nothing hand-written goes in ocaml-output/ except the two allowlisted assume-val realisations)

assume val realisation

A patch file in formal/fstar/minimal_regrettable_glue_code_each_with_an_open_issue/<issue>_<desc>.sh referenced by ocaml-patches.sh + an open GitHub issue

Vendored 3rd-party F* code

formal/third_party/<lib>/ (see I/O verification design doc)

Architecture decision doc

docs/designissues/<YYYY-MM-DD>-<topic>.md

How-to / operational guide

skills/<topic>/SKILL.md (agentskills.io format; add it to CLAUDE.md's ## Skills section)

Anti-pattern war story

New numbered entry in docs/claude-rules/anti-patterns.md; one-line summary in CLAUDE.md

W3C test data

Don't add — submodules under third_party/testing/. Update the submodule pin if the W3C suite version changes

External (non-W3C) test suite

tests/external/<project>/ + THIRD_PARTY_NOTICES.md (licence-clean only; see test-suites skill)

"I see X in a commit message — what's it mean?"

Yod6, Tet3, Lamed3, Mem5, Pe5, Bet7, Tav5, Heth3, Vav3, Psi3, …: see docs/code-name-glossary.md. No new short-codes. Use descriptive names for new things.

Omega3: F*-purity CI gate (.github/workflows/check-fstar-purity.yml).

Mim3, Mim2: pre-warm fallback infrastructure (mostly retired).

The recovery plan (docs/designissues/2026-05-07-query-planning-fstar-recovery.md) maps every short-code to a real name + target F* module.

What this skill does NOT do

Doesn't navigate inside files — for that, just open them.

Doesn't track every tweak to the layout — major moves are recorded in docs/designissues/ plan docs.