feat(WIP): pretty output in Python

Work on repairing the regexes in pretty_output

Co-Authored-By: Anja Rabich <a.rabich@uni-luebeck.de>

marzipan/README.md

@@ -5,4 +5,4 @@
 
 * call the old script from the Rosenpass repository's root directory with `./analyze.sh`
 * call the new script:
-  * `nix run .# -- analyze $repo` where `$repo` is the absolute(?) path to the root directory of the Rosenpass repository.
+  * `nix run .# -- analyze analyze $repo` where `$repo` is the absolute(?) path to the root directory of the Rosenpass repository.

marzipan/TODO.md

@@ -16,6 +16,8 @@
 * `pretty_output` Bash function
   * ~~pretty_output_line~~
   * awk RESULT flush in marzipan()
+  * click function intervention weirdness
+  * why is everything red in the pretty output? (see line 96 in __init__.py)
 * move the whole metaverif function to Python
 * move the whole analyze function to Python
   * find the files

marzipan/src/__init__.py

@@ -53,18 +53,21 @@ def awk_prep(cpp_prep, awk_prep):
         file.write("\nprocess main")
 
 
-@click.command()
+#@click.command()
-@click.argument("prefix")
+#@click.argument("prefix", required=True)
-@click.argument("mark")
+#@click.argument("mark", required=True)
-@click.argument("color")
+#@click.argument("color", required=True)
-@click.argument("text")
+#@click.argument("text", default='')
 def pretty_output_line(prefix, mark, color, text):
-    colored = f"[grey42]{prefix}[/grey42][{color}]{mark} {text}[/{color}]"
+    prefix = f"[grey42]{prefix}[/grey42]"
-    rich_print(colored)
+    content = f"[{color}]{mark} {text}[/{color}]"
+
+    output = prefix + content
+    rich_print(output)
 
 
 @click.command()
-@click.argument("file")
+@click.argument("file_path")
 def pretty_output(file_path):
     expected = []
     descs = []
@@ -72,29 +75,29 @@ def pretty_output(file_path):
     # Process lemmas first
     with open(file_path, 'r') as file:
         content = file.read()
-        expected += pkgs.re.findall(r'@(lemma)(?=\s+"[^\"]*")', content)
+        result = pkgs.re.findall(r'@(lemma)(?=\s+\"([^\"]*)\")', content)
-        expected = ['true' if e == '@lemma' else e for e in expected]
+        if result:
-        descs += pkgs.re.findall(r'@(lemma)\s+"([^\"]*)"', content)
+            expected.extend(['true' if e[0] == 'lemma' else e[0] for e in result])
-        descs = [d[1] for d in descs]
+            descs.extend([e[1] for e in result])
 
         # Then process regular queries
-        expected += pkgs.re.findall(r'@(query|reachable)(?=\s+"[^\"]*")', content)
+        result = pkgs.re.findall(r'@(query|reachable)(?=\s+"[^\"]*")', content)
-        expected = ['true' if e == '@query' else 'false' for e in expected]
+        if result:
-        descs += pkgs.re.findall(r'@(query|reachable)\s+"([^\"]*)"', content)
+            expected.extend(['true' if e == '@query' else 'false' for e in result])
-        descs = [d[1] for d in descs]
+            reachable_result = pkgs.re.findall(r'@(query|reachable)\s+"([^\"]*)"', content)
+            descs.extend([e[1] for e in reachable_result])
 
     res = 0
     ctr = 0
     ta = pkgs.time.time()
 
-    for outp in expected:
+    for outp in pkgs.sys.stdin:
         tz = pkgs.time.time()
         if outp == expected[ctr]:
             pretty_output_line(f"{int(tz - ta)}s ", "✔", "green", descs[ctr])
         else:
             res = 1
             pretty_output_line(f"{int(tz - ta)}s ", "✖", "red", descs[ctr])
-        print()
 
         ctr += 1
         ta = tz
@@ -151,6 +154,6 @@ main.add_command(clean)
 main.add_command(run_proverif)
 main.add_command(cpp)
 main.add_command(awk_prep)
-main.add_command(pretty_output_line)
+#main.add_command(pretty_output_line)
 main.add_command(pretty_output)
 main.add_command(clean_warnings)

marzipan/src/analyze.sh

@@ -29,41 +29,7 @@ pretty_output_line() {
 }
 
 pretty_output() {
-  local file; file="$1"; shift
+  exc rosenpass-marzipan pretty-output "${@}"
-  local expected=() descs=()
-
-  # Lemmas are processed first
-  readarray -t -O "${#expected[@]}" expected < <(
-    < "$file" grep -Po '@(lemma)(?=\s+"[^\"]*")' \
-      | sed 's/@lemma/true/')
-  readarray -t -O "${#descs[@]}" descs < <(
-    < "$file" grep -Po '@(lemma)\s+"[^\"]*"' \
-      | sed 's/@\w\+\s\+//; s/"//g')
-
-  # Then regular queries
-  readarray -t -O "${#expected[@]}" expected < <(
-    < "$file" grep -Po '@(query|reachable)(?=\s+"[^\"]*")' \
-      | sed 's/@query/true/; s/@reachable/false/')
-  readarray -t -O "${#descs[@]}" descs < <(
-    < "$file" grep -Po '@(query|reachable)\s+"[^\"]*"' \
-      | sed 's/@\w\+\s\+//; s/"//g')
-
-  local outp ctr res ta tz; ctr=0; res=0; ta="$(date +%s)"
-  while read -r outp; do
-    tz="$(date +%s)"
-    if [[ "${outp}" = "${expected[$ctr]}" ]]; then
-      pretty_output_line "$((tz - ta))s " "${checkmark}" "${color_green}" "${descs[$ctr]}"
-    else
-      res=1
-      pretty_output_line "$((tz - ta))s " "${cross}" "${color_red}" "${descs[$ctr]}"
-    fi
-    echo
-
-    (( ctr += 1 ))
-    ta="${tz}"
-  done
-
-  return "$res"
 }
 
 metaverif() {
@@ -89,10 +55,11 @@ metaverif() {
           }' \
       | pretty_output "${cpp_prep}"
   } || {
-    if ! grep -q "^Verification summary" "${log}"; then
+    echo "TODO: Commented out some debug output"
-      echo -ne "\033[0\r"
+    #if ! grep -q "^Verification summary" "${log}"; then
-      cat "${log}"
+    #  echo -ne "\033[0\r"
-    fi
+    #  cat "${log}"
+    #fi
   }
 }
 
@@ -134,7 +101,6 @@ main() {
 
   case "${cmd}" in
     analyze) analyze ;;
-    pretty) pretty_output_line PREFIX MARK green TEXT ;;
     clean_warnings) clean_warnings ;;
     *) err_usage
   esac