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
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions tools/Cargo.lock

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

3 changes: 3 additions & 0 deletions tools/hermes/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -10,9 +10,12 @@ publish.workspace = true
log = "0.4.29"
miette = { version = "7.6.0", features = ["derive", "fancy"] }
proc-macro2 = { version = "1.0.105", features = ["span-locations"] }
serde = { version = "1.0.228", features = ["derive"] }
serde_json = "1.0.149"
syn = { version = "2.0.114", features = ["full", "visit", "extra-traits", "parsing"] }
thiserror = "2.0.18"

[dev-dependencies]
syn = { version = "2.0.114", features = ["printing", "full", "visit", "extra-traits", "parsing"] }
proc-macro2 = { version = "1.0.105", features = ["span-locations"] }
ui_test = "0.30.4"
37 changes: 36 additions & 1 deletion tools/hermes/src/main.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,39 @@
mod errors;
mod parse;
mod ui_test_shim;

fn main() {}
use std::{env, fs, path::PathBuf, process::exit};

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 file_path = PathBuf::from(&args[1]);
let source = match fs::read_to_string(&file_path) {
Ok(s) => s,
Err(e) => {
eprintln!("Error reading file: {}", e);
exit(1);
}
};

let mut has_errors = false;
parse::visit_hermes_items_in_file(&file_path, &source, |res| {
if let Err(e) = res {
has_errors = true;
eprint!("{:?}", miette::Report::new(e));
}
});

if has_errors {
exit(1);
}
}
4 changes: 2 additions & 2 deletions tools/hermes/src/parse.rs
Original file line number Diff line number Diff line change
Expand Up @@ -77,7 +77,7 @@ where
/// Parses the given Rust source code from a file path and invokes the callback `f`
/// for each item annotated with a `/// ```lean` block. Parsing errors and generated
/// items will be associated with this file path.
fn visit_hermes_items_in_file<F>(path: &Path, source: &str, f: F)
pub fn visit_hermes_items_in_file<F>(path: &Path, source: &str, f: F)
where
F: FnMut(Result<ParsedLeanItem, HermesError>),
{
Expand All @@ -94,7 +94,7 @@ where
.as_ref()
.map(|p| p.display().to_string())
.unwrap_or_else(|| "<input>".to_string());
dbg!(&f);

f
};
let _x = source_file
Expand Down
128 changes: 128 additions & 0 deletions tools/hermes/src/ui_test_shim.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,128 @@
use std::{env, fs, path::PathBuf, process::exit};

use miette::Diagnostic as _;
use serde::Serialize;

use crate::{errors::HermesError, parse};

/// The entrypoint for running under the `ui_test` crate, which expects us to be
/// `rustc`. This is a bit of a hack, but it works.
pub fn run() {
let args: Vec<String> = env::args().collect();

// Spoof version if requested
if args.contains(&"-vV".to_string()) || args.contains(&"--version".to_string()) {
println!("rustc 1.93.0-nightly (hermes-shim)");
println!("binary: rustc");
println!("commit-hash: 0000000000000000000000000000000000000000");
println!("commit-date: 2025-01-01");
println!("host: x86_64-unknown-linux-gnu");
println!("release: 1.93.0-nightly");
exit(0);
}

// Find the file (ignoring rustc flags like --out-dir)
let file_path = args
.iter()
.skip(1)
.find(|arg| arg.ends_with(".rs") && !arg.starts_with("--"))
.map(PathBuf::from)
.unwrap_or_else(|| {
// If no file found, maybe it's just a flag check. Exit successfully
// to appease ui_test.
exit(0);
});

// Run logic with JSON emitter
let source = fs::read_to_string(&file_path).unwrap_or_default();
Copy link
Contributor

Choose a reason for hiding this comment

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

medium

Using unwrap_or_default() can hide file reading errors. If fs::read_to_string fails, it will proceed with an empty string, and the test will likely pass silently because no hermes items will be found. This can make debugging tests more difficult. It's better to panic with a clear message if the test file cannot be read.

Suggested change
let source = fs::read_to_string(&file_path).unwrap_or_default();
let source = fs::read_to_string(&file_path).expect("Failed to read test file");

let mut has_errors = false;

parse::visit_hermes_items_in_file(&file_path, &source, |res| {
if let Err(e) = res {
has_errors = true;
emit_rustc_json(&e, &source, file_path.to_str().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

Calling .unwrap() on file_path.to_str() can cause a panic if the file path contains non-UTF-8 characters, which is possible on some systems. It's safer and more idiomatic to use display() to get a string representation of the path, which gracefully handles non-UTF-8 characters.

Suggested change
emit_rustc_json(&e, &source, file_path.to_str().unwrap());
emit_rustc_json(&e, &source, &file_path.display().to_string());

}
});

if has_errors {
exit(1);
}
}

#[derive(Serialize)]
struct RustcDiagnostic {
message: String,
level: String,
spans: Vec<RustcSpan>,
children: Vec<RustcDiagnostic>,
rendered: String,
}

#[derive(Serialize)]
struct RustcSpan {
file_name: String,
byte_start: usize,
byte_end: usize,
line_start: usize,
line_end: usize,
column_start: usize,
column_end: usize,
is_primary: bool,
text: Vec<RustcSpanLine>, // ui_test sometimes checks the snippet context
}

#[derive(Serialize)]
struct RustcSpanLine {
text: String,
highlight_start: usize,
highlight_end: usize,
}

pub fn emit_rustc_json(e: &HermesError, source: &str, file: &str) {
let msg = e.to_string();
// Use miette's span to get byte offsets.
let span = e.labels().and_then(|mut l| l.next());

let mut spans = Vec::new();
if let Some(labeled_span) = span {
let offset = labeled_span.offset();
let len = labeled_span.len();

// Calculate lines/cols manually (miette makes this hard to extract
// without a Report). This is isolated here now, so it's fine.
let prefix = &source[..offset];
let line_start = prefix.lines().count().max(1);
let last_nl = prefix.rfind('\n').map(|i| i + 1).unwrap_or(0);
let column_start = (offset - last_nl) + 1;

// Grab the line text for the snippet
let line_end_idx = source[offset..].find('\n').map(|i| offset + i).unwrap_or(source.len());
let line_text = source[last_nl..line_end_idx].to_string();

spans.push(RustcSpan {
file_name: file.to_string(),
byte_start: offset,
byte_end: offset + len,
line_start,
line_end: line_start, // Assuming single line for simplicity
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 current implementation assumes that errors span only a single line by setting line_end: line_start. While this is sufficient for the current error types, it could produce incorrect diagnostic spans for more complex, multi-line errors in the future. To make this more robust, consider calculating line_end properly based on the full span of the error.

column_start,
column_end: column_start + len,
is_primary: true,
text: vec![RustcSpanLine {
text: line_text,
highlight_start: column_start,
highlight_end: column_start + len,
}],
});
}

let diag = RustcDiagnostic {
message: msg.clone(),
level: "error".to_string(),
spans,
children: vec![],
rendered: format!("error: {}\n", msg),
};

eprintln!("{}", serde_json::to_string(&diag).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

Using .unwrap() can cause a panic without a descriptive message if JSON serialization fails. While unlikely for this structure, it's good practice to use .expect() to provide a more informative error message in case of a panic, which aids in debugging.

Suggested change
eprintln!("{}", serde_json::to_string(&diag).unwrap());
eprintln!("{}", serde_json::to_string(&diag).expect("Failed to serialize diagnostic to JSON"));

}
40 changes: 40 additions & 0 deletions tools/hermes/tests/ui.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,40 @@
use std::{path::PathBuf, process::Command};

use ui_test::*;

#[test]
fn ui() {
std::env::set_var("HERMES_UI_TEST_MODE", "true");

let mut config = Config::rustc(PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("tests/ui"));

let args = Args::test().unwrap();
config.with_args(&args);

let binary_path = compile_and_find_binary("hermes");
config.program.program = binary_path;

run_tests(config).unwrap();
}

fn compile_and_find_binary(name: &str) -> PathBuf {
let manifest_dir = env!("CARGO_MANIFEST_DIR");
let status = Command::new("cargo")
.arg("build")
.arg("--bin")
.arg(name)
.current_dir(manifest_dir)
.status()
.expect("Failed to execute cargo build");

assert!(status.success(), "Failed to build binary '{}'", name);

let mut path = PathBuf::from(manifest_dir);
path.push("..");
Copy link
Contributor

Choose a reason for hiding this comment

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

critical

The path to the compiled binary is constructed incorrectly. The target directory is located at the workspace root, which is two levels above the hermes crate's manifest directory (tools/hermes/). The current code only goes up one level (..), which will result in an incorrect path (tools/target/...). This will cause the assert! on line 38 to fail. You need to go up two levels to find the workspace's target directory.

Suggested change
path.push("..");
path.push("..");
path.push("..");

path.push("target");
path.push("debug");
path.push(name);

assert!(path.exists(), "Binary not found at {:?}", path);
path
}
3 changes: 3 additions & 0 deletions tools/hermes/tests/ui/fail_precondition.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
/// ```lean
//~^ ERROR: Unclosed ```lean block in documentation
unsafe fn unsafe_op(x: u32) -> u32 { x }
1 change: 1 addition & 0 deletions tools/hermes/tests/ui/fail_precondition.stderr
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
error: Documentation block error: Unclosed ```lean block in documentation
7 changes: 7 additions & 0 deletions tools/hermes/tests/ui/pass_simple.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
//@ check-pass

/// ```lean
/// ```
fn safe_function(x: u32) -> u32 {
x
}
Loading