import Lake
open Lake DSL

package Putnam2025 where
  leanOptions := #[
    ⟨`pp.unicode.fun, true⟩,
    ⟨`autoImplicit, false⟩
  ]

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git" @ "v4.21.0"

require batteries from git
  "https://github.com/leanprover-community/batteries" @ "v4.21.0"

require aesop from git
  "https://github.com/leanprover-community/aesop" @ "v4.21.0"

require Qq from git
  "https://github.com/leanprover-community/quote4" @ "v4.21.0"

def problems : List String := ["A1", "A2", "A3", "A4", "A5", "A6", "B1", "B2", "B3", "B4", "B5", "B6"]

-- Problem files.
lean_lib A1_problem where roots := #[`Putnam2025.A1.problem]
lean_lib A2_problem where roots := #[`Putnam2025.A2.problem]
lean_lib A3_problem where roots := #[`Putnam2025.A3.problem]
lean_lib A4_problem where roots := #[`Putnam2025.A4.problem]
lean_lib A5_problem where roots := #[`Putnam2025.A5.problem]
lean_lib A6_problem where roots := #[`Putnam2025.A6.problem]
lean_lib B1_problem where roots := #[`Putnam2025.B1.problem]
lean_lib B2_problem where roots := #[`Putnam2025.B2.problem]
lean_lib B3_problem where roots := #[`Putnam2025.B3.problem]
lean_lib B4_problem where roots := #[`Putnam2025.B4.problem]
lean_lib B5_problem where roots := #[`Putnam2025.B5.problem]
lean_lib B6_problem where roots := #[`Putnam2025.B6.problem]

-- Solution files.
lean_lib A1 where roots := #[`Putnam2025.A1.solution]
lean_lib A2 where roots := #[`Putnam2025.A2.solution]
lean_lib A3 where roots := #[`Putnam2025.A3.solution]
lean_lib A4 where roots := #[`Putnam2025.A4.solution]
lean_lib A5 where roots := #[`Putnam2025.A5.solution]
lean_lib A6 where roots := #[`Putnam2025.A6.solution]
lean_lib B1 where roots := #[`Putnam2025.B1.solution]
lean_lib B2 where roots := #[`Putnam2025.B2.solution]
lean_lib B3 where roots := #[`Putnam2025.B3.solution]
lean_lib B4 where roots := #[`Putnam2025.B4.solution]
lean_lib B5 where roots := #[`Putnam2025.B5.solution]
lean_lib B6 where roots := #[`Putnam2025.B6.solution]

/-- Verification using SafeVerify -/
script verify do
  let mut failed : List String := []
  let mut passed : List String := []
  let stdout ← IO.getStdout

  for prob in problems do
    stdout.putStr s!"Verifying Putnam 2025 {prob} solution ... "
    stdout.flush
    let problemOlean := s!".lake/build/lib/lean/Putnam2025/{prob}/problem.olean"
    let solutionOlean := s!".lake/build/lib/lean/Putnam2025/{prob}/solution.olean"

    let result ← IO.Process.output {
      cmd := "lake"
      args := #["env", "lean", "--run", "SafeVerify.lean", problemOlean, solutionOlean]
    }

    if result.exitCode == 0 then
      IO.println "✅"
      passed := passed ++ [prob]
    else
      IO.println "❌"
      IO.eprintln result.stderr
      failed := failed ++ [prob]

  IO.println ""
  IO.println s!"Passed: {passed.length}/12"
  if failed.isEmpty then
    return 0
  else
    IO.println s!"Failed: {failed}"
    return 1
