Skip to content

Commit

Permalink
chore: update-stage0-commit cmake target (#3692)
Browse files Browse the repository at this point in the history
Automate creating the commit
  • Loading branch information
Kha authored Apr 4, 2024
1 parent e41cd31 commit 46964b6
Show file tree
Hide file tree
Showing 3 changed files with 10 additions and 14 deletions.
4 changes: 4 additions & 0 deletions CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -78,6 +78,10 @@ add_custom_target(update-stage0
COMMAND $(MAKE) -C stage1 update-stage0
DEPENDS stage1)

add_custom_target(update-stage0-commit
COMMAND $(MAKE) -C stage1 update-stage0-commit
DEPENDS stage1)

add_custom_target(test
COMMAND $(MAKE) -C stage1 test
DEPENDS stage1)
Expand Down
16 changes: 2 additions & 14 deletions doc/dev/bootstrap.md
Original file line number Diff line number Diff line change
Expand Up @@ -81,20 +81,8 @@ or using Github CLI with
gh workflow run update-stage0.yml
```

Leaving stage0 updates to the CI automation is preferrable, but should you need
to do it locally, you can use `make update-stage0` in `build/release`, to
update `stage0` from `stage1`, `make -C stageN update-stage0` to update from
another stage, or `nix run .#update-stage0-commit` to update using nix.

Updates to `stage0` should be their own commits in the Git history. So should
you have to include the stage0 update in your PR (rather than using above
automation after merging changes), commit your work before running `make
update-stage0`, commit the updated `stage0` compiler code with the commit
message:
```
chore: update stage0
```
and coordinate with the admins to not squash your PR.
Leaving stage0 updates to the CI automation is preferable, but should you need to do it locally, you can use `make update-stage0-commit` in `build/release` to update `stage0` from `stage1` or `make -C stageN update-stage0-commit` to update from another stage.
This command will automatically stage the updated files and introduce a commit, so make sure to commit your work before that. Then coordinate with the admins to not squash your PR so that stage 0 updates are preserved as separate commits.

## Further Bootstrapping Complications

Expand Down
4 changes: 4 additions & 0 deletions src/CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -588,6 +588,10 @@ if(PREV_STAGE)
COMMAND bash -c 'CSRCS=${CMAKE_BINARY_DIR}/lib/temp script/update-stage0'
DEPENDS make_stdlib
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/..")

add_custom_target(update-stage0-commit
COMMAND git commit -m "chore: update stage0"
DEPENDS update-stage0)
endif()

# use Bash version for building, use Lean version in bin/ for tests & distribution
Expand Down

0 comments on commit 46964b6

Please sign in to comment.