Commit Graph

424 Commits (d70c8b78f85d750557e52c63dff29c52a84feff9)

Author SHA1 Message Date
Henrik Böving d70c8b78f8 fix: always keep a consistent font size 2023-11-13 23:19:19 +01:00
Henrik Böving 162de4ad98 feat: consistent font inheritance 2023-11-11 17:18:46 +01:00
Henrik Böving 756e5a0db8 feat: make @YaelDillies happier 2023-11-11 16:03:50 +01:00
Henrik Böving 78e472a973 feat: totally uncontroversial font change 2023-11-11 15:41:38 +01:00
Henrik Böving e859e2f777 chore: update dependencies 2023-11-05 09:59:30 +01:00
Henrik Böving ec2561f34b feat: use Kyle Miller's instance analysis algorithm 2023-11-05 09:57:31 +01:00
Scott Morrison 8bccb92b53
chore: bump lean-toolchain to v4.2.0-rc4
Fixes a potential data loss bug. All projects should update their toolchain as soon as possible.

Please see https://github.com/leanprover/lean4/releases/tag/v4.2.0-rc4
and the [zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Potential.20data.20loss.20from.20.60lake.20clean.60.20with.204.2E2.2E0-rc2.2F3/near/397875701) for more information.
2023-10-22 09:25:36 +11:00
Henrik Böving 0f1b99c1c1 fix: Second miss-handling of free variables 2023-10-17 21:32:48 +02:00
Henrik Böving bc9cba13b1 fix: First miss-handling of free variables 2023-10-17 20:21:24 +02:00
Henrik Böving f15d561411 chore: update toolchain 2023-10-17 20:21:24 +02:00
Alex J Best 5b4d779b31 Update DocGen4/Output/DocString.lean 2023-10-16 20:42:29 +02:00
Alex J. Best 074c783259 feat: html escape docstrings 2023-10-16 20:42:29 +02: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 402cfda104 fix: reintroduce basic definition lemmas
Closes: #155
2023-10-08 11:33:27 +02:00
Henrik Böving 3a9cfabe58 fix: trace lake jobs properly 2023-10-08 11:30:11 +02:00
Henrik Böving fa8c9d771a feat: Always document the transitive closure of a module 2023-10-07 21:07:55 +02:00
Henrik Böving 649e7791fa feat: Respect srcDir configuration in lake 2023-09-27 09:52:22 +02:00
Henrik Böving e1bd706c91 ux: better git error reporting 2023-09-26 23:18:31 +02:00
Mario Carneiro 96870507c5 feat: add jump-src.js for #src links 2023-09-21 11:38:22 +02:00
Mario Carneiro 800041825e fix: don't fetch unused cache, FF fixes 2023-09-21 09:24:37 +02:00
Alex J. Best cf072e2be0 fix navbar break 2023-09-18 23:55:19 +02:00
Alex J. Best a088f648b1 clean the expand-nav implementation up a bit 2023-09-18 23:55:19 +02:00
Alex J. Best 924be4c7d8 feat: expand the current file in the navbar 2023-09-18 23:55:19 +02:00
Henrik Böving 34185d4fef chore: debug 2023-09-18 22:54:37 +02:00
Henrik Böving 7e89b462f0 chore: update toolchain 2023-09-18 22:08:46 +02:00
Ruben Van de Velde 19568c0659 feat: autolink references to files 2023-09-16 14:37:22 +02:00
Henrik Böving f9b5a2903a fix: header-data.bmp 2023-09-15 00:39:28 +02:00
Henrik f7307953d8 fix: sort expression printing 2023-09-10 14:44:14 +02:00
Henrik f0967b7072 chore: reduce debounce time 2023-09-10 12:53:48 +02:00
Henrik 08de0ad10c feat: reduce JSON data size 2023-09-10 12:39:49 +02:00
josojo a0779fa7de Update lean-toolchain
Usually, the tags are named with a prefixed v. The same is true for the current releases
2023-09-10 12:22:14 +02:00
Henrik 3c033966e7 feat: logStep in the facet to show progress 2023-09-10 11:47:36 +02:00
Henrik a090875215 refactor: Remove unnecessary cases in type analysis 2023-09-10 11:07:22 +02:00
Henrik 7dc8018130 refactor: Less manual manipulation of expressions 2023-09-10 10:13:30 +02:00
Henrik 6abc8bb769 feat: print location of errors during documentation 2023-09-10 01:02:52 +02:00
Henrik b2119d4db6 feat: add the proposed search timeout 2023-09-10 00:39:39 +02:00
Henrik 8ea6a55a82 chore: print named instance arguments 2023-09-10 00:18:52 +02:00
Henrik 36e1b863a7 chore: remove pointless prints 2023-09-09 23:59:25 +02:00
Henrik b0319462f1 feat: print nameless instances properly 2023-09-09 23:56:21 +02:00
Henrik 3c80369cca Merge remote-tracking branch 'alexjbest/only-linkify-lean' into only-linkify-lean 2023-09-09 23:26:00 +02:00
Henrik 13fb60f8a3 feat: deprecated attr 2023-09-08 23:06:56 +02:00
Henrik 9efe8f1df7 chore: update toolchain 2023-09-08 09:51:38 +02:00
tydeu 0b52010291 fix: source links for Lake 2023-08-30 19:01:03 +02:00
Henrik dc9549e2e6 feat: cleanup def rendering and add reducible attribute 2023-08-28 20:38:19 +02:00
tydeu 34165f36e6 feat: include Lake as part of the core docs 2023-08-24 10:10:16 +02:00
Scott Morrison a9da3c9e48 chore: update toolchain 2023-08-22 19:25:10 +02:00
Henrik d805539b34 chore: update toolchain 2023-08-18 11:07:52 +02:00
Eric Wieser 627bcb0626 Remove extra spacing 2023-08-18 11:00:32 +02:00
Eric Wieser d3d67c1d92 Do the same for inductives 2023-08-18 11:00:32 +02:00
Eric Wieser e5ff71991d Put field docstrings after the field 2023-08-18 11:00:32 +02:00