Add step by step flush runner to the GUI

flake.nix

@@ -1,21 +1,29 @@
 {
   inputs = {
-    flakelight.url = "github:nix-community/flakelight";
+    nixpkgs.url = "github:nixos/nixpkgs/nixpkgs-unstable";
+    flakelight = {
+      url = "github:nix-community/flakelight";
+      inputs.nixpkgs.follows = "nixpkgs";
+    };
   };
-  outputs = { flakelight, ... }@inputs:
+  outputs =
+    { flakelight, ... }@inputs:
     flakelight ./. {
       inherit inputs;
-
-      systems = [ "x86_64-linux" "aarch64-linux" "x86_64-darwin" "aarch64-darwin" ];
-      devShell = pkgs: {
-        packages = pkgs: (with pkgs; [
-          poetry
-          dafny
-        ]) ++ (pkgs.lib.optionals pkgs.stdenv.isDarwin (with pkgs.darwin.apple_sdk.frameworks; [
-          AppKit
-          pkgs.libiconv
-        ]));
-      };
-      formatter = pkgs: pkgs.nixpkgs-fmt;
+      systems = [
+        "x86_64-linux"
+        "aarch64-linux"
+        "x86_64-darwin"
+        "aarch64-darwin"
+      ];
+      devShell.packages = pkgs: [
+        pkgs.poetry
+        (pkgs.dafny.override {
+          z3 = pkgs.z3.override {
+            stdenv = pkgs.llvmPackages_16.stdenv;
+          };
+        })
+      ];
+      formatter = pkgs: pkgs.nixfmt-rfc-style;
     };
 }

gui/src/main.rs

@@ -31,7 +31,7 @@ fn should_restore() -> bool {
 fn main() -> eframe::Result {
     env_logger::init();
     let options = eframe::NativeOptions {
-        viewport: egui::ViewportBuilder::default().with_inner_size([800.0, 720.0]),
+        viewport: egui::ViewportBuilder::default().with_inner_size([1000.0, 720.0]),
         ..Default::default()
     };
 
@@ -83,6 +83,7 @@ enum BenchMode {
     Generate,
     Validating,
     StepByStep,
+    StepByStepFlush,
 }
 
 impl BenchMode {
@@ -91,7 +92,8 @@ impl BenchMode {
             BenchMode::Invariants
             | BenchMode::Generic
             | BenchMode::Validating
-            | BenchMode::StepByStep => basename(path).to_string(),
+            | BenchMode::StepByStep
+            | BenchMode::StepByStepFlush => basename(path).to_string(),
             BenchMode::Generate => {
                 let base = basename(path);
                 base.chars()
@@ -110,6 +112,7 @@ impl BenchMode {
             BenchMode::Generate => "Generate",
             BenchMode::Validating => "Validating",
             BenchMode::StepByStep => "Step by step",
+            BenchMode::StepByStepFlush => "Step by step (flush repeated errors)",
         }
     }
 
@@ -120,6 +123,7 @@ impl BenchMode {
             BenchMode::Generate,
             BenchMode::Validating,
             BenchMode::StepByStep,
+            BenchMode::StepByStepFlush,
         ];
         MODES
     }
@@ -133,6 +137,7 @@ impl Display for BenchMode {
             BenchMode::Generate => write!(f, "generate"),
             BenchMode::Validating => write!(f, "validating"),
             BenchMode::StepByStep => write!(f, "step-by-step"),
+            BenchMode::StepByStepFlush => write!(f, "step-by-step-flush"),
         }
     }
 }