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

doc: mdbook init

Browse source
This commit is contained in:
Sebastian Ullrich 2020-10-30 12:54:20 +01:00
parent 486d8457fa
commit 18472e1933
4 changed files with 15 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
doc/.gitignore vendored
View file

@ -1,2 +1 @@
html
*.org.*.lean
out

1
doc/SUMMARY.md Normal file
View file

@ -0,0 +1 @@
# Language Reference

12
doc/book.toml Normal file
View file

@ -0,0 +1,12 @@
[book]
authors = ["Leonardo de Moura", "Sebastian Ullrich"]
language = "en"
multilingual = false
src = "."
title = "Lean Manual"
[build]
build-dir = "out"
[output.html]
git-repository-url = "https://github.com/leanprover/lean4"

2
shell.nix
View file

@ -27,7 +27,7 @@ exit 0
};
shell = pkgs.mkShell.override { stdenv = lean.stdenv; } rec {
inputsFrom = [ lean ];
buildInputs = with pkgs; [ temci ccache ];
buildInputs = with pkgs; [ temci ccache mdbook ];
# https://github.com/NixOS/nixpkgs/issues/60919
hardeningDisable = [ "all" ];
# more convenient `ctest` output