Commit Graph

  • 1e234aa736 Fix subshell usage. main Joshua Potter 2023-12-16 07:58:24 -0700
  • 9bd217dc37 Fixup run_pdflatex script now that bookshelf-doc is no longer used as a submodule. Joshua Potter 2023-12-15 19:43:18 -0700
  • 5eb0d9f1de Update toolchain to v4.3.0. Joshua Potter 2023-12-15 18:21:01 -0700
  • cfa8d0e042 Update dependencies. Joshua Potter 2023-12-15 16:00:43 -0700
  • c29c914910 Allow using environment variables for project url and commit. Joshua Potter 2023-12-15 14:41:28 -0700
  • d2db077fc4
    Update README.md Joshua Potter 2023-12-14 17:14:04 -0700
  • cda229ac12 Add nameext to distinguish PDF and HTML files. Joshua Potter 2023-12-14 16:55:32 -0700
  • aa25e084d2 Update index and add pdflatex generation script. Joshua Potter 2023-12-14 15:27:12 -0700
  • 86d5c219a9 feat: compress module urls and importedBy info into one Henrik Böving 2023-12-10 00:37:14 +0100
  • 53ecc225fe doc: fix path to root of docs Bulhwi Cha 2023-12-04 12:13:18 +0900
  • 3cc5df1be7 feat: fix #166 Henrik Böving 2023-11-24 13:40:20 +0100
  • e5118b8f20 feat: show the type of exists and fun arguments Henrik Böving 2023-11-24 13:13:19 +0100
  • e966ab8523 fix: we want to catch runtime exceptions in doc-gen4 Henrik Böving 2023-11-18 23:49:28 +0100
  • d70b47c9af fix: try to increase heartbeat limit further Henrik Böving 2023-11-18 23:43:02 +0100
  • 8c9e5cf135 fix: temporarily disable equation rendering Henrik Böving 2023-11-18 23:06:55 +0100
  • b85fd6cbeb fix: lake changed the build directory Henrik Böving 2023-11-18 22:13:54 +0100
  • ca82b428ed doc: Document and fix lake config changes with -R Henrik Böving 2023-11-18 22:04:42 +0100
  • 2ba3e84eca doc: Clearly spell out what happens on projects that fail to compile Henrik Böving 2023-11-18 22:00:12 +0100
  • 96147eaa0c feat: type doc right below initial type naming Henrik Böving 2023-11-13 23:13:58 +0100
  • d70c8b78f8 fix: always keep a consistent font size Henrik Böving 2023-11-13 23:13:26 +0100
  • 162de4ad98 feat: consistent font inheritance Henrik Böving 2023-11-11 17:18:46 +0100
  • 756e5a0db8 feat: make @YaelDillies happier Henrik Böving 2023-11-11 16:03:50 +0100
  • 78e472a973 feat: totally uncontroversial font change Henrik Böving 2023-11-11 15:34:42 +0100
  • e859e2f777 chore: update dependencies Henrik Böving 2023-11-05 09:59:30 +0100
  • ec2561f34b feat: use Kyle Miller's instance analysis algorithm Henrik Böving 2023-11-05 09:38:22 +0100
  • 8bccb92b53
    chore: bump lean-toolchain to v4.2.0-rc4 Scott Morrison 2023-10-22 09:25:36 +1100
  • 0f1b99c1c1 fix: Second miss-handling of free variables Henrik Böving 2023-10-17 21:32:48 +0200
  • bc9cba13b1 fix: First miss-handling of free variables Henrik Böving 2023-10-17 20:21:14 +0200
  • f15d561411 chore: update toolchain Henrik Böving 2023-10-17 20:21:00 +0200
  • 5b4d779b31 Update DocGen4/Output/DocString.lean Alex J Best 2023-10-16 17:29:39 +0100
  • 074c783259 feat: html escape docstrings Alex J. Best 2023-10-16 17:27:36 +0100
  • f9d9875671 perf: Don't call Lake from within doc-gen anymore Henrik Böving 2023-10-09 09:30:16 +0200
  • 402cfda104 fix: reintroduce basic definition lemmas Henrik Böving 2023-10-08 11:33:27 +0200
  • 3a9cfabe58 fix: trace lake jobs properly Henrik Böving 2023-10-08 11:30:11 +0200
  • fa8c9d771a feat: Always document the transitive closure of a module Henrik Böving 2023-10-07 21:07:55 +0200
  • 649e7791fa feat: Respect srcDir configuration in lake Henrik Böving 2023-09-27 09:52:22 +0200
  • e1bd706c91 ux: better git error reporting Henrik Böving 2023-09-26 23:15:58 +0200
  • 96870507c5 feat: add jump-src.js for #src links Mario Carneiro 2023-09-21 05:27:33 -0400
  • 800041825e fix: don't fetch unused cache, FF fixes Mario Carneiro 2023-09-20 21:37:52 -0400
  • cf072e2be0 fix navbar break Alex J. Best 2023-09-18 22:11:40 +0100
  • a088f648b1 clean the expand-nav implementation up a bit Alex J. Best 2023-09-18 22:08:34 +0100
  • 924be4c7d8 feat: expand the current file in the navbar Alex J. Best 2023-09-18 22:03:40 +0100
  • 34185d4fef chore: debug Henrik Böving 2023-09-18 22:54:37 +0200
  • 7e89b462f0 chore: update toolchain Henrik Böving 2023-09-18 22:03:27 +0200
  • 19568c0659 feat: autolink references to files Ruben Van de Velde 2023-09-13 21:56:04 +0200
  • f9b5a2903a fix: header-data.bmp Henrik Böving 2023-09-15 00:39:28 +0200
  • f7307953d8 fix: sort expression printing Henrik 2023-09-10 14:44:14 +0200
  • f0967b7072 chore: reduce debounce time Henrik 2023-09-10 12:53:48 +0200
  • 08de0ad10c feat: reduce JSON data size Henrik 2023-09-10 12:39:37 +0200
  • a0779fa7de Update lean-toolchain josojo 2023-09-10 12:09:09 +0200
  • 3c033966e7 feat: logStep in the facet to show progress Henrik 2023-09-10 11:47:36 +0200
  • a090875215 refactor: Remove unnecessary cases in type analysis Henrik 2023-09-10 11:07:22 +0200
  • 7dc8018130 refactor: Less manual manipulation of expressions Henrik 2023-09-10 10:13:30 +0200
  • 6abc8bb769 feat: print location of errors during documentation Henrik 2023-09-10 01:02:52 +0200
  • b2119d4db6 feat: add the proposed search timeout Henrik 2023-09-10 00:39:39 +0200
  • 8ea6a55a82 chore: print named instance arguments Henrik 2023-09-10 00:18:52 +0200
  • 36e1b863a7 chore: remove pointless prints Henrik 2023-09-09 23:59:25 +0200
  • b0319462f1 feat: print nameless instances properly Henrik 2023-09-09 23:56:21 +0200
  • 3c80369cca Merge remote-tracking branch 'alexjbest/only-linkify-lean' into only-linkify-lean Henrik 2023-09-09 23:26:00 +0200
  • 13fb60f8a3 feat: deprecated attr Henrik 2023-09-08 23:06:56 +0200
  • 9efe8f1df7 chore: update toolchain Henrik 2023-09-08 09:51:38 +0200
  • 0b52010291 fix: source links for Lake tydeu 2023-08-29 17:45:58 -0400
  • dc9549e2e6 feat: cleanup def rendering and add reducible attribute Henrik 2023-08-28 20:38:19 +0200
  • 34165f36e6 feat: include Lake as part of the core docs tydeu 2023-08-23 14:50:03 -0400
  • a9da3c9e48 chore: update toolchain Scott Morrison 2023-08-22 11:50:34 +1000
  • d805539b34 chore: update toolchain Henrik 2023-08-18 11:07:52 +0200
  • 627bcb0626 Remove extra spacing Eric Wieser 2023-08-18 08:47:25 +0100
  • d3d67c1d92 Do the same for inductives Eric Wieser 2023-08-18 08:40:27 +0100
  • e5ff71991d Put field docstrings after the field Eric Wieser 2023-08-18 08:38:59 +0100
  • 596782c1fe chore: update toolchain Henrik 2023-08-06 16:07:24 +0200
  • 718b182a31 feat: more declaration data as JSON Henrik 2023-08-06 15:36:43 +0200
  • e09280bb3c feat: order instances and make them unique in their listing Henrik 2023-07-31 20:42:15 +0200
  • d688d05089 chore: update to new Lean/Lake version tydeu 2023-07-30 14:40:24 -0400
  • c312f00c88 chore: update toolchain Henrik 2023-07-30 20:45:40 +0200
  • 9b524d7c5a chore: mitigate #133 for now Henrik 2023-07-20 23:41:44 +0200
  • d65d26d7b9 fix: declaration-data.js local storage Henrik 2023-07-20 23:06:33 +0200
  • 92650029f0 chore: cleanup the other declaration-data.js singleton Henrik 2023-07-20 22:55:09 +0200
  • 5ce54e8e10 fix: race condition in declaration-data.js Henrik 2023-07-20 22:42:49 +0200
  • 9af4c720f0 chore: disable LeanInk because of weird panics Henrik 2023-06-25 15:14:43 +0200
  • 76a137dabc fix colors if media set to dark Calvin Lee 2023-06-09 14:10:06 -0700
  • 75d06a8153 hide color-changer if javascript is disabled Calvin Lee 2023-06-09 13:26:17 -0700
  • cc552ed570 add colorscheme toggle Calvin Lee 2023-06-07 22:52:51 -0700
  • b9cfae7f53 add dark mode Calvin Lee 2023-06-06 23:01:32 -0700
  • 2e021cc13c chore: update toolchain Henrik 2023-06-04 02:47:53 +0200
  • b91272c643 Improve installation instructions Denis Gorbachev 2023-05-26 15:05:21 +0700
  • e0eecc3334 feat: trigger search input when event handler is added Alex J. Best 2023-05-24 07:19:15 -0600
  • 5e2869b66d feat: don't copy .git folders in test Alex J. Best 2023-05-23 16:58:29 -0600
  • 306959b921 feat: list instances for defs also Alex J. Best 2023-05-23 16:57:16 -0600
  • e888e9cc38 feat: doc strings on ctors and fields are not monospaced anymore Henrik 2023-05-11 22:36:27 +0200
  • 007e03db3b chore: update toolchain and deps Henrik 2023-05-11 22:35:07 +0200
  • cf86cb4815 feat: attempt to source link directory dependencies Henrik 2023-04-24 00:18:29 +0200
  • 9ebc79338e chore: update toolchain Henrik 2023-04-22 01:25:13 +0200
  • a5c41d25a4 chore: cleanup CI after partial migration to mathlib4 Henrik 2023-04-22 01:01:19 +0200
  • 9b028566ec fix: get rid off deleted attribute Henrik Böving 2023-04-16 09:54:48 +0200
  • e5b44f1cdf chore: update toolchain Henrik Böving 2023-04-16 01:30:21 +0200
  • b9421b9a12 fix: Use Z(separator) instead of S(ymbol) category Henrik Böving 2023-03-27 14:38:13 +0200
  • 23eb55fc22 chore: update deps further Henrik Böving 2023-03-17 18:11:26 +0100
  • 7b65322c78 chore: update toolchain Henrik Böving 2023-03-17 08:26:21 +0100
  • 628ef2878e fix: properly comment out for the workaround Henrik Böving 2023-03-16 20:24:44 +0100
  • 5ab7d0bdd8 fix: unicode dependency F. G. Dorais 2023-03-14 07:32:32 -0400