Skip to content

Commit 6cd8edf

Browse files
crumplecupCopilot
andcommitted
merge: dev → main
- fix(ci): exclude nightly-only crates from stable clippy and doc check - fix(elicitation_creusot): add rust-toolchain.toml for publish verification - fix(proof-crate-gen): emit description and inherit all workspace pkg fields - chore(elicit_proofs): regenerate with description and full workspace metadata - chore(elicitation_verus): bump to 0.11.1, update verus deps to 2026-05-31 Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
2 parents e615e91 + 3bedec7 commit 6cd8edf

4 files changed

Lines changed: 42 additions & 11 deletions

File tree

crates/elicit_proofs/Cargo.toml

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,13 @@
33
name = "elicit_proofs"
44
version.workspace = true
55
edition.workspace = true
6+
description = "Formal verification proof harnesses for elicit_server"
67
license.workspace = true
8+
repository.workspace = true
9+
authors.workspace = true
10+
homepage.workspace = true
11+
documentation.workspace = true
12+
readme.workspace = true
713

814
[features]
915
kani = []

crates/elicitation/src/cli/generate/proof_crate_gen.rs

Lines changed: 30 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -117,6 +117,7 @@ pub fn generate_proof_crate(
117117
"Cargo.toml",
118118
&render_cargo_toml(
119119
&proof_name,
120+
&sources[0].name,
120121
&source_dep_lines,
121122
elicitation_rel.as_deref(),
122123
creusot_std_rel.as_deref(),
@@ -362,6 +363,7 @@ fn patch_module_tree_kani_reexports(
362363

363364
fn render_cargo_toml(
364365
proof_name: &str,
366+
primary_source: &str,
365367
source_dep_lines: &[&str],
366368
elicitation_rel: Option<&Path>,
367369
creusot_std_rel: Option<&Path>,
@@ -382,17 +384,38 @@ fn render_cargo_toml(
382384
} else {
383385
"edition = \"2024\"".to_string()
384386
};
385-
let license_field = if has_wpkg("license") {
386-
Some("license.workspace = true".to_string())
387+
388+
// description is required by crates.io; inherit from workspace or synthesize
389+
let description_field = if has_wpkg("description") {
390+
"description.workspace = true".to_string()
387391
} else {
388-
None
392+
format!(
393+
"description = \"Formal verification proof harnesses for {}\"",
394+
primary_source
395+
)
389396
};
390397

398+
// Optional publishable fields — inherit from workspace when present
399+
let optional_fields: &[&str] = &[
400+
"license",
401+
"license-file",
402+
"repository",
403+
"authors",
404+
"homepage",
405+
"documentation",
406+
"readme",
407+
"keywords",
408+
"categories",
409+
];
410+
let inherited: Vec<String> = optional_fields
411+
.iter()
412+
.filter(|&&f| has_wpkg(f))
413+
.map(|&f| format!("{f}.workspace = true"))
414+
.collect();
415+
391416
let pkg_fields = {
392-
let mut parts = vec![version_field, edition_field];
393-
if let Some(l) = license_field {
394-
parts.push(l);
395-
}
417+
let mut parts = vec![version_field, edition_field, description_field];
418+
parts.extend(inherited);
396419
parts.join("\n")
397420
};
398421

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
[toolchain]
2+
channel = "nightly-2026-02-27"

crates/elicitation_verus/Cargo.toml

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
[package]
22
name = "elicitation_verus"
3-
version = "0.11.0"
3+
version = "0.11.1"
44
edition = "2024"
55
license = "MIT OR Apache-2.0"
66
repository = "https://github.com/crumplecup/elicitation"
@@ -23,9 +23,9 @@ readme = "README.md"
2323
verify = true
2424

2525
[dependencies]
26-
elicitation = { version = "0.11.0" }
27-
verus_builtin_macros = "0.0.0-2026-05-10-0145"
28-
vstd = "0.0.0-2026-05-17-0151"
26+
elicitation = { version = "0.11.1" }
27+
verus_builtin_macros = "0.0.0-2026-05-31-0205"
28+
vstd = "0.0.0-2026-05-31-0205"
2929

3030
[lints.rust]
3131
unexpected_cfgs = { level = "warn", check-cfg = [

0 commit comments

Comments
 (0)