Build tooling: updated OCaml bootstrapper, compile-modules, bundle.sh, sx-build-all. WASM browser: rebuilt sx_browser.bc.js/wasm, sx-platform-2.js, .sxbc bytecode files. CSSX/Tailwind: reworked cssx.sx templates and tw-layout, added tw-type support. Content: refreshed essays, plans, geography, reactive islands, docs, demos, handlers. New tools: bisect_sxbc.sh, test-spa.js, render-trace.sx, morph playwright spec. Tests: added test-match.sx, test-examples.sx, updated test-tw.sx and web tests. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
237 lines
14 KiB
Plaintext
237 lines
14 KiB
Plaintext
;; ---------------------------------------------------------------------------
|
|
;; Self-Hosting Bootstrapper — py.sx (COMPLETE)
|
|
;; ---------------------------------------------------------------------------
|
|
;; @css bg-green-100 text-green-800 bg-green-50 border-green-200 text-green-700 text-green-600
|
|
|
|
(defcomp ~plans/self-hosting-bootstrapper/plan-self-hosting-bootstrapper-content ()
|
|
(~docs/page :title "Self-Hosting Bootstrapper"
|
|
|
|
;; -----------------------------------------------------------------------
|
|
;; Status banner
|
|
;; -----------------------------------------------------------------------
|
|
|
|
(div (~tw :tokens "rounded-lg bg-green-50 border border-green-200 p-4 mb-8")
|
|
(div (~tw :tokens "flex items-center gap-3")
|
|
(span (~tw :tokens "inline-flex items-center rounded-full bg-green-100 px-3 py-1 text-sm font-semibold text-green-800")
|
|
"Complete")
|
|
(p (~tw :tokens "text-green-700 text-sm")
|
|
(code "py.sx") " is implemented and verified. G0 == G1: 128/128 defines match, "
|
|
"1490 lines, 88,955 bytes — byte-for-byte identical. "
|
|
(a :href "/sx/(language.(bootstrapper.self-hosting))" (~tw :tokens "underline text-green-600 font-medium")
|
|
"See live verification."))))
|
|
|
|
;; -----------------------------------------------------------------------
|
|
;; The Idea
|
|
;; -----------------------------------------------------------------------
|
|
|
|
(~docs/section :title "The Idea" :id "idea"
|
|
(p "We have " (code "bootstrap_py.py") " — a Python program that reads "
|
|
(code ".sx") " spec files and emits " (code "sx_ref.py")
|
|
", a standalone Python evaluator. It's a compiler written in the host language.")
|
|
(p "We also have " (code "z3.sx") " — a translator written in SX itself that "
|
|
"converts SX spec declarations into SMT-LIB for Z3. It's proof that "
|
|
"SX can generate code in another language.")
|
|
(p (strong "py.sx") " — an SX-to-Python translator written in SX. "
|
|
"Feed it through the existing Python evaluator against the spec files and it produces "
|
|
(code "sx_ref.py") ". The bootstrapper bootstraps itself.")
|
|
(p (code "py.sx") " produces output identical to " (code "bootstrap_py.py")
|
|
". The Python bootstrapper is redundant. "
|
|
"The spec defines itself."))
|
|
|
|
;; -----------------------------------------------------------------------
|
|
;; Results
|
|
;; -----------------------------------------------------------------------
|
|
|
|
(~docs/section :title "Results" :id "results"
|
|
(div (~tw :tokens "overflow-x-auto rounded border border-stone-200 my-4")
|
|
(table (~tw :tokens "w-full text-sm")
|
|
(thead (~tw :tokens "bg-stone-50")
|
|
(tr
|
|
(th (~tw :tokens "px-4 py-2 text-left font-semibold text-stone-700") "Metric")
|
|
(th (~tw :tokens "px-4 py-2 text-left font-semibold text-stone-700") "Value")))
|
|
(tbody
|
|
(tr (~tw :tokens "border-t border-stone-100")
|
|
(td (~tw :tokens "px-4 py-2 text-stone-600") "py.sx size")
|
|
(td (~tw :tokens "px-4 py-2 font-mono") "1,182 lines"))
|
|
(tr (~tw :tokens "border-t border-stone-100")
|
|
(td (~tw :tokens "px-4 py-2 text-stone-600") "bootstrap_py.py size (replaced)")
|
|
(td (~tw :tokens "px-4 py-2 font-mono") "902 lines (PyEmitter class)"))
|
|
(tr (~tw :tokens "border-t border-stone-100")
|
|
(td (~tw :tokens "px-4 py-2 text-stone-600") "Defines translated")
|
|
(td (~tw :tokens "px-4 py-2 font-mono") "128/128 exact match"))
|
|
(tr (~tw :tokens "border-t border-stone-100")
|
|
(td (~tw :tokens "px-4 py-2 text-stone-600") "Spec files processed")
|
|
(td (~tw :tokens "px-4 py-2 font-mono") "7 (eval, forms, render, adapter-html, adapter-sx, deps, signals)"))
|
|
(tr (~tw :tokens "border-t border-stone-100")
|
|
(td (~tw :tokens "px-4 py-2 text-stone-600") "Output size")
|
|
(td (~tw :tokens "px-4 py-2 font-mono") "1,490 lines / 88,955 bytes"))
|
|
(tr (~tw :tokens "border-t border-stone-100 bg-green-50")
|
|
(td (~tw :tokens "px-4 py-2 font-semibold text-green-700") "G0 == G1")
|
|
(td (~tw :tokens "px-4 py-2 font-semibold text-green-700") "Identical (diff is empty)"))))))
|
|
|
|
;; -----------------------------------------------------------------------
|
|
;; Architecture
|
|
;; -----------------------------------------------------------------------
|
|
|
|
(~docs/section :title "Architecture" :id "architecture"
|
|
(p "Three bootstrapper generations:")
|
|
(div (~tw :tokens "overflow-x-auto rounded border border-stone-200 my-4")
|
|
(table (~tw :tokens "w-full text-sm")
|
|
(thead (~tw :tokens "bg-stone-50")
|
|
(tr
|
|
(th (~tw :tokens "px-4 py-2 text-left font-semibold text-stone-700") "Gen")
|
|
(th (~tw :tokens "px-4 py-2 text-left font-semibold text-stone-700") "Source")
|
|
(th (~tw :tokens "px-4 py-2 text-left font-semibold text-stone-700") "Runs on")
|
|
(th (~tw :tokens "px-4 py-2 text-left font-semibold text-stone-700") "Reads")
|
|
(th (~tw :tokens "px-4 py-2 text-left font-semibold text-stone-700") "Produces")))
|
|
(tbody
|
|
(tr (~tw :tokens "border-t border-stone-100")
|
|
(td (~tw :tokens "px-4 py-2 font-mono text-stone-600") "G0")
|
|
(td (~tw :tokens "px-4 py-2") (code "bootstrap_py.py"))
|
|
(td (~tw :tokens "px-4 py-2") "Python (manual)")
|
|
(td (~tw :tokens "px-4 py-2") (code "eval.sx") ", " (code "render.sx") ", ...")
|
|
(td (~tw :tokens "px-4 py-2") (code "sx_ref.py")))
|
|
(tr (~tw :tokens "border-t border-stone-100 bg-green-50")
|
|
(td (~tw :tokens "px-4 py-2 font-mono text-green-700") "G1")
|
|
(td (~tw :tokens "px-4 py-2") (code "py.sx"))
|
|
(td (~tw :tokens "px-4 py-2") "Python evaluator + SX")
|
|
(td (~tw :tokens "px-4 py-2") (code "eval.sx") ", " (code "render.sx") ", ...")
|
|
(td (~tw :tokens "px-4 py-2 font-semibold text-green-700") (code "sx_ref.py") " (identical)"))
|
|
(tr (~tw :tokens "border-t border-stone-100")
|
|
(td (~tw :tokens "px-4 py-2 font-mono text-stone-600") "G2")
|
|
(td (~tw :tokens "px-4 py-2") (code "py.sx"))
|
|
(td (~tw :tokens "px-4 py-2") (code "sx_ref.py") " from G1 + SX")
|
|
(td (~tw :tokens "px-4 py-2") (code "eval.sx") ", " (code "render.sx") ", ...")
|
|
(td (~tw :tokens "px-4 py-2") (code "sx_ref.py") " (fixed-point)")))))
|
|
|
|
(p "G0 is the hand-written compiler. G1 replaces it with SX. "
|
|
"G2 proves the fixed-point: " (code "py.sx") " compiled by its own output "
|
|
"produces the same output. That's the definition of self-hosting."))
|
|
|
|
;; -----------------------------------------------------------------------
|
|
;; Translation Rules
|
|
;; -----------------------------------------------------------------------
|
|
|
|
(~docs/section :title "Translation Rules" :id "translation"
|
|
|
|
(~docs/subsection :title "Name Mangling"
|
|
(p "SX identifiers become valid Python identifiers. "
|
|
"The RENAMES dict (200+ entries) handles explicit mappings; "
|
|
"general rules handle the rest:")
|
|
(div (~tw :tokens "overflow-x-auto rounded border border-stone-200 my-4")
|
|
(table (~tw :tokens "w-full text-sm")
|
|
(thead (~tw :tokens "bg-stone-50")
|
|
(tr
|
|
(th (~tw :tokens "px-4 py-2 text-left font-semibold text-stone-700") "SX")
|
|
(th (~tw :tokens "px-4 py-2 text-left font-semibold text-stone-700") "Python")
|
|
(th (~tw :tokens "px-4 py-2 text-left font-semibold text-stone-700") "Rule")))
|
|
(tbody
|
|
(tr (~tw :tokens "border-t border-stone-100")
|
|
(td (~tw :tokens "px-4 py-2 font-mono") "eval-expr")
|
|
(td (~tw :tokens "px-4 py-2 font-mono") "eval_expr")
|
|
(td (~tw :tokens "px-4 py-2") "kebab → snake"))
|
|
(tr (~tw :tokens "border-t border-stone-100")
|
|
(td (~tw :tokens "px-4 py-2 font-mono") "nil?")
|
|
(td (~tw :tokens "px-4 py-2 font-mono") "is_nil")
|
|
(td (~tw :tokens "px-4 py-2") "predicate rename"))
|
|
(tr (~tw :tokens "border-t border-stone-100")
|
|
(td (~tw :tokens "px-4 py-2 font-mono") "empty?")
|
|
(td (~tw :tokens "px-4 py-2 font-mono") "empty_p")
|
|
(td (~tw :tokens "px-4 py-2") "? → _p (general)"))
|
|
(tr (~tw :tokens "border-t border-stone-100")
|
|
(td (~tw :tokens "px-4 py-2 font-mono") "set!")
|
|
(td (~tw :tokens "px-4 py-2 font-mono") "set_b")
|
|
(td (~tw :tokens "px-4 py-2") "! → _b"))
|
|
(tr (~tw :tokens "border-t border-stone-100")
|
|
(td (~tw :tokens "px-4 py-2 font-mono") "type")
|
|
(td (~tw :tokens "px-4 py-2 font-mono") "type_")
|
|
(td (~tw :tokens "px-4 py-2") "Python reserved word escape"))))))
|
|
|
|
(~docs/subsection :title "Special Forms"
|
|
(p "Each SX special form maps to a Python expression pattern:")
|
|
(div (~tw :tokens "overflow-x-auto rounded border border-stone-200 my-4")
|
|
(table (~tw :tokens "w-full text-sm")
|
|
(thead (~tw :tokens "bg-stone-50")
|
|
(tr
|
|
(th (~tw :tokens "px-4 py-2 text-left font-semibold text-stone-700") "SX")
|
|
(th (~tw :tokens "px-4 py-2 text-left font-semibold text-stone-700") "Python")))
|
|
(tbody
|
|
(tr (~tw :tokens "border-t border-stone-100")
|
|
(td (~tw :tokens "px-4 py-2 font-mono") "(if c t e)")
|
|
(td (~tw :tokens "px-4 py-2 font-mono") "(t if sx_truthy(c) else e)"))
|
|
(tr (~tw :tokens "border-t border-stone-100")
|
|
(td (~tw :tokens "px-4 py-2 font-mono") "(let ((a 1)) body)")
|
|
(td (~tw :tokens "px-4 py-2 font-mono") "(lambda a: body)(1)"))
|
|
(tr (~tw :tokens "border-t border-stone-100")
|
|
(td (~tw :tokens "px-4 py-2 font-mono") "(fn (x) body)")
|
|
(td (~tw :tokens "px-4 py-2 font-mono") "lambda x: body"))
|
|
(tr (~tw :tokens "border-t border-stone-100")
|
|
(td (~tw :tokens "px-4 py-2 font-mono") "(and a b c)")
|
|
(td (~tw :tokens "px-4 py-2 font-mono") "(a if not sx_truthy(a) else ...)"))
|
|
(tr (~tw :tokens "border-t border-stone-100")
|
|
(td (~tw :tokens "px-4 py-2 font-mono") "(case x \"a\" 1)")
|
|
(td (~tw :tokens "px-4 py-2 font-mono") "_sx_case(x, [(\"a\", lambda: 1)])"))))))
|
|
|
|
(~docs/subsection :title "Mutation: set! and Cell Variables"
|
|
(p "Python closures can read but not rebind outer variables. "
|
|
(code "py.sx") " detects " (code "set!") " targets that cross lambda boundaries "
|
|
"and routes them through a " (code "_cells") " dict:")
|
|
(~docs/code :src (highlight ";; SX ;; Python
|
|
(define counter def counter():
|
|
(fn () _cells = {}
|
|
(let ((n 0)) _cells['n'] = 0
|
|
(fn () return lambda: _sx_begin(
|
|
(set! n (+ n 1)) _sx_cell_set(_cells, 'n', ...),
|
|
n)))) _cells['n'])" "python"))
|
|
(p "This is the hardest translation rule. " (code "py-find-nested-set-vars")
|
|
" scans the AST for " (code "set!") " inside nested " (code "fn") " bodies. "
|
|
(code "py-emit-define-as-def") " emits a " (code "def") " with " (code "_cells")
|
|
" dict instead of a lambda.")))
|
|
|
|
;; -----------------------------------------------------------------------
|
|
;; Scope
|
|
;; -----------------------------------------------------------------------
|
|
|
|
(~docs/section :title "Scope" :id "scope"
|
|
(p (code "py.sx") " is a general-purpose SX-to-Python translator. "
|
|
"The translation rules are mechanical and apply to " (em "all") " SX, "
|
|
"not just the spec subset.")
|
|
(p "The spec files are the " (em "first test case") " — because we can verify correctness "
|
|
"by diffing G0 and G1 output. But the translator itself is target-agnostic: "
|
|
"it translates SX syntax, not SX semantics. Every SX form has a "
|
|
"straightforward Python equivalent.")
|
|
(p "The roadmap:")
|
|
(ul (~tw :tokens "list-disc pl-6 space-y-1 text-stone-700")
|
|
(li (code "py.sx") " → Python — " (strong "done"))
|
|
(li (code "js.sx") " → JavaScript (replaces " (code "bootstrap_js.py") ")")
|
|
(li (code "go.sx") " → Go (new host)")
|
|
(li (code "rs.sx") " → Rust (new host)")
|
|
(li (code "hs.sx") " → Haskell (new host)"))
|
|
(p "Each new host only needs: (1) a minimal evaluator to run "
|
|
(code "{host}.sx") " once, and (2) the platform interface in the target language."))
|
|
|
|
;; -----------------------------------------------------------------------
|
|
;; Implications
|
|
;; -----------------------------------------------------------------------
|
|
|
|
(~docs/section :title "Implications" :id "implications"
|
|
(~docs/subsection :title "Practical"
|
|
(p "One less Python file to maintain. Changes to the transpilation logic "
|
|
"are written in SX and tested with the SX test harness. The spec and its "
|
|
"compiler live in the same language."))
|
|
|
|
(~docs/subsection :title "Architectural"
|
|
(p "With " (code "z3.sx") " (SMT-LIB) and " (code "py.sx") " (Python), "
|
|
"the pattern is clear: SX translators are SX programs. "
|
|
"Adding a new target language means writing one " (code ".sx") " file, "
|
|
"not a new Python compiler."))
|
|
|
|
(~docs/subsection :title "Philosophical"
|
|
(p "A self-hosting bootstrapper is a fixed point. The spec defines behavior. "
|
|
"The translator is itself defined in terms of that behavior. Running the "
|
|
"translator on the spec produces a program that can run the translator on "
|
|
"the spec and get the same program.")
|
|
(p "Gödel showed that any sufficiently powerful formal system can encode statements "
|
|
"about itself. A self-hosting bootstrapper is the constructive version: "
|
|
"the system doesn't just " (em "talk") " about itself, it " (em "builds") " itself.")))))
|