re-add support for --werr for cli and test servers

it's not yet supported for the lsp server, as that is a bit more
complicated. the main reason to fix this now is to fix the unit tests
which rely on --werr

src/ast/diagnostic.rs

@@ -457,6 +457,14 @@ impl Diagnostic {
  self
  }
 
+ pub fn kind(&self) -> ReportKind {
+ self.0.kind
+ }
+
+ pub fn span(&self) -> Span {
+ self.0.location
+ }
+
  /// Generate the [`ariadne::ReportBuilder`].
  pub fn into_ariadne(self, files: &Files) -> ReportBuilder<CharSpan> {
  // note that ariadne's report doesn't use the span end
@@ -477,10 +485,6 @@ impl Diagnostic {
  builder
  }
 
- pub fn span(&self) -> Span {
- self.0.location
- }
-
  pub fn into_lsp_diagnostic(
  &self,
  files: &Files,

src/main.rs

@@ -214,7 +214,7 @@ async fn run_cli(options: Options) -> ExitCode {
  return ExitCode::from(1);
  }
 
- let mut client = CliServer::new();
+ let mut client = CliServer::new(&options);
  let user_files: Vec<FileId> = options
  .files
  .iter()
@@ -333,15 +333,17 @@ pub async fn verify_files(
 pub(crate) fn verify_test(source: &str) -> (Result<bool, VerifyError>, servers::TestServer) {
  use ast::SourceFilePath;
 
- let mut server = servers::TestServer::new();
+ let mut options = Options::default();
+ options.werr = true;
+
+ let mut server = servers::TestServer::new(&options);
  let file_id = server
  .get_files_internal()
  .lock()
  .unwrap()
  .add(SourceFilePath::Builtin, source.to_owned())
  .id;
- let mut options = Options::default();
- options.werr = true;
+
  let options = Arc::new(options);
  let limits_ref = LimitsRef::new(None);
  let res = verify_files_main(&options, limits_ref, &mut server, &[file_id]);
@@ -352,15 +354,16 @@ pub(crate) fn verify_test(source: &str) -> (Result<bool, VerifyError>, servers::
 pub(crate) fn single_desugar_test(source: &str) -> Result<String, VerifyError> {
  use ast::SourceFilePath;
 
- let mut client = servers::TestServer::new();
+ let mut options = Options::default();
+ options.werr = true;
+
+ let mut client = servers::TestServer::new(&options);
  let file_id = client
  .get_files_internal()
  .lock()
  .unwrap()
  .add(SourceFilePath::Builtin, source.to_owned())
  .id;
- let mut options = Options::default();
- options.werr = true;
 
  let mut source_units: Vec<Item<SourceUnit>> =
  SourceUnit::parse(&client.get_file(file_id).unwrap(), options.raw)
@@ -371,6 +374,7 @@ pub(crate) fn single_desugar_test(source: &str) -> Result<String, VerifyError> {
  // 2. Resolving (and declaring) idents
  let mut tcx = TyCtx::new(TyKind::EUReal);
  let mut files = client.get_files_internal().lock().unwrap();
+ init_calculi(&mut files, &mut tcx);
  init_encodings(&mut files, &mut tcx);
  init_distributions(&mut files, &mut tcx);
  init_lists(&mut files, &mut tcx);
@@ -462,9 +466,7 @@ fn verify_files_main(
 
  let monotonicity_res = source_unit.check_monotonicity();
  if let Err(err) = monotonicity_res {
- server
- .add_diagnostic(err)
- .map_err(VerifyError::ServerError)?;
+ server.add_diagnostic(err)?;
  }
  }
 
@@ -473,9 +475,7 @@ fn verify_files_main(
  let source_unit = source_unit.enter();
  let jani_res = source_unit.write_to_jani_if_requested(options, &tcx);
  match jani_res {
- Err(VerifyError::Diagnostic(diagnostic)) => server
- .add_diagnostic(diagnostic)
- .map_err(VerifyError::ServerError)?,
+ Err(VerifyError::Diagnostic(diagnostic)) => server.add_diagnostic(diagnostic)?,
  Err(err) => Err(err)?,
  _ => (),
  }

src/servers/cli.rs

@@ -4,17 +4,22 @@ use std::{
  sync::{Arc, Mutex},
 };
 
-use crate::ast::{Diagnostic, FileId, Files, SourceFilePath, Span, StoredFile};
+use crate::{
+ ast::{Diagnostic, FileId, Files, SourceFilePath, Span, StoredFile},
+ Options, VerifyError,
+};
 
-use super::{Server, ServerError};
+use super::{unless_fatal_error, Server, ServerError};
 
 pub struct CliServer {
+ werr: bool,
  files: Arc<Mutex<Files>>,
 }
 
 impl CliServer {
- pub fn new() -> Self {
+ pub fn new(options: &Options) -> Self {
  CliServer {
+ werr: options.werr,
  files: Default::default(),
  }
  }
@@ -53,7 +58,8 @@ impl Server for CliServer {
  &self.files
  }
 
- fn add_diagnostic(&mut self, diagnostic: Diagnostic) -> Result<(), ServerError> {
+ fn add_diagnostic(&mut self, diagnostic: Diagnostic) -> Result<(), VerifyError> {
+ let diagnostic = unless_fatal_error(self.werr, diagnostic)?;
  let files = self.files.lock().unwrap();
  print_diagnostic(&files, diagnostic)?;
  Ok(())

src/servers/lsp.rs

@@ -96,10 +96,15 @@ impl LspServer {
  .id;
  drop(files);
  self.clear_all();
- verify(self, &[file_id])?;
+ let result = verify(self, &[file_id]);
+ let res = match &result {
+ Ok(_) => Response::new_ok(id, Value::Null),
+ Err(err) => Response::new_err(id, 0, format!("{}", err)),
+ };
  sender
- .send(Message::Response(Response::new_ok(id, Value::Null)))
+ .send(Message::Response(res))
  .map_err(|e| VerifyError::ServerError(e.into()))?;
+ result?;
  }
  }
  Message::Response(_) => todo!(),
@@ -239,9 +244,11 @@ impl Server for LspServer {
  &self.files
  }
 
- fn add_diagnostic(&mut self, diagnostic: Diagnostic) -> Result<(), ServerError> {
+ fn add_diagnostic(&mut self, diagnostic: Diagnostic) -> Result<(), VerifyError> {
+ // TODO: add --werr support
  self.diagnostics.push(diagnostic);
- self.publish_diagnostics()?;
+ self.publish_diagnostics()
+ .map_err(VerifyError::ServerError)?;
  Ok(())
  }
 

src/servers/mod.rs

@@ -3,13 +3,17 @@ use std::{
  sync::{Arc, Mutex},
 };
 
-use crate::ast::{Diagnostic, FileId, Files, Span, StoredFile};
+use crate::{
+ ast::{Diagnostic, FileId, Files, Span, StoredFile},
+ VerifyError,
+};
 
 mod cli;
 mod lsp;
 #[cfg(test)]
 mod test;
 
+use ariadne::ReportKind;
 pub use cli::CliServer;
 pub use lsp::LspServer;
 #[cfg(test)]
@@ -27,9 +31,18 @@ pub trait Server: Send {
 
  fn get_files_internal(&mut self) -> &Mutex<Files>;
 
- /// Add a new [`Diagnostic`].
- fn add_diagnostic(&mut self, diagnostic: Diagnostic) -> Result<(), ServerError>;
+ /// Add a new [`Diagnostic`]. Abort with a [`VerifyError::Diagnostic`] if
+ /// the diagnostic is fatal.
+ fn add_diagnostic(&mut self, diagnostic: Diagnostic) -> Result<(), VerifyError>;
 
  /// Send a verification status message to the client (a custom notification).
  fn set_verify_status(&mut self, span: Span, status: bool) -> Result<(), ServerError>;
 }
+
+fn unless_fatal_error(werr: bool, diagnostic: Diagnostic) -> Result<Diagnostic, VerifyError> {
+ if diagnostic.kind() == ReportKind::Error || werr {
+ Err(VerifyError::Diagnostic(diagnostic))
+ } else {
+ Ok(diagnostic)
+ }
+}

src/servers/test.rs

@@ -3,20 +3,25 @@ use std::{
  sync::{Arc, Mutex},
 };
 
-use crate::ast::{Diagnostic, FileId, Files, Span, StoredFile};
+use crate::{
+ ast::{Diagnostic, FileId, Files, Span, StoredFile},
+ Options, VerifyError,
+};
 
-use super::{Server, ServerError};
+use super::{unless_fatal_error, Server, ServerError};
 
 pub struct TestServer {
  pub files: Arc<Mutex<Files>>,
+ werr: bool,
  pub diagnostics: Vec<Diagnostic>,
  pub statuses: HashMap<Span, bool>,
 }
 
 impl TestServer {
- pub fn new() -> Self {
+ pub fn new(options: &Options) -> Self {
  TestServer {
  files: Default::default(),
+ werr: options.werr,
  diagnostics: Default::default(),
  statuses: Default::default(),
  }
@@ -36,8 +41,9 @@ impl Server for TestServer {
  &self.files
  }
 
- fn add_diagnostic(&mut self, diagnostic: Diagnostic) -> Result<(), ServerError> {
- self.diagnostics.push(diagnostic);
+ fn add_diagnostic(&mut self, diagnostic: Diagnostic) -> Result<(), VerifyError> {
+ self.diagnostics
+ .push(unless_fatal_error(self.werr, diagnostic)?);
  Ok(())
  }