Skip to content

Commit 51b758b

Browse files
authored
Add a note on the style for diagnostic output (rust-lang#2198)
Some contributors are already following this guide regarding diagnostic output style, but this isn't mentioned anywhere. This PR is more of a proposal to officially adopt these style guidelines. It adds a sentence noting this and linking to the guide itself.
1 parent a7adb0b commit 51b758b

File tree

2 files changed

+14
-1
lines changed

2 files changed

+14
-1
lines changed

docs/src/conventions.md

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -70,11 +70,15 @@ Make sure to add user-friendly errors for constructs that we can't handle.
7070
For example, Kani cannot handle the panic unwind strategy, and it will fail compilation if the crate uses this
7171
configuration.
7272

73+
In general, it's preferred that error messages follow [these guidelines](https://rustc-dev-guide.rust-lang.org/diagnostics.html#diagnostic-output-style-guide) used for `rustc` development.
74+
If the errors are being emitted from `kani-compiler`, you should use the compiler error message utilities (e.g., the `Session::span_err` method). However, if the
75+
errors are being emitted from `kani-driver`, you should use the functions provided in the `util` module in `kani-driver`.
76+
7377
### Internal compiler errors
7478

7579
Even though this doesn't provide users the best experience, you are encouraged to add checks in the compiler for any
7680
assumptions you make during development.
77-
Those check can be on the form of `assert!()` or `unreachable!()`
81+
Those checks can be on the form of `assert!()` or `unreachable!()`
7882
statement.
7983
Please provide a meaningful message to help user understand why something failed, and try to explain, at least with
8084
a comment, why this is the case.

kani-driver/src/util.rs

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,15 @@
11
// Copyright Kani Contributors
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33

4+
//! Module that provides functions which are convenient for different purposes.
5+
//!
6+
//! In particular, the `warning` and `error` functions must be used for
7+
//! diagnostic output across the `kani-driver` components. Please follow the
8+
//! recommendations in <https://model-checking.github.io/kani/conventions.html>
9+
//! when reporting any kind of diagnostic for users. Note that it's recommended
10+
//! to use the Rust compiler's error message utilities if you're working on the
11+
//! `kani-compiler`.
12+
413
use std::ffi::OsString;
514
use std::path::{Path, PathBuf};
615
use std::process::Command;

0 commit comments

Comments
 (0)