From ffc9a929d6a423119ca3ae5364bcf2bdc9aa904a Mon Sep 17 00:00:00 2001
From: Lorenzo Manacorda <lorenzo@mailbox.org>
Date: Fri, 21 Feb 2020 18:00:11 +0100
Subject: [PATCH 1/5] debug report

---
 libexec/klab-prove-all        | 2 +-
 libexec/klab-setup-ci-project | 1 +
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/libexec/klab-prove-all b/libexec/klab-prove-all
index 4558d0f8..4b13a9c5 100755
--- a/libexec/klab-prove-all
+++ b/libexec/klab-prove-all
@@ -1,5 +1,5 @@
 #!/usr/bin/env bash
-set -e
+set -ex
 
 red=$(tput setaf 1)
 green=$(tput setaf 2)
diff --git a/libexec/klab-setup-ci-project b/libexec/klab-setup-ci-project
index 460e7131..df8c70b2 100755
--- a/libexec/klab-setup-ci-project
+++ b/libexec/klab-setup-ci-project
@@ -1,4 +1,5 @@
 #!/usr/bin/env bash
+set +x
 
 while [[ $1 ]]; do
     case "$1" in

From 7983ea764d3988b74c8cc15feef6b1d353e043dc Mon Sep 17 00:00:00 2001
From: Lorenzo Manacorda <lorenzo@mailbox.org>
Date: Fri, 21 Feb 2020 18:25:33 +0100
Subject: [PATCH 2/5] klab-prove-all: fail on undefined variables

---
 libexec/klab-prove-all | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/libexec/klab-prove-all b/libexec/klab-prove-all
index 4b13a9c5..39e270f5 100755
--- a/libexec/klab-prove-all
+++ b/libexec/klab-prove-all
@@ -1,5 +1,5 @@
 #!/usr/bin/env bash
-set -ex
+set -eux
 
 red=$(tput setaf 1)
 green=$(tput setaf 2)

From 8d4c6953f47399c38b1095465efdd704e09f7d85 Mon Sep 17 00:00:00 2001
From: Lorenzo Manacorda <lorenzo@mailbox.org>
Date: Fri, 21 Feb 2020 18:31:28 +0100
Subject: [PATCH 3/5] klab-prove-all: always setup project

Stop branching on so many variables existing.
---
 libexec/klab-prove-all | 20 +++++++++-----------
 1 file changed, 9 insertions(+), 11 deletions(-)

diff --git a/libexec/klab-prove-all b/libexec/klab-prove-all
index 39e270f5..a19521a0 100755
--- a/libexec/klab-prove-all
+++ b/libexec/klab-prove-all
@@ -39,18 +39,16 @@ export PNAME
 if [ -d ".git" ]; then
   build_hash=$(klab get-build-id)
   export build_hash
-  if [ -n "$KLAB_REPORT_DIR" ]; then
-    export KLAB_REPORT_NAME_DIR=$KLAB_REPORT_DIR/$PNAME
-    export KLAB_REPORT_PROJECT_DIR=$KLAB_REPORT_DIR/$PNAME/$build_hash
-    if [ -n "$PNAME" ]; then
-      klab setup-ci-project --no-overwrite --report-dir "${KLAB_REPORT_DIR}" --project-name "${PNAME}"
-    fi;
-    if [ ! -f "$KLAB_REPORT_DIR/$PNAME"/report.json ]; then
-      echo "{}" > "$KLAB_REPORT_DIR/$PNAME"/report.json
-    fi;
-    jq -r '.src.rules[]'     < config.json | xargs -I {} cp {} "$KLAB_REPORT_PROJECT_DIR"
-    jq -r '.src.smt_prelude' < config.json | xargs -I {} cp {} "$KLAB_REPORT_PROJECT_DIR"
+  export KLAB_REPORT_NAME_DIR=$KLAB_REPORT_DIR/$PNAME
+  export KLAB_REPORT_PROJECT_DIR=$KLAB_REPORT_DIR/$PNAME/$build_hash
+  if [ -n "$PNAME" ]; then
+    klab setup-ci-project --no-overwrite --report-dir "${KLAB_REPORT_DIR}" --project-name "${PNAME}"
   fi;
+  if [ ! -f "$KLAB_REPORT_DIR/$PNAME"/report.json ]; then
+    echo "{}" > "$KLAB_REPORT_DIR/$PNAME"/report.json
+  fi;
+  jq -r '.src.rules[]'     < config.json | xargs -I {} cp {} "$KLAB_REPORT_PROJECT_DIR"
+  jq -r '.src.smt_prelude' < config.json | xargs -I {} cp {} "$KLAB_REPORT_PROJECT_DIR"
 fi;
 
 report () {

From 39bed9a78e65216bd8078e0687dc5888a6e3b133 Mon Sep 17 00:00:00 2001
From: Lorenzo Manacorda <lorenzo@mailbox.org>
Date: Fri, 21 Feb 2020 18:56:03 +0100
Subject: [PATCH 4/5] klab-prove-all: more removals of conditionals

Let's simplify the execution flow.
---
 libexec/klab-prove-all | 46 +++++++++++++++++-------------------------
 1 file changed, 18 insertions(+), 28 deletions(-)

diff --git a/libexec/klab-prove-all b/libexec/klab-prove-all
index a19521a0..87246649 100755
--- a/libexec/klab-prove-all
+++ b/libexec/klab-prove-all
@@ -33,7 +33,10 @@ export OBLIGATIONS=$KLAB_OUT/obligations.batch
 export BATCH_LIMIT=8
 export THREADS=${THREADS:-2}
 PNAME=$(jq -r '.name' < config.json)
-if [ "$PNAME" == "null" ]; then PNAME=""; fi
+if [ "$PNAME" == "null" ]; then
+   echo "Please set a name in config.json"
+   exit 1
+fi
 export PNAME
 
 if [ -d ".git" ]; then
@@ -41,10 +44,9 @@ if [ -d ".git" ]; then
   export build_hash
   export KLAB_REPORT_NAME_DIR=$KLAB_REPORT_DIR/$PNAME
   export KLAB_REPORT_PROJECT_DIR=$KLAB_REPORT_DIR/$PNAME/$build_hash
-  if [ -n "$PNAME" ]; then
-    klab setup-ci-project --no-overwrite --report-dir "${KLAB_REPORT_DIR}" --project-name "${PNAME}"
-  fi;
+  klab setup-ci-project --no-overwrite --report-dir "${KLAB_REPORT_DIR}" --project-name "${PNAME}"
   if [ ! -f "$KLAB_REPORT_DIR/$PNAME"/report.json ]; then
+    echo "Initializing empty report.json"
     echo "{}" > "$KLAB_REPORT_DIR/$PNAME"/report.json
   fi;
   jq -r '.src.rules[]'     < config.json | xargs -I {} cp {} "$KLAB_REPORT_PROJECT_DIR"
@@ -53,22 +55,14 @@ fi;
 
 report () {
   set -e
-  if [ ! -z "$KLAB_REPORT_NAME_DIR" ]; then
-    exec 3>"$KLAB_REPORT_NAME_DIR"/report.json.lock
-    flock -x 3 || exit 0
-  fi;
+  exec 3>"$KLAB_REPORT_NAME_DIR"/report.json.lock
+  flock -x 3 || exit 0
   klab report
-  if [ -n "$KLAB_REPORT_PROJECT_DIR" ]; then
-    cp "$KLAB_OUT/report/index.html" "$KLAB_REPORT_PROJECT_DIR"
-    concat=$(jq -s '.[0] * .[1]' "$KLAB_REPORT_DIR/$PNAME/report.json" "$KLAB_OUT/report/report.json")
-    echo "$concat" > "$KLAB_REPORT_DIR/$PNAME/report.json"
-    echo "Report exported to $KLAB_REPORT_PROJECT_DIR"
-  else
-    echo "Report saved to ${KLAB_OUT}/report/index.html"
-  fi;
-  if [ ! -z "$KLAB_REPORT_NAME_DIR" ]; then
-    exec 3>&-
-  fi;
+  cp "$KLAB_OUT/report/index.html" "$KLAB_REPORT_PROJECT_DIR"
+  concat=$(jq -s '.[0] * .[1]' "$KLAB_REPORT_DIR/$PNAME/report.json" "$KLAB_OUT/report/report.json")
+  echo "$concat" > "$KLAB_REPORT_DIR/$PNAME/report.json"
+  echo "Report exported to $KLAB_REPORT_PROJECT_DIR"
+  exec 3>&-
 }
 export -f report
 
@@ -154,10 +148,8 @@ function clean_running_dir {
 trap clean_running_dir EXIT
 
 
-make_batch () {
-  if [ -n "$KLAB_REPORT_PROJECT_DIR" ]; then
-    cp -n "$KLAB_OUT"/specs/*.k "$KLAB_REPORT_NAME_DIR"
-  fi;
+make_batch() {
+  cp -n "$KLAB_OUT"/specs/*.k "$KLAB_REPORT_NAME_DIR"
   parallel -u -P "$THREADS" do_proof {} < "$OBLIGATIONS" & parallel_id=$!
   trap 'echo "Trapped SIGTERM in klab-prove-all" && kill -s INT $parallel_id && exit 1' TERM
   trap 'echo "Trapped SIGINT  in klab-prove-all" && kill -s INT $parallel_id && exit 1' INT
@@ -183,11 +175,9 @@ mkdir -p "$KLAB_OUT/timeout"
 rm -fdr "$KLAB_OUT/meta/name"
 rm -fdr "$KLAB_OUT/specs"
 klab build >/dev/null
-if [ ! -z "$KLAB_REPORT_NAME_DIR" ]; then
-  rm -f "$KLAB_REPORT_NAME_DIR/latest"
-  ln -s "$KLAB_REPORT_PROJECT_DIR" "$KLAB_REPORT_NAME_DIR/latest"
-fi
-if [ -n "$KLAB_REPORT_PROJECT_DIR" ] && [ -f "$KLAB_OUT/bin_runtime.k" ]; then
+rm -f "$KLAB_REPORT_NAME_DIR/latest"
+ln -s "$KLAB_REPORT_PROJECT_DIR" "$KLAB_REPORT_NAME_DIR/latest"
+if [ -f "$KLAB_OUT/bin_runtime.k" ]; then
   cp "$KLAB_OUT/bin_runtime.k" "$KLAB_REPORT_PROJECT_DIR"
 fi
 

From 46038665402d81f0b0917d46bc59f15bf27bd873 Mon Sep 17 00:00:00 2001
From: Lorenzo Manacorda <lorenzo@mailbox.org>
Date: Fri, 21 Feb 2020 18:58:02 +0100
Subject: [PATCH 5/5] klab-prove-all: no whitespace after fn name

For better greppability.
---
 libexec/klab-prove-all | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/libexec/klab-prove-all b/libexec/klab-prove-all
index 87246649..a983509f 100755
--- a/libexec/klab-prove-all
+++ b/libexec/klab-prove-all
@@ -53,7 +53,7 @@ if [ -d ".git" ]; then
   jq -r '.src.smt_prelude' < config.json | xargs -I {} cp {} "$KLAB_REPORT_PROJECT_DIR"
 fi;
 
-report () {
+report() {
   set -e
   exec 3>"$KLAB_REPORT_NAME_DIR"/report.json.lock
   flock -x 3 || exit 0
@@ -76,7 +76,7 @@ savelogs() {
 export -f savelogs
 
 # perform a single proof and exit
-do_proof () {
+do_proof() {
   set -e
 
   name=$1