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

doc: describe commit conventions for update-stage0

Browse source 
Updates to stage0 should be their own commits.
This commit is contained in:
David Christiansen 2023-10-10 22:13:05 +02:00 • committed by Sebastian Ullrich
parent 97f5ad7804
commit 7450a8cfa3
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/bootstrap.md
View file

@ -69,6 +69,13 @@ Finally, when we want to use new language features in the library, we need to
update the stage 0 compiler, which can be done via `make -C stageN update-stage0`.
`make update-stage0` without `-C` defaults to stage1.
Updates to `stage0` should be their own commits in the Git history. In
other words, before running `make update-stage0`, please commit your
work. Then, commit the updated `stage0` compiler code with the commit message:
```
chore: update stage0
```
## Further Bootstrapping Complications
As written above, changes in meta code in the current stage usually will only