Skip to content

Commit bbe5419

Browse files
committed
[hermes] Add package/target/root resolution
gherrit-pr-id: Gb7f1abf97eed8a035dbcaf7b0363b5890baaec05
1 parent 3150404 commit bbe5419

File tree

409 files changed

+62159
-485
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

409 files changed

+62159
-485
lines changed

tools/Cargo.lock

Lines changed: 139 additions & 2 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

tools/hermes/Cargo.toml

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,10 @@ license.workspace = true
77
publish.workspace = true
88

99
[dependencies]
10+
anyhow = "1.0.101"
11+
cargo_metadata = "0.23.1"
12+
clap = { version = "4.5.57", features = ["derive"] }
13+
clap-cargo = { version = "0.18.3", features = ["cargo_metadata"] }
1014
log = "0.4.29"
1115
miette = { version = "7.6.0", features = ["derive", "fancy"] }
1216
proc-macro2 = { version = "1.0.105", features = ["span-locations"] }

tools/hermes/src/main.rs

Lines changed: 36 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -1,44 +1,55 @@
11
mod errors;
22
mod parse;
3+
mod resolve;
34
mod transform;
45
mod ui_test_shim;
56

6-
use std::{env, path::PathBuf, process::exit};
7+
use std::{env, process::exit};
8+
9+
use clap::Parser;
10+
11+
/// Hermes: A Literate Verification Toolchain
12+
#[derive(Parser, Debug)]
13+
#[command(name = "hermes", version, about, long_about = None)]
14+
struct Cli {
15+
#[command(flatten)]
16+
resolve: resolve::Args,
17+
}
718

819
fn main() {
920
if env::var("HERMES_UI_TEST_MODE").is_ok() {
1021
ui_test_shim::run();
1122
return;
1223
}
1324

14-
let args: Vec<String> = env::args().collect();
15-
if args.len() < 2 {
16-
eprintln!("Usage: hermes <file.rs>");
17-
exit(1);
18-
}
25+
let args = Cli::parse();
1926

20-
let file_path = PathBuf::from(&args[1]);
27+
// TODO: Better error handling than `.unwrap()`.
28+
let roots = resolve::resolve_roots(&args.resolve).unwrap();
2129

30+
// TODO: From each root, parse and walk referenced modules.
2231
let mut has_errors = false;
23-
let mut edits = Vec::new();
24-
let res = parse::read_file_and_visit_hermes_items(&file_path, |_src, res| {
25-
if let Err(e) = res {
26-
has_errors = true;
27-
eprint!("{:?}", miette::Report::new(e));
28-
} else if let Ok(item) = res {
29-
transform::append_edits(&item, &mut edits);
32+
for (package, kind, path) in roots {
33+
let mut edits = Vec::new();
34+
let res = parse::read_file_and_visit_hermes_items(path.as_std_path(), |_src, res| {
35+
if let Err(e) = res {
36+
has_errors = true;
37+
eprint!("{:?}", miette::Report::new(e));
38+
} else if let Ok(item) = res {
39+
transform::append_edits(&item, &mut edits);
40+
}
41+
});
42+
43+
let source = res.unwrap_or_else(|e| {
44+
eprintln!("Error parsing file: {}", e);
45+
exit(1);
46+
});
47+
48+
if has_errors {
49+
exit(1);
3050
}
31-
});
32-
33-
let source = res.unwrap_or_else(|e| {
34-
eprintln!("Error parsing file: {}", e);
35-
exit(1);
36-
});
3751

38-
if has_errors {
39-
exit(1);
52+
let mut source = source.into_bytes();
53+
transform::apply_edits(&mut source, &edits);
4054
}
41-
42-
let mut source = source.into_bytes();
43-
transform::apply_edits(&mut source, &edits);
4455
}

0 commit comments

Comments
 (0)