The Tool nodes folio-assistant-sci declares in its tools graph — one instance’s slice of every instance’s tools.
A skill states a capability generically: what an actor needs to know to perform a task. A Tool is one concrete way to exercise it, with an installation, an invocation and typed inputs and outputs. One skill may be satisfied by several tools, and one tool may satisfy several skills.
They are separate graphs and this is the tools one. The relation between them
is satisfies, and it runs from a tool to a skill — this tool is one way
to do that, never this skill is a tool.
How they are invoked, and installed
A tool may declare more than one invocation, so these do not sum to the total.
| invocation | tools |
|---|---|
| shell | 6 |
| container | 1 |
| inProcess | 1 |
| mcp | 1 |
| installation | tools |
|---|---|
none | 7 |
container | 1 |
Does every satisfies name a skill that exists?
Yes — all 4 skills named across 8 tools resolve to a
skill document in this checkout. A satisfies pointing at nothing would be a
tool advertising a capability the graph cannot locate.
Every tool
| tool | what it does | invoked | satisfies | i/o |
|---|---|---|---|---|
latex-imageCompile LaTeX in a container | Compile a rendered paper’s main.tex with latexmk inside a TeX Live (full) image, for a host with Docker but no TeX engine. The image carries TeX Live, latexmk, Pandoc, latexdiff, graphviz and poppler-utils; it does not run the content pipeline, which renders the chapters on the host first. | container | latex-build-cache | 1 in / 1 out |
lean-cacheLake olean cache | Restore, verify, seed and diagnose the prebuilt .lake/ artefacts for a Lean package. Always try restore first: a from-source Mathlib build is 30–60 minutes, a restore about two. | shell | lean-cache-restore | 3 in / 1 out |
lean-formal-edgesFormal edges from the Lean build | Extract ELABORATED formal dependencies between a folio’s lean.ref declarations (LeanArchitect’s rule over the folio’s own lean.ref set). Needs a Lean toolchain and a built Lake project. Tagged declarations missing from the build are reported, never recorded as dependency-free; with ingest the result is recorded in the formal cache as source “elaborated”. | inProcess mcp | lean-formal-edges | 3 in / 1 out |
lean-html-docsBuild a Lean package’s HTML docs (doc-gen4) | Build the doc-gen4 HTML render of a folio’s Lake package — the visualiser of a declared lean directory — with lake -R -Kenv=dev build <Lib>:docs, cache-aware: refuses while another lake/lean process holds .lake/, refuses on a restored tree that carries no traces (a Lake build there EVICTS the cache), checks or restores the warm cache first, and enables a sentinel-commented doc-gen4 [[require]] for this build only, restoring the lakefile on exit. Never runs lake update. Output: <lake-root>/.lake/build/doc. | shell | lean-html-docs | 6 in / 1 out |
lean-kg-publishPublish the dynamic Lean viewer: doc-gen4 declaration data as knowledge-graph shards | Ingest doc-gen4’s per-module declaration data (.lake/build/doc-data/declaration-data-<Module>.bmp) into JSON-LD shards — one per module, with declaration nodes, imports edges and formalizes edges to the content blocks whose lean.ref names each declaration — and publish them under the folio’s site with a single viewer page that loads modules, signature chunks and the search list on demand. Signatures are chunked 500 declarations per file so a 12,804-declaration module stays usable. With --base it writes a STAGING overlay: only modules whose content hash differs from the published base, plus overlay.json; the viewer loads the rest from the base. Rails the viewer page with the same pass as lean-render-publish. | shell | lean-html-docs | 14 in / 1 out |
lean-render-publishPublish a Lean render under a folio site, with the harness rail | Stage a doc-gen4 render under a folio’s built site (<site>/<route>/, default lean/) and give every page the harness navbar and rail by running cat-harness/scripts/rail-standalone-pages.ts --foreign-site over the site — the same rail stage-folio-local.ts applies to the folio’s own pages. Leaves out Lake’s .hash/.trace bookkeeping, marks doc-gen4’s iframe navbar and find/ redirect folio-navbar: none so no rail is drawn inside the sidebar, adds a layout shim so the rail does not cover doc-gen4’s fixed sidebar, and with --modules prunes to the folio’s own modules, repointing links into dropped ones to the community docs. Then asserts every staged page is railed or declined. | shell | lean-html-docs | 9 in / 1 out |
paper-feature-buildPaper feature build (changed chapters + latexdiff) | Quick preview of a paper folio’s branch: render the paper with the sci print template (plus the folio’s notation fragment when it has one), then compile ONLY the chapters changed against a base ref, and a colored and a plain latexdiff of each. Margin notes are off by default (FAST_PREVIEW=1, about 2x). Cross-references to chapters outside the build print as ‘??’. A preview, never a publish build. Run from the folio. Without a TeX engine the render still runs and the compile steps are skipped with a message. | shell | latex-build-cache | 6 in / 1 out |
tex-installInstall TeX Live in a sandbox | Install TeX Live (full) and latexmk where no TeX engine is present, disabling the firewalled launchpad PPAs that otherwise abort apt-get update. Idempotent: does nothing when pdflatex and memoize.sty are already present. About 5 GB and 10-20 minutes, so run it in the background. pdflatex unpacks early but is not usable until the post-install format build ends (kpsewhich memoize.sty returning a path is the ready signal). | shell | latex-build-cache | 0 in / 1 out |