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

chore: Nix: renderLean/renderDir

Browse source
This commit is contained in:
Sebastian Ullrich 2022-07-15 18:44:17 +02:00
parent 0835145246
commit 392c72db86
1 changed files with 10 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
doc/flake.nix
View file

@ -40,7 +40,7 @@
# necessary for `additional-css`...?
cp -r --no-preserve=mode $src/doc/* .
# overwrite stub .lean.md files
cp -r ${examples}/* .
cp -r ${examples}/* examples/
mdbook build -d $out
'';
};
@ -78,16 +78,17 @@
(with python3Packages; [ pygments dominate beautifulsoup4 docutils ]);
doCheck = false;
};
examples = let
renderLean = name: file: runCommandNoCC "${name}.md" { buildInputs = [ alectryon ]; } ''
mkdir -p $out/examples
alectryon --frontend lean4+markup ${file} --backend webpage -o $out/examples/${name}.md
'';
ents = builtins.readDir ./examples;
renderLean = name: file: runCommandNoCC "${name}.md" { buildInputs = [ alectryon ]; } ''
mkdir -p $out/examples
alectryon --frontend lean4+markup ${file} --backend webpage -o $out/${name}.md
'';
renderDir = name: dir: let
ents = builtins.readDir dir;
inputs = lib.filterAttrs (n: t: builtins.match ".*\.lean" n != null && t == "regular") ents;
outputs = lib.mapAttrs (n: _: renderLean n ./examples/${n}) inputs;
outputs = lib.mapAttrs (n: _: renderLean n "${dir}/${n}") inputs;
in
outputs // symlinkJoin { name = "examples"; paths = lib.attrValues outputs; };
outputs // symlinkJoin { inherit name; paths = lib.attrValues outputs; };
examples = renderDir "examples" ./examples;
doc = book;
};
defaultPackage = self.packages.${system}.doc;