Joachim Breitner
c91ece4f58
doc: typo Runnign ( #3018 )
2023-12-04 16:55:07 +00:00
Joachim Breitner
5c2292a923
doc: In testing doc, suggest make to pick up new tests ( #2815 )
2023-12-04 10:29:49 +00:00
Sebastian Ullrich
ea5b55b8f2
doc: remove Nix docs
2023-12-01 08:32:20 +00:00
Sebastian Ullrich
3a0edd05e6
doc: VS Code dev setup ( #2961 )
...
* multi-root workspace
* default settings including .lean line length
* tasks `build` and `test`
---------
Co-authored-by: mhuisi <mhuisi@protonmail.com>
2023-11-30 08:35:03 +00:00
Joachim Breitner
fbefbce8c7
doc: Adjust contributor's docs to squash merging ( #2927 )
...
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
2023-11-21 10:13:43 +00:00
Eric Rodriguez
df6626f06b
doc: fix a link in development documentation #2780
2023-10-30 10:58:25 +11:00
David Christiansen
0700925bbe
doc: add a brief description of ccache
2023-10-11 09:30:46 +02:00
David Christiansen
7450a8cfa3
doc: describe commit conventions for update-stage0
...
Updates to stage0 should be their own commits.
2023-10-11 09:30:46 +02:00
David Thrane Christiansen
b3ff006eb8
doc: add missing character in testing.md
...
The testing docs omit the `s` in the `tests` directory at one point. The incorrect directory name threw me off - it will probably throw others off.
2023-10-06 11:07:10 +02:00
Sebastian Ullrich
dc60150b5a
chore: update domain
2023-09-20 15:13:27 -07:00
Sebastian Ullrich
befc4b997b
doc: writing good tests
2023-08-09 08:52:55 -07:00
Sebastian Ullrich
254582c000
doc: link to FFI examples
2023-08-04 10:45:53 +02:00
Scott Morrison
7213ff0065
doc: document generating releases via tags ( #2302 )
2023-07-13 17:39:54 +02:00
Mario Carneiro
dd5948d641
chore: snake-case attributes (part 1)
2022-10-19 09:28:08 -07:00
David Renshaw
5c7cf76575
doc: fix link to initialization section in ffi section
...
The current link goes to doc/dev#init, where there is nothing
about initialization. This PR fixes the link so that it points
to the initialization section lower down on the ffi page.
2022-10-07 19:11:59 +02:00
David Renshaw
4fa1a496b3
doc: Lean USize maps to C++ size_t, not usize_t
...
usize_t is not a standard C++ type.
See src/include/lean/lean.h for translations between USize and size_t.
2022-10-07 17:51:58 +02:00
Sebastian Ullrich
3ef1baae4a
doc: refine mdbook docs
2022-09-19 06:30:11 -07:00
Chris Lovett
e8335240d8
doc: update the mdbook instructions ( #1521 )
2022-09-03 11:08:38 +02:00
Mario Carneiro
37252e5fa7
chore: remove Bootstrap package
2022-09-02 16:39:03 -07:00
Mario Carneiro
bf89c5a0f5
chore: move Std -> Bootstrap
2022-08-29 01:26:12 -07:00
Sebastian Ullrich
be11e8e29b
doc: missing linebreak
2022-07-18 22:31:16 +02:00
Sebastian Ullrich
b6446902c2
feat: server.stderrAsMessages option
...
/cc @leodemoura
2022-04-19 22:29:26 +02:00
Sebastian Ullrich
d2c626e158
doc: refine development manual
2022-04-05 16:03:24 +02:00
Sebastian Ullrich
adcdd16d7a
doc: include missing chapter
2022-04-04 17:56:19 +02:00
Chris Lovett
6dc576121d
doc: replace quickstart leanpkg info with info about lake
2022-03-11 16:31:58 -08:00
Sebastian Ullrich
a7ba103e0a
chore: remove leanpkg
2022-02-04 19:03:40 +01:00
Sebastian Ullrich
f0f26728ed
doc: more about initializers
2022-01-20 18:55:57 +01:00
Sebastian Ullrich
c5b6968c86
chore: symlink to source from build dir
2021-11-19 10:09:26 +01:00
Sebastian Ullrich
941b4c21e0
chore: CRLF be gone
2021-11-09 09:49:09 +01:00
Sebastian Ullrich
c29ad9a9b3
doc: ubuntu: specify fewer versions that will become outdated anyway
2021-11-09 09:41:18 +01:00
Sebastian Ullrich
b2f331f502
doc: --load-dynlib
2021-11-04 15:32:07 -07:00
Sebastian Ullrich
571fc66864
doc: ffi: move into dev/
2021-10-29 08:46:31 -07:00
Chris Lovett
2860ba96f5
doc: fix some syntax and link in the docs, and more
2021-10-10 11:36:43 +02:00
Chris Lovett
2ca4188fc3
doc: somehow wsl2.md was created so the page on https://leanprover.github.io/lean4/doc/make/wsl2.html is empty. This fixes that.
2021-09-23 23:26:35 +02:00
Chris Lovett
3a20b6be8a
doc: add wsl setup docs and reorganize a new "dev" folder
2021-09-23 09:21:39 +02:00
