diff --git a/marzipan/README.md b/marzipan/README.md index 5354c6b..b6750f3 100644 --- a/marzipan/README.md +++ b/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. diff --git a/marzipan/TODO.md b/marzipan/TODO.md index 972917c..57d8813 100644 --- a/marzipan/TODO.md +++ b/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 diff --git a/marzipan/src/__init__.py b/marzipan/src/__init__.py index 13746b2..c317c4a 100644 --- a/marzipan/src/__init__.py +++ b/marzipan/src/__init__.py @@ -53,18 +53,21 @@ def awk_prep(cpp_prep, awk_prep): file.write("\nprocess main") -@click.command() -@click.argument("prefix") -@click.argument("mark") -@click.argument("color") -@click.argument("text") +#@click.command() +#@click.argument("prefix", required=True) +#@click.argument("mark", required=True) +#@click.argument("color", required=True) +#@click.argument("text", default='') def pretty_output_line(prefix, mark, color, text): - colored = f"[grey42]{prefix}[/grey42][{color}]{mark} {text}[/{color}]" - rich_print(colored) + prefix = f"[grey42]{prefix}[/grey42]" + 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) - 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] + result = pkgs.re.findall(r'@(lemma)(?=\s+\"([^\"]*)\")', content) + if result: + expected.extend(['true' if e[0] == 'lemma' else e[0] for e in result]) + descs.extend([e[1] for e in result]) # 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] + result = pkgs.re.findall(r'@(query|reachable)(?=\s+"[^\"]*")', content) + if result: + expected.extend(['true' if e == '@query' else 'false' for e in result]) + 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) diff --git a/marzipan/src/analyze.sh b/marzipan/src/analyze.sh index f94ead4..1825ef1 100755 --- a/marzipan/src/analyze.sh +++ b/marzipan/src/analyze.sh @@ -29,41 +29,7 @@ pretty_output_line() { } pretty_output() { - local file; file="$1"; shift - 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" + exc rosenpass-marzipan pretty-output "${@}" } metaverif() { @@ -89,10 +55,11 @@ metaverif() { }' \ | pretty_output "${cpp_prep}" } || { - if ! grep -q "^Verification summary" "${log}"; then - echo -ne "\033[0\r" - cat "${log}" - fi + echo "TODO: Commented out some debug output" + #if ! grep -q "^Verification summary" "${log}"; then + # echo -ne "\033[0\r" + # 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