max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: Nix: render examples using LeanInk+Alectryon

Browse source
This commit is contained in:
Sebastian Ullrich 2022-03-24 23:40:07 +01:00
parent 282147631f
commit bef34e30e7
4 changed files with 18 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
.github/workflows/nix-ci.yml vendored
View file

@ -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

2
RELEASES.md
View file

@ -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)
---------

8
doc/examples.md
View file

@ -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)

13
doc/flake.nix
View file

@ -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;
});