From 744cf6fb5047a4f7ac4e61a0dee2b0bc62426a8d Mon Sep 17 00:00:00 2001
From: Benjamin Lipp <blipp@mailbox.org>
Date: Tue, 3 Jun 2025 16:22:56 +0200
Subject: [PATCH] feat: pretty output line

---
 marzipan/README.md       |  3 +--
 marzipan/TODO.md         |  5 +++-
 marzipan/src/__init__.py | 54 ++++++++++++++++++++++++++++++++++++----
 marzipan/src/analyze.sh  | 15 +++++------
 4 files changed, 60 insertions(+), 17 deletions(-)

diff --git a/marzipan/README.md b/marzipan/README.md
index 8957f7e..5354c6b 100644
--- a/marzipan/README.md
+++ b/marzipan/README.md
@@ -5,5 +5,4 @@
 
 * call the old script from the Rosenpass repository's root directory with `./analyze.sh`
 * call the new script:
-  * in `analyze_py/marzipan`: `nix shell`
-  * `src/analyze.sh analyze $repo` where `$repo` is the absolute(?) path to the root directory of the Rosenpass repository.
+  * `nix run .# -- analyze $repo` where `$repo` is the absolute(?) path to the root directory of the Rosenpass repository.
diff --git a/marzipan/TODO.md b/marzipan/TODO.md
index 2c8573d..972917c 100644
--- a/marzipan/TODO.md
+++ b/marzipan/TODO.md
@@ -14,7 +14,7 @@
 ## Next Steps
 
 * `pretty_output` Bash function
-  * pretty_output_line
+  * ~~pretty_output_line~~
   * awk RESULT flush in marzipan()
 * move the whole metaverif function to Python
 * move the whole analyze function to Python
@@ -25,4 +25,7 @@
   * integrate this upstream, into the CI?
   * “make it beautiful” steps? more resiliency to working directory?
   * rewrite our awk usages into Python/…?
+    * yes, possibly as extension to the LARK grammar
+    * and rewrite the AST within Python
+    * reconstruct ProVerif input file for ProVerif
   * rewrite our CPP usages into Python/…?
diff --git a/marzipan/src/__init__.py b/marzipan/src/__init__.py
index 2b40f14..13746b2 100644
--- a/marzipan/src/__init__.py
+++ b/marzipan/src/__init__.py
@@ -1,7 +1,8 @@
 from .util import pkgs, setup_exports, export, rename
-from rich import print
+from rich import print as rich_print
 import click
 
+
 (__all__, export) = setup_exports()
 export(setup_exports)
 
@@ -58,16 +59,58 @@ def awk_prep(cpp_prep, awk_prep):
 @click.argument("color")
 @click.argument("text")
 def pretty_output_line(prefix, mark, color, text):
-    colored_prefix = f"[grey42]{prefix}[/grey42]"
-    colored_mark_text = f"[{color}]{mark} {text}[/{color}]"
-    print(colored_prefix, colored_mark_text)
+    colored = f"[grey42]{prefix}[/grey42][{color}]{mark} {text}[/{color}]"
+    rich_print(colored)
 
 
 @click.command()
+@click.argument("file")
+def pretty_output(file_path):
+    expected = []
+    descs = []
+
+    # Process lemmas first
+    with open(file_path, 'r') as file:
+        content = file.read()
+        expected += pkgs.re.findall(r'@(lemma)(?=\s+"[^\"]*")', content)
+        expected = ['true' if e == '@lemma' else e for e in expected]
+        descs += pkgs.re.findall(r'@(lemma)\s+"([^\"]*)"', content)
+        descs = [d[1] for d in descs]
+
+        # Then process regular queries
+        expected += pkgs.re.findall(r'@(query|reachable)(?=\s+"[^\"]*")', content)
+        expected = ['true' if e == '@query' else 'false' for e in expected]
+        descs += pkgs.re.findall(r'@(query|reachable)\s+"([^\"]*)"', content)
+        descs = [d[1] for d in descs]
+
+    res = 0
+    ctr = 0
+    ta = pkgs.time.time()
+
+    for outp in expected:
+        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
+
+    return res
+
+
+
+
+@click.command()
+@click.argument("command")
 @click.argument("path")
-def analyze(path):
+def analyze(command, path):
     exc([
         f"{pkgs.pathlib.Path(__file__).resolve().parent}/analyze.sh",
+        command,
         path
     ])
 
@@ -109,4 +152,5 @@ 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)
 main.add_command(clean_warnings)
diff --git a/marzipan/src/analyze.sh b/marzipan/src/analyze.sh
index 79614cd..f94ead4 100755
--- a/marzipan/src/analyze.sh
+++ b/marzipan/src/analyze.sh
@@ -16,20 +16,16 @@ clean_warnings() {
     exc rosenpass-marzipan clean-warnings
 }
 
-color_red='\033[0;31m'
-color_green='\033[0;32m'
-color_gray='\033[0;30m'
-color_clear='\033[0m'
+color_red='red'
+color_green='green'
+color_gray='gray'
+color_clear=''
 
 checkmark="✔"
 cross="❌"
 
 pretty_output_line() {
-  local prefix; prefix="$1"; shift
-  local mark; mark="$1"; shift
-  local color; color="$1"; shift
-  local text; text="$1"; shift
-  echo -ne "\033[0\r${color_gray}${prefix}${color}${mark} ${text}${color_clear}"
+  exc rosenpass-marzipan pretty-output-line "${@}"
 }
 
 pretty_output() {
@@ -138,6 +134,7 @@ main() {
 
   case "${cmd}" in
     analyze) analyze ;;
+    pretty) pretty_output_line PREFIX MARK green TEXT ;;
     clean_warnings) clean_warnings ;;
     *) err_usage
   esac