Render src/nova/*.nova to syntax-highlighted HTML, deploy to GitHub Pages

.github/workflows/nova.yml

@@ -69,3 +69,59 @@ jobs:
 
       - name: Run tests
         run: ./test.sh
+
+      - name: Build nova-docs
+        run: pack build nova-docs.ipkg
+
+      - name: Render Nova sources
+        run: |
+          mkdir -p build/docs/nova
+          pack run nova-docs.ipkg build/docs/nova src/nova/*.nova
+          cp tools/nova-docs.css build/docs/nova/
+
+      - name: Upload rendered Nova sources
+        uses: actions/upload-artifact@v4
+        with:
+          name: rendered-nova-docs
+          path: build/docs/nova
+
+  deploy-pages:
+    needs: [specs, build-and-test]
+    if: github.ref == 'refs/heads/main' && github.event_name == 'push'
+    runs-on: ubuntu-24.04
+    permissions:
+      pages: write
+      id-token: write
+    environment:
+      name: github-pages
+      url: ${{ steps.deployment.outputs.page_url }}
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: Download rendered specs
+        uses: actions/download-artifact@v4
+        with:
+          name: rendered-specs
+          path: site
+
+      - name: Download rendered Nova sources
+        uses: actions/download-artifact@v4
+        with:
+          name: rendered-nova-docs
+          path: site/nova
+
+      - name: Add landing page
+        run: cp tools/pages-index.html site/index.html
+
+      - name: Configure Pages
+        uses: actions/configure-pages@v5
+
+      - name: Upload Pages artifact
+        uses: actions/upload-pages-artifact@v3
+        with:
+          path: site
+
+      - name: Deploy to GitHub Pages
+        id: deployment
+        uses: actions/deploy-pages@v4

nova-docs.ipkg

@@ -0,0 +1,46 @@
+package nova-docs
+version = 0.1.0
+
+depends = contrib, just-a-parser, lsp-lib
+
+executable = nova-docs
+main = Nova.Docs.Render
+
+modules = Nova.Kernel.Syntax
+        , Nova.Kernel.Subst
+        , Nova.Kernel.Beta
+        , Nova.Kernel
+        , Nova.Kernel.QIIT
+        , Nova.Compute
+        , Nova.Elaboration.Named
+        , Nova.Elaboration
+        , Nova.Elaboration.Surface
+        , Nova.Elaboration.Parser
+        , Nova.Elaboration.Loader
+        , Nova.Kernel.Parser
+
+        , Solver.CommutativeMonoid
+        , Solver.CommutativeMonoid.Evaluation
+        , Solver.CommutativeMonoid.Language
+        , Solver.CommutativeMonoid.Normalisation
+        , Solver.CommutativeMonoid.Parser
+        , Solver.CommutativeMonoid.Quotation
+        , Solver.CommutativeMonoid.Value
+
+        , Data.Util
+
+        , Control.Monad.EitherSt
+        , Control.Monad.IOEither
+        , Control.Monad.Id
+        , Control.Monad.MaybeSt
+        , Control.Monad.Reader
+        , Control.Monad.St
+        , Control.Monad.StEither
+
+        , Nova.LSP.Capabilities
+        , Nova.LSP.Encoding
+        , Nova.LSP.SemanticTokens
+
+        , Nova.Docs.Render
+
+sourcedir = "src/idris"

src/idris/Nova/Docs/Render.idr

@@ -0,0 +1,179 @@
+module Nova.Docs.Render
+
+-- Batch static-HTML renderer for .nova surface files: runs the same
+-- load/elaborate pipeline the `nova elab` CLI runs (Nova.Elaboration.
+-- Loader.loadProgram), reuses the LSP's own token classification and
+-- hole-state overlay (Nova.LSP.SemanticTokens), and paints the source
+-- with one <span class="tok-..."> per classified token — so a
+-- rendered page's highlighting always matches what an editor's LSP
+-- client shows, with no separate classifier to keep in sync.
+
+import Data.List
+import Data.List1
+import Data.Maybe
+import Data.String
+import Data.SnocList
+
+import System
+import System.File
+
+import Me.Russoul.Text.Range
+import Me.Russoul.Text.Position
+
+import Nova.Kernel.Parser
+import Nova.Elaboration
+import Nova.Elaboration.Loader
+import Nova.LSP.Capabilities
+import Nova.LSP.SemanticTokens
+
+%default covering
+
+-- ===== rendering =====
+
+htmlEscape : String -> String
+htmlEscape = concatMap esc . unpack
+  where
+    esc : Char -> String
+    esc '&' = "&amp;"
+    esc '<' = "&lt;"
+    esc '>' = "&gt;"
+    esc c   = singleton c
+
+nth : Nat -> List a -> Maybe a
+nth _        []        = Nothing
+nth Z        (x :: _)  = Just x
+nth (S k)    (_ :: xs) = nth k xs
+
+||| `overlay`'s classified index, resolved back to a CSS class name via
+||| the same legend the LSP advertises (Nova.LSP.Capabilities.
+||| tokenTypeNames) — one source of truth for both.
+classFor : Int -> String
+classFor i = fromMaybe "plain" (nth (integerToNat (cast i)) tokenTypeNames)
+
+||| Render one source line against the (start-ordered) tokens whose
+||| span begins on it, returning the line's HTML and the tokens left
+||| over for later lines. `pos` is the codepoint column already
+||| emitted on this line.
+renderLine : (lineNo : Int) -> (pos : Int) -> List Char -> List (Range, Int)
+           -> (String, List (Range, Int))
+renderLine _ _ cs [] = (htmlEscape (pack cs), [])
+renderLine lineNo pos cs (tok :: rest) =
+  let (MkRange (MkPosition sl sc) (MkPosition _ ec), kind) = tok in
+  if sl /= lineNo
+    then (htmlEscape (pack cs), tok :: rest)
+    else
+      let (gapChars, afterGap) = splitAt (integerToNat (cast (sc - pos))) cs
+          (tokChars, afterTok) = splitAt (integerToNat (cast (ec - sc))) afterGap
+          gapHtml = htmlEscape (pack gapChars)
+          tokHtml = "<span class=\"tok-" ++ classFor kind ++ "\">" ++ htmlEscape (pack tokChars) ++ "</span>"
+          (restHtml, leftover) = renderLine lineNo ec afterTok rest
+      in (gapHtml ++ tokHtml ++ restHtml, leftover)
+
+renderLines : (lineNo : Int) -> List String -> List (Range, Int) -> List String
+renderLines _ [] _ = []
+renderLines lineNo (l :: ls) toks =
+  let (html, leftover) = renderLine lineNo 0 (unpack l) toks
+  in html :: renderLines (lineNo + 1) ls leftover
+
+||| Same classification+hole-overlay a `semanticTokens/full` response
+||| carries (Nova.LSP.SemanticTokens.getSemanticTokens), just emitted
+||| as HTML spans instead of the LSP wire format's delta-encoded ints.
+renderSource : String -> List (Range, TokenKind) -> List (Range, Bool) -> String
+renderSource source rawToks holeOccs =
+  let overlaid = sortTokens (map (overlay holeOccs) rawToks)
+  in joinBy "\n" (renderLines 0 (lines source) overlaid)
+
+htmlPage : (title : String) -> String -> String
+htmlPage title body = joinBy "\n"
+  [ "<!DOCTYPE html>"
+  , "<html>"
+  , "<head>"
+  , "<meta charset=\"utf-8\">"
+  , "<title>" ++ htmlEscape title ++ "</title>"
+  , "<link rel=\"stylesheet\" href=\"nova-docs.css\">"
+  , "</head>"
+  , "<body>"
+  , "<h1>" ++ htmlEscape title ++ "</h1>"
+  , "<pre><code class=\"nova-source\">"
+  ++ body ++
+  "</code></pre>"
+  , "</body>"
+  , "</html>"
+  ]
+
+-- ===== driver =====
+
+||| Surface hole syntax only (`?x`/`_x`/`_`), recolored by solved
+||| state — same restriction and same source (ElabReport.holeTable)
+||| as Nova.LSP.ProcessMessage's TextDocumentSemanticTokensFull.
+holeOccsOf : ElabReport -> List (Range, Bool)
+holeOccsOf report =
+  [ (r, isJust h.hiSolution)
+  | h <- report.holeTable
+  , isPrefixOf "?" h.hiName || isPrefixOf "_" h.hiName
+  , r <- h.hiOccs
+  ]
+
+baseNameOf : String -> String
+baseNameOf path =
+  let name = List1.last (split (== '/') path) in
+  if isSuffixOf ".nova" name
+    then pack (reverse (drop 5 (reverse (unpack name))))
+    else name
+
+||| Load, elaborate (for hole state) and render one .nova file to a
+||| standalone HTML page. Errors (parse/load failure) are reported,
+||| not thrown — one bad file shouldn't abort the whole batch.
+renderFile : String -> IO (Either String (String, String))
+renderFile path = do
+  Right units <- loadProgram path
+    | Left err => pure (Left err.lmsg)
+  let Just root = last' units
+    | Nothing => pure (Left "loadProgram returned no modules for \{path}")
+  Right source <- readFile path
+    | Left err => pure (Left "cannot read \{path}: \{show err}")
+  let report = elabProgramReport units
+  let holeOccs = holeOccsOf report
+  let body = renderSource source (toList root.mtokens) holeOccs
+  let base = baseNameOf path
+  pure (Right (base, htmlPage base body))
+
+indexPage : List String -> String
+indexPage bases = joinBy "\n" $
+  [ "<!DOCTYPE html>"
+  , "<html>"
+  , "<head>"
+  , "<meta charset=\"utf-8\">"
+  , "<title>Nova sources</title>"
+  , "<link rel=\"stylesheet\" href=\"nova-docs.css\">"
+  , "</head>"
+  , "<body>"
+  , "<h1>Nova sources</h1>"
+  , "<ul>"
+  ] ++ map (\b => "<li><a href=\"" ++ b ++ ".html\">" ++ htmlEscape b ++ "</a></li>") bases ++
+  [ "</ul>"
+  , "</body>"
+  , "</html>"
+  ]
+
+processFile : (outDir : String) -> String -> IO (Maybe String)
+processFile outDir path = do
+  Right (base, html) <- renderFile path
+    | Left err => do putStrLn "Error in \{path}: \{err}"; pure Nothing
+  Right () <- writeFile (outDir ++ "/" ++ base ++ ".html") html
+    | Left err => do putStrLn "Cannot write output for \{path}: \{show err}"; pure Nothing
+  putStrLn "Rendered \{path} -> \{outDir}/\{base}.html"
+  pure (Just base)
+
+usage : String
+usage = "Usage: nova-docs <output-dir> <file.nova> [<file.nova> ...]"
+
+main : IO ()
+main = do
+  (_ :: outDir :: files@(_ :: _)) <- getArgs
+    | _ => die usage
+  bases <- traverse (processFile outDir) files
+  let oks = catMaybes bases
+  Right () <- writeFile (outDir ++ "/index.html") (indexPage oks)
+    | Left err => do putStrLn "Cannot write index: \{show err}"; exitFailure
+  when (length oks /= length files) exitFailure

src/idris/Nova/LSP/Capabilities.idr

@@ -55,9 +55,16 @@ export
 solvedHoleIndex : Int
 solvedHoleIndex = 6
 
+||| Token type names in legend order (index must match `tokenKindIndex`/
+||| `unsolvedHoleIndex`/`solvedHoleIndex`) — exported so non-LSP
+||| consumers (e.g. static HTML rendering) can resolve a classified
+||| token's index back to a name without duplicating this list.
+export
+tokenTypeNames : List String
+tokenTypeNames = map tokenKindName tokenKinds ++ ["unsolved_meta", "solved_meta"]
+
 semanticTokensLegend : SemanticTokensLegend
-semanticTokensLegend = MkSemanticTokensLegend
-  (map tokenKindName tokenKinds ++ ["unsolved_meta", "solved_meta"]) []
+semanticTokensLegend = MkSemanticTokensLegend tokenTypeNames []
 
 semanticTokensOptions : SemanticTokensOptions
 semanticTokensOptions = MkSemanticTokensOptions

src/idris/Nova/LSP/SemanticTokens.idr

@@ -18,6 +18,10 @@ compareStart (r1, _) (r2, _) =
 
 ||| LSP's relative-delta encoding is only meaningful over a single,
 ||| start-position-ordered pass, so this always runs before `encode`.
+||| Exported for non-LSP consumers (e.g. static HTML rendering) that
+||| want the same start-ordered, hole-overlaid classification without
+||| the wire-format delta encoding.
+export
 sortTokens : List (Range, a) -> List (Range, a)
 sortTokens = sortBy compareStart
 
@@ -59,6 +63,7 @@ within inner outer = posLE outer.start inner.start && posLE inner.end outer.end
 ||| reclassify every token inside a hole occurrence range by the
 ||| hole's state instead. `holeOccs` pairs each occurrence range with
 ||| whether the hole is SOLVED.
+export
 overlay : List (Range, Bool) -> (Range, TokenKind) -> (Range, Int)
 overlay occs (r, k) =
   case find (\(hr, _) => within r hr) occs of

tools/nova-docs.css

@@ -0,0 +1,48 @@
+/* Palette matches tools/render-specs.py's CSS, so the rendered specs
+   page and rendered .nova sources read as one system. */
+:root {
+  --paper:#f7f8fa; --ink:#20242d; --faint:#5c6472; --hair:#d8dce2;
+  --panel:#eef0f4; --tos:#0e7c86; --nova:#2f5fc0; --meta:#7862a8;
+  --link:#0e7c86; --gold:#92700c; --natc:#b03a70;
+}
+@media (prefers-color-scheme: dark) { :root {
+  --paper:#191b20; --ink:#dcdee4; --faint:#9aa1ae; --hair:#33373f;
+  --panel:#20232a; --tos:#53cad4; --nova:#82a5ea; --meta:#a995d6;
+  --link:#53cad4; --gold:#d8b45e; --natc:#e592bb;
+}}
+:root[data-theme="dark"] {
+  --paper:#191b20; --ink:#dcdee4; --faint:#9aa1ae; --hair:#33373f;
+  --panel:#20232a; --tos:#53cad4; --nova:#82a5ea; --meta:#a995d6;
+  --link:#53cad4; --gold:#d8b45e; --natc:#e592bb;
+}
+:root[data-theme="light"] {
+  --paper:#f7f8fa; --ink:#20242d; --faint:#5c6472; --hair:#d8dce2;
+  --panel:#eef0f4; --tos:#0e7c86; --nova:#2f5fc0; --meta:#7862a8;
+  --link:#0e7c86; --gold:#92700c; --natc:#b03a70;
+}
+* { box-sizing:border-box; }
+body {
+  margin:0 auto; max-width:900px; padding:1.5rem 1.25rem 4rem;
+  background:var(--paper); color:var(--ink);
+  font-family:ui-sans-serif,system-ui,sans-serif;
+}
+h1 { font-size:1.15rem; font-weight:600; }
+a { color:var(--link); }
+ul { line-height:1.9; }
+pre {
+  background:var(--panel); border:1px solid var(--hair); border-radius:6px;
+  padding:1rem; overflow-x:auto;
+}
+code.nova-source {
+  font-family:ui-monospace,"SF Mono",Menlo,Consolas,monospace;
+  font-size:14px; line-height:1.5; white-space:pre;
+}
+.tok-keyword    { color:var(--gold); font-weight:600; }
+.tok-variable   { color:var(--ink); }
+.tok-operator   { color:var(--nova); }
+.tok-number     { color:var(--natc); }
+.tok-comment    { color:var(--faint); font-style:italic; }
+.tok-unsolved_meta {
+  color:var(--meta); text-decoration:underline dotted var(--meta);
+}
+.tok-solved_meta { color:var(--tos); }

tools/pages-index.html

@@ -0,0 +1,14 @@
+<!DOCTYPE html>
+<html>
+<head>
+<meta charset="utf-8">
+<title>Nova</title>
+</head>
+<body>
+<h1>Nova</h1>
+<ul>
+<li><a href="specs.html">Theory specs</a> — NovaFoundation, NovaSyntax, NovaModel, NovaKernel, NovaElaboration, NovaPipeline</li>
+<li><a href="nova/index.html">Nova sources</a> — src/nova/*.nova, syntax-highlighted via the LSP's own semantic tokens</li>
+</ul>
+</body>
+</html>