Skip to content

Version bump guide

Jump to bottom
Thomas Zhu edited this page Oct 29, 2025 · 10 revisions

LeanHammer version bump guide

This guide provides instructions for updating LeanHammer to a new Lean version.

Bumping Lean version of LeanHammer

We want to have a tag of LeanHammer for each release (candidate) of Lean. To do this, you need to bump all dependencies of LeanHammer.

LeanHammer has these components / dependencies that we manage:

  • premise-selection
  • Lean-auto @ hammer branch
  • Duper @ hammer branch
  • HammerCore (the HammerCore subdirectory of LeanHammer)
  • Hammer (the root directory of LeanHammer)
  • (To be added)

and these external dependencies:

  • Batteries
  • Qq
  • Aesop

We need to manually bump the Lean versions of the former set, and set the tags for the Lean versions in the latter set in lakefile files.

Example: Say we are updating to Lean v4.21.0. The steps are:

  • In premise-selection
    • Change all dependencies in lakefile.lean to use the v4.21.0 tag. premise-selection currently has no dependencies, so nothing has to be done.
    • Change lean-toolchain to leanprover/lean4:v4.21.0.
    • Run lake update and then lake build.
    • Fix any errors. (Usually there will be no errors).
    • Run lake test. It should run the PremiseSelectionTest.lean without errors.
    • Push the results to a branch/fork, and open and merge a bump PR.
    • Create a tag v4.21.0.
  • In the hammer branch of lean-auto
    • Change all dependencies in lakefile.lean to use the v4.21.0 tag. Lean-auto currently has no dependencies, so nothing has to be done.
    • Change lean-toolchain to leanprover/lean4:v4.21.0.
    • Run lake update and then lake build.
    • Fix any errors. (This is the most time-consuming step)
    • Push the results to a branch/fork, and open and merge a bump PR.
  • In the hammer branch of duper
    • Change all dependencies in lakefile.lean to use the v4.21.0 tag. Currently, this is changing the tag for Batteries to v4.21.0.
    • Change lean-toolchain to leanprover/lean4:v4.21.0.
    • Run lake update and then lake build.
    • Fix any errors. (This is the most time-consuming step)
    • Push the results to a branch/fork, and open and merge a bump PR.
  • In the HammerCore subdirectory of LeanHammer
    • Change all dependencies in lakefile.lean to use the v4.21.0 tag. Currently, this is changing the tag for Aesop to v4.21.0.
    • Change lean-toolchain to leanprover/lean4:v4.21.0.
    • Run lake update and then lake build.
    • Fix any errors. (This is the most time-consuming step)
  • In the root directory of LeanHammer
    • Change all dependencies in lakefile.lean to use the v4.21.0 tag. Currently, this is changing the tags for premise-selection and Qq to v4.21.0.
    • Change lean-toolchain to leanprover/lean4:v4.21.0.
    • Run lake update and then lake build.
    • Fix any errors.
    • Push the results to a branch/fork, and open and merge a bump PR.
    • Create a tag v4.21.0.

Updating data and model in leanpremise.net

Preliminary

You need access to a machine with 4 GPUs. The following paths assume access to the Babel HPC at CMU LTI; otherwise change the paths / SLURM configs accordingly.

There are two global paths that are used throughout the following guides:

  • data directory:
    • Holds extracted mathlib & upstream premises from ntp-toolkit
    • Default: /data/user_data/thomaszh/mathlib on Babel
  • model path:
    • Holds the trained model
    • Default: /data/user_data/thomaszh/models/all-distilroberta-v1-lr2e-4-bs256-nneg3-ml-ne2 on Babel, where the final string depends on some hyperparameters

Data extraction (daily/weekly)

  • Go to the hammer branch of https://github.com/cmu-l3/ntp-toolkit
  • Edit both configs/config_mathlib.json and configs/config_mathlib_full.json, and edit both commit and lean in either file to reflect the new version.
  • Run the command: 
    python scripts/extract_repos.py --config configs/config_mathlib_full.json --cwd "`pwd`"
    • This command does nothing except updating lakefile.lean, lake-manifest.json, and lean-toolchain in ntp-toolkit. It is expected to throw an error; it doesn’t matter.
  • Ensure that lake update && lake build works. If it doesn’t, fix the relevant errors (in TrainingData/ or scripts/) that result from the version bump.
  • Push the changes.
  • In a compute cluster (perhaps your own laptop is also fine), on a clone of ntp-toolkit, checkout the hammer branch, pull the changes.
    • (NB(Thomas): I have ntp-toolkit on babel at /home/thomaszh/ntp-toolkit-hammer. In there there is also a script check_integrity.py to check the extracted data; the TrainingDataWithPremises can tolerate some malformed data but the extracted Imports and Declarations need to be accurate.)
  • Run extract.sh to extract all Mathlib & upstream premises
    • The data directory is set to $OUTPUT_DIR in ntp-toolkit/extract.sh. You may change OUTPUT_DIR to extract to a different location.
    • For SLURM (e.g. on Babel), sbatch extract.sh takes a night to complete
    • There will be a revision file in data directory storing the Lean version, and this file is read by the following scripts.
  • Follow the guide below to upload everything to Hugging Face and leanpremise.net.
    • (In .env in lean-premise-server, you can update DATA_REVISION only without updating MODEL_REVISION, since the model is not updated.)

Model training (weekly/monthly)

  • Clone LeanHammer-training
  • Do the steps of data extraction.
  • Train the model by running train-4gpu.sh.
    • If the data directory is changed during extraction, set DATA_DIR in train-4gpu.sh to point to the data directory.
    • The model path is set to $OUTPUT_DIR/<model_name>/final in train-4gpu.sh, where <model_name> is a string like all-distilroberta-v1-lr2e-4-bs256-nneg3-ml-ne2 that depends on hyperparameters. You may change OUTPUT_DIR to a different location.
    • For example, on babel, sbatch train-4gpu.sh takes about 37 hours, using 4 GPUs and 2 epochs. You may experiment with hyperparameters and using 8 GPUs, etc.
    • If training is interrupted, simply run train-4gpu.sh again which will automatically resume training from a periodic checkpoint.
    • Similar to data directory, there will be a revision file in model path storing the Lean version, and this file is read by the following scripts.
  • Follow the guide below to upload everything to Hugging Face and leanpremise.net.

Uploading model and data to Hugging Face and leanpremise.net server:

cd /opt/dlami/nvme/lean-premise-server  # or path to lean-premise-server
git pull
docker compose down
docker compose -f docker-compose.yaml -f docker-compose.gpu.yaml up
  • Watch the logs and make sure the model is running. Go to http://leanpremise.net/max-new-premises to see if you can access the server (it should say a number like 2048).
  • Go to the test file PremiseSelectionTest.lean in premise-selection to ensure the server is working. You can also do this by running lake test.
  • Bump premise-selection to the newest Lean version by updating its lean-toolchain and running lake build, ensuring everything compiles (fix any errors resulting from the bump). Tag the new commit (e.g. v4.21.0).
    • (This can be done asynchronously with data/model updates. In practice, this can be done per LeanHammer tag.)

Clone this wiki locally