From 1a8590bc37efe3c5cb835898da11dfd5b55d2437 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Philipp=20Schro=CC=88er?= Date: Fri, 10 May 2024 20:27:37 +0200 Subject: [PATCH] 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 | 12 ++++++++---- src/main.rs | 26 +++++++++++++------------- src/servers/cli.rs | 14 ++++++++++---- src/servers/lsp.rs | 15 +++++++++++---- src/servers/mod.rs | 19 ++++++++++++++++--- src/servers/test.rs | 16 +++++++++++----- 6 files changed, 69 insertions(+), 33 deletions(-) diff --git a/src/ast/diagnostic.rs b/src/ast/diagnostic.rs index bad847d..7a931c9 100644 --- a/src/ast/diagnostic.rs +++ b/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 { // 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, diff --git a/src/main.rs b/src/main.rs index a2edd20..5a2ed0d 100644 --- a/src/main.rs +++ b/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 = options .files .iter() @@ -333,15 +333,17 @@ pub async fn verify_files( pub(crate) fn verify_test(source: &str) -> (Result, 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, servers:: pub(crate) fn single_desugar_test(source: &str) -> Result { 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> = SourceUnit::parse(&client.get_file(file_id).unwrap(), options.raw) @@ -371,6 +374,7 @@ pub(crate) fn single_desugar_test(source: &str) -> Result { // 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)?, _ => (), } diff --git a/src/servers/cli.rs b/src/servers/cli.rs index e579768..5b93424 100644 --- a/src/servers/cli.rs +++ b/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>, } 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(()) diff --git a/src/servers/lsp.rs b/src/servers/lsp.rs index 094352a..db0a017 100644 --- a/src/servers/lsp.rs +++ b/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(()) } diff --git a/src/servers/mod.rs b/src/servers/mod.rs index 9744a60..8d416bb 100644 --- a/src/servers/mod.rs +++ b/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; - /// 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 { + if diagnostic.kind() == ReportKind::Error || werr { + Err(VerifyError::Diagnostic(diagnostic)) + } else { + Ok(diagnostic) + } +} diff --git a/src/servers/test.rs b/src/servers/test.rs index 532a9e3..c4afddd 100644 --- a/src/servers/test.rs +++ b/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>, + werr: bool, pub diagnostics: Vec, pub statuses: HashMap, } 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(()) }