Commit Graph

  • 71af8db54b feat: Declaration data into separate directory Henrik Böving 2022-07-21 21:05:19 +0200
  • f0a1ec2835
    Merge pull request #71 from leanprover/inductive-docstring Henrik Böving 2022-07-21 20:29:55 +0200
  • ddaf76a401 chore: remove unused code Henrik Böving 2022-07-21 20:27:54 +0200
  • 601b895e89 feat: Inductive constructor doc strings Henrik Böving 2022-07-21 20:23:27 +0200
  • 55f0399ed3
    Merge pull request #70 from leanprover/setup-single Henrik Böving 2022-07-21 19:17:26 +0200
  • 9b2326dec3 feat: merge init and finalize Henrik Böving 2022-07-21 19:07:35 +0200
  • 8d6376c019 doc: Document the staged build Henrik Böving 2022-07-21 18:32:09 +0200
  • 4bc7a682ec feat: implementation of separate staged builds Henrik Böving 2022-07-21 18:26:01 +0200
  • fbbdb21795 fix: remove redundant argument Henrik Böving 2022-07-21 02:25:26 +0200
  • 9962e5037a prettify: Make the Output.lean refactor prettier Henrik Böving 2022-07-21 02:21:07 +0200
  • 25b1ddb66b feat: Preparations to split doc-gen build process Henrik Böving 2022-07-21 01:40:04 +0200
  • 0f9b80abb2
    Merge pull request #68 from leanprover/update-lean Henrik Böving 2022-07-20 16:38:06 +0200
  • 5f45c8dadc chore: update toolchain Henrik Böving 2022-07-20 16:18:57 +0200
  • 6e3e65015d
    Merge pull request #66 from leanprover/update Henrik Böving 2022-07-04 09:23:05 +0200
  • 351cbc56b6 chore: update lean nightly Henrik Böving 2022-07-03 15:35:21 +0200
  • 1f6ab11ead chore: update toolchain Henrik Böving 2022-06-24 20:46:36 +0200
  • 5b56be76f2 chore: Cleanup HTML syntax and pretty printing Henrik Böving 2022-06-21 20:54:29 +0200
  • 38e02c5f65
    Merge pull request #56 from leanprover/leanink Henrik Böving 2022-06-20 23:16:46 +0200
  • 898496ca51 feat: update CI and README Henrik Böving 2022-06-20 22:51:22 +0200
  • be3caa9e1a feat: Basic semantic highlighting support Henrik Böving 2022-06-20 22:06:24 +0200
  • 49b2f019b7 feat: type hovers Henrik Böving 2022-06-20 19:21:50 +0200
  • 9f50966339 feat: initial LeanInk HTML generation Henrik Böving 2022-06-20 18:39:55 +0200
  • 199c7af17a feat: LeanInk all the files, HTML generation missing Henrik Böving 2022-06-20 00:31:09 +0200
  • 0acf82bcbe chore: update Unicode.lean Henrik Böving 2022-06-19 17:03:26 +0200
  • e485bec9a6
    Merge pull request #55 from leanprover/update-lean Henrik Böving 2022-06-19 16:46:26 +0200
  • 7c9237ffb4 chore: update compiler and lake Henrik Böving 2022-06-19 16:41:59 +0200
  • f5b2d7ab36
    Merge pull request #54 from leanprover/update Henrik Böving 2022-05-27 22:25:51 +0200
  • eb9e8fc5f2 Merge branch 'update' of github.com:leanprover/doc-gen4 into update Henrik Böving 2022-05-27 22:20:50 +0200
  • e8fb9a7f0f chore: update to latest nightly Henrik Böving 2022-05-21 12:50:55 +0200
  • 5aa58aac4c chore: update to latest nightly Henrik Böving 2022-05-21 12:50:55 +0200
  • 3de930be31
    Merge pull request #53 from leanprover/structuring Henrik Böving 2022-05-20 09:47:44 +0200
  • 036769357a doc: Document Process.Attributes Henrik Böving 2022-05-20 09:41:52 +0200
  • e31d544e27 doc: Process.Analyze Henrik Böving 2022-05-20 09:30:59 +0200
  • 56bd8c3ced doc: Process.Base Henrik Böving 2022-05-20 09:23:33 +0200
  • d519ef6b58 fix: adapt the rest of the program to the process refactor Henrik Böving 2022-05-20 00:36:43 +0200
  • b58b1b315b refactor: finally split upt the process module Henrik Böving 2022-05-20 00:36:21 +0200
  • 8e70777059 chore: copyright header Henrik Böving 2022-05-19 21:56:43 +0200
  • 12fe918b2d doc: Output.Template Henrik Böving 2022-05-19 21:53:03 +0200
  • 8e4b7bdb50 doc: Output.Structure Henrik Böving 2022-05-19 21:52:54 +0200
  • 3fd17bd261 doc: Output.NotFound Henrik Böving 2022-05-19 21:49:50 +0200
  • 94ce87d11a doc: Output.Navbar Henrik Böving 2022-05-19 21:49:25 +0200
  • 20e136bb27 refactor: centralized methods for internal linking infrastructure Henrik Böving 2022-05-19 21:40:22 +0200
  • e0bf4ad28c doc: Output/Definition Henrik Böving 2022-05-19 21:07:44 +0200
  • bdd4a5f612 doc: Output.Base Henrik Böving 2022-05-19 21:05:17 +0200
  • 0b8f7a1397 doc: Output top level module Henrik Böving 2022-05-19 20:54:42 +0200
  • 653c67e9b7 doc: SourceLinker Henrik Böving 2022-05-19 20:52:54 +0200
  • 43f7786523 refactor: pull source linker into submodule Henrik Böving 2022-05-19 20:48:26 +0200
  • c05a9cf5e5 doc: Load Henrik Böving 2022-05-19 20:45:12 +0200
  • 5fd076530e doc: IncludeStr Henrik Böving 2022-05-19 20:41:45 +0200
  • 279df92555 refactor: restructure the modules Henrik Böving 2022-05-19 20:36:35 +0200
  • 2e4642e17c chore: port legacy syntax to rawIdent Henrik Böving 2022-05-19 17:16:40 +0200
  • 953d9dc304
    Merge pull request #52 from Kha/rawIdent Henrik Böving 2022-05-19 11:43:28 +0200
  • 41f6eb0835 refactor: use `rawIdent` Sebastian Ullrich 2022-05-19 11:14:47 +0200
  • fc48deaf81
    Merge pull request #51 from leanprover/compiler-attrs Henrik Böving 2022-04-19 20:32:56 +0200
  • 24a24d75c7 feat: csimp attribute Henrik Böving 2022-04-19 20:28:30 +0200
  • 9a6bf85588 chore: update toolchain Henrik Böving 2022-04-19 20:18:28 +0200
  • ea66f7f243 feat: export attribute Henrik Böving 2022-04-12 19:09:42 +0200
  • 2128e789ca
    Merge pull request #49 from leanprover/ctor-field-docs Henrik Böving 2022-04-09 22:34:04 +0200
  • a7c00d95e6 feat: Render doc comments for structure fields Henrik Böving 2022-04-09 21:39:34 +0200
  • 89dd2fa46e chore: upgrade compiler version Henrik Böving 2022-04-09 19:18:21 +0200
  • 211ade7828 feat: doc strings in ctors and structure fields Henrik Böving 2022-04-09 17:27:06 +0200
  • fa2f2b8e05
    Merge pull request #48 from leanprover/fix-search Henrik Böving 2022-04-07 13:20:31 +0200
  • 3ac6ddd1ab fix: port the SITE_ROOT fix to find.js Henrik Böving 2022-04-07 13:14:01 +0200
  • 67402506c7 fix: links in search Henrik Böving 2022-04-07 12:44:33 +0200
  • 06c20ee46f dynamically change SITE_ROOT since we are relative now Henrik Böving 2022-04-07 12:39:32 +0200
  • 00837fd089
    Merge pull request #39 from bollu/feb-21-relative-paths-manual-depth Henrik Böving 2022-04-07 08:29:01 +0200
  • 4bc149a1fb Fix diff nits Siddharth Bhat 2022-04-07 00:53:06 +0100
  • 10ed2d489d update README Siddharth Bhat 2022-04-07 00:49:05 +0100
  • 9570f25312 cleanup code Siddharth Bhat 2022-04-07 00:48:12 +0100
  • f5b9e02766 modify deploy_docs to not need relative path Siddharth Bhat 2022-04-07 00:44:49 +0100
  • 9eec1cf1ad URLs now work; Data fetching does not? Siddharth Bhat 2022-04-07 00:31:27 +0100
  • 45374eeced
    Merge pull request #47 from xubaiw/brave-indexeddb Henrik Böving 2022-03-14 18:58:03 +0100
  • 0ec492ba98 fix: error handling for declaration data Xubai Wang 2022-03-14 10:59:25 +0800
  • 5e2e30c4f6
    Merge pull request #46 from leanprover/lake Henrik Böving 2022-03-06 18:55:29 +0100
  • 9cc4c787e6 feat: lake integration Henrik Böving 2022-03-06 18:51:06 +0100
  • 5535616725 chore: Bump toolchain Henrik Böving 2022-03-06 16:48:49 +0100
  • 6492f827b7 chore: bump toolchain Henrik Böving 2022-02-27 18:01:34 +0100
  • 24b0094574
    Merge pull request #45 from xubaiw/better-includestr Henrik Böving 2022-02-26 16:39:38 +0100
  • 5f7d380ab7 refactor: make include_str relative to file Xubai Wang 2022-02-26 09:41:25 +0800
  • d63145c304
    Merge pull request #42 from leanprover/cli Henrik Böving 2022-02-23 22:57:52 +0100
  • 34d2239b68 feat: actual CLI Henrik Böving 2022-02-23 22:54:10 +0100
  • 9dd5e316c1
    Merge pull request #38 from xubaiw/win-find Henrik Böving 2022-02-23 19:44:47 +0100
  • 58ce86f93d
    Merge pull request #41 from xubaiw/navbar Henrik Böving 2022-02-23 19:18:22 +0100
  • dca4e42665 fix: filter out nonexist modules Xubai Wang 2022-02-23 23:33:34 +0800
  • a50ca857aa fix: wrap navbar overflow Xubai Wang 2022-02-23 23:28:15 +0800
  • a5dfba5f1c fix: fix navbar centering Xubai Wang 2022-02-23 23:09:10 +0800
  • 2b217ecda0 fix: fix find search Xubai Wang 2022-02-23 05:32:37 +0800
  • a18e343829 refactor: change find syntax Xubai Wang 2022-02-23 04:26:20 +0800
  • e4ccc5cf50 feat: add browser cache for data fix search name Xubai Wang 2022-02-22 23:20:20 +0800
  • 004977e6e4 refactor: use strict match for find Xubai Wang 2022-02-22 15:01:14 +0800
  • f23556739f refactor: clean up javascript code Xubai Wang 2022-02-22 12:40:14 +0800
  • 9e867f5151 refactor: make site-root an actual file Xubai Wang 2022-02-21 23:29:23 +0800
  • 91891fc4fd Generate relative paths for documentation. Siddharth Bhat 2022-02-15 11:12:17 +0000
  • bc0dd3b48a feat: add src endpoint Xubai Wang 2022-02-21 01:38:12 +0800
  • 59707cda58 refactor: use js for find Xubai Wang 2022-02-21 01:12:49 +0800
  • 5e93038023 refactor: use js modules Xubai Wang 2022-02-21 00:06:15 +0800
  • 842e243241 revert: use bmp extension again Xubai Wang 2022-02-20 23:45:31 +0800
  • 73f7906357 refactor: move script into head Xubai Wang 2022-02-20 23:42:46 +0800
  • 28bb2abe40
    Merge pull request #36 from leanprover/better-equations Henrik Böving 2022-02-20 16:24:50 +0100
  • a89cf7d7a4 refactor: move siteRoot to separate file Xubai Wang 2022-02-20 23:24:08 +0800