max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: add a brief description of ccache

Browse source
This commit is contained in:
David Christiansen 2023-10-10 22:16:29 +02:00 • committed by Sebastian Ullrich
parent 7450a8cfa3
commit 0700925bbe
1 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
doc/dev/index.md
View file

@ -64,3 +64,10 @@ simply by pushing a tag to your fork of the Lean 4 github repository
If you push `my-tag` to a fork in your github account `my_name`,
you can then put `my_name/lean4:my-tag` in your `lean-toolchain` file in a project using `lake`.
(You must use a tag name that does not start with a numeral, or contain `_`).
### `ccache`
Lean's build process uses [`ccache`](https://ccache.dev/) if it is
installed to speed up recompilation of the generated C code. Without
`ccache`, you'll likely spend more time than necessary waiting on
rebuilds - it's a good idea to make sure it's installed.