From 7a7afbeb3ea645c6efe9c92c0ab489f3c7540cc6 Mon Sep 17 00:00:00 2001 From: Russoul Date: Mon, 3 Aug 2026 21:20:18 +0400 Subject: [PATCH] Render src/nova/*.nova to syntax-highlighted HTML, deploy to GitHub Pages Reuses the LSP's own token classification and hole-state overlay (Nova.LSP.SemanticTokens) instead of a separate classifier, so the highlighting always matches what an editor's LSP client shows. CI now builds and deploys the rendered sources alongside the existing spec pages. --- .github/workflows/nova.yml | 56 ++++++++ nova-docs.ipkg | 46 +++++++ src/idris/Nova/Docs/Render.idr | 179 ++++++++++++++++++++++++++ src/idris/Nova/LSP/Capabilities.idr | 11 +- src/idris/Nova/LSP/SemanticTokens.idr | 5 + tools/nova-docs.css | 48 +++++++ tools/pages-index.html | 14 ++ 7 files changed, 357 insertions(+), 2 deletions(-) create mode 100644 nova-docs.ipkg create mode 100644 src/idris/Nova/Docs/Render.idr create mode 100644 tools/nova-docs.css create mode 100644 tools/pages-index.html diff --git a/.github/workflows/nova.yml b/.github/workflows/nova.yml index e4b9c250..d5504a8a 100644 --- a/.github/workflows/nova.yml +++ b/.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 diff --git a/nova-docs.ipkg b/nova-docs.ipkg new file mode 100644 index 00000000..2b3e7f59 --- /dev/null +++ b/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" diff --git a/src/idris/Nova/Docs/Render.idr b/src/idris/Nova/Docs/Render.idr new file mode 100644 index 00000000..348da166 --- /dev/null +++ b/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 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 '&' = "&" + esc '<' = "<" + esc '>' = ">" + 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 = "" ++ htmlEscape (pack tokChars) ++ "" + (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" + [ "" + , "" + , "" + , "" + , "" ++ htmlEscape title ++ "" + , "" + , "" + , "" + , "

" ++ htmlEscape title ++ "

" + , "
"
+  ++ body ++
+  "
" + , "" + , "" + ] + +-- ===== 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" $ + [ "" + , "" + , "" + , "" + , "Nova sources" + , "" + , "" + , "" + , "

Nova sources

" + , "" + , "" + , "" + ] + +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 [ ...]" + +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 diff --git a/src/idris/Nova/LSP/Capabilities.idr b/src/idris/Nova/LSP/Capabilities.idr index 766e2b2e..d8a1d6c8 100644 --- a/src/idris/Nova/LSP/Capabilities.idr +++ b/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 diff --git a/src/idris/Nova/LSP/SemanticTokens.idr b/src/idris/Nova/LSP/SemanticTokens.idr index 5bf54b2b..ccfa0871 100644 --- a/src/idris/Nova/LSP/SemanticTokens.idr +++ b/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 diff --git a/tools/nova-docs.css b/tools/nova-docs.css new file mode 100644 index 00000000..54ca67e4 --- /dev/null +++ b/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); } diff --git a/tools/pages-index.html b/tools/pages-index.html new file mode 100644 index 00000000..ae532f94 --- /dev/null +++ b/tools/pages-index.html @@ -0,0 +1,14 @@ + + + + +Nova + + +

Nova

+
    +
  • Theory specs — NovaFoundation, NovaSyntax, NovaModel, NovaKernel, NovaElaboration, NovaPipeline
    • +
  • Nova sources — src/nova/*.nova, syntax-highlighted via the LSP's own semantic tokens
    • +
+ +