Skip to content

fix: split package name and crate name for hyphenated packages #46

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Marsman1996 merged 1 commit into from
Sep 4, 2026
Merged

fix: split package name and crate name for hyphenated packages #46

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
13 changes: 7 additions & 6 deletions src/commands.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -269,22 +269,22 @@ impl CargoBuildExterns {
full
}

pub fn parse_from_build_log(package: &str, stdout: &str, stderr: &str) -> Self {
pub fn parse_from_build_log(crate_name: &str, stdout: &str, stderr: &str) -> Self {
let mut cargo_build = CargoBuildExterns::new(true);
cargo_build.parse_library(stdout);
cargo_build.parse_last_level(package, stderr);
cargo_build.parse_last_level(crate_name, stderr);
cargo_build
}

pub fn parse_last_level(&mut self, package: &str, stderr: &str) {
pub fn parse_last_level(&mut self, crate_name: &str, stderr: &str) {
let rustc_regex =
Regex::new(r"^\s+Running\s+`.*rustc\s+.*--crate-name\s+(\S+)\s+.*$").unwrap();
let extern_regex = Regex::new(r"--extern\s+([^=\s]+)=([^\s]+)").unwrap();

for line in stderr.lines() {
if let Some(caps) = rustc_regex.captures(line) {
let crate_name = caps.get(1).unwrap().as_str();
if crate_name != package {
let line_crate = caps.get(1).unwrap().as_str();
if line_crate != crate_name {
continue;
}
}
Expand Down Expand Up @@ -352,6 +352,7 @@ impl CargoBuildExterns {
/// But the package itself is not required to be built.
pub fn cargo_build_resolve_deps(
package: &str,
crate_name: &str,
env: &HashMap<String, String>,
release: bool,
) -> CargoBuildExterns {
Expand All @@ -377,7 +378,7 @@ pub fn cargo_build_resolve_deps(
.arg(crate::verus::VERIFICATION_RUST_TARGET);

let res = run_build_log_capture(&mut cmd);
CargoBuildExterns::parse_from_build_log(package, res.stdout.as_str(), res.stderr.as_str())
CargoBuildExterns::parse_from_build_log(crate_name, res.stdout.as_str(), res.stderr.as_str())
}

pub fn cargo_build(package: &str, env: &HashMap<String, String>, release: bool) {
Expand Down
3 changes: 2 additions & 1 deletion src/count.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -290,7 +290,8 @@ fn run_module_line_count(
print_all: bool,
) -> Result<(), DynError> {
let module = module
.strip_prefix(&format!("{}::", target.name))
.strip_prefix(&format!("{}::", target.crate_name))
.or_else(|| module.strip_prefix(&format!("{}::", target.name)))
.unwrap_or(module);
let paths = module_source_paths(&target.file, module)?;

Expand Down
15 changes: 9 additions & 6 deletions src/doc.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -137,11 +137,14 @@ fn generate_single_target_doc(
// Add dependencies that this target actually needs
let deps = verus::get_local_dependency(target);
for (_name, dep_target) in deps.iter() {
if dep_target.name != target.name {
if let Some(rlib_path) = find_local_dependency_rlib(&target_dir, &dep_target.name) {
let extern_name = dep_target.name.replace('-', "_");
cmd.arg("--extern")
.arg(format!("{}={}", extern_name, rlib_path.display()));
if dep_target.crate_name != target.crate_name {
if let Some(rlib_path) = find_local_dependency_rlib(&target_dir, &dep_target.crate_name)
{
cmd.arg("--extern").arg(format!(
"{}={}",
dep_target.crate_name,
rlib_path.display()
));
} else {
return Err(format!(
"Missing built dependency '{}' for target '{}'.\n\nPlease run:\n cargo dv build",
Expand Down Expand Up @@ -217,7 +220,7 @@ fn generate_single_target_doc(

// Set crate type and name
cmd.arg("--crate-type=lib")
.arg(format!("--crate-name={}", target.name.replace('-', "_")));
.arg(format!("--crate-name={}", target.crate_name));

if json_output {
cmd.arg("--output-format").arg("json");
Expand Down
6 changes: 4 additions & 2 deletions src/pre_commit.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,9 @@ fn main() {
let mut found_errors = false;
for (vt, t) in targets.iter() {
let verus_target = t.root_file();
let package = members.get(vt).unwrap_or_else(|| {
// `targets` is keyed by crate identifier; metadata packages are keyed
// by the manifest package name.
let package = members.get(&t.name).unwrap_or_else(|| {
fatal!("Unable to find target {} in metadata", vt);
});

Expand All @@ -36,7 +38,7 @@ fn main() {
if verus_target == cargo_target {
warn!("Target [{}] has cargo target source path `{}` which is the same as the Verus target.\n\
Consider change `path=...` in `{}` to `path=src/.dummy.rs` to avoid build errors.",
vt, cargo_target, package.manifest_path);
t.name, cargo_target, package.manifest_path);
found_errors = true;
}
}
Expand Down
45 changes: 29 additions & 16 deletions src/verus.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -159,8 +159,11 @@ pub struct VerusDependency {

#[derive(Clone, Debug, PartialEq, Eq, Hash)]
pub struct VerusTarget {
/// name of the package
/// name of the package, as declared in `Cargo.toml` (e.g. `id-alloc`)
pub name: String,
/// crate identifier of the package (e.g. `id_alloc`); differs from `name`
/// for packages with hyphens
pub crate_name: String,
/// version of the package
pub version: String,
/// directory of the package
Expand Down Expand Up @@ -250,15 +253,15 @@ impl VerusTarget {

pub fn library_proof(&self) -> PathBuf {
get_target_dir()
.join(format!("{}.verusdata", self.name))
.join(format!("{}.verusdata", self.crate_name))
.to_path_buf()
}

pub fn library_path(&self) -> PathBuf {
let lib = format!(
"{}{}.{}",
self.library_prefix(),
self.name,
self.crate_name,
self.library_suffix()
);
get_target_dir().join(lib).to_path_buf()
Expand Down Expand Up @@ -357,7 +360,8 @@ pub fn verus_targets() -> HashMap<String, VerusTarget> {

// check if the package has a target
if let Some(target) = package.targets.first() {
let name = package.name.as_str().replace('-', "_");
let name = package.name.as_str().to_string();
let crate_name = name.replace('-', "_");
let version = package.version.to_string();
let dir = Path::new(&package.manifest_path)
.parent()
Expand Down Expand Up @@ -386,9 +390,10 @@ pub fn verus_targets() -> HashMap<String, VerusTarget> {
let features = extract_features(package, ws_features.as_slice());

targets.insert(
name.clone(),
crate_name.clone(),
VerusTarget {
name,
crate_name,
version,
dir,
file,
Expand All @@ -410,8 +415,11 @@ pub fn verus_targets() -> HashMap<String, VerusTarget> {
pub fn find_target(t: &str) -> Result<VerusTarget, String> {
let all = verus_targets();
let s = files::dir_as_package(t);
// Target names are keyed by crate identifier (`-` -> `_`); accept both
// spellings so users can pass the package name as well.
let key = s.replace('-', "_");

let target = all.get(&s).cloned().unwrap_or_else(|| {
let target = all.get(&key).cloned().unwrap_or_else(|| {
error!(
"Cannot find target {}\n\n Targets available:\n{}",
t,
Expand All @@ -435,12 +443,13 @@ fn get_local_dependency_direct(target: &VerusTarget) -> IndexMap<String, VerusTa
// Not a local path dependency
continue;
}
if !all.contains_key(dep.name.as_str()) {
let dep_key = dep.name.replace('-', "_");
if !all.contains_key(&dep_key) {
// Not in current workspace
continue;
}
let dep_target = all.get(dep.name.as_str()).unwrap();
deps.insert(dep.name.clone(), dep_target.clone());
let dep_target = all.get(&dep_key).unwrap();
deps.insert(dep_key, dep_target.clone());
}

deps
Expand All @@ -456,7 +465,7 @@ pub fn get_local_dependency(target: &VerusTarget) -> IndexMap<String, VerusTarge
visited: &mut std::collections::HashSet<String>,
_is_root: bool,
) {
let target_name = target.name.replace('-', "_");
let target_name = target.crate_name.clone();

// Prevent infinite recursion
if visited.contains(&target_name) {
Expand All @@ -469,9 +478,8 @@ pub fn get_local_dependency(target: &VerusTarget) -> IndexMap<String, VerusTarge

// Add direct dependencies to result (unless it's the root target)
for (dep_name, dep_target) in direct_deps.iter() {
let dep_key = dep_name.replace('-', "_");
if !result.contains_key(&dep_key) {
result.insert(dep_key, dep_target.clone());
if !result.contains_key(dep_name) {
result.insert(dep_name.clone(), dep_target.clone());
}
// Recursively collect dependencies of this dependency
collect_deps_recursively(dep_target, result, visited, false);
Expand All @@ -489,7 +497,7 @@ pub fn get_remote_dependency(target: &VerusTarget, release: bool) -> IndexMap<St

let local_verus = verus_targets()
.values()
.map(|t| t.name.replace('-', "_"))
.map(|t| t.crate_name.clone())
.collect::<HashSet<_>>();

for (name, path) in externs.iter() {
Expand Down Expand Up @@ -546,7 +554,12 @@ pub fn resolve_deps(target: &VerusTarget, release: bool) -> CargoBuildExterns {
let dummy_rs = target.dir.join("src").join(".dummy.rs");
files::touch(&dummy_rs.to_string_lossy());

let mut externs = commands::cargo_build_resolve_deps(&target.name, &HashMap::new(), release);
let mut externs = commands::cargo_build_resolve_deps(
&target.name,
&target.crate_name,
&HashMap::new(),
release,
);

if externs.deps_ready {
reorder_deps(target, &mut externs);
Expand Down Expand Up @@ -682,7 +695,7 @@ pub fn exec_verify(targets: &[VerusTarget], options: &ExtraOptions) -> Result<()

if options.log && target.is_some() {
let target = target.unwrap();
move_verus_log_files(&target.name);
move_verus_log_files(&target.crate_name);
}
} else {
error!(
Expand Down
Loading