From 74adb0961c985bcf13bbc79e1973b65cacd2b999 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 2 May 2024 14:26:25 +0200 Subject: [PATCH] chore: add ./script/rebase-stage0.sh (#3984) heavily based on an script by Kim. --- doc/dev/bootstrap.md | 9 ++++++--- nix/bootstrap.nix | 2 +- script/lib/README.md | 2 ++ script/lib/rebase-editor.sh | 19 +++++++++++++++++++ script/{ => lib}/update-stage0 | 0 script/rebase-stage0.sh | 24 ++++++++++++++++++++++++ src/CMakeLists.txt | 2 +- 7 files changed, 53 insertions(+), 5 deletions(-) create mode 100644 script/lib/README.md create mode 100755 script/lib/rebase-editor.sh rename script/{ => lib}/update-stage0 (100%) create mode 100755 script/rebase-stage0.sh diff --git a/doc/dev/bootstrap.md b/doc/dev/bootstrap.md index 971fbf1341..554c39a308 100644 --- a/doc/dev/bootstrap.md +++ b/doc/dev/bootstrap.md @@ -84,10 +84,12 @@ gh workflow run update-stage0.yml 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. +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. -This command will automatically stage the updated files and introduce a commit, -so make sure to commit your work before that. +If you rebased the branch (either onto a newer version of `master`, or fixing +up some commits prior to the stage0 update, recreate the stage0 update commits. +The script `script/rebase-stage0.sh` can be used for that. The CI should prevent PRs with changes to stage0 (besides `stdlib_flags.h`) from entering `master` through the (squashing!) merge queue, and label such PRs @@ -95,6 +97,7 @@ with the `changes-stage0` label. Such PRs should have a cleaned up history, with separate stage0 update commits; then coordinate with the admins to merge your PR using rebase merge, bypassing the merge queue. + ## Further Bootstrapping Complications As written above, changes in meta code in the current stage usually will only diff --git a/nix/bootstrap.nix b/nix/bootstrap.nix index 5bd2cfff22..1b57f5dda3 100644 --- a/nix/bootstrap.nix +++ b/nix/bootstrap.nix @@ -180,7 +180,7 @@ rec { update-stage0 = let cTree = symlinkJoin { name = "cs"; paths = [ Init.cTree Lean.cTree ]; }; in writeShellScriptBin "update-stage0" '' - CSRCS=${cTree} CP_C_PARAMS="--dereference --no-preserve=all" ${src + "/script/update-stage0"} + CSRCS=${cTree} CP_C_PARAMS="--dereference --no-preserve=all" ${src + "/script/lib/update-stage0"} ''; update-stage0-commit = writeShellScriptBin "update-stage0-commit" '' set -euo pipefail diff --git a/script/lib/README.md b/script/lib/README.md new file mode 100644 index 0000000000..bad13a18ba --- /dev/null +++ b/script/lib/README.md @@ -0,0 +1,2 @@ +This directory contains various scripts that are *not* meant to be called +directly, but through other scripts or makefiles. diff --git a/script/lib/rebase-editor.sh b/script/lib/rebase-editor.sh new file mode 100755 index 0000000000..875e1d8af9 --- /dev/null +++ b/script/lib/rebase-editor.sh @@ -0,0 +1,19 @@ +#!/usr/bin/env bash + + +# Script internal to `./script/rebase-stage0.sh` + +# Determine OS type for sed in-place editing +SED_CMD=("sed" "-i") +if [[ "$OSTYPE" == "darwin"* ]] +then + # macOS requires an empty string argument with -i for in-place editing + SED_CMD=("sed" "-i" "") +fi + +if [ "$STAGE0_WITH_NIX" = true ] +then + "${SED_CMD[@]}" '/chore: update stage0/ s,.*,x nix run .#update-stage0-commit,' "$1" +else + "${SED_CMD[@]}" '/chore: update stage0/ s,.*,x make -j32 -C build/release update-stage0 \&\& git commit -m "chore: update stage0",' "$1" +fi diff --git a/script/update-stage0 b/script/lib/update-stage0 similarity index 100% rename from script/update-stage0 rename to script/lib/update-stage0 diff --git a/script/rebase-stage0.sh b/script/rebase-stage0.sh new file mode 100755 index 0000000000..899a39596c --- /dev/null +++ b/script/rebase-stage0.sh @@ -0,0 +1,24 @@ +#!/usr/bin/env bash + +# This script rebases onto the given branch/commit, and updates +# all `chore: update stage0` commits along the way. + +# Whether to use nix or make to update stage0 +if [ "$1" = "-nix" ] +then + export STAGE0_WITH_NIX=true + shift +fi + +# Check if an argument is provided +if [ "$#" -eq 0 ]; then + echo "Usage: $0 [-nix] " + exit 1 +fi + +REPO_ROOT=$(git rev-parse --show-toplevel) + +# Run git rebase in interactive mode, but automatically edit the todo list +# using the defined GIT_SEQUENCE_EDITOR command +GIT_SEQUENCE_EDITOR="$REPO_ROOT/script/lib/rebase-editor.sh" git rebase -i "$@" + diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 364a543aeb..875693298a 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -591,7 +591,7 @@ endif() if(PREV_STAGE) add_custom_target(update-stage0 - COMMAND bash -c 'CSRCS=${CMAKE_BINARY_DIR}/lib/temp script/update-stage0' + COMMAND bash -c 'CSRCS=${CMAKE_BINARY_DIR}/lib/temp script/lib/update-stage0' DEPENDS make_stdlib WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/..")