skill-lean-version

# Lean Version Management Skill (Direct Execution)

Direct execution skill for managing Lean toolchain and Mathlib versions. Provides check, upgrade, rollback, and dry-run modes. Creates backups before upgrades and supports interactive user confirmation.

This skill executes inline without spawning a subagent.

## Execution

### Step 1: Parse Arguments

Extract mode and flags:
- First non-flag argument: Mode (`check`, `upgrade`, `rollback`) - default: `check`
- `--dry-run`: Preview mode
- `--version VERSION`: Target version for upgrade

```bash
mode="check"
dry_run=false
target_version=""

for arg in "$@"; do
  case "$arg" in
    check|upgrade|rollback) mode="$arg" ;;
    --dry-run) dry_run=true ;;
    --version=*) target_version="${arg#*=}" ;;
  esac
done
```

---

### Step 2: Read Current State

```bash
# Read current toolchain
if [ -f "lean-toolchain" ]; then
  current_toolchain=$(cat lean-toolchain | tr -d '\n')
else
  current_toolchain="not found"
fi

# Read current Mathlib version from lakefile.lean
if [ -f "lakefile.lean" ]; then
  current_mathlib=$(grep -oP 'mathlib.*@\s*"\K[^"]+' lakefile.lean 2>/dev/null || echo "not found")
else
  current_mathlib="not found"
fi
```

---

### Step 3: Route by Mode

- **check** -> Display current version status
- **upgrade** -> Perform interactive upgrade with backup
- **rollback** -> Restore from a previous backup

---

## Check Mode

Display current version status:

```
Lean Version Status
===================

Current Configuration:
- Toolchain: {current_toolchain}
- Mathlib: {current_mathlib}

Installed Toolchains:
{elan_status}

Backups Available:
{backup_list}
```

---

## Upgrade Mode

### Create Backup

```bash
mkdir -p .lean-version-backup
timestamp=$(date +%Y%m%d_%H%M%S)
cp lean-toolchain ".lean-version-backup/lean-toolchain.$timestamp"
cp lakefile.lean ".lean-version-backup/lakefile.lean.$timestamp"
```

### Apply Changes

```bash
echo "$new_toolchain" > lean-toolchain
sed -i "s|@ \"v[0-9.]*\(-rc[0-9]*\)\?\"|@ \"$new_mathlib\"|g" lakefile.lean
```

### Post-Upgrade

```bash
lake update
lake exe cache get
```

---

## Rollback Mode

### List Backups

```bash
timestamps=$(ls .lean-version-backup/lean-toolchain.* 2>/dev/null | \
  sed 's|.*/lean-toolchain\.||' | sort -r | head -5)
```

### Restore

```bash
cp ".lean-version-backup/lean-toolchain.$selected_timestamp" lean-toolchain
cp ".lean-version-backup/lakefile.lean.$selected_timestamp" lakefile.lean
lake update
lake exe cache get
```

---

## Safety Measures

### Backup Before Changes
- Always create timestamped backup before upgrade
- Backup includes: `lean-toolchain`, `lakefile.lean`, `lake-manifest.json`
- Location: `.lean-version-backup/`
- Retention: Keep 3 most recent

### Dry-Run Support
- `--dry-run` previews all changes without applying

### User Confirmation
- Upgrade mode requires explicit confirmation via AskUserQuestion