Add support for multilang validating runners, use stateful runners (#5)

Co-authored-by: WeetHet <[email protected]>
Co-authored-by: Igor Engel <[email protected]>

.github/workflows/test-pytest.yml → .github/workflows/test-pytest-ruff.yml

@@ -1,4 +1,4 @@
-name: Run pytest
+name: Run pytest, ruff, and pyright
 
 on: [push]
 
@@ -8,7 +8,7 @@ env:
   POETRY_URL: https://install.python-poetry.org
 
 jobs:
-  run-pytest:
+  run-tests:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout
@@ -34,5 +34,11 @@ jobs:
           echo "$HOME/.local/bin" >> $GITHUB_PATH
       - name: Install Dependencies
         run: poetry install
+      - name: Run ruff format check
+        run: poetry run ruff format verified_cogen --check
+      - name: Run ruff linter
+        run: poetry run ruff check verified_cogen
+      - name: Run pyright
+        run: poetry run pyright verified_cogen
       - name: Run pytest
         run: poetry run pytest

.gitignore

@@ -6,6 +6,7 @@ llm-generated
 **/.DS_Store
 pyrightconfig.json
 benches/DafnyBench/
+benches/HumanEval-Dafny-Mini/
 break_assert.rs
 .venv
 **/target
@@ -17,3 +18,5 @@ run.sh
 **/.pytest_cache
 run_nagini.py
 /tmp
+results
+results/*

.gitmodules

@@ -1,3 +1,7 @@
 [submodule "Nagini-Conversion"]
 	path = Nagini-Conversion
 	url = https://github.com/alex28sh/Nagini-Convertion
+
+[submodule "benches/HumanEval-Dafny"]
+	path = benches/HumanEval-Dafny
+	url = https://github.com/JetBrains-Research/HumanEval-Dafny

gui/Cargo.toml

@@ -8,6 +8,7 @@ anyhow = "1.0.86"
 directories = "5.0.1"
 eframe = { version = "0.28.1", features = ["persistence"] }
 egui_extras = { version = "0.28.1", features = ["syntect"] }
+egui_plot = "0.28.1"
 env_logger = "0.11.3"
 log = "0.4.22"
 once_cell = "1.19.0"

gui/src/helpers.rs

@@ -3,7 +3,7 @@ use std::{
     process::{Command, Output},
 };
 
-use eframe::egui::{self, TextEdit};
+use eframe::egui::{self, TextEdit, Ui};
 
 use crate::Settings;
 
@@ -59,12 +59,20 @@ fn add_common_arguments<'a>(
     token: &str,
     settings: &Settings,
 ) -> &'a mut Command {
+    let bench_type = if settings.incremental_run {
+        String::from("validating")
+    } else {
+        settings.bench_type.to_string()
+    };
+    if settings.do_filter {
+        cmd.args(["--filter-by-ext", &settings.filter_by_ext]);
+    }
     cmd.args(["--verifier-command", &settings.verifier_command])
         .args(["--prompts-directory", &settings.prompts_directory])
         .args(["--insert-conditions-mode", "llm-single-step"])
         .args(["--llm-profile", settings.llm_profile.as_grazie()])
         .args(["--grazie-token", token])
-        .args(["--bench-type", &settings.bench_type.to_string()])
+        .args(["--bench-type", &bench_type])
         .args(["--tries", &make_tries(&settings.tries)])
         .args(["--retries", &make_retries(&settings.retries)])
         .args(["--verifier-timeout", &make_timeout(&settings.timeout)])
@@ -130,3 +138,9 @@ pub fn integer_edit_field(
     }
     res
 }
+
+pub(crate) fn paint_code(ui: &mut Ui, code: &str, lang: &str) {
+    let theme = egui_extras::syntax_highlighting::CodeTheme::from_memory(ui.ctx());
+
+    egui_extras::syntax_highlighting::code_view_ui(ui, &theme, code, lang);
+}