From 8900d58b670ff05be2a53571011fb27eb028d535 Mon Sep 17 00:00:00 2001 From: Aum Patel Date: Mon, 16 Jun 2025 22:09:18 -0700 Subject: [PATCH 1/7] chore: add Taskfile with deps & test tasks --- Taskfile.yml | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 Taskfile.yml diff --git a/Taskfile.yml b/Taskfile.yml new file mode 100644 index 0000000..517070b --- /dev/null +++ b/Taskfile.yml @@ -0,0 +1,16 @@ +version: "3" + +tasks: + deps: + desc: "Install Python packages and Lean toolchain" + cmds: + - pip install --upgrade pip + - pip install -r requirements.txt + - curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | bash -s -- -y + - echo "source $HOME/.elan/env" >> ~/.bashrc + + test: + desc: "Run PyTest suite" + deps: [deps] + cmds: + - pytest -q tests/ From 28895d36490d1082c2be185f0409f9eba87a921c Mon Sep 17 00:00:00 2001 From: Aum Patel Date: Mon, 16 Jun 2025 22:29:44 -0700 Subject: [PATCH 2/7] test: add standalone loss-decrease sanity check --- tests/test_sanity_loss.py | 37 +++++++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) create mode 100644 tests/test_sanity_loss.py diff --git a/tests/test_sanity_loss.py b/tests/test_sanity_loss.py new file mode 100644 index 0000000..1d3cb6a --- /dev/null +++ b/tests/test_sanity_loss.py @@ -0,0 +1,37 @@ +# tests/test_sanity_loss.py +import torch +import torch.nn as nn + +def test_dummy_loss_decreases(): + """ + Sanity-check that a mini training step actually lowers loss. + Uses a 2-layer MLP on random data so it runs in <2 s on CPU. + """ + torch.manual_seed(0) + + model = nn.Sequential( + nn.Linear(4, 8), + nn.ReLU(), + nn.Linear(8, 1) + ) + + x = torch.randn(32, 4) + y = torch.randn(32, 1) + + criterion = nn.MSELoss() + optimizer = torch.optim.SGD(model.parameters(), lr=0.1) + + # loss before training + loss_start = criterion(model(x), y).item() + + # one quick training step + optimizer.zero_grad() + criterion(model(x), y).backward() + optimizer.step() + + # loss after training + loss_end = criterion(model(x), y).item() + + assert loss_end < loss_start, ( + f"loss did not decrease: start={loss_start:.4f}, end={loss_end:.4f}" + ) \ No newline at end of file From bede5801120b1dd41723eb75c0ba0f03b4a298e5 Mon Sep 17 00:00:00 2001 From: Aum Patel Date: Mon, 16 Jun 2025 22:35:05 -0700 Subject: [PATCH 3/7] test: add (stub) tactic-generation sanity check --- tests/test_sanity_tactic.py | 6 ++++++ tests/util_stub.py | 3 +++ 2 files changed, 9 insertions(+) create mode 100644 tests/test_sanity_tactic.py create mode 100644 tests/util_stub.py diff --git a/tests/test_sanity_tactic.py b/tests/test_sanity_tactic.py new file mode 100644 index 0000000..346df4f --- /dev/null +++ b/tests/test_sanity_tactic.py @@ -0,0 +1,6 @@ +from tests.util_stub import suggest_tactics + +def test_tactic_generator_nonempty(): + """Generator should emit at least one tactic string.""" + tactics = suggest_tactics("⊢ 1 = 1") + assert tactics and any(t.strip() for t in tactics), "generator returned nothing" diff --git a/tests/util_stub.py b/tests/util_stub.py new file mode 100644 index 0000000..586f666 --- /dev/null +++ b/tests/util_stub.py @@ -0,0 +1,3 @@ +def suggest_tactics(state, top_k=3): + """Return a dummy tactic list (acts like a stand-in for the real generator).""" + return ["rfl"] # works for the goal ⊢ 1 = 1 From cec43c207805f9b45e0e8c58f9213653d5d3758b Mon Sep 17 00:00:00 2001 From: Aum Patel Date: Mon, 16 Jun 2025 22:40:58 -0700 Subject: [PATCH 4/7] fix(test): source elan env so Lean is on PATH --- Taskfile.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/Taskfile.yml b/Taskfile.yml index 517070b..2017d3e 100644 --- a/Taskfile.yml +++ b/Taskfile.yml @@ -4,6 +4,7 @@ tasks: deps: desc: "Install Python packages and Lean toolchain" cmds: + - . "$HOME/.elan/env" - pip install --upgrade pip - pip install -r requirements.txt - curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | bash -s -- -y From 8e8edf86694591639d9135ea097387ea9285b4dc Mon Sep 17 00:00:00 2001 From: Aum Patel Date: Mon, 16 Jun 2025 22:42:41 -0700 Subject: [PATCH 5/7] fix(task): keep Lean on PATH during pytest run --- Taskfile.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Taskfile.yml b/Taskfile.yml index 2017d3e..f78c88e 100644 --- a/Taskfile.yml +++ b/Taskfile.yml @@ -4,7 +4,7 @@ tasks: deps: desc: "Install Python packages and Lean toolchain" cmds: - - . "$HOME/.elan/env" + - bash -c '. "$HOME/.elan/env" && export PYTHONPATH="$PWD" && pytest -q tests/' - pip install --upgrade pip - pip install -r requirements.txt - curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | bash -s -- -y From 635085d9baea7167a47fa5f0af1e984cafbec209 Mon Sep 17 00:00:00 2001 From: Aum Patel Date: Mon, 16 Jun 2025 22:53:24 -0700 Subject: [PATCH 6/7] fix(task): source elan env inside test task again --- Taskfile.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Taskfile.yml b/Taskfile.yml index f78c88e..d6808b6 100644 --- a/Taskfile.yml +++ b/Taskfile.yml @@ -14,4 +14,4 @@ tasks: desc: "Run PyTest suite" deps: [deps] cmds: - - pytest -q tests/ + - bash -c '. "$HOME/.elan/env" && export PYTHONPATH="$PWD" && pytest -q tests/' From 446418ac10ca89e98cafa9b01ee6cd0f027bf976 Mon Sep 17 00:00:00 2001 From: Aum Patel Date: Mon, 16 Jun 2025 22:56:57 -0700 Subject: [PATCH 7/7] chore(task): split deps and test properly --- Taskfile.yml | 1 - 1 file changed, 1 deletion(-) diff --git a/Taskfile.yml b/Taskfile.yml index d6808b6..1e81bfc 100644 --- a/Taskfile.yml +++ b/Taskfile.yml @@ -4,7 +4,6 @@ tasks: deps: desc: "Install Python packages and Lean toolchain" cmds: - - bash -c '. "$HOME/.elan/env" && export PYTHONPATH="$PWD" && pytest -q tests/' - pip install --upgrade pip - pip install -r requirements.txt - curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | bash -s -- -y