skill-lean-version

Other Community

Repo stars 435
Author repo nvim

Interpretation is structured for decision-making; original keeps the upstream SKILL.md unchanged.

Decide Fit First

Core job: Manage Lean toolchain and Mathlib versions with backup, upgrade, and rollback support Direct execution skill for managing Lean t…
Best fit: Use it when the task has reusable inputs, steps, and validation criteria rather than a one-off answer.
Avoid forcing it: If the source lacks commands, platform support, or external-service evidence, keep those fields unknown instead of guessing.

Design Intent

Structure: The skill is organized around “Execution”, “Step 1: Parse Arguments”, “Step 2: Read Current State”, “Step 3: Route by Mode”, showing how the author expects the agent to judge fit, collect context, and produce verifiable output.
Trigger evidence: Prioritize the author’s wording around when to use it, what context to collect, and what output shape to produce.
Evidence boundary: Author text states facts, repository files prove commands and paths, and Fluxly only adds fit, limits, and usage judgment.

How To Use It

Inputs: Provide target material, scope, expected result, forbidden changes, and validation method.
Invocation: Name skill-lean-version directly; if the source includes slash commands, start with the command and then add task context.
Validation: Start small and check whether the result follows “Execution / Step 1: Parse Arguments / Step 2: Read Current State” before expanding.

Boundaries And Review

Dependencies: It usually needs no extra API key, so start with a small validation task.
Permissions: Declared permissions include read / write / shell-exec; ask the agent to state file, command, and rollback boundaries before acting.
Quality bar: A useful result names the deliverable, evidence, and next action. Generic prose means the task needs tighter context.

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

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

# 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

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

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

Post-Upgrade

lake update
lake exe cache get

Rollback Mode

List Backups

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

Restore

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

Fluxly profile Author and license come from source; runtime, permissions, and network are Fluxly detections or estimates

Fluxly category: Other
Author-declared agents: No explicit declaration found; this is not inferred or tested compatibility
Static check: 88 / 100 · heuristic scan, not runtime safety proof
Author / version / license: @benbrastmckie · no license declared
Fluxly token estimate: Lean
Fluxly setup estimate: Guided setup
External API key: No requirement detected
Detected OS requirements: Unspecified
Runtime requirements: Unspecified
Detected file/system behavior: Read-only
Write / modify
Shell exec
Detected network behavior: Local-only
Install commands: None (reference only)

Profile is derived at build time from SKILL.md and install vectors. Subject to drift from author intent.

Heads up: 未限定 allowed-tools，默认拥有全部工具权限。

Output preview skill-lean-version.preview

The current SKILL.md does not define a fixed output example.

SKILL.md SKILL.md

# 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)

…

Evidence boundary and execution chain

Author text anchors workflow facts; Fluxly only indexes current sections, terms, files, and commands.

sections -> Execution → Step 1: Parse Arguments → Step 2: Read Current State → Step 3: Route by Mode → Check Mode → Upgrade Mode
terms    -> check · upgrade · rollback · Direct execution skill for managing Lean toolchain and Mathlib versions. · This skill executes inline without spawning a subagent.
files/cmd -> check · upgrade · rollback · --dry-run · --version VERSION · lean-toolchain · lakefile.lean · lake-manifest.json
body sha256 -> 52d4af513449