Update tactic_generator.py

lean-dojo · Aug 29, 2024 · b5c1e5b · b5c1e5b
1 parent 903fac4
commit b5c1e5b
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/prover/tactic_generator.py b/prover/tactic_generator.py
@@ -314,7 +314,6 @@ async def generate(
         theorem_pos: Pos,
         num_samples: int,
     ) -> List[Tuple[str, float]]:
-        # prompt = f"<|begin_of_text|><|start_header_id|>user<|end_header_id|>\n\n[GOAL]\n{state}\n[PROOFSTEP]\n<|eot_id|><|start_header_id|>assistant<|end_header_id|>\n\n"
         prompt = self.template % state
         response = await self.vllm_actor.generate.remote(prompt, num_samples)
         return [