Joshua Potter
aa25e084d2
Update index and add pdflatex generation script.
2023-12-14 16:39:20 -07:00
e859e2f777
chore: update dependencies
2023-11-05 09:59:30 +01:00
f9d9875671
perf: Don't call Lake from within doc-gen anymore
2023-10-09 09:30:16 +02:00
3a9cfabe58
fix: trace lake jobs properly
2023-10-08 11:30:11 +02:00
fa8c9d771a
feat: Always document the transitive closure of a module
2023-10-07 21:07:55 +02:00
96870507c5
feat: add jump-src.js for #src links
2023-09-21 11:38:22 +02:00
924be4c7d8
feat: expand the current file in the navbar
2023-09-18 23:55:19 +02:00
7e89b462f0
chore: update toolchain
2023-09-18 22:08:46 +02:00
3c033966e7
feat: logStep in the facet to show progress
2023-09-10 11:47:36 +02:00
596782c1fe
chore: update toolchain
2023-08-06 16:07:24 +02:00
d688d05089
chore: update to new Lean/Lake version
2023-07-30 20:52:37 +02:00
c312f00c88
chore: update toolchain
2023-07-30 20:45:40 +02:00
9af4c720f0
chore: disable LeanInk because of weird panics
2023-06-25 15:14:43 +02:00
cc552ed570
add colorscheme toggle
2023-06-09 23:39:59 +02:00
e5b44f1cdf
chore: update toolchain
2023-04-16 01:30:21 +02:00
5ab7d0bdd8
fix: unicode dependency
2023-03-15 11:54:57 +01:00
5f59fbaac4
refactor: switch to maintained unicode lib
2023-03-11 18:06:32 +01:00
033003c6cb
Add a search page to the docs.
...
Now instead of clicking the "Google Site Search"' button, the user has the option
of clicking the "Search" button, which will take them to a results page. Currently,
the results are identical to the autocomplete results, but the number of results
is not limited to 30. In the future, more information and search options could
be added to this page to make a more powerful search.
Fixes #107
2023-01-28 23:00:53 +01:00
7009910876
chore: update toolchain
2022-12-03 17:43:12 +01:00
9aef28b16e
chore: update toolchain 10-20 ( #86 )
2022-10-20 19:51:26 +02:00
64f627a295
chore: toolchain upgrade ( #82 )
...
Halleluja!
2022-10-05 12:05:58 +02:00
4a7c5e214a
chore: drop unused import
...
I didn't even know one could import modules from executables! Not sure how to feel about that.
2022-08-12 23:04:36 +02:00
23ddabb0da
Merge branch 'main' into LeanInkLink
2022-08-11 23:51:26 +02:00
cdfd8ff49c
feat: implement facet
2022-08-11 22:58:25 +02:00
6534a71cca
chore: update toolchain
2022-08-11 18:30:28 +02:00
d29e14a26a
chore: update toolchain and dependencies
2022-08-09 23:30:43 +02:00
763784e116
fix: whenever you force push a kitten dies
2022-07-26 15:17:56 +02:00
5e78890ec0
feat: experimental module facet for producing docs
2022-07-23 21:18:35 -04:00
5f45c8dadc
chore: update toolchain
2022-07-20 16:29:18 +02:00
351cbc56b6
chore: update lean nightly
2022-07-04 09:11:10 +02:00
199c7af17a
feat: LeanInk all the files, HTML generation missing
2022-06-20 00:31:09 +02:00
0acf82bcbe
chore: update Unicode.lean
2022-06-19 17:03:26 +02:00
7c9237ffb4
chore: update compiler and lake
2022-06-19 16:41:59 +02:00
e8fb9a7f0f
chore: update to latest nightly
2022-05-27 22:19:34 +02:00
89dd2fa46e
chore: upgrade compiler version
2022-04-09 19:30:33 +02:00
9cc4c787e6
feat: lake integration
2022-03-06 18:51:06 +01:00
34d2239b68
feat: actual CLI
2022-02-23 22:54:10 +01:00
794923a997
fix: update Unicode.lean
2022-02-20 04:50:04 +08:00
5e550c7833
refactor: docstring between basic and extra info
...
clean up code
2022-02-20 03:14:58 +08:00
5679be6bbc
chore: bump lean version
...
update cmark version
2022-02-17 08:54:06 +08:00
8da2e2a63d
feat: basic docstring support
2022-02-17 08:16:02 +08:00
deb6739fcc
chore: Initial Lake project
2021-12-12 13:37:18 +01:00
Joshua Potter
Henrik Böving
Mario Carneiro
Alex J. Best
tydeu
Calvin Lee
F. G. Dorais
Jeremy Salwen
Sebastian Ullrich
Xubai Wang