From 48f2f2cb5aae100a57bbdaf676100daa5015ac96 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 5 Oct 2024 15:38:35 -0700 Subject: [PATCH] feat: Add handling for errors in compilation --- experiments/dsp/main.py | 15 ++++++++++++++- experiments/dsp/solve/prompts.py | 2 +- 2 files changed, 15 insertions(+), 2 deletions(-) diff --git a/experiments/dsp/main.py b/experiments/dsp/main.py index 1dd5d26..14f8f70 100644 --- a/experiments/dsp/main.py +++ b/experiments/dsp/main.py @@ -183,7 +183,20 @@ def prove( # If this throws index out of bound errors it means the source doesn't contain walled off Lean sections. print(colored("Sketch:", "yellow"), fl_sketch) lean_code, = [extract_lean_code(sketch)[0] for sketch in fl_sketch] - state, = server.load_sorry(lean_code) + print(colored("Lean code:", "light_grey"), lean_code) + states = server.load_sorry(lean_code) + + if len(states) != 1: + print(colored("Model must output one compilation unit", "red")) + raise NotImplemented + + state = states[0] + + if isinstance(state, list) and len(state) > 0: + print(colored("Sketch failed:", "red"), "\n".join(state)) + # what should we do? + raise NotImplemented + agent = HammerAgent() result = agent.search(server, state) print(colored(f"Result: {result}", "blue")) diff --git a/experiments/dsp/solve/prompts.py b/experiments/dsp/solve/prompts.py index ac56037..c8a11c7 100644 --- a/experiments/dsp/solve/prompts.py +++ b/experiments/dsp/solve/prompts.py @@ -100,7 +100,7 @@ SYSTEM_PROMPT_SKETCH_V0 = 'You are an expert mathematician and an expert in the STOP_TOKENS_SKETCH_V0: list[str] = ['Informal:', '(*### Problem', '###Solution', 'Formal:'] prompt_sketch_template_lean4_v0 = ("Translate the informal solution into a sketch in the " f"formal Lean 4 proof. Add {TOKEN_PLACEHOLDER} in the formal sketch whenever possible. " -f"{TOKEN_PLACEHOLDER} will be used to call a automated theorem prover or tactic in Lean 4. " +f"{TOKEN_PLACEHOLDER} will be used to call a automated theorem prover or tactic in Lean 4. Do not use any lemmas." "Here are some examples:\n" ) def get_prompt_sketch_template_4_lean_v0(