lean: check the populated solutions in CI

.github/workflows/lean.yml

@@ -37,3 +37,18 @@ jobs:
       working-directory: lean4
       run: |
         lake exe cache pack
+
+    - name: Insert solutions
+      working-directory: lean4
+      run: |
+        python scripts/rewrite_solutions.py
+
+    - name: Build
+      working-directory: lean4
+      run: |
+        lake build putnam_with_solutions
+
+    - name: Save olean cache
+      working-directory: lean4
+      run: |
+        lake exe cache pack

lean4/lakefile.lean

@@ -8,3 +8,6 @@ require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v
 @[default_target]
 lean_lib «putnam» where
   globs := #[.submodules `src]
+
+lean_lib «putnam_with_solutions» where
+  globs := #[.submodules `solutions_replaced_new]

lean4/scripts/rewrite_solutions.py

@@ -1,10 +1,12 @@
 import os
-import argparse
+from pathlib import Path
+import re
 
-def rewrite_solutions(file):
+
+def rewrite_solutions(file, out_file):
     # first read the entire file, and proceed line by line
-    problem_name = file.split('.')[0]
-    with open("src/"+file, "r") as f:
+    problem_name = file.stem
+    with file.open("r", encoding='utf8') as f:
         lines = f.readlines()
         # find all lines which contain the string "abbrev", and then take the line after that
         # and replace the line with the line after that
@@ -16,14 +18,19 @@ def rewrite_solutions(file):
                 for j, word in enumerate(split_line):
                     if word == "abbrev":
                         solution_name = split_line[j + 1].strip()
-                print(lines[i+1].split('--'))
+                        break
+                else:
+                    raise ValueError(f"Could not parse solution name from: {line}")
+
                 solution = lines[i + 1].split('--')[1].strip()
                 # the type comes between the first and second colon in the ith line
                 # the solution comes after the second colon in the ith line
-                type = lines[i].split(':')[1].strip()
+                if m := re.fullmatch(r'.*?:\s*(.*)\s*:=\s*sorry\n', line):
+                    type = m.group(1)
+                else:
+                    raise ValueError(f"Could not parse type from: {line}")
                 solution_dictionary[solution_name] = {'solution' : solution.replace("\n", ""), 'type' : type}
-
-    with open(f"/lean4/solutions_replaced_new/{problem_name}_sol.lean", "w") as f:
+    with out_file.open("w", encoding='utf8') as f:
         for line in lines:
             for solution_name, solution in solution_dictionary.items():
                 if solution_name in line and 'abbrev' not in line:
@@ -35,8 +42,15 @@ def rewrite_solutions(file):
             f.write(line)
 
 if __name__ == '__main__':
-    # inputs a single year, and rewrites in the problem statement each instance of the solution
-    # with the solution itself
-    for file in os.listdir('/home/gtsoukal/Projects/PUTNAM/lean4/src'):
-        if file.endswith('.lean'):
-            rewrite_solutions(file)
+    root_dir = Path(__file__).parent.parent
+    out_dir = root_dir / 'solutions_replaced_new'
+    out_dir.mkdir(exist_ok=True)
+    errors = []
+    for file in (root_dir / 'src').glob('*.lean'):
+        out_file = out_dir / f'{file.stem}_sol.lean'
+        try:
+            rewrite_solutions(file, out_file)
+        except ValueError as e:
+            errors.append(e)
+    if errors:
+        raise ExceptionGroup("Could not process some files", errors)

lean4/src/putnam_2007_a3.lean

@@ -2,6 +2,7 @@ import Mathlib
 open BigOperators
 
 open Set
+open scoped Nat
 
 abbrev putnam_2007_a3_solution : ℕ → ℚ := sorry
 -- fun k ↦ (k)! * (k + 1)! / ((3 * k + 1) * (2 * k)!)

lean4/src/putnam_2012_b4.lean

@@ -3,7 +3,7 @@ open BigOperators
 
 open Matrix Function Real Topology Filter
 
-noncomputable abbrev putnam_2012_b4_solution : Prop := True
+noncomputable abbrev putnam_2012_b4_solution : Prop := sorry
 -- True
 theorem putnam_2012_b4
 (a : ℕ → ℝ)

lean4/src/putnam_2016_a2.lean

@@ -4,7 +4,7 @@ open BigOperators
 open Polynomial Filter Topology Real Set Nat
 
 noncomputable abbrev putnam_2016_a2_solution : ℝ := sorry
--- (3 + sqrt 5) / 2
+-- (3 + √ 5) / 2
 theorem putnam_2016_a2
 (p : ℕ → ℕ → Prop)
 (hp : p = fun n ↦ fun m ↦ Nat.choose m (n - 1) > Nat.choose (m - 1) n)