From 4194fb17ffaedf90498af68b17dbd7509615a1f4 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 21 Aug 2024 16:40:19 +0000 Subject: [PATCH 1/2] lean: check the populated solutions in CI --- .github/workflows/lean.yml | 15 +++++++++++ lean4/lakefile.lean | 3 +++ lean4/scripts/rewrite_solutions.py | 40 ++++++++++++++++++++---------- lean4/src/putnam_2012_b4.lean | 2 +- 4 files changed, 46 insertions(+), 14 deletions(-) diff --git a/.github/workflows/lean.yml b/.github/workflows/lean.yml index fb4a7762..d9a0f0b6 100644 --- a/.github/workflows/lean.yml +++ b/.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 diff --git a/lean4/lakefile.lean b/lean4/lakefile.lean index abf5441a..e3241c25 100644 --- a/lean4/lakefile.lean +++ b/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] diff --git a/lean4/scripts/rewrite_solutions.py b/lean4/scripts/rewrite_solutions.py index 0ff71c01..59ac403e 100644 --- a/lean4/scripts/rewrite_solutions.py +++ b/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) \ No newline at end of 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) diff --git a/lean4/src/putnam_2012_b4.lean b/lean4/src/putnam_2012_b4.lean index 010c93a3..faf9b38d 100644 --- a/lean4/src/putnam_2012_b4.lean +++ b/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 : ℕ → ℝ) From 1c469e6880798db8a3d38ed032a900824660bd4a Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 21 Aug 2024 21:07:02 +0000 Subject: [PATCH 2/2] fix the problems --- lean4/src/putnam_2007_a3.lean | 1 + lean4/src/putnam_2016_a2.lean | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/lean4/src/putnam_2007_a3.lean b/lean4/src/putnam_2007_a3.lean index 2dd7fc02..0b8a3ec3 100644 --- a/lean4/src/putnam_2007_a3.lean +++ b/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)!) diff --git a/lean4/src/putnam_2016_a2.lean b/lean4/src/putnam_2016_a2.lean index bf058516..645aa804 100644 --- a/lean4/src/putnam_2016_a2.lean +++ b/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)