Commit Graph

50 Commits (main)

Author SHA1 Message Date
Joshua Potter cda229ac12 Add nameext to distinguish PDF and HTML files. 2023-12-14 17:09:10 -07: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 d70b47c9af fix: try to increase heartbeat limit further 2023-11-18 23:43:02 +01:00
Henrik Böving 8c9e5cf135 fix: temporarily disable equation rendering 2023-11-18 23:11:44 +01:00
Henrik Böving ec2561f34b feat: use Kyle Miller's instance analysis algorithm 2023-11-05 09:57:31 +01: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 402cfda104 fix: reintroduce basic definition lemmas
Closes: #155
2023-10-08 11:33:27 +02:00
Mario Carneiro 96870507c5 feat: add jump-src.js for #src links 2023-09-21 11:38:22 +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
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 8ea6a55a82 chore: print named instance arguments 2023-09-10 00:18:52 +02:00
Henrik b0319462f1 feat: print nameless instances properly 2023-09-09 23:56:21 +02:00
Henrik 13fb60f8a3 feat: deprecated attr 2023-09-08 23:06:56 +02:00
Henrik dc9549e2e6 feat: cleanup def rendering and add reducible attribute 2023-08-28 20:38:19 +02:00
Calvin Lee cc552ed570 add colorscheme toggle 2023-06-09 23:39:59 +02:00
Henrik Böving 9b028566ec fix: get rid off deleted attribute 2023-04-16 09:54:48 +02:00
Henrik Böving 5ab6766eb1 fix: #113 2023-02-16 19:51:35 +01:00
Jeremy Salwen 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
Henrik Böving 3a5c0db46b style: refactor process to Lean 4 compiler style 2023-01-01 19:30:28 +01:00
Henrik Böving 345036e800 chore: update toolchain 2022-12-22 16:19:23 +01:00
Henrik Böving 72034b0831 feat: linkify builtin types 2022-11-22 21:07:59 +01:00
Henrik Böving e402ee94b1 feat: look for builtin type instances 2022-11-22 21:07:59 +01:00
Mario Carneiro 9aef28b16e
chore: update toolchain 10-20 (#86) 2022-10-20 19:51:26 +02:00
Henrik Böving 64f627a295
chore: toolchain upgrade (#82)
Halleluja!
2022-10-05 12:05:58 +02:00
Henrik Böving d29e14a26a chore: update toolchain and dependencies 2022-08-09 23:30:43 +02:00
tydeu 2cc851aaf1 fix: include top-level modules in hierarchy and exclude non-html 2022-07-23 22:02:20 -04:00
Henrik Böving 247b930364 feat: instances for 2022-07-23 15:40:08 +02:00
Henrik Böving 3aae640f69 chore: structure ctor style 2022-07-23 13:37:17 +02:00
Henrik Böving 04387711de chore: remove unused variables 2022-07-23 13:04:36 +02:00
Henrik Böving ed4cee2eae chore: style, change $ to <| 2022-07-23 13:01:25 +02:00
Henrik Böving 2ffff99f90 feat: instances from JSON 2022-07-22 16:15:37 +02:00
Henrik Böving bb9b55ef2c feat: Step 1 for full separate builds with global info 2022-07-22 14:48:36 +02:00
Henrik Böving c29cf7b70c feat: index shall not depend on importing things 2022-07-22 00:34:13 +02:00
Henrik Böving c35d750e67 feat: Single shall not be transitive 2022-07-21 23:15:20 +02:00
Henrik Böving eea23d332a feat: Fully separated builds 2022-07-21 22:43:33 +02:00
Henrik Böving 4bc7a682ec feat: implementation of separate staged builds 2022-07-21 18:26:01 +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 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 036769357a doc: Document Process.Attributes 2022-05-20 09:41:52 +02:00
Henrik Böving e31d544e27 doc: Process.Analyze 2022-05-20 09:30:59 +02:00
Henrik Böving 56bd8c3ced doc: Process.Base 2022-05-20 09:23:33 +02:00
Henrik Böving b58b1b315b refactor: finally split upt the process module 2022-05-20 00:36:21 +02:00
Henrik Böving 279df92555 refactor: restructure the modules 2022-05-19 20:41:07 +02:00