Commit Graph

32 Commits (main)

Author SHA1 Message Date
Henrik Böving e5118b8f20 feat: show the type of exists and fun arguments 2023-11-24 13:18:38 +01:00
Henrik Böving e966ab8523 fix: we want to catch runtime exceptions in doc-gen4 2023-11-18 23:58:00 +01:00
Henrik Böving f9d9875671 perf: Don't call Lake from within doc-gen anymore 2023-10-09 09:30:16 +02:00
Henrik Böving 7e89b462f0 chore: update toolchain 2023-09-18 22:08:46 +02:00
Henrik 36e1b863a7 chore: remove pointless prints 2023-09-09 23:59:25 +02:00
tydeu 34165f36e6 feat: include Lake as part of the core docs 2023-08-24 10:10:16 +02:00
Henrik Böving 5e96952a58 chore: update toolchain 2022-12-02 17:55:27 +01:00
Henrik Böving 64f627a295
chore: toolchain upgrade (#82)
Halleluja!
2022-10-05 12:05:58 +02:00
Henrik Böving cdfd8ff49c feat: implement facet 2022-08-11 22:58:25 +02:00
Henrik Böving 6534a71cca chore: update toolchain 2022-08-11 18:30:28 +02:00
Henrik Böving ed4cee2eae chore: style, change $ to <| 2022-07-23 13:01:25 +02:00
Henrik Böving 4bc7a682ec feat: implementation of separate staged builds 2022-07-21 18:26:01 +02:00
Henrik Böving fbbdb21795 fix: remove redundant argument 2022-07-21 02:25:26 +02:00
Henrik Böving 25b1ddb66b feat: Preparations to split doc-gen build process 2022-07-21 01:40:04 +02:00
Henrik Böving 5f45c8dadc chore: update toolchain 2022-07-20 16:29:18 +02:00
Henrik Böving 351cbc56b6 chore: update lean nightly 2022-07-04 09:11:10 +02:00
Henrik Böving 7c9237ffb4 chore: update compiler and lake 2022-06-19 16:41:59 +02:00
Henrik Böving e8fb9a7f0f chore: update to latest nightly 2022-05-27 22:19:34 +02:00
Henrik Böving d519ef6b58 fix: adapt the rest of the program to the process refactor 2022-05-20 00:36:43 +02:00
Henrik Böving c05a9cf5e5 doc: Load 2022-05-19 20:45:12 +02:00
Henrik Böving 9cc4c787e6 feat: lake integration 2022-03-06 18:51:06 +01:00
Henrik Böving 5535616725 chore: Bump toolchain 2022-03-06 16:48:49 +01:00
Henrik Böving 34d2239b68 feat: actual CLI 2022-02-23 22:54:10 +01:00
Henrik Böving d39b14cf7a chore: bump toolchain, bye auto pure 2022-02-12 15:09:13 +01:00
Henrik Böving 5e0956c4b0 feat: Proper linking of all constants
Previously constants in function applications where either not linked
at all or linked in a weird way, this change fixes it by making use of
a (as of now umerged) compiler modification as well as Lean.Widget's
TaggedText.
2022-01-03 14:25:50 +01:00
Henrik Böving cb582aab57 feat: Some more progress logging 2021-12-15 12:02:05 +01:00
Henrik Böving ded884ce9c feat: HTML Index + CSS 2021-12-12 13:38:31 +01:00
Henrik Böving 77cb52e9cb chore: Inline licensing 2021-12-12 13:38:31 +01:00
Henrik Böving 29a249e8fd feat: Automatic search path + modules as CLI arguments 2021-12-12 13:38:27 +01:00
Henrik Böving d2fddd7cff feat: Print count of declarations and modules processed 2021-12-12 13:37:38 +01:00
Henrik Böving dd0cebb44a feat: Sort everything into modules instead of just declaration lists 2021-12-12 13:37:28 +01:00
Henrik Böving 2574c22e4a feat: First experimentations 2021-12-12 13:37:25 +01:00