update-stage0

Stream: lean4 dev

[Tobias Grosser]

Hi, I am currently trying to run make update-stage0 but it seems I do not yet get the flow right. In particular, I can run:

mkdir -p build/release
cd build/release
cmake ../../
make update-stage0

This all compiles and goes through, but my stage0 directory in the git checkout is not updated. I guess I am missing some additional step, but could not find documentation which one this is. Do I need to mv/cp some directories from build/release/stage0 to stage0/?

[Mario Carneiro]

did you run make? AFAICT make update-stage0 should modify the stage0/ folder directly (assuming there are changes to apply), but normally I would run make before make update-stage0 so that's the only thing I can think of that might be causing a problem

[Mario Carneiro]

it does not commit those changes, so usually I do something more like

make update-stage0
git add ../../stage0/
git ci -m "chore: update stage0"

from the build/release folder