changed prompt

prompts/humaneval-nagini-cot-instruct/steps/001/examples/001/answer.txt

@@ -0,0 +1 @@
+understood

prompts/humaneval-nagini-cot-instruct/steps/001/examples/001/question.txt

@@ -0,0 +1,37 @@
+You are an expert in Nagini, a verification framework in Python.
+You remember the following aspects of Nagini syntax:
+
+1. Nagini DOES NOT SUPPORT some Python features as list comprehensions (k + 1 for k in range(5)), as double inequalities (a <= b <= c).
+Instead of double inequalities it's customary to use two separate inequalities (a <= b and b <= c).
+
+2. In Nagini method preconditions (Requires) and postconditions (Ensures) placed right after method signature, like here:
+"
+def Sum(a : List[int], s : int, t : int) -> int :
+    Requires(Acc(list_pred(a)))
+    Requires(((0) <= (s)) and ((s) <= (t)) and ((t) <= (len(a))))
+    Ensures(Acc(list_pred(a)))
+    ...
+"
+
+3. Invariant are placed right after `while` statement and before the code of `while` body:
+"
+    while i < len(numbers):
+        Invariant(Acc(list_pred(numbers)))
+        Invariant(0 <= i and i <= len(numbers))
+        s = s + numbers[i]
+"
+Invariants CANNOT be placed in any other position.
+You remember that each invariant (and each expression) should contain equal number of opening and closing brackets, so that it is valid.
+You should sustain balanced parentheses.
+
+4. Nagini requires special annotations for working with lists `Acc(list_pred(..))`. You can use these constructs only inside `Invariant`,
+anywhere else you should not use `Acc()` or `list_pred()`:
+"
+    while i < len(numbers):
+        Invariant(Acc(list_pred(numbers)))
+"
+
+5. Nagini contains `Forall` and `Exists` constructs that can be used in invariants. First argument of Forall/Exists is typically a type (i.e `int`),
+second argument is a lambda. `Forall(type, lambda x : a)` denotes that assertion `a` is true for every element `x` of type `type`.
+
+Respond with 'understood' to this message. Remember this knowledge to solve the task that will be given further

prompts/humaneval-nagini-cot-instruct/steps/001/question.txt

@@ -34,4 +34,4 @@ anywhere else you should not use `Acc()` or `list_pred()`:
 5. Nagini contains `Forall` and `Exists` constructs that can be used in invariants. First argument of Forall/Exists is typically a type (i.e `int`),
 second argument is a lambda. `Forall(type, lambda x : a)` denotes that assertion `a` is true for every element `x` of type `type`.
 
-Don't respond to this code. Remember this knowledge to solve the task that will be given further
+Respond with 'understood' to this message. Remember this knowledge to solve the task that will be given further

verified_cogen/runners/languages/nagini.py

@@ -36,6 +36,8 @@ def __init__(self, remove_annotations: list[AnnotationType]):  # type: ignore
         )
 
     def separate_validator_errors(self, errors: str) -> tuple[str, str]:
-        raise NotImplementedError(
-            "Separating validator errors is not implemented for Verus yet"
-        )
+        lines = errors.split("\n")
+        lines = [
+            line for line in lines if "Verification successful" not in line and "Verification took" not in line
+        ]
+        return "\n".join(lines), ""