Repro script for ProofWidgets not up-to-date bug (leanprover/lean4#13127)

repro.sh

#!/usr/bin/env bash
set -uo pipefail

PASS=0
FAIL=0

run_expect_success() {
  echo "  \$ $*"
  output=$("$@" 2>&1)
  if [ $? -eq 0 ]; then
    echo "  --> ok"
    ((PASS++))
  else
    echo "  --> UNEXPECTED FAILURE"
    echo "$output" | tail -5 | sed 's/^/  | /'
    ((FAIL++))
  fi
}

run_expect_failure() {
  local pattern="$1"; shift
  echo "  \$ $*"
  output=$("$@" 2>&1)
  if [ $? -ne 0 ] && echo "$output" | grep -q "$pattern"; then
    echo "  --> ok (failed as expected: $(echo "$output" | grep "$pattern" | head -1 | sed 's/^[[:space:]]*//'))"
    ((PASS++))
  elif [ $? -eq 0 ]; then
    echo "  --> UNEXPECTED SUCCESS"
    ((FAIL++))
  else
    echo "  --> FAILED but wrong error"
    echo "$output" | tail -5 | sed 's/^/  | /'
    ((FAIL++))
  fi
}

echo "Reproducing ProofWidgets not up-to-date bug"
echo "============================================"

echo
echo "Step 0: Clone mathlib4 into /tmp"
echo "  \$ rm -rf /tmp/mathlib4-pw-repro"
rm -rf /tmp/mathlib4-pw-repro
run_expect_success git clone https://github.com/leanprover-community/mathlib4.git /tmp/mathlib4-pw-repro
cd /tmp/mathlib4-pw-repro

echo
echo "Step 1: Cache get and build at old commit (PW v0.0.92, rc6)"
run_expect_success git checkout 5215e9b0d498e4ce8d6787d82fe52e8f0df31dc5
run_expect_success lake exe cache get
run_expect_success lake build Mathlib.Tactic.Common

echo
echo "Step 2: Switch to new commit (PW v0.0.93, rc7), cache get, build -- fails"
run_expect_success git checkout 276bbda7c2ab277ae1582c27f8aa8bfa3fed4c9c
run_expect_success lake exe cache get
run_expect_failure "ProofWidgets not up-to-date" lake build Mathlib.Tactic.Common

echo
echo "Step 3: lake clean + cache get does not fix it"
run_expect_success lake clean
run_expect_success lake exe cache get
run_expect_failure "ProofWidgets not up-to-date" lake build Mathlib.Tactic.Common

echo
echo "Step 4: lake exe cache get! does not fix it"
run_expect_success lake exe cache get!
run_expect_failure "ProofWidgets not up-to-date" lake build Mathlib.Tactic.Common

echo
echo "Step 5: rm -rf .lake + cache get fixes it"
echo "  \$ rm -rf .lake"
rm -rf .lake
run_expect_success lake exe cache get
run_expect_success lake build Mathlib.Tactic.Common

echo
echo "============================================"
echo "Results: $PASS passed, $FAIL failed"
if [ $FAIL -ne 0 ]; then
  echo "REPRO FAILED"
  exit 1
else
  echo "Bug reproduced successfully."
fi