Skip to content

Commit

Permalink
resolved
Browse files Browse the repository at this point in the history
  • Loading branch information
alex28sh committed Sep 18, 2024
2 parents a1e8a2e + 1d2d8ad commit 28474b4
Show file tree
Hide file tree
Showing 17 changed files with 340 additions and 80 deletions.
6 changes: 4 additions & 2 deletions .github/workflows/test-pytest-ruff.yml
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
name: Run pytest and ruff
name: Run pytest, ruff, and pyright

on: [push]

Expand All @@ -8,7 +8,7 @@ env:
POETRY_URL: https://install.python-poetry.org

jobs:
run-pytest:
run-tests:
runs-on: ubuntu-latest
steps:
- name: Checkout
Expand Down Expand Up @@ -38,5 +38,7 @@ jobs:
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
1 change: 1 addition & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ llm-generated
**/.DS_Store
pyrightconfig.json
benches/DafnyBench/
benches/HumanEval-Dafny-Mini/
break_assert.rs
.venv
**/target
Expand Down
6 changes: 3 additions & 3 deletions gui/src/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -110,7 +110,7 @@ impl Display for BenchMode {
}
}

type IncrementalRunResults = HashMap<String, usize>;
type RunResults = HashMap<String, f64>;

#[derive(Default)]
struct AppState {
Expand All @@ -122,8 +122,8 @@ struct AppState {
running: Arc<AtomicBool>,
last_verified_code: Arc<RwLock<Option<String>>>,
last_verified_extension: Arc<RwLock<Option<String>>>,
incremental_run_results: Arc<RwLock<Option<IncrementalRunResults>>>,
incremental_file_count: Arc<AtomicUsize>,
run_results: Arc<RwLock<Option<RunResults>>>,
file_count: Arc<AtomicUsize>,
output: Arc<RwLock<Option<(String, String)>>>,
log: Arc<RwLock<Option<String>>>,
}
Expand Down
8 changes: 3 additions & 5 deletions gui/src/ui/output.rs
Original file line number Diff line number Diff line change
Expand Up @@ -15,12 +15,10 @@ impl AppState {
ui.add(Separator::default().vertical().grow(panel_height));

ui.vertical(|ui| {
if let Ok(incremental_run_results) = self.incremental_run_results.read() {
if let Ok(run_results) = self.run_results.read() {
part += 1.0;
if let Some(results) = incremental_run_results.as_ref() {
let cnt = self
.incremental_file_count
.load(std::sync::atomic::Ordering::SeqCst);
if let Some(results) = run_results.as_ref() {
let cnt = self.file_count.load(std::sync::atomic::Ordering::SeqCst);
ui.push_id("plot", |ui| {
ui.set_max_height(panel_height / part);
self.plot(results, cnt, ui);
Expand Down
10 changes: 5 additions & 5 deletions gui/src/ui/plot.rs
Original file line number Diff line number Diff line change
@@ -1,18 +1,18 @@
use eframe::egui::Ui;
use egui_plot::{uniform_grid_spacer, Line, Plot};

use crate::{AppState, IncrementalRunResults};
use crate::{AppState, RunResults};

impl AppState {
pub fn plot(&self, results: &IncrementalRunResults, file_cnt: usize, ui: &mut Ui) {
pub fn plot(&self, results: &RunResults, file_cnt: usize, ui: &mut Ui) {
let tries: Vec<_> = results.values().copied().collect();
let max_tries = *tries
.iter()
.max()
.max_by(|a, b| a.total_cmp(b))
.expect("results should contain at least one file");
let mut cnt = vec![0; max_tries + 1];
let mut cnt = vec![0; max_tries.ceil() as usize + 1];
for t in tries {
cnt[t] += 1;
cnt[t.ceil() as usize] += 1;
}
let percent = cnt
.into_iter()
Expand Down
52 changes: 29 additions & 23 deletions gui/src/ui/run.rs
Original file line number Diff line number Diff line change
Expand Up @@ -41,9 +41,9 @@ impl AppState {
let last_verified_code = Arc::clone(&self.last_verified_code);
let last_verified_ext = Arc::clone(&self.last_verified_extension);
let incremental_run = self.settings.incremental_run;
let incremental_file_count = Arc::clone(&self.incremental_file_count);
let file_count = Arc::clone(&self.file_count);
let cnt = self.files.as_ref().map(|f| f.len());
let incremental_run_results = Arc::clone(&self.incremental_run_results);
let run_results = Arc::clone(&self.run_results);

let settings = self.settings.clone();
let file_mode = self.settings.file_mode.clone();
Expand All @@ -57,7 +57,7 @@ impl AppState {
if let Ok(mut output) = output.write() {
*output = None;
}
if let Ok(mut results) = incremental_run_results.write() {
if let Ok(mut results) = run_results.write() {
*results = None;
}
let log_dir = APP_DIRS.cache_dir().join("log");
Expand Down Expand Up @@ -100,6 +100,32 @@ impl AppState {
if let Ok(mut output) = output.write() {
*output = Some(py_output);
}

let mut results_contents = String::new();
let name = basename(directory);

let results_path = match incremental_run {
true => {
PathBuf::from("results").join(format!("tries_{name}.json"))
}
false => APP_DIRS.cache_dir().join("total_cnt.json"),
};

File::open(results_path)
.expect("results are not where they should be")
.read_to_string(&mut results_contents)
.expect("failed read");

if let Ok(mut results) = run_results.write() {
*results = Some(
serde_json::from_str(&results_contents)
.expect("results must contain a valid json"),
);
file_count.store(
cnt.expect("should be dir"),
std::sync::atomic::Ordering::SeqCst,
);
}
}
}
}
Expand All @@ -114,26 +140,6 @@ impl AppState {
}
*log = None;
}
let p = path.as_ref().map(|p| p.to_string_lossy());
if let (true, Ok(mut results), Some(path)) =
(incremental_run, incremental_run_results.write(), p)
{
let mut results_contents = String::new();
let name = basename(&path);
File::open(PathBuf::from("results").join(format!("tries_{name}.json")))
.expect("results are not where they should be")
.read_to_string(&mut results_contents)
.expect("failed read");

*results = Some(
serde_json::from_str(&results_contents)
.expect("results must contain a valid json"),
);
incremental_file_count.store(
cnt.expect("should be dir"),
std::sync::atomic::Ordering::SeqCst,
);
}
});
if let Err(err) = result {
if let Ok(mut output) = output.write() {
Expand Down
31 changes: 30 additions & 1 deletion poetry.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

1 change: 1 addition & 0 deletions pyproject.toml
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,7 @@ ruff = "^0.5.4"
pytest = "^8.3.1"
matplotlib = "^3.9.2"
ipykernel = "^6.29.5"
pyright = "^1.1.380"

[build-system]
requires = ["poetry-core"]
Expand Down
Loading

0 comments on commit 28474b4

Please sign in to comment.