Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
141 changes: 139 additions & 2 deletions tools/Cargo.lock

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

4 changes: 4 additions & 0 deletions tools/hermes/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,10 @@ license.workspace = true
publish.workspace = true

[dependencies]
anyhow = "1.0.101"
cargo_metadata = "0.23.1"
clap = { version = "4.5.57", features = ["derive"] }
clap-cargo = { version = "0.18.3", features = ["cargo_metadata"] }
log = "0.4.29"
miette = { version = "7.6.0", features = ["derive", "fancy"] }
proc-macro2 = { version = "1.0.105", features = ["span-locations"] }
Expand Down
61 changes: 36 additions & 25 deletions tools/hermes/src/main.rs
Original file line number Diff line number Diff line change
@@ -1,44 +1,55 @@
mod errors;
mod parse;
mod resolve;
mod transform;
mod ui_test_shim;

use std::{env, path::PathBuf, process::exit};
use std::{env, process::exit};

use clap::Parser;

/// Hermes: A Literate Verification Toolchain
#[derive(Parser, Debug)]
#[command(name = "hermes", version, about, long_about = None)]
struct Cli {
#[command(flatten)]
resolve: resolve::Args,
}

fn main() {
if env::var("HERMES_UI_TEST_MODE").is_ok() {
ui_test_shim::run();
return;
}

let args: Vec<String> = env::args().collect();
if args.len() < 2 {
eprintln!("Usage: hermes <file.rs>");
exit(1);
}
let args = Cli::parse();

let file_path = PathBuf::from(&args[1]);
// TODO: Better error handling than `.unwrap()`.
let roots = resolve::resolve_roots(&args.resolve).unwrap();
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

medium

As noted in the TODO comment, using .unwrap() here can cause the program to panic if resolve_roots returns an error. It would be more user-friendly to handle the error gracefully and print a descriptive message instead of panicking. Since anyhow is a dependency, you can use unwrap_or_else to achieve this.

Suggested change
let roots = resolve::resolve_roots(&args.resolve).unwrap();
let roots = resolve::resolve_roots(&args.resolve).unwrap_or_else(|e| {
eprintln!("error: failed to resolve verification roots: {e:?}");
exit(1);
});


// TODO: From each root, parse and walk referenced modules.
let mut has_errors = false;
let mut edits = Vec::new();
let res = parse::read_file_and_visit_hermes_items(&file_path, |_src, res| {
if let Err(e) = res {
has_errors = true;
eprint!("{:?}", miette::Report::new(e));
} else if let Ok(item) = res {
transform::append_edits(&item, &mut edits);
for (package, kind, path) in roots {
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

medium

The package and kind variables are unused within this loop. To improve code clarity and avoid compiler warnings, you can replace them with _.

Suggested change
for (package, kind, path) in roots {
for (_, _, path) in roots {

let mut edits = Vec::new();
let res = parse::read_file_and_visit_hermes_items(path.as_std_path(), |_src, res| {
if let Err(e) = res {
has_errors = true;
eprint!("{:?}", miette::Report::new(e));
} else if let Ok(item) = res {
transform::append_edits(&item, &mut edits);
}
});

let source = res.unwrap_or_else(|e| {
eprintln!("Error parsing file: {}", e);
exit(1);
});

if has_errors {
exit(1);
}
});

let source = res.unwrap_or_else(|e| {
eprintln!("Error parsing file: {}", e);
exit(1);
});

if has_errors {
exit(1);
let mut source = source.into_bytes();
transform::apply_edits(&mut source, &edits);
}

let mut source = source.into_bytes();
transform::apply_edits(&mut source, &edits);
}
Loading
Loading