From bef34e30e77eb4ef3c8351e947fef65ef21b19b2 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 24 Mar 2022 23:40:07 +0100
Subject: [PATCH] feat: Nix: render examples using LeanInk+Alectryon

---
 .github/workflows/nix-ci.yml |  2 +-
 RELEASES.md                  |  2 +-
 doc/examples.md              |  8 ++++----
 doc/flake.nix                | 13 ++++++++++++-
 4 files changed, 18 insertions(+), 7 deletions(-)

diff --git a/.github/workflows/nix-ci.yml b/.github/workflows/nix-ci.yml
index 4644106fc7..287974ba12 100644
--- a/.github/workflows/nix-ci.yml
+++ b/.github/workflows/nix-ci.yml
@@ -92,7 +92,7 @@ jobs:
           nix build $NIX_BUILD_ARGS .#test -o push-test
       - name: Build manual
         run: |
-          nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc#lean-mdbook ./doc#test -o push-doc
+          nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc#{lean-mdbook,leanInk,alectryon,test} -o push-doc
           nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc
         if: matrix.name == 'Nix Linux'
       - name: Push to Cachix
diff --git a/RELEASES.md b/RELEASES.md
index e07c5fa4e8..a25118c56f 100644
--- a/RELEASES.md
+++ b/RELEASES.md
@@ -3,7 +3,7 @@ Unreleased
 
 * Add cross-compiled [aarch64 Linux](https://github.com/leanprover/lean4/pull/1066) and [aarch64 macOS](https://github.com/leanprover/lean4/pull/1076) releases.
 
-* [Added tutorial-like examples to our documentation](https://github.com/leanprover/lean4/tree/master/doc/examples). They will be soon rendered using LeanInk+Alectryon.
+* [Add tutorial-like examples to our documentation](https://github.com/leanprover/lean4/tree/master/doc/examples), rendered using LeanInk+Alectryon.
 
 v4.0.0-m4 (23 March 2022)
 ---------
diff --git a/doc/examples.md b/doc/examples.md
index bde89053e2..bd8b4a72c9 100644
--- a/doc/examples.md
+++ b/doc/examples.md
@@ -1,7 +1,7 @@
 Examples
 ========
 
-- [A Certified Type Checker](https://github.com/leanprover/lean4/blob/master/doc/examples/tc.lean)
-- [The Well-Typed Interpreter](https://github.com/leanprover/lean4/blob/master/doc/examples/interp.lean)
-- [Dependent de Bruijn Indices](https://github.com/leanprover/lean4/blob/master/doc/examples/deBruijn.lean)
-- [Parametric Higher-Order Abstract Syntax](https://github.com/leanprover/lean4/blob/master/doc/examples/phoas.lean)
+- [A Certified Type Checker](examples/tc.lean.html)
+- [The Well-Typed Interpreter](examples/interp.lean.html)
+- [Dependent de Bruijn Indices](examples/deBruijn.lean.html)
+- [Parametric Higher-Order Abstract Syntax](examples/phoas.lean.html)
diff --git a/doc/flake.nix b/doc/flake.nix
index 6ae149a49f..669f6dce5b 100644
--- a/doc/flake.nix
+++ b/doc/flake.nix
@@ -31,7 +31,7 @@
         });
         doCheck = false;
       });
-      doc = stdenv.mkDerivation {
+      book = stdenv.mkDerivation {
         name ="lean-doc";
         src = doc-src;
         buildInputs = [ lean-mdbook ];
@@ -69,6 +69,17 @@
           (with python3Packages; [ pygments dominate beautifulsoup4 docutils ]);
         doCheck = false;
       };
+      examples = let
+        renderLean = name: file: runCommandNoCC "${name}.html" { buildInputs = [ alectryon ]; } ''
+          mkdir -p $out/examples
+          alectryon --frontend lean4+rst ${file} -o $out/examples/${name}.html
+        '';
+        ents = builtins.readDir ./examples;
+        inputs = lib.filterAttrs (n: t: t == "regular") ents;
+        outputs = lib.mapAttrs (n: _: renderLean n ./examples/${n}) inputs;
+      in
+        outputs // symlinkJoin { name = "examples"; paths = lib.attrValues outputs; };
+      doc = symlinkJoin { name = "doc"; paths = [ book examples ]; };
     };
     defaultPackage = self.packages.${system}.doc;
   });