One place to unify all our work to make sure it is logically consistent with the tools we have built so far.
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.
Parent gitlink SHAs versus checkout main were not compared.
| Path | URL | Checkout SHA (module main) |
Purpose | State |
|---|---|---|---|---|
grok-build |
git@github.com:SurmountSystems/grok-build (gitmodules ../grok-build) |
5a251d02fe502233231325ca558e5da0d4d9ec7a |
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 |
7f4514b7fc8cb4b3ff0141bd4b2a00d2c3ec9029 |
Specs 0000 through 0012 and Lean | Populated. Nested gitlinks checked out. Superproject gitlink did not move. |
majestic |
/home/hunter/majestic |
bf0cb578859672eeb2dd8b95cd6091e622a08ccb |
Crate majestic, command memex (0012) |
Populated. 0.1 proof of concept. Local filesystem URL. |
surmount-server |
git@github.com:SurmountSystems/surmount-server |
60ca27c3af8fa4ab8207335772d0567d7babe00c |
Mail and web NixOS host | Populated. |
iso |
git@github.com:cryptoquick/systems-lean.git |
8feb42074b82777c861cd102a67adda208965197 |
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 |
74febda7679a858af666903756a191f7a0437482 |
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 74febda7679a858af666903756a191f7a0437482 |
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 8feb42074b82777c861cd102a67adda208965197 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 8feb42074b82777c861cd102a67adda208965197. 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.