One place to unify all our work to make sure it is logically consistent with the tools we have built so far.
Standing process law for this superproject lives in AGENTS.md. That file is the company model: this tree coordinates member projects at L0. Nested product trees keep their own AGENTS.md. Session-board L0 (durable residual in a Grok OSS session) is a different namespace. This README is not that law.
This tree is git@github.com:SurmountSystems/surmount.git. Five product homes are already gitlinks and populated here: Grok OSS (grok-build), numbered specs (specs), Majestic Memex (majestic), Surmount Server (surmount-server), and Systems Lean (iso). Specs also declare three nested gitlinks that are populated at the pins below.
Checkout SHAs in the table below are each module origin/main.
| Path | URL | Checkout SHA (module main) |
Purpose | State |
|---|---|---|---|---|
grok-build |
git@github.com:SurmountSystems/grok-build (gitmodules ../grok-build) |
525538172dc21391bc690a4cc4a8706a5c554e47 |
Grok OSS (grok-oss) |
Populated. SOURCE_REV ea094a8c369475f97c85540d01730baec0dce5d6 is a different upstream export pin. FORK.md also names origin SurmountSystems/grok-oss. |
specs |
git@github.com:SurmountSystems/specs |
10389637869a725f463cf880d1fcd245cd9d5f01 |
Specs 0000 through 0012 and Lean | Populated. Nested gitlinks checked out at the same Form 1 pins. |
majestic |
/home/hunter/majestic |
8ca8308441f9b47b156e5c5b9133e0f4f6fb8608 |
Crate majestic, command memex (0012) |
Populated. 0.1 proof of concept. Local filesystem URL. |
surmount-server |
git@github.com:SurmountSystems/surmount-server |
6896f53a768670955b56159d471d62a4e54c0bc5 |
Mail and web NixOS host | Populated. |
iso |
git@github.com:SurmountSystems/systems-lean.git |
1af02f7fb33211955c70fbb2a91ff9845f6dc5a3 |
Systems Lean / Slake (0002) | Populated. Nested Lean 4, Idris 2, CompCert, and Rust under iso/ref/ were not fetched. |
specs/ref/semver |
https://github.com/semver/semver.git |
7c834b3f3a4940d77ab593bc32583004d6a426a9 (tag v2.0.0) |
Form 1 SemVer | Populated. |
specs/ref/btc-verified |
https://github.com/cryptoquick/btc-verified.git |
6c279c18914f5a22fb33e772f466b9362d6a4fcb |
Form 1 CompactSize proofs | Populated. |
specs/skills/lean4-skills |
git@github.com:SurmountSystems/lean4-skills.git |
b6243b85b9b0a0ddff5bb6773889044daf687f8e |
MIT Lean 4 skill pack | Populated. Not a Clause 12 pin. |
Nested specs Form 1 pins and lean4-skills are initialized at the SHAs in the table above. Do not fetch iso/ref/ engines unless named.
Do not add to specs ref/: Lean 4, Idris 2, CompCert, and Rust (they live under iso/ref/ and stay unfetched here). LMDB, LevelDB, RocksDB, SQLite, and heed. Form 2 RFC 2119, ECMA-48, and ITU-T T.416 stay ordinary files.
Do not add as superproject gitlinks without an operator decision: beastdb, SSSSS, fargo, Carbonado, SSSP, Lean Machine, SurmountSystems/site, grok-build third_party graph ports, Zed gpui, and coordinator-gui/.
| Component | Current home | Submodule? | Progress / state | Should become submodule? | Why |
|---|---|---|---|---|---|
| Grok OSS | grok-build/ |
yes | populated shipping fork | already | Superproject .gitmodules. |
| Numbered specs | specs/ |
yes | 0000-0012 published | already | Specs home. thisRepoSeparates. |
| SemVer pin | specs/ref/semver |
yes (nested) | populated 7c834b3f3a4940d77ab593bc32583004d6a426a9 |
already | Form 1. |
| btc-verified pin | specs/ref/btc-verified |
yes (nested) | populated 6c279c18914f5a22fb33e772f466b9362d6a4fcb |
already | Form 1. |
| lean4-skills | specs/skills/lean4-skills |
yes (nested) | populated b6243b85b9b0a0ddff5bb6773889044daf687f8e |
already | Skill pack, not Clause 12. |
| RFC 2119 / ECMA-48 / T.416 | specs/ref/ |
no | Form 2 files present | no | No publisher git. |
| Majestic Memex | majestic/ and ~/majestic |
yes | 0.1 proof of concept | already | 0012. |
| Surmount Server | surmount-server/ |
yes | live host product | already | Superproject. |
| Server operator crates | surmount-server/crates/ |
no | in that repo | no | Stay in-tree of that product. |
| Public site | flake input | no | locked in flake.lock |
unknown | Nix git fetch, not a gitlink. |
| Systems Lean / Slake | iso/ |
yes | populated 1af02f7fb33211955c70fbb2a91ff9845f6dc5a3 without recursive engines |
already | 0002 home. |
| Lean 4, CompCert, Idris 2, Rust | iso ref/ |
yes, in iso | named in 0002 | no, not here | Must not copy into specs ref/. |
| beastdb product | none claimed | no | ongoing, not ready | unknown | No path. |
| SSSSS product | none claimed | no | ongoing, not ready | unknown | No path. |
| CI (0007) | specs contract | no | ongoing, not ready | no | Process spec, not a repo. |
| CATE / RSI / DOGE / Unlicense / Formal Vibefication | specs | no | published contracts | no | Stay in specs. |
| Tech Tree (0011) | specs graph | no | Lake-local .sstt writer |
no | Not a shipped product tree. |
| fargo | unspecified | no | grok-oss residual owner | unknown | No number, no repo. |
| Carbonado | unspecified | no | deferred | no numbered file | Residual forbids inventing one. |
| SSSP, Lean Machine | named only | no | unspecified | unknown | No files. |
grok-build third_party mermaid/dagre |
grok-build/third_party/ |
no | in-tree ports | no | First-party-adjacent. |
| crates.io vendoring | deleted from grok-build | no | fargo unwind | no | grok-build AGENTS.md constraint 21. |
coordinator-gui |
superproject ordinary files | no | path dep missing | unknown | Broken path to grok-build crate; Zed pin outside. |
| Zed gpui | ../../zed |
no | path pin | unknown | Not Surmount product law. |
The superproject already holds every Surmount git home that exists in this checkout, including iso at 1af02f7fb33211955c70fbb2a91ff9845f6dc5a3. Specs law is strict about what must not be a submodule of specs. Nested specs gitlinks are populated. Fetching iso nested engines is a later operator choice. Readiness of beastdb, SSSSS, and CI is blocked by product work, not by missing gitlinks. Spec 0010: thisRepoSeparates and productTreeUnifies MAY both hold because they name different homes.
Solid arrows are uses, cites, or a required pin. Dotted arrows are blocked-by unspecified or not-ready product, or optional later load (0012 MAY load .sstt files without mixing formats).
flowchart TB
spec0000["0000 spec spec"]
rfc2119["ref/rfc2119 Form 2"]
semver["ref/semver Form 1"]
spec0005["0005 CATE"]
spec0008["0008 Formal Vibefication"]
spec0009["0009 Unlicense"]
spec0006["0006 RSI"]
spec0001["0001 DOGE"]
ecma["ref/ecma48 Form 2"]
t416["ref/itu_t416 Form 2"]
spec0002["0002 Systems Lean"]
iso["iso product tree"]
lean4["ref/lean4 in iso"]
idris["ref/Idris2 in iso"]
compcert["ref/CompCert in iso"]
rust["ref/rust in iso"]
spec0003["0003 beastdb"]
spec0004["0004 SSSSS"]
spec0007["0007 CI"]
spec0010["0010 Surmount Systems"]
spec0011["0011 Tech Tree"]
btc["ref/btc-verified Form 1"]
spec0012["0012 Majestic Memex"]
majestic["crate majestic ~/majestic"]
fargo["fargo unspecified"]
carbonado["Carbonado unspecified"]
leanmachine["Lean Machine unspecified"]
grok["grok-build Grok OSS"]
server["surmount-server"]
site["SurmountSystems/site flake"]
specsrepo["specs repository"]
spec0000 --> rfc2119
spec0000 --> spec0005
spec0001 --> spec0000
spec0001 --> ecma
spec0001 --> t416
spec0002 --> spec0000
spec0002 --> semver
spec0002 --> iso
iso --> lean4
iso --> idris
iso --> compcert
iso --> rust
spec0003 --> spec0000
spec0003 --> spec0002
spec0003 -.-> fargo
spec0003 -.-> carbonado
spec0004 --> spec0002
spec0004 --> spec0003
spec0004 -.-> leanmachine
spec0006 --> spec0000
spec0006 --> spec0005
spec0007 --> spec0000
spec0007 --> spec0005
spec0007 --> spec0006
spec0007 --> spec0002
spec0007 --> spec0003
spec0007 --> spec0004
spec0008 --> spec0000
spec0009 --> spec0000
spec0010 --> spec0002
spec0010 --> spec0003
spec0010 --> spec0004
spec0010 --> spec0005
spec0010 --> spec0006
spec0010 --> spec0007
spec0010 --> spec0008
spec0010 --> spec0009
spec0010 --> spec0011
spec0010 --> spec0012
spec0011 --> spec0000
spec0011 --> spec0010
spec0011 --> btc
spec0012 --> spec0000
spec0012 --> spec0005
spec0012 --> spec0008
spec0012 --> spec0009
spec0012 --> spec0010
spec0012 --> spec0011
spec0012 --> majestic
majestic -.-> spec0011
spec0003 -.-> iso
spec0004 -.-> iso
grok -.-> fargo
server --> site
specsrepo --> spec0000
0010 composes 0002 through 0012. 0002 feeds 0003 and 0004 and the iso tree. 0012 may later load 0011 .sstt files without mixing formats.