hax_types/diagnostics/
message.rs

1use crate::cli_options::{Backend, BackendName, MessageFormat};
2use crate::diagnostics::report::ReportCtx;
3use crate::prelude::*;
4
5/// What a `hax.toml` entry resolved to.
6#[derive_group(Serializers)]
7#[derive(Debug, Clone, JsonSchema, Hash, Eq, PartialEq)]
8#[serde(rename_all = "snake_case")]
9pub enum ResolvedValue {
10    Version(String),
11    /// The path of a `path` entry, as given.
12    Path(String),
13}
14
15/// One resolved tool or declared version: what it is, what it resolved to,
16/// and a description of where that came from.
17#[derive_group(Serializers)]
18#[derive(Debug, Clone, JsonSchema, Hash, Eq, PartialEq)]
19pub struct ToolResolution {
20    pub name: String,
21    #[serde(flatten)]
22    pub resolved: ResolvedValue,
23    pub source: String,
24}
25
26impl ToolResolution {
27    /// The resolved version or path, as shown.
28    fn value(&self) -> &str {
29        match &self.resolved {
30            ResolvedValue::Version(value) | ResolvedValue::Path(value) => value,
31        }
32    }
33}
34
35/// How a resolved `hax-lib` version relates to the range a `cargo-hax`
36/// binary accepts.
37#[derive_group(Serializers)]
38#[derive(Debug, Clone, Copy, JsonSchema, Hash, Eq, PartialEq)]
39pub enum HaxLibCompatibility {
40    Compatible,
41    /// Older than the binary: the project's dependency needs updating
42    /// (or an older cargo-hax is needed).
43    TooOld,
44    /// Newer than the binary (typically after a `cargo update`): update
45    /// cargo-hax, or pin `hax-lib` back to the binary's version.
46    TooNew,
47}
48
49impl HaxLibCompatibility {
50    /// The parenthesized status `tools show` annotates a `hax-lib` row with.
51    fn describe(self) -> &'static str {
52        match self {
53            Self::Compatible => "compatible",
54            Self::TooOld => "INCOMPATIBLE: too old for this cargo-hax",
55            Self::TooNew => "INCOMPATIBLE: newer than this cargo-hax",
56        }
57    }
58}
59
60/// The `hax-lib` version one crate's direct dependency resolved to.
61#[derive_group(Serializers)]
62#[derive(Debug, Clone, JsonSchema, Hash, Eq, PartialEq)]
63pub struct HaxLibStatus {
64    #[serde(rename = "crate")]
65    pub crate_name: String,
66    pub version: String,
67    pub compatibility: HaxLibCompatibility,
68}
69
70/// The entries one member crate resolves differently from the workspace.
71#[derive_group(Serializers)]
72#[derive(Debug, Clone, JsonSchema, Hash, Eq, PartialEq)]
73pub struct MemberOverride {
74    #[serde(rename = "crate")]
75    pub crate_name: String,
76    pub tools: Vec<ToolResolution>,
77    pub versions: Vec<ToolResolution>,
78}
79
80/// One version of one tool, as `tools list` reports it.
81#[derive_group(Serializers)]
82#[derive(Debug, Clone, JsonSchema, Hash, Eq, PartialEq)]
83pub struct ToolVersionListing {
84    pub version: String,
85    pub installed: bool,
86    pub in_manifest: bool,
87    pub default: bool,
88    /// Whether the cached copy was checksum-verified at install time.
89    /// Meaningless unless `installed`.
90    pub verified: bool,
91}
92
93/// The versions of one tool, as `tools list` reports them.
94#[derive_group(Serializers)]
95#[derive(Debug, Clone, JsonSchema, Hash, Eq, PartialEq)]
96pub struct ToolListing {
97    pub tool: String,
98    pub versions: Vec<ToolVersionListing>,
99    /// How many versions were left out of `versions` as too old.
100    pub omitted: usize,
101}
102
103/// How one version came to be in the cache.
104#[derive_group(Serializers)]
105#[derive(Debug, Clone, Copy, JsonSchema, Hash, Eq, PartialEq)]
106pub enum InstallStatus {
107    /// Already in the cache, `verified` as recorded at install time.
108    Cached { verified: bool },
109    /// Freshly downloaded and installed.
110    Installed { verified: bool },
111}
112
113/// One tool version an `install` run accounted for.
114#[derive_group(Serializers)]
115#[derive(Debug, Clone, JsonSchema, Hash, Eq, PartialEq)]
116pub struct InstalledTool {
117    pub tool: String,
118    pub version: String,
119    pub status: InstallStatus,
120}
121
122/// One entry a `pin` run wrote into `hax.toml`.
123#[derive_group(Serializers)]
124#[derive(Debug, Clone, JsonSchema, Hash, Eq, PartialEq)]
125pub struct PinChange {
126    pub name: String,
127    pub version: String,
128    /// The version the entry pinned before, if it existed.
129    pub previous: Option<String>,
130}
131
132#[derive_group(Serializers)]
133#[derive(Debug, Clone, JsonSchema, Hash, Eq, PartialEq)]
134#[repr(u8)]
135pub enum HaxMessage {
136    Diagnostic {
137        diagnostic: super::Diagnostics,
138        working_dir: Option<PathBuf>,
139    } = 254,
140    BinaryNotFound {
141        binary_name: String,
142        env_var: String,
143        hint: Option<String>,
144    } = 0,
145    ProducedFile {
146        path: PathBuf,
147        wrote: bool,
148    } = 1,
149    HaxEngineFailure {
150        exit_code: i32,
151    } = 2,
152    CargoBuildFailure = 3,
153    WarnExperimentalBackend {
154        backend: Backend,
155    } = 4,
156    ProfilingData(crate::engine_api::ProfilingData) = 5,
157    Stats {
158        errors_per_item: Vec<(hax_frontend_exporter::DefId, usize)>,
159    } = 6,
160    GenericError {
161        message: String,
162    } = 7,
163    GenericWarning {
164        message: String,
165    } = 8,
166    Step {
167        verb: String,
168        target: String,
169    } = 9,
170    SubprocessOutput {
171        prefix: String,
172        line: String,
173    } = 10,
174    OutputTruncated {
175        prefix: String,
176        remaining: usize,
177        log_path: PathBuf,
178    } = 11,
179    UnsupportedOption {
180        option: String,
181        backend: BackendName,
182    } = 12,
183    HaxTomlWarning {
184        path: PathBuf,
185        message: String,
186    } = 13,
187    HaxTomlError {
188        path: PathBuf,
189        message: String,
190    } = 14,
191    MemberToolOverrides {
192        crate_name: String,
193        path: PathBuf,
194        entries: Vec<String>,
195    } = 15,
196    StrayHaxToml {
197        path: PathBuf,
198    } = 16,
199    UnverifiedInstall {
200        tool: String,
201        version: String,
202        url: String,
203    } = 17,
204    NonDefaultToolVersion {
205        tool: String,
206        used: String,
207        tested: String,
208    } = 18,
209    HaxLibIncompatible {
210        crate_name: String,
211        found: String,
212        binary: String,
213        expected: String,
214        newer: bool,
215    } = 19,
216    CachedUnverifiedToolInUse {
217        tool: String,
218        version: String,
219    } = 20,
220    /// The result of `cargo hax tools show`.
221    ToolsShow {
222        /// The workspace-wide resolution of each managed tool.
223        tools: Vec<ToolResolution>,
224        /// The workspace-wide resolution of each declared-only version.
225        versions: Vec<ToolResolution>,
226        /// Every crate with a direct `hax-lib` dependency.
227        hax_lib: Vec<HaxLibStatus>,
228        member_overrides: Vec<MemberOverride>,
229    } = 21,
230    /// The result of `cargo hax tools list`.
231    ToolsList {
232        tools: Vec<ToolListing>,
233        /// Whether the listing was restricted to cached versions, which is
234        /// what an empty listing means.
235        installed_only: bool,
236    } = 22,
237    /// The result of `cargo hax tools install`: the versions now in the
238    /// cache. Versions that failed to install are reported as errors of
239    /// their own and are absent here.
240    ToolsInstalled {
241        installed: Vec<InstalledTool>,
242    } = 23,
243    /// An existing generated Lean project file pins a version that
244    /// differs from the current resolution.
245    LakefilePinDrift {
246        path: PathBuf,
247        /// What is pinned: a lakefile `[[require]]` name, or `lean` for
248        /// the toolchain file.
249        name: String,
250        found: String,
251        expected: String,
252    } = 24,
253    /// The result of `cargo hax tools remove`: the version deleted from
254    /// the cache.
255    ToolRemoved {
256        tool: String,
257        version: String,
258    } = 25,
259    /// The result of `cargo hax tools clean`: how many cached tool
260    /// versions the deleted cache held.
261    ToolsCleaned {
262        removed: usize,
263    } = 26,
264    /// The result of `cargo hax tools pin`: the entries written into the
265    /// edited `hax.toml`, and the path-pinned ones left untouched. Empty
266    /// `changes` means the file was not written.
267    ToolsPinned {
268        path: PathBuf,
269        changes: Vec<PinChange>,
270        skipped: Vec<String>,
271    } = 27,
272    /// A file the root module of a generated Lean package should import
273    /// exists, but the root module does not import it.
274    RootModuleMissingImport {
275        path: PathBuf,
276        import: String,
277    } = 28,
278    /// The root module of a generated Lean package imports an extraction
279    /// file that no longer exists.
280    RootModuleStaleImport {
281        path: PathBuf,
282        import: String,
283    } = 29,
284    /// The resolved invocation of one proof scenario, as
285    /// `extract --dry-run` prints it.
286    ScenarioDryRun {
287        name: String,
288        package: String,
289        /// The resolved invocation, one display line per entry.
290        lines: Vec<String>,
291    } = 30,
292    /// The summary of an `extract` run.
293    ScenarioSummary {
294        total: usize,
295        failed: Vec<String>,
296    } = 31,
297}
298
299impl HaxMessage {
300    // https://doc.rust-lang.org/reference/items/enumerations.html#pointer-casting
301    pub fn discriminant(&self) -> u16 {
302        unsafe { *(self as *const Self as *const u16) }
303    }
304
305    pub fn code(&self) -> String {
306        match self {
307            HaxMessage::Diagnostic { diagnostic, .. } => diagnostic.kind.code(),
308            _ => format!("CARGOHAX{:0>4}", self.discriminant()),
309        }
310    }
311}
312
313/// Whether this process reported an error-severity message.
314/// [`HaxMessage::report`] sets it, and [`errors_reported`] exposes it: a
315/// reported error and a successful exit status must never combine, so an
316/// exit path with a zero code has to consult it.
317static ERROR_REPORTED: std::sync::atomic::AtomicBool = std::sync::atomic::AtomicBool::new(false);
318
319/// Whether an error-severity message was reported in this process.
320pub fn errors_reported() -> bool {
321    ERROR_REPORTED.load(std::sync::atomic::Ordering::Relaxed)
322}
323
324const ENGINE_BINARY_NAME: &str = "hax-engine";
325
326use annotate_snippets::{Level, Renderer};
327
328/// Render a warning with a `help` footer, the shape most warnings share.
329fn warn_with_help(renderer: &Renderer, title: &str, remedy: &str) -> String {
330    format!(
331        "{}",
332        renderer.render(
333            Level::Warning
334                .title(title)
335                .footer(Level::Help.title(remedy))
336        )
337    )
338}
339
340/// Make a path relative to the current directory for display, if possible.
341fn relative_to_cwd(path: PathBuf) -> PathBuf {
342    std::env::current_dir()
343        .ok()
344        .and_then(|current_dir| path.strip_prefix(current_dir).ok())
345        .map(|relative| PathBuf::from(".").join(relative))
346        .unwrap_or(path)
347}
348
349impl HaxMessage {
350    /// Whether this message reports an error, i.e. renders at error level.
351    /// Reporting one commits the process to a failing exit status. Kept
352    /// exhaustive so that a new variant forces a decision here, matching
353    /// the level [`Self::render_styled`] gives it.
354    pub fn is_error(&self) -> bool {
355        match self {
356            Self::Diagnostic { .. }
357            | Self::BinaryNotFound { .. }
358            | Self::HaxEngineFailure { .. }
359            | Self::GenericError { .. }
360            | Self::HaxTomlError { .. }
361            | Self::HaxLibIncompatible { .. } => true,
362            Self::ScenarioSummary { failed, .. } => !failed.is_empty(),
363            Self::ProducedFile { .. }
364            | Self::CargoBuildFailure
365            | Self::WarnExperimentalBackend { .. }
366            | Self::ProfilingData(..)
367            | Self::Stats { .. }
368            | Self::GenericWarning { .. }
369            | Self::Step { .. }
370            | Self::SubprocessOutput { .. }
371            | Self::OutputTruncated { .. }
372            | Self::UnsupportedOption { .. }
373            | Self::HaxTomlWarning { .. }
374            | Self::MemberToolOverrides { .. }
375            | Self::StrayHaxToml { .. }
376            | Self::UnverifiedInstall { .. }
377            | Self::NonDefaultToolVersion { .. }
378            | Self::CachedUnverifiedToolInUse { .. }
379            | Self::ToolsShow { .. }
380            | Self::ToolsList { .. }
381            | Self::ToolsInstalled { .. }
382            | Self::LakefilePinDrift { .. }
383            | Self::ToolRemoved { .. }
384            | Self::ToolsCleaned { .. }
385            | Self::ToolsPinned { .. }
386            | Self::RootModuleMissingImport { .. }
387            | Self::RootModuleStaleImport { .. }
388            | Self::ScenarioDryRun { .. } => false,
389        }
390    }
391
392    pub fn report(self, message_format: MessageFormat, rctx: Option<&mut ReportCtx>) {
393        if self.is_error() {
394            ERROR_REPORTED.store(true, std::sync::atomic::Ordering::Relaxed);
395        }
396        // A message that renders to nothing has nothing to print: a report
397        // of an empty listing must not become a blank line.
398        if let Some(rendered) = self.render(message_format, rctx)
399            && !rendered.is_empty()
400        {
401            println!("{rendered}")
402        }
403    }
404    pub fn report_styled(self, rctx: Option<&mut ReportCtx>) {
405        if self.is_error() {
406            ERROR_REPORTED.store(true, std::sync::atomic::Ordering::Relaxed);
407        }
408        println!("{}", self.render_styled(rctx))
409    }
410
411    pub fn render(
412        self,
413        message_format: MessageFormat,
414        mut rctx: Option<&mut ReportCtx>,
415    ) -> Option<String> {
416        if let (Some(r), HaxMessage::Diagnostic { diagnostic, .. }) = (rctx.as_mut(), &self)
417            && r.seen_already(diagnostic.clone())
418        {
419            return None;
420        }
421        Some(match message_format {
422            MessageFormat::Json => serde_json::to_string(&self).unwrap(),
423            MessageFormat::Human => self.render_styled(rctx),
424        })
425    }
426    pub fn render_styled(self, rctx: Option<&mut ReportCtx>) -> String {
427        let renderer = Renderer::styled();
428        match self {
429            Self::Diagnostic {
430                diagnostic,
431                working_dir,
432            } => {
433                let mut _rctx = None;
434                let rctx = rctx.unwrap_or_else(|| _rctx.get_or_insert(ReportCtx::default()));
435                diagnostic.with_message(
436                    rctx,
437                    working_dir.as_ref().map(PathBuf::as_path),
438                    Level::Error,
439                    |msg| format!("{}", renderer.render(msg)),
440                )
441            }
442            Self::BinaryNotFound {
443                binary_name,
444                env_var,
445                hint,
446            } => {
447                use colored::Colorize;
448                let mut message = format!(
449                    "hax: The binary [{}] was not found in your [PATH].\n\
450                     Please make sure it is installed and is in PATH!\n\
451                     Hint: set the [{}] environment variable to provide its path explicitly.",
452                    binary_name, env_var
453                );
454                if let Some(hint) = hint {
455                    message.push_str(&format!("\n{}", hint.bright_black()));
456                }
457                format!("{}", renderer.render(Level::Error.title(&message)))
458            }
459            Self::ProducedFile { path, wrote } => {
460                let path = relative_to_cwd(path);
461                let title = if wrote {
462                    format!("hax: wrote file {}", path.display())
463                } else {
464                    format!("hax: unchanged file {}", path.display())
465                };
466                format!("{}", renderer.render(Level::Info.title(&title)))
467            }
468            Self::HaxEngineFailure { exit_code } => {
469                let title = format!(
470                    "hax: {} exited with non-zero code {}",
471                    ENGINE_BINARY_NAME, exit_code,
472                );
473                format!("{}", renderer.render(Level::Error.title(&title)))
474            }
475            Self::ProfilingData(data) => {
476                fn format_with_dot(shift: u32, n: u64) -> String {
477                    let factor = 10u64.pow(shift);
478                    format!("{}.{}", n / factor, n % factor)
479                }
480                let title = format!(
481                    "hax[profiling]: {}: {}ms, memory={}, {} item{}{}",
482                    data.context,
483                    format_with_dot(6, data.time_ns),
484                    data.memory,
485                    data.quantity,
486                    if data.quantity > 1 { "s" } else { "" },
487                    if data.errored {
488                        " (note: this failed!)"
489                    } else {
490                        ""
491                    }
492                );
493                format!("{}", renderer.render(Level::Info.title(&title)))
494            }
495            Self::Stats { errors_per_item } => {
496                let success_items = errors_per_item.iter().filter(|(_, n)| *n == 0).count();
497                let total = errors_per_item.len();
498                let title = format!(
499                    "hax: {}/{} items were successfully translated ({}% success rate)",
500                    success_items,
501                    total,
502                    (success_items * 100) / total
503                );
504                format!("{}", renderer.render(Level::Info.title(&title)))
505            }
506            Self::CargoBuildFailure => {
507                let title =
508                    "hax: running `cargo build` was not successful, continuing anyway.".to_string();
509                format!("{}", renderer.render(Level::Warning.title(&title)))
510            }
511            Self::WarnExperimentalBackend { backend } => {
512                let title = format!(
513                    "hax: Experimental backend \"{}\" is work in progress.",
514                    backend
515                );
516                format!("{}", renderer.render(Level::Warning.title(&title)))
517            }
518            Self::GenericError { message } => {
519                let title = format!("hax: {}", message);
520                format!("{}", renderer.render(Level::Error.title(&title)))
521            }
522            Self::GenericWarning { message } => {
523                let title = format!("hax: {}", message);
524                format!("{}", renderer.render(Level::Warning.title(&title)))
525            }
526            Self::Step { verb, target } => {
527                use colored::Colorize;
528                format!("{:>12} {}", verb.bold().green(), target)
529            }
530            Self::SubprocessOutput { prefix, line } => {
531                format!("{:>12} > {}", prefix, line)
532            }
533            Self::OutputTruncated {
534                prefix,
535                remaining,
536                log_path,
537            } => {
538                format!(
539                    "{:>12} > ... ({} more lines, full output in {})",
540                    prefix,
541                    remaining,
542                    log_path.display()
543                )
544            }
545            Self::UnsupportedOption { option, backend } => {
546                let title = format!(
547                    "hax: option {} is not supported by the {} backend and will be ignored",
548                    option, backend
549                );
550                format!("{}", renderer.render(Level::Warning.title(&title)))
551            }
552            Self::HaxTomlWarning { path, message } => {
553                let title = format!("hax: {}: {}", path.display(), message);
554                format!("{}", renderer.render(Level::Warning.title(&title)))
555            }
556            Self::HaxTomlError { path, message } => {
557                let title = format!("hax: {}: {}", path.display(), message);
558                format!("{}", renderer.render(Level::Error.title(&title)))
559            }
560            Self::MemberToolOverrides {
561                crate_name,
562                path,
563                entries,
564            } => {
565                let title = format!(
566                    "hax: crate `{}` overrides the workspace tool configuration ({}) in {}. \
567                     Prefer a single workspace-wide pin where possible.",
568                    crate_name,
569                    entries.join(", "),
570                    path.display()
571                );
572                format!("{}", renderer.render(Level::Warning.title(&title)))
573            }
574            Self::HaxLibIncompatible {
575                crate_name,
576                found,
577                binary,
578                expected,
579                newer,
580            } => {
581                let remedy = if newer {
582                    format!(
583                        "update cargo-hax to the release matching hax-lib {found}, or pin\n\
584                         the `hax-lib` dependency to {expected} in Cargo.toml"
585                    )
586                } else {
587                    format!(
588                        "update the `hax-lib` dependency to {expected}, e.g. with\n\
589                         `cargo update -p hax-lib --precise {expected}`, or install cargo-hax {found}"
590                    )
591                };
592                let title = format!(
593                    "incompatible `hax-lib` version\n\n\
594                     this cargo-hax binary ({binary}) requires hax-lib {expected}\n\
595                     found hax-lib {found} in Cargo.lock (crate `{crate_name}`)\n\n\
596                     {remedy}"
597                );
598                format!("{}", renderer.render(Level::Error.title(&title)))
599            }
600            Self::NonDefaultToolVersion { tool, used, tested } => {
601                let title =
602                    format!("hax: using {tool} {used}; this hax release was tested with {tested}");
603                format!("{}", renderer.render(Level::Info.title(&title)))
604            }
605            Self::LakefilePinDrift {
606                path,
607                name,
608                found,
609                expected,
610            } => {
611                let path = relative_to_cwd(path);
612                let title = format!(
613                    "hax: {} pins {name} {found}; the current configuration expects {expected}",
614                    path.display()
615                );
616                let remedy = "update the pin, or delete the file and re-run to regenerate it";
617                warn_with_help(&renderer, &title, remedy)
618            }
619            Self::RootModuleMissingImport { path, import } => {
620                let path = relative_to_cwd(path);
621                let title = format!(
622                    "hax: {} does not import {import}, so `lake build` will not \
623                     check that file",
624                    path.display()
625                );
626                let remedy = format!(
627                    "add `import {import}`, or comment it out (`-- import {import}`) \
628                     to silence this warning"
629                );
630                warn_with_help(&renderer, &title, &remedy)
631            }
632            Self::RootModuleStaleImport { path, import } => {
633                let path = relative_to_cwd(path);
634                let title = format!(
635                    "hax: {} imports {import}, but the extraction no longer \
636                     produces that file",
637                    path.display()
638                );
639                let remedy = "remove or comment out the import line";
640                warn_with_help(&renderer, &title, remedy)
641            }
642            Self::UnverifiedInstall { tool, version, url } => {
643                let title = format!(
644                    "{tool} {version} is not in this release's manifest; \
645                     installing without checksum verification"
646                );
647                let source = format!("source {url}");
648                let remedy = format!(
649                    "once a checksum ships, run \
650                     `cargo hax tools install {tool}@{version} --force` to verify"
651                );
652                format!(
653                    "{}",
654                    renderer.render(
655                        Level::Warning
656                            .title(&title)
657                            .footer(Level::Note.title(&source))
658                            .footer(Level::Help.title(&remedy))
659                    )
660                )
661            }
662            Self::StrayHaxToml { path } => {
663                let title = format!(
664                    "hax: found {} outside the workspace root and member crate roots; \
665                     it has no effect and is ignored",
666                    path.display()
667                );
668                format!("{}", renderer.render(Level::Warning.title(&title)))
669            }
670            Self::CachedUnverifiedToolInUse { tool, version } => {
671                let title = format!(
672                    "using {tool} {version} from the cache; it was installed \
673                     without checksum verification"
674                );
675                let remedy = format!(
676                    "run `cargo hax tools install {tool}@{version} --force` to \
677                     re-download and verify it once a checksum ships"
678                );
679                warn_with_help(&renderer, &title, &remedy)
680            }
681            Self::ToolsShow {
682                tools,
683                versions,
684                hax_lib,
685                member_overrides,
686            } => render_tools_show(&tools, &versions, &hax_lib, &member_overrides),
687            Self::ToolsList {
688                tools,
689                installed_only,
690            } => render_tools_list(&tools, installed_only),
691            Self::ToolsInstalled { installed } => render_tools_installed(&installed),
692            Self::ToolRemoved { tool, version } => {
693                use colored::Colorize;
694                format!("{:>12} {tool} {version}", "Removed".bold().green())
695            }
696            Self::ToolsCleaned { removed } => {
697                use colored::Colorize;
698                let noun = if removed == 1 {
699                    "tool version"
700                } else {
701                    "tool versions"
702                };
703                format!("{:>12} {removed} {noun}", "Removed".bold().green())
704            }
705            Self::ToolsPinned {
706                path,
707                changes,
708                skipped,
709            } => render_tools_pinned(&path, &changes, &skipped),
710            Self::ScenarioDryRun {
711                name,
712                package,
713                lines,
714            } => {
715                let mut block = vec![format!("scenario `{name}` (package `{package}`):")];
716                block.extend(lines.iter().map(|line| format!("  {line}")));
717                block.join("\n")
718            }
719            Self::ScenarioSummary { total, failed } => {
720                let plural = |n: usize| if n == 1 { "" } else { "s" };
721                if failed.is_empty() {
722                    let title = format!("hax: {total} scenario{} extracted", plural(total));
723                    format!("{}", renderer.render(Level::Info.title(&title)))
724                } else {
725                    let title = format!(
726                        "hax: {} of {total} scenario{} failed: {}",
727                        failed.len(),
728                        plural(total),
729                        failed.join(", ")
730                    );
731                    format!("{}", renderer.render(Level::Error.title(&title)))
732                }
733            }
734        }
735    }
736}
737
738/// The name the `hax-lib` rows of `tools show` are labelled with.
739const HAX_LIB_ROW: &str = "hax-lib";
740
741/// One `  <name>  <value>  (<source>)` row of the `tools show` grid.
742fn resolution_rows(
743    entries: &[ToolResolution],
744    name_width: usize,
745    value_width: usize,
746) -> impl Iterator<Item = String> + '_ {
747    entries.iter().map(move |entry| {
748        format!(
749            "  {name:name_width$}  {value:value_width$}  ({source})",
750            name = entry.name,
751            value = entry.value(),
752            source = entry.source,
753        )
754    })
755}
756
757/// `tools show`: the resolutions of the project, section by section, with
758/// the name and value columns aligned across every section so the source
759/// annotations line up in a single grid.
760fn render_tools_show(
761    tools: &[ToolResolution],
762    versions: &[ToolResolution],
763    hax_lib: &[HaxLibStatus],
764    member_overrides: &[MemberOverride],
765) -> String {
766    let all = || {
767        tools.iter().chain(versions).chain(
768            member_overrides
769                .iter()
770                .flat_map(|member| member.tools.iter().chain(&member.versions)),
771        )
772    };
773    // The `hax-lib` rows share the grid too, so `hax-lib` reads as a named
774    // row rather than a bare version line.
775    let name_width = all()
776        .map(|entry| entry.name.len())
777        .chain(hax_lib.iter().map(|_| HAX_LIB_ROW.len()))
778        .max()
779        .unwrap_or(0);
780    let value_width = all()
781        .map(|entry| entry.value().len())
782        .chain(hax_lib.iter().map(|status| status.version.len()))
783        .max()
784        .unwrap_or(0);
785    let hax_lib_row = |status: &HaxLibStatus, annotation: String| {
786        format!(
787            "  {name:name_width$}  {value:value_width$}  ({annotation})",
788            name = HAX_LIB_ROW,
789            value = status.version,
790        )
791    };
792
793    let mut lines = vec!["tools:".to_string()];
794    lines.extend(resolution_rows(tools, name_width, value_width));
795    lines.push(String::new());
796    lines.push("versions:".to_string());
797    lines.extend(resolution_rows(versions, name_width, value_width));
798
799    // One version across the project (or a single crate) is one row; crates
800    // that disagree get one row each, naming the crate.
801    let uniform = hax_lib.iter().all(|status| {
802        (&status.version, status.compatibility) == (&hax_lib[0].version, hax_lib[0].compatibility)
803    });
804    match hax_lib {
805        [] => {}
806        [first, ..] => {
807            lines.push(String::new());
808            lines.push("libraries:".to_string());
809            if uniform {
810                lines.push(hax_lib_row(
811                    first,
812                    first.compatibility.describe().to_string(),
813                ));
814            } else {
815                lines.extend(hax_lib.iter().map(|status| {
816                    hax_lib_row(
817                        status,
818                        format!(
819                            "crate `{}`: {}",
820                            status.crate_name,
821                            status.compatibility.describe()
822                        ),
823                    )
824                }));
825            }
826        }
827    }
828
829    for member in member_overrides {
830        lines.push(String::new());
831        lines.push(format!("crate `{}` (overrides):", member.crate_name));
832        lines.extend(resolution_rows(&member.tools, name_width, value_width));
833        lines.extend(resolution_rows(&member.versions, name_width, value_width));
834    }
835    lines.join("\n")
836}
837
838/// `tools list`: one block per tool, each version annotated with what is
839/// known about it.
840fn render_tools_list(tools: &[ToolListing], installed_only: bool) -> String {
841    let mut blocks = Vec::new();
842    for listing in tools {
843        let mut lines = vec![format!("{}:", listing.tool)];
844        if listing.versions.is_empty() {
845            lines.push(format!(
846                "  ({})",
847                if installed_only {
848                    "none installed"
849                } else {
850                    "none"
851                }
852            ));
853        }
854        // Pad the version column so the markers line up.
855        let width = listing
856            .versions
857            .iter()
858            .map(|version| version.version.len())
859            .max()
860            .unwrap_or(0);
861        for version in &listing.versions {
862            let mut marks = Vec::new();
863            if version.default {
864                marks.push("default".to_string());
865            }
866            if version.installed {
867                marks.push("installed".to_string());
868                if !version.verified {
869                    marks.push("unverified".to_string());
870                }
871            }
872            if !version.in_manifest {
873                marks.push("not in manifest".to_string());
874            }
875            lines.push(if marks.is_empty() {
876                format!("  {}", version.version)
877            } else {
878                format!(
879                    "  {version:width$}  ({marks})",
880                    version = version.version,
881                    marks = marks.join(", ")
882                )
883            });
884        }
885        if listing.omitted > 0 {
886            lines.push(format!(
887                "  ... {} older versions omitted (use --all)",
888                listing.omitted
889            ));
890        }
891        blocks.push(lines.join("\n"));
892    }
893    blocks.join("\n\n")
894}
895
896/// `tools pin`: one Cargo-style line per skipped and per written entry,
897/// closed by the state of the file.
898fn render_tools_pinned(
899    path: &std::path::Path,
900    changes: &[PinChange],
901    skipped: &[String],
902) -> String {
903    use colored::Colorize;
904    let path = relative_to_cwd(path.to_path_buf());
905    let mut lines: Vec<String> = skipped
906        .iter()
907        .map(|name| {
908            format!(
909                "{:>12} {name} (pinned to a path)",
910                "Skipped".bold().yellow()
911            )
912        })
913        .chain(changes.iter().map(|change| {
914            let previous = match &change.previous {
915                Some(previous) => format!(" (was {previous})"),
916                None => String::new(),
917            };
918            format!(
919                "{:>12} {} {}{previous}",
920                "Pinned".bold().green(),
921                change.name,
922                change.version
923            )
924        }))
925        .collect();
926    lines.push(if !changes.is_empty() {
927        format!(
928            "{:>12} {} (run `cargo hax tools install` to pre-fetch)",
929            "Wrote".bold().green(),
930            path.display()
931        )
932    } else if !skipped.is_empty() {
933        format!("{:>12} {}", "Unchanged".bold().green(), path.display())
934    } else {
935        format!(
936            "{:>12} {} already pins these versions",
937            "Unchanged".bold().green(),
938            path.display()
939        )
940    });
941    lines.join("\n")
942}
943
944/// `tools install`: one Cargo-style line per version now in the cache.
945fn render_tools_installed(installed: &[InstalledTool]) -> String {
946    use colored::Colorize;
947    installed
948        .iter()
949        .map(|entry| {
950            let (verb, verified) = match entry.status {
951                InstallStatus::Cached { verified } => ("Cached", verified),
952                InstallStatus::Installed { verified } => ("Installed", verified),
953            };
954            let suffix = if verified { "" } else { " (unverified)" };
955            format!(
956                "{:>12} {} {}{}",
957                verb.bold().green(),
958                entry.tool,
959                entry.version,
960                suffix
961            )
962        })
963        .collect::<Vec<_>>()
964        .join("\n")
965}
966
967#[cfg(test)]
968mod tests {
969    use super::*;
970
971    #[test]
972    fn a_reported_error_must_not_exit_successfully() {
973        let warning = HaxMessage::GenericWarning {
974            message: "w".into(),
975        };
976        assert!(!warning.is_error());
977
978        let error = HaxMessage::GenericError {
979            message: "e".into(),
980        };
981        assert!(error.is_error());
982        error.report(MessageFormat::Json, None);
983        assert!(errors_reported());
984    }
985}
hax_types/diagnostics/message.rs

hax_types/diagnostics/
message.rs
