27cbf8ddd2
chore: update toolchain
2023-03-04 12:48:47 +01:00
c3faad1730
help break_within to split names at `.`
2023-03-04 12:47:30 +01:00
9220cd74b1
fix implicit arg wrapping
2023-03-04 12:20:05 +01:00
5ab6766eb1
fix : #113
2023-02-16 19:51:35 +01:00
54cf445e12
fix : #114
2023-02-16 18:14:40 +01:00
162de994c2
Add comment to README about need for copying css and js files.
2023-02-03 21:10:44 +01:00
1cb84f6d74
Add filters for search results based on kind.
...
This allows you to search defs, theorems, etc independently.
2023-02-01 15:15:45 +01:00
1c44e861be
fix: search.html for relative roots
2023-01-29 14:07:21 +01:00
3a977a94ca
Fix issues with Search page impelementation
...
- Makes the autocomplete results highlight with up/down arrows.
- Allows you to unselect autocomplete results by using arrow keys.
- Fixed a bug in previous commits where enter did not take you to autocomplete result.
- Return now goes to the search page if no autocomplete result is selected.
- Search results table now properly wraps. (It would be nice to make it wider but I wasn't able to).
- Fixed a bug in the previous commit where docs were not showing, due to failure to copy a modified js file.
2023-01-28 23:00:53 +01:00
1575eeedd2
Add definition doc string to search result page.
...
Adds a two-column table to the search results so you can see the doc string next to
the result. The doc string is not parsed/converted to markdown yet, but that could
be done later.
2023-01-28 23:00:53 +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
7b0ebfa527
Add section to README about development of doc-gen4
2023-01-25 18:32:45 +01:00
09dbebed9c
chore: QoL updates for deploy_docs.sh
2023-01-05 00:02:41 +01:00
f37579aaf7
feat: use mathlib4 build cache
2023-01-04 23:25:35 +01:00
8ac4e35587
fix: s/master/main
2023-01-02 10:07:10 +01:00
247dca1182
feat: truly limit the deploy to master
2023-01-01 22:15:08 +01:00
dd5aae412d
fix: attempt to fix CI again
2023-01-01 21:11:30 +01:00
a18b27f4c1
feat: attempt to improve usability of the file tree
2023-01-01 20:21:10 +01:00
d5ef8006b7
style: Lean 4 compiler style in LeanInk
2023-01-01 19:53:21 +01:00
f74443a673
style: Lean 4 compiler style in output
2023-01-01 19:51:01 +01:00
3a5c0db46b
style: refactor process to Lean 4 compiler style
2023-01-01 19:30:28 +01:00
a5caefc03f
fix: regression in import names
2023-01-01 18:59:19 +01:00
bdf803b100
chore: update toolchain
2022-12-23 18:20:56 +01:00
03e6572584
fix: mention (a : α) → β a notation in foundational types section
2022-12-23 13:28:57 +01:00
345036e800
chore: update toolchain
2022-12-22 16:19:23 +01:00
f221bbdcff
fix: save the expansion state of the tree again
2022-12-13 20:01:11 +01:00
8fd0520dc0
chore: slow down CI cycles
2022-12-13 19:37:28 +01:00
327fdf0ddd
feat: short names in side bar
2022-12-13 19:37:28 +01:00
84a116ac43
chore: update toolchain
2022-12-13 19:37:28 +01:00
7009910876
chore: update toolchain
2022-12-03 17:43:12 +01:00
5e96952a58
chore: update toolchain
2022-12-02 17:55:27 +01:00
69d48b174d
chore: update toolchain
2022-11-22 21:21:54 +01:00
72034b0831
feat: linkify builtin types
2022-11-22 21:07:59 +01:00
b22818b971
feat: render foundational types info
2022-11-22 21:07:59 +01:00
bdede38f12
chore: update toolchain
2022-11-22 21:07:59 +01:00
e402ee94b1
feat: look for builtin type instances
2022-11-22 21:07:59 +01:00
664a86e08b
fix: minor style improvements
2022-11-06 13:53:23 +01:00
6c8b79a539
chore: update toolchain
2022-10-28 23:47:09 +02:00
120a81d25e
chore: upgrade dependencies
2022-10-20 19:53:02 +02:00
9aef28b16e
chore: update toolchain 10-20 ( #86 )
2022-10-20 19:51:26 +02:00
153982f982
Work around unsupported RegExp lookbehind in WebKit. ( #85 )
...
* Work around unsupported RegExp lookbehind in WebKit.
* Update static/find/find.js
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
2022-10-20 18:21:33 +02:00
d7fe046e94
ci: also run on scheduled builds
2022-10-06 22:10:53 +02:00
72227e4b11
attempt to fix master CI ( #84 )
2022-10-05 13:00:43 +02:00
64f627a295
chore: toolchain upgrade ( #82 )
...
Halleluja!
2022-10-05 12:05:58 +02:00
b07faa65fe
Merge pull request #81 from leanprover/fix-ci
...
fix : CI
2022-08-18 22:12:53 +02:00
07332cad93
fix : CI
2022-08-18 22:03:07 +02:00
b18f4e52ed
Merge pull request #80 from gebner/bump220818
...
chore: update toolchain
2022-08-18 13:41:59 +02:00
9dc1889de6
chore: update toolchain
2022-08-18 11:33:49 +02:00
422e6bec91
Merge pull request #79 from leanprover/unused-import
...
chore: drop unused import
2022-08-13 12:09:20 +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
Henrik Böving
Max Taldykin
Jeremy Salwen
Seppel3210
Parth Shastri
Mario Carneiro
Ruben Van de Velde
Gabriel Ebner
Sebastian Ullrich