96 lines
3.1 KiB
Nix
96 lines
3.1 KiB
Nix
{
|
|
description = "Lean documentation";
|
|
|
|
inputs.lean.url = path:../.;
|
|
inputs.flake-utils.follows = "lean/flake-utils";
|
|
inputs.mdBook = {
|
|
url = github:leanprover/mdBook;
|
|
flake = false;
|
|
};
|
|
inputs.alectryon = {
|
|
url = github:Kha/alectryon/typeid;
|
|
flake = false;
|
|
};
|
|
inputs.leanInk = {
|
|
url = github:leanprover/LeanInk;
|
|
flake = false;
|
|
};
|
|
|
|
outputs = inputs@{ self, ... }: inputs.flake-utils.lib.eachDefaultSystem (system:
|
|
with inputs.lean.packages.${system}; with nixpkgs;
|
|
let
|
|
doc-src = lib.sourceByRegex ../. ["doc.*" "tests(/lean(/beginEndAsMacro.lean)?)?"];
|
|
in {
|
|
packages = rec {
|
|
lean-mdbook = mdbook.overrideAttrs (drv: rec {
|
|
name = "lean-${mdbook.name}";
|
|
src = inputs.mdBook;
|
|
cargoDeps = drv.cargoDeps.overrideAttrs (_: {
|
|
inherit src;
|
|
outputHash = "sha256-mhTWHs/bsmm3FH59SkUxBTl5lEH2Rlz/aF9CuBTu1TE=";
|
|
});
|
|
doCheck = false;
|
|
});
|
|
book = stdenv.mkDerivation {
|
|
name ="lean-doc";
|
|
src = doc-src;
|
|
buildInputs = [ lean-mdbook ];
|
|
buildCommand = ''
|
|
mkdir $out
|
|
# necessary for `additional-css`...?
|
|
cp -r --no-preserve=mode $src/doc/* .
|
|
# overwrite stub .lean.md files
|
|
cp -r ${examples}/* examples/
|
|
mdbook build -d $out
|
|
'';
|
|
};
|
|
# We use a separate derivation instead of `checkPhase` so we can push it but not `doc` to the binary cache
|
|
test = stdenv.mkDerivation {
|
|
name ="lean-doc-test";
|
|
src = doc-src;
|
|
buildInputs = [ lean-mdbook stage1.Lean.lean-package strace ];
|
|
patchPhase = ''
|
|
cd doc
|
|
patchShebangs test
|
|
'';
|
|
buildPhase = ''
|
|
mdbook test
|
|
touch $out
|
|
'';
|
|
dontInstall = true;
|
|
};
|
|
leanInk = (buildLeanPackage {
|
|
name = "Main";
|
|
src = inputs.leanInk;
|
|
deps = [ (buildLeanPackage {
|
|
name = "LeanInk";
|
|
src = inputs.leanInk;
|
|
}) ];
|
|
executableName = "leanInk";
|
|
linkFlags = ["-rdynamic"];
|
|
}).executable;
|
|
alectryon = python3Packages.buildPythonApplication {
|
|
name = "alectryon";
|
|
src = inputs.alectryon;
|
|
propagatedBuildInputs =
|
|
[ leanInk lean-all ] ++
|
|
# https://github.com/cpitclaudel/alectryon/blob/master/setup.cfg
|
|
(with python3Packages; [ pygments dominate beautifulsoup4 docutils ]);
|
|
doCheck = false;
|
|
};
|
|
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 "${dir}/${n}") inputs;
|
|
in
|
|
outputs // symlinkJoin { inherit name; paths = lib.attrValues outputs; };
|
|
examples = renderDir "examples" ./examples;
|
|
doc = book;
|
|
};
|
|
defaultPackage = self.packages.${system}.doc;
|
|
});
|
|
}
|