feat: adopt Taskfile workflow – developers and users can now run all operations via Taskfile pattern

Author: vishnya

.env.template

@@ -0,0 +1 @@
+GITHUB_ACCESS_TOKEN=XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

.gitignore

@@ -130,3 +130,6 @@ dmypy.json
 # Pyre type checker
 .pyre/
 /.lake
+
+# Large data, model checkpoints, and downloads generated by task downloads
+data/

README.md

@@ -5,117 +5,53 @@
 ## Documentation
 Generated docs by Devin are here: [https://deepwiki.com/lean-dojo/LeanAgent]. It includes a detailed explanation + diagrams.
 
-## Requirements
-
-- Supported platforms: Linux and macOS
-- Git >= 2.25
-- 3.9 <= Python < 3.12
-- wget
-- [elan](https://github.com/leanprover/elan)
-- Sufficient disk space for model checkpoints and data
-
 ## Setup
 
-### Step 1: Configure `run_leanagent.sh`
-1. Set the `RAID_DIR` variable to your desired directory path
-2. Install Conda if not already installed
-3. Update the Conda path in the `source` command to match your installation
-4. Create and activate a dedicated environment:
-```
-conda create -n "LeanAgent" python=3.10
-conda activate LeanAgent
-pip install -r requirements.txt
-```
-5. Create a [GitHub personal access token](https://docs.github.com/en/authentication/keeping-your-account-and-data-secure/managing-your-personal-access-tokens#personal-access-tokens-classic) and set the environment variable `GITHUB_ACCESS_TOKEN` in the script to it
-
-### Step 2: Update File Paths
-1. Modify the `RAID_DIR` variable in `replace_files.sh`
-2. Execute the script:
-```
-bash replace_files.sh
-```
-
-### Step 3: Modify `leanagent.py`
-1. Set the following global variables:
-    - `repo_dir`: Path to your repository
-    - `DATA_DIR`: Directory for storing data
-    - `CHECKPOINT_DIR`: Directory for model checkpoints
-    - `EVAL_RESULTS_FILE_PATH`: Path for evaluation results
-    - `DB_FILE_NAME`: Database filename
-    - `PROOF_LOG_FILE_NAME`: Proof logging filename
-    - `ENCOUNTERED_THEOREMS_FILE`: Path for tracking encountered theorems
-    - (Optional) `FISHER_DIR`: Directory for Fisher Information Matrices (FIMs)
-2. Adjust the options at the beginning of the `main()` function according to your requirements. The default options correspond to the LeanAgent configuration, and alternate options can be used to replicate ablation studies from the paper.
-3. Adjust the Lean toolchain paths in `generate_benchmark_lean4.py` if needed:
-```
-lean_dir2 = f"/.elan/toolchains/leanprover--lean4---{v}"
-lean_dir3 = f"~/.elan/toolchains/leanprover--lean4---{v}"
-```
-These should match your system's Lean installation paths.
-
-### Step 4: Install Models
-1. For ReProver's Tactic Generator:
-```
-pip install gdown
-gdown https://drive.google.com/uc?id=11DXxixg6S4-hUA-u-78geOxEB7J7rCoX
-```
-Move the downloaded file to `{RAID_DIR}/`
+## Quick Start with Taskfile
 
-2. For ReProver's Starting Retriever:
+### Prerequisites
+1. Install Homebrew (https://brew.sh) if you don't have it.
+2. Install Taskfile ( https://taskfile.dev/#/installation)
+3. Modify the `.env.template` secret file in the repository root to provide GitHub token and rename `.env.template` to `.env`.
 
+To see all the tasks available to run, run 
+```bash
+task
 ```
-gdown https://drive.google.com/uc?id=1aRd1jQPu_TX15Ib5htzn3wZqHYowl3ax
-```
-
-Move the downloaded file to:
+### Environment and Package Setup
 
-- `{RAID_DIR}/checkpoints/`
+Run the following command to install all necessary packages.
 
-- `{RAID_DIR}/{CHECKPOINT_DIR}/`
-
-3. For the latest LeanAgent checkpoint from the paper:
-```
-gdown https://drive.google.com/uc?id=1plkC7Y5n0OVCJ0Ad6pH8_mwbALKYY_FY
+```bash
+task setup
 ```
 
-Move the downloaded file to `{RAID_DIR}/checkpoints/`
+### Run LeanAgent
 
-### Step 5: Run LeanAgent
-1. After completing all configuration steps, execute:
-```
-bash run_leanagent.sh
+Runs the main LeanAgent script, which orchestrates an end-to-end loop that downloads compatible Lean repositories, searches for unsolved theorems, trains and updates neural components, and attempts automated proof discovery to commit back synthesized proofs.
+```bash
+task run
 ```
 
-If you want to use Elastic Weight Consolidation (EWC) for lifelong learning, as shown in our ablation studies, follow these additional steps:
+### Run EWC (Elastic Weight Consolidation) for Lifelong Learning
+Runs an alternating loop of one training epoch (`task run`) followed by Fisher-matrix computation (`task run_fisher`). This reproduces the Elastic Weight Consolidation (EWC) implementation reported in the LeanAgent paper \[[1](https://arxiv.org/abs/2410.06209)\].  
 
-### Step 6: Configure `compute_fisher.py`
+The authors found that EWC (i.e. using the Fisher Information Matrix) resulted in **sub-optimal lifelong-learning performance** compared with the default curriculum/progressive strategy. Therefore **you only need this step if you want to replicate those results**. For normal training, simply run `task run` each epoch and skip the Fisher stage.
 
-1. Create and set the `new_data_path`: Path to new training data
+```bash
+# one training → Fisher cycle
+task run_ewc
 
-2. Download the starting FIM for mathlib:
+# five train→Fisher cycles 
+task run_ewc -- 5
 ```
-gdown https://drive.google.com/uc?id=1Q8yHq7XTAaHXGCiCGmhwZhTfkhHhN1cP
-```
-Move the downloaded file to your `FISHER_DIR`.
-
-### Step 7: Configure `run_compute_fisher.sh`
-1. Set the `RAID_DIR` variable to your desired directory path
-2. Update the Conda path in the `source` command to match your installation
-3. Add your GitHub personal access token as the environment variable `GITHUB_ACCESS_TOKEN`
-
-To use EWC in the training process, alternate between running `run_leanagent.sh` and `run_compute_fisher.sh`:
-1. Run `bash run_leanagent.sh` for one epoch. Setting `use_fisher = True` in `leanagent.py` does this automatically.
-2. Run `bash run_compute_fisher.sh` to compute the FIM
-3. Run `bash run_leanagent.sh` again for the next epoch
-4. Repeat steps 2-3 as needed
 
-## Running Tests
+### Running Tests
 
-To run the unit test suite, first activate the conda environment and then use `pytest`:
+To run the unit test suite, use the `task` command after setup is complete:
 
 ```bash
-conda activate LeanAgent
-python -m pytest tests/
+task test
 ```
 
 ## Architecture Overview

Taskfile.yaml

@@ -0,0 +1,230 @@
+version: '3' # Taskfile build version
+
+vars:
+  # Variables
+  env_name: "LeanAgent"
+  python_version: "3.10"
+  raid_dir: "data/raid" # root folder that stores all LeanAgent artifacts (repos, datasets, checkpoints)
+  repo_dir: "{{.raid_dir}}/repos_new" # where GitHub Lean repositories are cloned to
+  tactic_generator_id: "11DXxixg6S4-hUA-u-78geOxEB7J7rCoX" # gdown file id for the pretrained tactic-generator ckpt
+  starting_retriever_id: "1aRd1jQPu_TX15Ib5htzn3wZqHYowl3ax" # gdown id for the baseline retriever checkpoint
+  leanagent_ckpt_id: "1plkC7Y5n0OVCJ0Ad6pH8_mwbALKYY_FY" # gdown id for a fully-trained LeanAgent model snapshot
+  fisher_start_id: "1Q8yHq7XTAaHXGCiCGmhwZhTfkhHhN1cP" # gdown id for initial Fisher matrix used in EWC ablation
+  cache_dir: "{{.raid_dir}}/.cache/lean_dojo" # disk cache used by LeanDojo tracing
+  ray_tmpdir: "{{.raid_dir}}/tmp" # scratch space for Ray object-store & spill files
+
+  # Paths
+  data_dir: "datasets" # subfolder (inside RAID_DIR) where processed Lean datasets live
+  checkpoint_dir: "checkpoints" # directory for model checkpoints saved during training
+  eval_results_file: "eval_results.json" # aggregated evaluation metrics written by LeanAgent
+  db_file: "leanagent_db.json" # JSON file backing the dynamic theorem database
+  proof_log_file: "proof_log.json" # chronological log of proof attempts / successes
+  encountered_theorems_file: "encountered_theorems.txt" # flat list of theorem names already processed
+  fisher_dir: "fisher" # folder where per-repository Fisher matrices are stored
+
+
+# Load project-local secrets (i.e. GitHub token)
+dotenv: ['.env']
+
+# Ensure Conda is discoverable for all tasks
+env:
+  PATH: "$HOME/miniconda/condabin:$HOME/miniconda/bin:$CONDA_HOME/bin:$PATH"
+
+tasks:
+  # ---------------------------------------------------------------------------
+  # Run pytest test-suite
+  # ---------------------------------------------------------------------------
+  test:
+    desc: "Run the pytest test suite."
+    cmds:
+      - "python -m pytest"
+
+  # ---------------------------------------------------------------------------
+  # Ensure GitHub token is available in .env
+  # ---------------------------------------------------------------------------
+  check_github_token:
+    desc: "Fail if .env is missing or lacks a non-empty GITHUB_ACCESS_TOKEN entry."
+    cmds:
+      - |
+        bash -c '
+        if [ ! -f ".env" ]; then
+          echo "ERROR: .env file missing — create it and add GITHUB_ACCESS_TOKEN=<token>" >&2
+          exit 1
+        fi
+        TOKEN=$(grep -E "^GITHUB_ACCESS_TOKEN=" .env | cut -d"=" -f2-)
+        if [ -z "$TOKEN" ]; then
+          echo "ERROR: GITHUB_ACCESS_TOKEN not set in .env" >&2
+          exit 1
+        fi
+        '
+  create_conda_env:
+    desc: "Create conda env {{.env_name}} if missing"
+    cmds:
+      - cmd: |
+          bash -c '
+          # Ensure conda executable is reachable
+          for d in "$HOME/miniconda/condabin" "$HOME/miniconda/bin" "$HOME/miniconda3/bin" "$HOME/anaconda3/bin" "$HOME/miniforge3/bin" "/opt/conda/bin"; do
+            if [ -d "$d" ] && [[ ":$PATH:" != *":$d:"* ]]; then
+              export PATH="$d:$PATH"
+            fi
+          done
+
+          # If conda still missing, install Miniconda silently
+          if ! command -v conda >/dev/null 2>&1; then
+            echo "Conda not found – installing Miniconda..." >&2
+            curl -sSLo "$HOME/miniconda.sh" https://repo.anaconda.com/miniconda/Miniconda3-latest-Linux-x86_64.sh
+            bash "$HOME/miniconda.sh" -b -p "$HOME/miniconda3"
+            export PATH="$HOME/miniconda3/bin:$PATH"
+            rm "$HOME/miniconda.sh"
+          fi
+
+          if ! command -v conda >/dev/null 2>&1; then
+            echo "Conda executable not found in PATH" >&2
+            exit 127
+          fi
+          if ! conda env list | grep -q "^{{.env_name}} "; then
+            conda create -n {{.env_name}} python={{.python_version}} -y
+          fi
+          '
+        
+  install_elan:
+    desc: "Ensure elan is installed"
+    cmds:
+      - cmd: |
+          bash -c '
+          if [ ! -f "$HOME/.elan/bin/elan" ]; then
+            echo "elan not found. Installing..."
+            curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
+          else
+            echo "elan is already installed."
+          fi
+          '
+        
+  install_requirements:
+    desc: "Install Python requirements"
+    
+    cmds:
+      - "conda run -n {{.env_name}} pip install -r requirements.txt"
+
+  download_checkpoint_data:
+    desc: "Download pretrained checkpoints via gdown"
+    cmds:
+      - cmd: |
+          bash -c '
+          conda run -n {{.env_name}} pip install --quiet gdown
+          conda run -n {{.env_name}} gdown https://drive.google.com/uc?id={{.tactic_generator_id}} -O /tmp/tactic_gen.ckpt
+          conda run -n {{.env_name}} gdown https://drive.google.com/uc?id={{.starting_retriever_id}} -O /tmp/start_retriever.ckpt
+          conda run -n {{.env_name}} gdown https://drive.google.com/uc?id={{.leanagent_ckpt_id}} -O /tmp/leanagent.ckpt
+
+          mkdir -p {{.raid_dir}}/{{.checkpoint_dir}}
+          mv /tmp/tactic_gen.ckpt {{.raid_dir}}/ # TODO: This is not used, investigate.
+          mv /tmp/start_retriever.ckpt {{.raid_dir}}/{{.checkpoint_dir}}/
+          mv /tmp/leanagent.ckpt {{.raid_dir}}/{{.checkpoint_dir}}/
+          '
+  replace_files:
+    desc: "Patch LeanAgent files with custom versions"
+    env:
+      RAID_DIR: "{{.raid_dir}}"
+    cmds:
+      - "bash replace_files.sh"
+        
+  # ---------------------------------------------------------------------------
+  # Composite setup task
+  # ---------------------------------------------------------------------------
+  setup:
+    desc: "Initial setup: conda env, elan, requirements, checkpoints, file patches"
+    deps:
+      - check_github_token
+      - install_elan
+      - create_conda_env
+      - install_requirements
+      - download_checkpoint_data
+      - replace_files
+    cmds: []
+
+  # ---------------------------------------------------------------------------
+  # Launch LeanAgent main training/proving process
+  # ---------------------------------------------------------------------------
+  run:
+    desc: "Launch LeanAgent main training/proving process."
+    deps:
+      - check_github_token
+    env:
+      PYTHONPATH: "$PYTHONPATH:{{.raid_dir}}/LeanAgent"
+      CACHE_DIR: "{{.cache_dir}}"
+      RAY_TMPDIR: "{{.ray_tmpdir}}"
+      RAID_DIR: "{{.raid_dir}}"
+      REPO_DIR: "{{.repo_dir}}"
+      DATA_DIR: "{{.data_dir}}"
+      CHECKPOINT_DIR: "{{.checkpoint_dir}}"
+      EVAL_RESULTS_FILE_PATH: "{{.eval_results_file}}"
+      DB_FILE_NAME: "{{.db_file}}"
+      PROOF_LOG_FILE_NAME: "{{.proof_log_file}}"
+      ENCOUNTERED_THEOREMS_FILE: "{{.encountered_theorems_file}}"
+      FISHER_DIR: "{{.fisher_dir}}"
+    cmds:
+      - |
+          bash -c '
+          source $(conda info --base)/etc/profile.d/conda.sh
+          conda activate {{.env_name}}
+          rm -rf $RAY_TMPDIR || true
+          mkdir -p "$RAY_TMPDIR"
+          ray stop --force || true
+          nvidia-smi || true
+          python leanagent.py
+          '
+
+  # ---------------------------------------------------------------------------
+  # Compute Fisher information matrix
+  # ---------------------------------------------------------------------------
+  run_fisher:
+    desc: "Elastic Weight Consolidation for lifelong learning."
+    env:
+      PYTHONPATH: "$PYTHONPATH:{{.raid_dir}}/LeanAgent"
+      NEW_DATA_PATH: "{{.raid_dir}}/datasets/new_data"
+      RAID_DIR: "{{.raid_dir}}"
+      CACHE_DIR: "{{.cache_dir}}"
+      RAY_TMPDIR: "{{.ray_tmpdir}}"
+    cmds:
+      - |
+        bash -c '
+        source $(conda info --base)/etc/profile.d/conda.sh
+        conda activate {{.env_name}}
+
+        # Ensure initial Fisher matrix is present
+        python -m pip install --quiet gdown
+        if [ ! -f "{{.raid_dir}}/fisher_start.pkl" ]; then
+          gdown https://drive.google.com/uc?id={{.fisher_start_id}} -O {{.raid_dir}}/fisher_start.pkl
+        fi
+
+        echo "Removing old Ray temp files" >&2
+        rm -rf /tmp/ray || true
+        rm -rf "$RAY_TMPDIR" || true
+        mkdir -p "$RAY_TMPDIR"
+        echo "Stopping Ray" >&2
+        ray stop --force || true
+
+        # Optional GPU status
+        nvidia-smi || true
+
+        echo "Running compute_fisher.py" >&2
+        python compute_fisher.py
+        ' 
+
+  # ---------------------------------------------------------------------------
+  # Lifelong learning: alternate training (run) and Fisher computation
+  # ---------------------------------------------------------------------------
+  run_ewc:
+    desc: "Alternate run and run_fisher tasks N times (default 1). Usage: task run_ewc -- 5"
+    cmds:
+      - |
+        bash -c '
+        COUNT={{default "1" (first .CLI_ARGS)}}
+        echo "Running EWC for $COUNT iteration(s)"
+        for i in $(seq 1 $COUNT); do
+          echo "--- Iteration $i: Training ---"
+          task run
+          echo "--- Iteration $i: Computing Fisher ---"
+          task run_fisher
+        done
+        ' 

compute_fisher.py

@@ -1,7 +1,8 @@
+import os
 from leanagent import *
 from retrieval.fisher_computation_module import FisherComputationModule
 
-new_data_path = "<NEW_DATA_PATH>/<NEW_DATASET_NAME>"
+new_data_path = os.environ.get("NEW_DATA_PATH", "datasets/new_data")
 
 def main():
     """