Skip to content

Commit 769a728

Browse files
SebTardifSebTardif
authored
fix(cli): doctor optional deps, init next step, and check --timeout (#1504)
## Summary Install-only users can run `assura check` after `cargo install` or a prebuilt binary: `doctor` no longer requires rustc, cargo, or a standalone `z3` CLI. `init` prints the first check command. `check --timeout` matches the spec, and watch mode uses the same solver and timeout. ## Problem - `assura doctor` failed after a crates.io or GitHub Release install because rustc, cargo, and `z3` on PATH were required. SMT already links Z3 through the z3 crate (`gh-release`). - `assura init` listed the scaffold files and stopped. The next command was not printed. - SPEC documents `assura check --timeout` (default 1000ms) and timeout diagnostics say "consider increasing --timeout", but the CLI flag was missing. Watch mode hardcoded Z3 and the default timeout. ## Change - Doctor: rustc, cargo, and the standalone z3 CLI are optional. Missing hints say `assura check` links Z3. Human footer is "`assura check` is ready". JSON `ok` is true without those CLIs. - Init: human and JSON `next` print `cd <dir>` and `assura check contracts/lib.assura`. - Check: `--timeout MS` overrides `VerifyOptions`. Watch receives the resolved options (solver + timeout). - Tests: encode_term Z3 and CVC5 helpers assert integer/boolean sorts, not only `Some`. Formatter keeps the full `&&` / `||` clause. - Library cleanup: if-encode and clause lower drop `expect`; IR codegen uses `let _ = writeln!` on `String`. - Docs: FAQ, SPEC §10.2/§10.3, MASTER-PLAN crate counts. ## Testing ```bash cargo fmt --all -- --check cargo clippy -p assura -p assura-smt -p assura-parser --lib --locked -- -D warnings bash scripts/guards.sh cargo test -p assura --test cli_integration --locked -- doctor_json_marks_toolchain cargo test -p assura --test cli_integration --locked -- check_timeout_flag_is_accepted ``` - [x] `cargo fmt --all -- --check` passes - [x] Targeted clippy on changed crates passes - [x] Tests added or updated - [ ] Full workspace clippy and demo check run in CI ## Related Ref #1410 Ref #1411 Ref #1396 Ref #436 Does not close those issues (human outreach and upstream cvc5-rs remain). --------- Signed-off-by: Sebastien Tardif <sebtardif@ncf.ca>
1 parent e850b93 commit 769a728

16 files changed

Lines changed: 293 additions & 207 deletions

File tree

‎MASTER-PLAN.md‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
# Assura Development Status
22

3-
> 201,006 lines of Rust, 5,794 tests, **21 workspace members** (re-counted 2026-08-13 via `scripts/count-crates.sh`).
3+
> 201,152 lines of Rust, 5,798 tests, **21 workspace members** (re-counted 2026-08-16 via `scripts/count-crates.sh`).
44
55
## What Works Today
66

@@ -36,28 +36,28 @@ Workspace members only (`Cargo.toml` `members = ["crates/*"]` with
3636

3737
| Crate (package) | LOC | Tests | Role |
3838
|-----------------|-----|-------|------|
39-
| assura-parser | 10,401 | 209 | Lexer (logos) + recursive-descent parser (rowan CST), Pratt expressions |
39+
| assura-parser | 10,395 | 209 | Lexer (logos) + recursive-descent parser (rowan CST), Pratt expressions |
4040
| assura-ast | 3,162 | 46 | Canonical AST, DeclVisitor, ExprVisitor, ExprFolder |
4141
| assura-resolve | 6,097 | 189 | Scope analysis, imports, stdlib prelude injection |
4242
| assura-types | 44,757 | 1,750 | 60+ checkers in CHECKER_PIPELINE, all 50 spec features |
43-
| assura-smt | 59,583 | 1,348 | Z3 + CVC5, Layer 2 verifier, prophecy/liveness/weak-memory, IR exec |
43+
| assura-smt | 59,591 | 1,348 | Z3 + CVC5, Layer 2 verifier, prophecy/liveness/weak-memory, IR exec |
4444
| assura-codegen | 16,706 | 670 | Multi-file Rust projects, proptest gen, WASM, IR body substitution |
4545
| assura-pipeline | 2,378 | 71 | Canonical compile/compile_full/verify_typed/run_at |
4646
| assura-config | 1,301 | 53 | assura.toml, VerifyOptions, CompilerConfig |
4747
| assura-diagnostics | 3,196 | 74 | Error codes, ariadne + JSON rendering |
48-
| assura (dir: assura-cli) | 39,635 | 951 | CLI binary: check, build, init, fmt, infer, check-rust, … |
48+
| assura (dir: assura-cli) | 39,777 | 955 | CLI binary: check, build, init, fmt, infer, check-rust, … |
4949
| assura-lsp | 1,965 | 55 | Language server (tower-lsp) |
5050
| assura-server | 809 | 27 | gRPC + HTTP/JSON API |
5151
| assura-mcp | 865 | 28 | MCP server for AI agent integration |
52-
| assura-fmt | 733 | 53 | Formatter |
52+
| assura-fmt | 735 | 53 | Formatter |
5353
| assura-macros | 1,974 | 58 | Proc macros (`#[contract]`, `#[trust]`) |
5454
| assura-stdlib | 409 | 18 | Stdlib modules (math, string, collections, …) |
5555
| assura-rust-analyzer | 2,514 | 92 | Syn-based Rust source parser for contract inference |
5656
| assura-test-support | 376 | 10 | Shared test helpers |
5757
| assura-bench | 421 | 0 | Criterion benchmarks |
5858
| assura-runtime | 262 | 10 | Runtime support for contracts |
5959
| assura-llm | 3,462 | 82 | LLM provider abstraction for auto-implement / suggest |
60-
| **Total** | **201,006** | **5,794** | |
60+
| **Total** | **201,152** | **5,798** | |
6161

6262
`crates/assura-driver` is **excluded** from the workspace (exploratory rustc
6363
driver). Refresh counts with `bash scripts/count-crates.sh`.

‎crates/assura-cli/src/check/run.rs‎

Lines changed: 12 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@ pub(crate) fn run_check(opts: CheckOptions<'_>) {
2121
show_cores,
2222
strict,
2323
showcase_only,
24+
timeout: cli_timeout,
2425
} = opts;
2526
// Load project config (assura.toml) if available
2627
let project = load_project_config(Path::new(filename));
@@ -50,6 +51,9 @@ pub(crate) fn run_check(opts: CheckOptions<'_>) {
5051
let mut cc = CompilerConfig::from_project(proj, output_mode, verbosity);
5152
cc.verify.layer = layer;
5253
cc.verify.solver = solver;
54+
if let Some(ms) = cli_timeout {
55+
cc.verify.timeout_ms = ms;
56+
}
5357
cc
5458
} else {
5559
CompilerConfig {
@@ -58,6 +62,8 @@ pub(crate) fn run_check(opts: CheckOptions<'_>) {
5862
verify: assura_config::VerifyOptions {
5963
layer,
6064
solver,
65+
timeout_ms: cli_timeout
66+
.unwrap_or(assura_config::VerifyOptions::default().timeout_ms),
6167
..Default::default()
6268
},
6369
..Default::default()
@@ -82,7 +88,12 @@ pub(crate) fn run_check(opts: CheckOptions<'_>) {
8288
}
8389
process::exit(2);
8490
}
85-
run_watch_loop(filename, output_mode, verbosity, layer);
91+
run_watch_loop(
92+
filename,
93+
output_mode,
94+
verbosity,
95+
compiler_config.verify.clone(),
96+
);
8697
// run_watch_loop never returns (loops until interrupted)
8798
}
8899

‎crates/assura-cli/src/check/types.rs‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,8 @@ pub(crate) struct CheckOptions<'a> {
1717
pub(crate) strict: bool,
1818
/// Directory mode: only files whose header marks SHOWCASE.
1919
pub(crate) showcase_only: bool,
20+
/// SMT timeout in milliseconds. `None` keeps assura.toml / default.
21+
pub(crate) timeout: Option<u64>,
2022
}
2123

2224
/// Context for verification + diagnostic reporting.

‎crates/assura-cli/src/check/watch.rs‎

Lines changed: 26 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ pub(crate) fn check_file_once(
1212
filename: &str,
1313
output_mode: OutputMode,
1414
verbosity: Verbosity,
15-
layer: u8,
15+
verify_options: assura_config::VerifyOptions,
1616
) -> bool {
1717
let source = match fs::read_to_string(filename) {
1818
Ok(s) => s,
@@ -64,11 +64,7 @@ pub(crate) fn check_file_once(
6464
has_errors: &mut has_errors,
6565
output_mode,
6666
verbosity,
67-
verify_options: assura_config::VerifyOptions {
68-
layer,
69-
solver: assura_smt::SolverChoice::Z3,
70-
..Default::default()
71-
},
67+
verify_options,
7268
show_cores: false,
7369
strict: false,
7470
});
@@ -90,7 +86,7 @@ pub(crate) fn run_watch_loop(
9086
filename: &str,
9187
output_mode: OutputMode,
9288
verbosity: Verbosity,
93-
layer: u8,
89+
verify_options: assura_config::VerifyOptions,
9490
) -> ! {
9591
use notify::{Event, EventKind, RecursiveMode, Watcher};
9692

@@ -126,7 +122,7 @@ pub(crate) fn run_watch_loop(
126122
incremental.register_module(filename.to_string(), last_hash.clone());
127123
}
128124
// In watch mode, we continue regardless of errors (intentionally ignoring result)
129-
let _had_errors = check_file_once(filename, output_mode, verbosity, layer);
125+
let _had_errors = check_file_once(filename, output_mode, verbosity, verify_options.clone());
130126
incremental.mark_checked(filename, 1);
131127
if !json {
132128
eprintln!();
@@ -220,7 +216,7 @@ pub(crate) fn run_watch_loop(
220216
eprintln!("[watch] File changed, re-checking {filename}...");
221217
eprintln!();
222218
}
223-
let _had_errors = check_file_once(filename, output_mode, verbosity, layer);
219+
let _had_errors = check_file_once(filename, output_mode, verbosity, verify_options.clone());
224220
incremental.mark_checked(filename, iteration);
225221
iteration += 1;
226222
if !json {
@@ -229,3 +225,24 @@ pub(crate) fn run_watch_loop(
229225
}
230226
}
231227
}
228+
229+
#[cfg(test)]
230+
mod tests {
231+
use super::*;
232+
233+
#[test]
234+
fn check_file_once_uses_passed_verify_options() {
235+
let mut opts = assura_config::VerifyOptions::default();
236+
opts.timeout_ms = 250;
237+
opts.solver = assura_smt::SolverChoice::Cvc5;
238+
assert!(
239+
check_file_once(
240+
"/no/such/watch/unit.assura",
241+
OutputMode::Json,
242+
Verbosity::Quiet,
243+
opts,
244+
),
245+
"missing path should count as a check error"
246+
);
247+
}
248+
}

‎crates/assura-cli/src/cli.rs‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -98,6 +98,10 @@ enum Commands {
9898
/// When FILE is a directory, only check demos marked SHOWCASE (must-pass)
9999
#[arg(long)]
100100
showcase_only: bool,
101+
102+
/// SMT solver timeout in milliseconds (overrides assura.toml [verify] timeout)
103+
#[arg(long, value_name = "MS")]
104+
timeout: Option<u64>,
101105
},
102106

103107
/// Verify inline contract annotations in Rust source files
@@ -480,6 +484,7 @@ pub fn run() {
480484
show_cores,
481485
strict,
482486
showcase_only,
487+
timeout,
483488
} => run_check(CheckOptions {
484489
filename: &file,
485490
output_mode,
@@ -492,6 +497,7 @@ pub fn run() {
492497
show_cores,
493498
strict,
494499
showcase_only,
500+
timeout,
495501
}),
496502
Commands::CheckRust {
497503
path,

‎crates/assura-cli/src/init.rs‎

Lines changed: 23 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -184,6 +184,7 @@ contract SafeDivision {
184184
});
185185

186186
// Report what was created
187+
let next = init_next_steps(project_name);
187188
if json {
188189
let report = serde_json::json!({
189190
"ok": true,
@@ -193,16 +194,30 @@ contract SafeDivision {
193194
contract_path.display().to_string(),
194195
ir_path.display().to_string(),
195196
],
197+
"next": next,
196198
});
197199
println!("{}", serde_json::to_string_pretty(&report).unwrap());
198200
} else {
199201
println!("Created new Assura project '{project_name}':");
200202
println!(" {}", toml_path.display());
201203
println!(" {}", contract_path.display());
202204
println!(" {}", ir_path.display());
205+
println!();
206+
println!("Next:");
207+
for step in next {
208+
println!(" {step}");
209+
}
203210
}
204211
}
205212

213+
/// First commands after `assura init` (human + JSON).
214+
fn init_next_steps(project_name: &str) -> [String; 2] {
215+
[
216+
format!("cd {project_name}"),
217+
"assura check contracts/lib.assura".to_string(),
218+
]
219+
}
220+
206221
pub(crate) fn run_explain(code: &str, output_mode: OutputMode) {
207222
match assura_diagnostics::explain(code) {
208223
Some(info) => {
@@ -263,7 +278,14 @@ pub(crate) fn run_explain(code: &str, output_mode: OutputMode) {
263278

264279
#[cfg(test)]
265280
mod init_name_tests {
266-
use super::validate_project_name;
281+
use super::{init_next_steps, validate_project_name};
282+
283+
#[test]
284+
fn next_steps_point_at_scaffold_check() {
285+
let steps = init_next_steps("demo");
286+
assert_eq!(steps[0], "cd demo");
287+
assert_eq!(steps[1], "assura check contracts/lib.assura");
288+
}
267289

268290
#[test]
269291
fn accepts_simple_names() {

‎crates/assura-cli/src/lsp_doctor.rs‎

Lines changed: 24 additions & 44 deletions
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,6 @@ pub(crate) fn run_lsp() {
2121

2222
pub(crate) fn run_doctor(output_mode: OutputMode, verbosity: Verbosity) {
2323
let mut checks: Vec<serde_json::Value> = Vec::new();
24-
let mut all_ok = true;
2524

2625
let version = env!("CARGO_PKG_VERSION");
2726

@@ -33,14 +32,11 @@ pub(crate) fn run_doctor(output_mode: OutputMode, verbosity: Verbosity) {
3332
let ver = ver.trim().strip_prefix("rustc ").unwrap_or(ver.trim());
3433
("ok", ver.to_string())
3534
}
36-
_ => {
37-
all_ok = false;
38-
("missing", "not found".into())
39-
}
35+
_ => ("optional", "not found".into()),
4036
};
4137
checks.push(serde_json::json!({
4238
"name": "rustc", "status": rustc_status, "detail": rustc_detail,
43-
"required": true,
39+
"required": false,
4440
}));
4541

4642
// cargo
@@ -51,14 +47,11 @@ pub(crate) fn run_doctor(output_mode: OutputMode, verbosity: Verbosity) {
5147
let ver = ver.trim().strip_prefix("cargo ").unwrap_or(ver.trim());
5248
("ok", ver.to_string())
5349
}
54-
_ => {
55-
all_ok = false;
56-
("missing", "not found".into())
57-
}
50+
_ => ("optional", "not found".into()),
5851
};
5952
checks.push(serde_json::json!({
6053
"name": "cargo", "status": cargo_status, "detail": cargo_detail,
61-
"required": true,
54+
"required": false,
6255
}));
6356

6457
// z3
@@ -72,14 +65,11 @@ pub(crate) fn run_doctor(output_mode: OutputMode, verbosity: Verbosity) {
7265
.unwrap_or(ver);
7366
("ok", short.to_string())
7467
}
75-
_ => {
76-
all_ok = false;
77-
("missing", "not found".into())
78-
}
68+
_ => ("optional", "not found".into()),
7969
};
8070
checks.push(serde_json::json!({
8171
"name": "z3", "status": z3_status, "detail": z3_detail,
82-
"required": true,
72+
"required": false,
8373
}));
8474

8575
// cvc5 (optional)
@@ -120,7 +110,7 @@ pub(crate) fn run_doctor(output_mode: OutputMode, verbosity: Verbosity) {
120110
if output_mode == OutputMode::Json {
121111
let json = serde_json::json!({
122112
"assura": version,
123-
"ok": all_ok,
113+
"ok": true,
124114
"checks": checks,
125115
});
126116
println!(
@@ -149,12 +139,22 @@ pub(crate) fn run_doctor(output_mode: OutputMode, verbosity: Verbosity) {
149139
};
150140
// Match historical layout: " rustc: 1.97.0 ... OK"
151141
println!(" {label:<pad$} {detail} ... {status_label}");
152-
if status == "missing" && name == "rustc" {
153-
println!(" Install: https://rustup.rs/");
142+
if name == "rustc" && status != "ok" {
143+
println!(
144+
" Optional: needed for `assura build` (https://rustup.rs/)."
145+
);
146+
println!(" `assura check` works without a local rustc.");
147+
}
148+
if name == "cargo" && status != "ok" {
149+
println!(
150+
" Optional: needed for `assura build` / `cargo test` on generated Rust."
151+
);
154152
}
155-
if status == "missing" && name == "z3" {
156-
println!(" Install: brew install z3 (macOS)");
157-
println!(" sudo apt-get install -y libz3-dev (Ubuntu)");
153+
if name == "z3" && status != "ok" {
154+
println!(
155+
" Optional: standalone `z3` CLI (brew install z3 / libz3-dev)."
156+
);
157+
println!(" `assura check` already links Z3 via the z3 crate.");
158158
}
159159
if name == "cvc5" && status != "ok" {
160160
println!(" Install: bash scripts/setup-cvc5.sh");
@@ -164,28 +164,8 @@ pub(crate) fn run_doctor(output_mode: OutputMode, verbosity: Verbosity) {
164164
}
165165
}
166166
println!();
167-
if all_ok {
168-
println!("All required dependencies are installed.");
169-
} else {
170-
println!(
171-
"Some required dependencies are missing. Install them and re-run `assura doctor`."
172-
);
173-
}
174-
} else if !all_ok {
175-
// Quiet human: only surface failure (required deps missing).
176-
eprintln!("assura doctor: required dependencies missing");
177-
for c in &checks {
178-
let status = c["status"].as_str().unwrap_or("?");
179-
let required = c["required"].as_bool().unwrap_or(false);
180-
if required && status == "missing" {
181-
let name = c["name"].as_str().unwrap_or("?");
182-
eprintln!(" missing: {name}");
183-
}
184-
}
185-
}
186-
187-
if !all_ok {
188-
process::exit(1);
167+
println!("`assura check` is ready. rustc/cargo are for `assura build`;");
168+
println!("the standalone `z3` CLI and cvc5 are optional.");
189169
}
190170
}
191171

0 commit comments

Comments
 (0)