From 70b5f139f6ff9f3a3c3e9cd5e8e28cea871a083c Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 20 Dec 2023 18:46:25 +0100 Subject: [PATCH 1/5] Stop compilation when the project file has an error (#4904) ### Description - Stop compilation when the project file has an error, to prevent showing more errors that don't make sense - Allow the option `--use-basename-for-filename` to work in error coming from the project file - Use the previous update to check more output in `cli/projectFile/projectFile.dfy` ### How has this been tested? - Updated an existing test `Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/projectFile.dfy` By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt). --- Source/DafnyCore/Options/DafnyProject.cs | 5 +- Source/DafnyDriver/Commands/DafnyCli.cs | 102 ++++++++++-------- .../Workspace/ProjectManagerDatabase.cs | 4 +- .../cli/projectFile/broken/invalidValue.toml | 3 + .../LitTest/cli/projectFile/projectFile.dfy | 27 ++--- .../cli/projectFile/projectFile.dfy.expect | 7 ++ 6 files changed, 90 insertions(+), 58 deletions(-) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/broken/invalidValue.toml diff --git a/Source/DafnyCore/Options/DafnyProject.cs b/Source/DafnyCore/Options/DafnyProject.cs index 36d689a243..a3c127d344 100644 --- a/Source/DafnyCore/Options/DafnyProject.cs +++ b/Source/DafnyCore/Options/DafnyProject.cs @@ -42,7 +42,7 @@ public class DafnyProject : IEquatable { public DafnyProject() { } - public static async Task Open(IFileSystem fileSystem, Uri uri) { + public static async Task Open(IFileSystem fileSystem, DafnyOptions dafnyOptions, Uri uri) { var emptyProject = new DafnyProject { Uri = uri @@ -65,7 +65,8 @@ public static async Task Open(IFileSystem fileSystem, Uri uri) { match => $"({match.Groups[1].Value},{match.Groups[2].Value}): the property {match.Groups[3].Value} does not exist."); result = emptyProject; - result.Errors.Error(MessageSource.Parser, result.StartingToken, $"The Dafny project file {uri.LocalPath} contains the following errors: {newMessage}"); + var path = dafnyOptions.UseBaseNameForFileName ? Path.GetFileName(uri.LocalPath) : uri.LocalPath; + result.Errors.Error(MessageSource.Parser, result.StartingToken, $"The Dafny project file {path} contains the following errors: {newMessage}"); } if (Path.GetFileName(uri.LocalPath) != FileName) { diff --git a/Source/DafnyDriver/Commands/DafnyCli.cs b/Source/DafnyDriver/Commands/DafnyCli.cs index 40f074c411..3950ff1c80 100644 --- a/Source/DafnyDriver/Commands/DafnyCli.cs +++ b/Source/DafnyDriver/Commands/DafnyCli.cs @@ -135,6 +135,15 @@ async Task Handle(InvocationContext context) { var options = new Options(optionValues, new Dictionary()); dafnyOptions.Options = options; + foreach (var argument in command.Arguments) { + var result = context.ParseResult.FindResultFor(argument)?.GetValueOrDefault(); + if (result != null) { + options.Arguments[argument] = result; + } + } + + ProcessOption(context, CommonOptionBag.UseBaseFileName, dafnyOptions); + var singleFile = context.ParseResult.GetValueForArgument(DafnyCommands.FileArgument); if (singleFile != null) { if (!await ProcessFile(dafnyOptions, singleFile)) { @@ -152,48 +161,11 @@ async Task Handle(InvocationContext context) { } } - foreach (var argument in command.Arguments) { - var result = context.ParseResult.FindResultFor(argument)?.GetValueOrDefault(); - if (result != null) { - options.Arguments[argument] = result; - } - } - foreach (var option in command.Options) { - var result = context.ParseResult.FindResultFor(option); - object projectFileValue = null; - var hasProjectFileValue = dafnyOptions.DafnyProject?.TryGetValue(option, dafnyOptions.ErrorWriter, out projectFileValue) ?? false; - object value; - if (option.Arity.MaximumNumberOfValues <= 1) { - // If multiple values aren't allowed, CLI options take precedence over project file options - value = (result == null || Equals(result.Token, null)) && hasProjectFileValue - ? projectFileValue - : GetValueForOption(context.ParseResult, option); - } else { - // If multiple values ARE allowed, CLI options come after project file options - var elementType = option.ValueType.GetGenericArguments()[0]; - var valueAsList = (IList)Activator.CreateInstance(typeof(List<>).MakeGenericType(elementType))!; - if (hasProjectFileValue) { - foreach (var element in (IEnumerable)projectFileValue) { - valueAsList.Add(element); - } - } - if (result != null) { - foreach (var element in (IEnumerable)GetValueForOption(context.ParseResult, option)) { - valueAsList.Add(element); - } - } - - value = valueAsList; + if (option == CommonOptionBag.UseBaseFileName) { + continue; } - - options.OptionArguments[option] = value; - try { - dafnyOptions.ApplyBinding(option); - } catch (Exception e) { - context.ExitCode = (int)ExitValue.PREPROCESSING_ERROR; - dafnyOptions.Printer.ErrorWriteLine(dafnyOptions.OutputWriter, - $"Invalid value for option {option.Name}: {e.Message}"); + if (!ProcessOption(context, option, dafnyOptions)) { return; } } @@ -206,6 +178,48 @@ async Task Handle(InvocationContext context) { command.SetHandler(Handle); } + private static bool ProcessOption(InvocationContext context, Option option, DafnyOptions dafnyOptions) { + var options = dafnyOptions.Options; + var result = context.ParseResult.FindResultFor(option); + object projectFileValue = null; + var hasProjectFileValue = dafnyOptions.DafnyProject?.TryGetValue(option, dafnyOptions.ErrorWriter, out projectFileValue) ?? false; + object value; + if (option.Arity.MaximumNumberOfValues <= 1) { + // If multiple values aren't allowed, CLI options take precedence over project file options + value = (result == null || Equals(result.Token, null)) && hasProjectFileValue + ? projectFileValue + : GetValueForOption(context.ParseResult, option); + } else { + // If multiple values ARE allowed, CLI options come after project file options + var elementType = option.ValueType.GetGenericArguments()[0]; + var valueAsList = (IList)Activator.CreateInstance(typeof(List<>).MakeGenericType(elementType))!; + if (hasProjectFileValue) { + foreach (var element in (IEnumerable)projectFileValue) { + valueAsList.Add(element); + } + } + if (result != null) { + foreach (var element in (IEnumerable)GetValueForOption(context.ParseResult, option)) { + valueAsList.Add(element); + } + } + + value = valueAsList; + } + + options.OptionArguments[option] = value; + try { + dafnyOptions.ApplyBinding(option); + } catch (Exception e) { + context.ExitCode = (int)ExitValue.PREPROCESSING_ERROR; + dafnyOptions.Printer.ErrorWriteLine(dafnyOptions.OutputWriter, + $"Invalid value for option {option.Name}: {e.Message}"); + return false; + } + + return true; + } + private static async Task Execute(TextWriter outputWriter, TextWriter errorWriter, TextReader inputReader, string[] arguments, @@ -301,7 +315,8 @@ private static async Task ProcessFile(DafnyOptions dafnyOptions, FileInfo : singleFile.FullName; if (Path.GetExtension(singleFile.FullName) == ".toml") { if (dafnyOptions.DafnyProject != null) { - await dafnyOptions.ErrorWriter.WriteLineAsync($"Only one project file can be used at a time. Both {dafnyOptions.DafnyProject.Uri.LocalPath} and {filePathForErrors} were specified"); + var first = dafnyOptions.UseBaseNameForFileName ? Path.GetFileName(dafnyOptions.DafnyProject.Uri.LocalPath) : dafnyOptions.DafnyProject.Uri.LocalPath; + await dafnyOptions.ErrorWriter.WriteLineAsync($"Only one project file can be used at a time. Both {first} and {filePathForErrors} were specified"); return false; } @@ -309,7 +324,7 @@ private static async Task ProcessFile(DafnyOptions dafnyOptions, FileInfo await dafnyOptions.ErrorWriter.WriteLineAsync($"Error: file {filePathForErrors} not found"); return false; } - var projectFile = await DafnyProject.Open(OnDiskFileSystem.Instance, new Uri(singleFile.FullName)); + var projectFile = await DafnyProject.Open(OnDiskFileSystem.Instance, dafnyOptions, new Uri(singleFile.FullName)); if (projectFile == null) { return false; } @@ -325,6 +340,9 @@ private static async Task ProcessFile(DafnyOptions dafnyOptions, FileInfo projectFile.Validate(dafnyOptions.OutputWriter, AllOptions); dafnyOptions.DafnyProject = projectFile; + if (projectFile.Errors.HasErrors) { + return false; + } } else { dafnyOptions.CliRootSourceUris.Add(new Uri(singleFile.FullName)); } diff --git a/Source/DafnyLanguageServer/Workspace/ProjectManagerDatabase.cs b/Source/DafnyLanguageServer/Workspace/ProjectManagerDatabase.cs index 3f93daa598..6961ea2faf 100644 --- a/Source/DafnyLanguageServer/Workspace/ProjectManagerDatabase.cs +++ b/Source/DafnyLanguageServer/Workspace/ProjectManagerDatabase.cs @@ -180,7 +180,7 @@ public void CloseDocument(TextDocumentIdentifier documentId) { public async Task GetProject(Uri uri) { return uri.LocalPath.EndsWith(DafnyProject.FileName) - ? await DafnyProject.Open(fileSystem, uri) + ? await DafnyProject.Open(fileSystem, serverOptions, uri) : (await FindProjectFile(uri) ?? ImplicitProject(uri)); } @@ -228,7 +228,7 @@ public static DafnyProject ImplicitProject(Uri uri) { return Task.FromResult(null); } - return DafnyProject.Open(fileSystem, configFileUri); + return DafnyProject.Open(fileSystem, serverOptions, configFileUri); } public IEnumerable Managers => managersByProject.Values; diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/broken/invalidValue.toml b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/broken/invalidValue.toml new file mode 100644 index 0000000000..ceb2fff648 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/broken/invalidValue.toml @@ -0,0 +1,3 @@ +includes = ["../src/input.dfy"] +[options] +print-mode = NoIncludes diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/projectFile.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/projectFile.dfy index d9d6eeb077..78ac5afaf0 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/projectFile.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/projectFile.dfy @@ -1,37 +1,40 @@ +// Invalid value gives error and stops compilation +// RUN: ! %resolve --warn-shadowing=true %S/broken/invalidValue.toml 2> "%t" + // A project file can specify input files and configure options -// RUN: %baredafny resolve --show-snippets:false --use-basename-for-filename "%S/dfyconfig.toml" > "%t" +// RUN: %resolve "%S/dfyconfig.toml" >> "%t" // Test using a URL instead of a local file as a project file -// RUN: ! %baredafny resolve --show-snippets:false --use-basename-for-filename "https://github.com/dafny-lang/dafny/blob/master/dfyconfig.toml" +// RUN: ! %resolve "https://github.com/dafny-lang/dafny/blob/master/web.toml" 2>> %t // Test option override behavior -// RUN: %baredafny resolve --show-snippets:false --use-basename-for-filename "%S/dfyconfig.toml" --warn-shadowing=false >> "%t" +// RUN: %resolve "%S/dfyconfig.toml" --warn-shadowing=false >> "%t" // Test option with default override behavior -// RUN: ! %baredafny resolve --show-snippets:false --use-basename-for-filename "%S/dfyconfig.toml" --function-syntax=3 >> "%t" +// RUN: ! %resolve "%S/dfyconfig.toml" --function-syntax=3 >> "%t" // Multiple project files are not allowed -// RUN: ! %baredafny resolve --show-snippets:false --use-basename-for-filename "%S/dfyconfig.toml" "%S/broken/dfyconfig.toml" +// RUN: ! %resolve "%S/dfyconfig.toml" "%S/broken/dfyconfig.toml" 2>> %t // Project files may not contain unknown properties -// RUN: ! %baredafny resolve --show-snippets:false --use-basename-for-filename "%S/broken/dfyconfig.toml" +// RUN: ! %resolve "%S/broken/dfyconfig.toml" 2>> %t // Warn if file contains options that don't exist -// RUN: %baredafny resolve --show-snippets:false --use-basename-for-filename "%S/broken/invalidOption.toml" >> "%t" +// RUN: %resolve "%S/broken/invalidOption.toml" >> "%t" // Project files must be files on disk. -// RUN: ! %baredafny resolve --show-snippets:false --use-basename-for-filename "%S/doesNotExist/dfyconfig.toml" +// RUN: ! %resolve "%S/doesNotExist.toml" 2>> %t // Project file options must have the right type -// RUN: ! %baredafny resolve --show-snippets:false --use-basename-for-filename "%S/badTypes/dfyconfig.toml" 2>> "%t" +// RUN: ! %resolve "%S/badTypes/dfyconfig.toml" 2>> "%t" // A project file without includes will take all .dfy files as input -// RUN: %baredafny resolve --show-snippets:false --use-basename-for-filename "%S/noIncludes/dfyconfig.toml" >> "%t" +// RUN: %resolve "%S/noIncludes/dfyconfig.toml" >> "%t" // Files included by the project file and on the CLI, duplicate is ignored. -// RUN: %baredafny resolve --show-snippets:false --use-basename-for-filename "%S/dfyconfig.toml" "%S/src/input.dfy" >> "%t" +// RUN: %resolve "%S/dfyconfig.toml" "%S/src/input.dfy" >> "%t" // Files excluded by the project file and included on the CLI, are included -// RUN: ! %baredafny resolve --show-snippets:false --use-basename-for-filename "%S/dfyconfig.toml" "%S/src/excluded.dfy" >> "%t" +// RUN: ! %resolve "%S/dfyconfig.toml" "%S/src/excluded.dfy" >> "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/projectFile.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/projectFile.dfy.expect index 32b6fb8073..fa9810dc1a 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/projectFile.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/projectFile.dfy.expect @@ -1,14 +1,21 @@ +Error: The Dafny project file invalidValue.toml contains the following errors: (3,14) : error : Unexpected token `NoIncludes` for a value + input.dfy(6,8): Warning: Shadowed local-variable name: x Dafny program verifier did not attempt verification +Error: file web.toml not found Dafny program verifier did not attempt verification input.dfy(10,0): Error: a function cannot be declared 'ghost' (it is 'ghost' by default when using --function-syntax:3) 1 parse errors detected in input.dfy +Only one project file can be used at a time. Both dfyconfig.toml and dfyconfig.toml were specified +Error: The Dafny project file dfyconfig.toml contains the following errors: (1,1): the property includdddes does not exist. + Warning: only Dafny project files named dfyconfig.toml are recognised by the Dafny IDE. Warning: option 'does-not-exist' that was specified in the project file, is not a valid Dafny option. Dafny program verifier did not attempt verification +Error: file doesNotExist.toml not found Error: Could not parse value '3' for option 'warn-shadowing' that has type 'Boolean' input.dfy(6,8): Warning: Shadowed local-variable name: x moreInput.dfy(6,8): Warning: Shadowed local-variable name: x From 2c39c525c09d092575228e35b30c3470744a0f17 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 21 Dec 2023 12:45:36 +0100 Subject: [PATCH 2/5] Relax 'check-deep-tests' workflow to make CI incorrectly fail less often (#4909) ### Description The 'check-deep-tests' step of the CI worflow often fails because the nightly is somewhere in the process of running, but apparently not in the `in_progress state`. This change makes sure that check only fails if nightly actually failed ### How has this been tested? Careful code review By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt). --- .github/workflows/check-for-workflow-run.js | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/.github/workflows/check-for-workflow-run.js b/.github/workflows/check-for-workflow-run.js index e0a2ee1c76..1b0b3d8490 100644 --- a/.github/workflows/check-for-workflow-run.js +++ b/.github/workflows/check-for-workflow-run.js @@ -15,15 +15,16 @@ module.exports = async ({github, context, core, workflow_id, sha, ...config}) => // run for this SHA we see. const runFilterDesc = sha ? `${workflow_id} on ${sha}` : workflow_id for (const run of result.data.workflow_runs) { - if ((!sha || run.head_sha === sha) && run.status !== "in_progress") { - if (run.conclusion !== "success") { - core.setFailed(`Last run of ${runFilterDesc} did not succeed: ${run.html_url}`) - } else { + if ((!sha || run.head_sha === sha)) { + if (run.conclusion === "success") { // The SHA is fully tested, exit with success console.log(`Last run of ${runFilterDesc} succeeded: ${run.html_url}`) + return + } else if (run.status === "failure" || run.status === "timed_out") { + core.setFailed(`Last run of ${runFilterDesc} did not succeed: ${run.html_url}`) + return } - return } } - core.setFailed(`No runs of ${runFilterDesc} found!`) + core.setFailed(`No completed runs of ${runFilterDesc} found!`) } From e97ad27f56e686ceeb7babd9181700485592454f Mon Sep 17 00:00:00 2001 From: Alex Chew Date: Thu, 21 Dec 2023 21:38:59 -0800 Subject: [PATCH 3/5] chore: update publishing plugin for Java runtime (#4912) ### Description This PR updates the Java runtime Gradle configuration to use the latest version of the [Maven publishing plugin](https://github.com/gradle-nexus/publish-plugin/). ### How has this been tested? The updated plugin was used to publish the 4.4.0 Java runtime to Maven Central: https://central.sonatype.com/artifact/org.dafny/DafnyRuntime/4.4.0 By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt). --- Source/DafnyRuntime/DafnyRuntimeJava/build.gradle | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/build.gradle b/Source/DafnyRuntime/DafnyRuntimeJava/build.gradle index b493575ed9..628c434fbc 100644 --- a/Source/DafnyRuntime/DafnyRuntimeJava/build.gradle +++ b/Source/DafnyRuntime/DafnyRuntimeJava/build.gradle @@ -2,7 +2,7 @@ plugins { id 'java-library' id 'maven-publish' id 'signing' - id 'io.github.gradle-nexus.publish-plugin' version '1.1.0' + id 'io.github.gradle-nexus.publish-plugin' version '1.3.0' } repositories { @@ -97,4 +97,3 @@ nexusPublishing { } } } - From d3c05bb017fcbe6c0fff84292e80ac2aa31be8c5 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 22 Dec 2023 20:44:58 +0100 Subject: [PATCH 4/5] Split responsibilities around CLI into different classes (#4913) ### Changes - Split `DafnyCli` into `DafnyNewCli` and `DafnyBackwardsCompatibleCli`, where `DafnyNewCli` only supports the new CLI, and `DafnyBackwardsCompatibleCli` extends `DafnyNewCli` to also support the old CLI. `DafnyNewCli` has a main entry point `Task Execute(IConsole console, string[] arguments)` that will run the new Dafny CLI and return an exit value. It also has an entry point `SetHandlerUsingDafnyOptionsContinuation` which is used by all Dafny commands to configure their handler. - Move `GetDafnyFiles` from `DafnyCLI` to `CompilerDriver` - Move class `ConsoleErrorReporter` into its own file - Move class `NoExecutableBackend` into its own file ### How has this been tested? This is purely a refactoring that does not need tests By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt). --- Source/Dafny/Dafny.cs | 2 +- .../DafnyCore/Generic/ConsoleErrorReporter.cs | 70 +++ Source/DafnyCore/Generic/Reporting.cs | 68 --- Source/DafnyCore/Options/DafnyCommands.cs | 1 + Source/DafnyDriver/Commands/AuditCommand.cs | 4 +- Source/DafnyDriver/Commands/BuildCommand.cs | 4 +- .../Commands/CoverageReportCommand.cs | 2 +- Source/DafnyDriver/Commands/DafnyCli.cs | 555 ------------------ .../DafnyDriver/Commands/DeadCodeCommand.cs | 2 +- Source/DafnyDriver/Commands/DocCommand.cs | 2 +- Source/DafnyDriver/Commands/FormatCommand.cs | 4 +- .../Commands/GenerateTestsCommand.cs | 4 +- .../Commands/MeasureComplexityCommand.cs | 4 +- Source/DafnyDriver/Commands/ResolveCommand.cs | 4 +- Source/DafnyDriver/Commands/RunCommand.cs | 4 +- Source/DafnyDriver/Commands/ServerCommand.cs | 2 +- Source/DafnyDriver/Commands/TestCommand.cs | 4 +- .../DafnyDriver/Commands/TranslateCommand.cs | 4 +- Source/DafnyDriver/Commands/VerifyCommand.cs | 4 +- Source/DafnyDriver/CompilerDriver.cs | 211 +++++-- .../DafnyBackwardsCompatibleCli.cs | 101 ++++ Source/DafnyDriver/DafnyDoc.cs | 2 +- Source/DafnyDriver/DafnyNewCli.cs | 305 ++++++++++ Source/DafnyDriver/NoExecutableBackend.cs | 50 ++ Source/DafnyPipeline.Test/RelativePaths.cs | 2 +- Source/IntegrationTests/LitTests.cs | 2 +- Source/TestDafny/MultiBackendTest.cs | 2 +- 27 files changed, 716 insertions(+), 703 deletions(-) create mode 100644 Source/DafnyCore/Generic/ConsoleErrorReporter.cs delete mode 100644 Source/DafnyDriver/Commands/DafnyCli.cs create mode 100644 Source/DafnyDriver/DafnyBackwardsCompatibleCli.cs create mode 100644 Source/DafnyDriver/DafnyNewCli.cs create mode 100644 Source/DafnyDriver/NoExecutableBackend.cs diff --git a/Source/Dafny/Dafny.cs b/Source/Dafny/Dafny.cs index fb5b8d9f05..79aa51fb95 100644 --- a/Source/Dafny/Dafny.cs +++ b/Source/Dafny/Dafny.cs @@ -4,6 +4,6 @@ namespace Dafny; public class Dafny { public static int Main(string[] args) { - return DafnyCli.Main(args); + return DafnyBackwardsCompatibleCli.Main(args); } } diff --git a/Source/DafnyCore/Generic/ConsoleErrorReporter.cs b/Source/DafnyCore/Generic/ConsoleErrorReporter.cs new file mode 100644 index 0000000000..3739335ce5 --- /dev/null +++ b/Source/DafnyCore/Generic/ConsoleErrorReporter.cs @@ -0,0 +1,70 @@ +using System; +using System.IO; + +namespace Microsoft.Dafny; + +public class ConsoleErrorReporter : BatchErrorReporter { + private ConsoleColor ColorForLevel(ErrorLevel level) { + switch (level) { + case ErrorLevel.Error: + return ConsoleColor.Red; + case ErrorLevel.Warning: + return ConsoleColor.Yellow; + case ErrorLevel.Info: + return ConsoleColor.Green; + default: + throw new cce.UnreachableException(); + } + } + + protected override bool MessageCore(MessageSource source, ErrorLevel level, string errorId, IToken tok, string msg) { + if (base.MessageCore(source, level, errorId, tok, msg) && (Options is { PrintTooltips: true } || level != ErrorLevel.Info)) { + // Extra indent added to make it easier to distinguish multiline error messages for clients that rely on the CLI + msg = msg.Replace("\n", "\n "); + + ConsoleColor previousColor = Console.ForegroundColor; + if (Options.OutputWriter == Console.Out) { + Console.ForegroundColor = ColorForLevel(level); + } + var errorLine = ErrorToString(level, tok, msg); + while (tok is NestedToken nestedToken) { + tok = nestedToken.Inner; + if (tok.Filepath == nestedToken.Filepath && + tok.line == nestedToken.line && + tok.col == nestedToken.col) { + continue; + } + msg = nestedToken.Message ?? "[Related location]"; + errorLine += $" {msg} {tok.TokenToString(Options)}"; + } + + if (Options.Verbose && !String.IsNullOrEmpty(errorId) && errorId != "none") { + errorLine += " (ID: " + errorId + ")\n"; + var info = ErrorRegistry.GetDetail(errorId); + if (info != null) { + errorLine += info; // already ends with eol character + } + } else { + errorLine += "\n"; + } + + Options.OutputWriter.Write(errorLine); + + if (Options.Get(DafnyConsolePrinter.ShowSnippets) && tok.Uri != null) { + TextWriter tw = new StringWriter(); + new DafnyConsolePrinter(Options).WriteSourceCodeSnippet(tok.ToRange(), tw); + Options.OutputWriter.Write(tw.ToString()); + } + + if (Options.OutputWriter == Console.Out) { + Console.ForegroundColor = previousColor; + } + return true; + } + + return false; + } + + public ConsoleErrorReporter(DafnyOptions options) : base(options) { + } +} \ No newline at end of file diff --git a/Source/DafnyCore/Generic/Reporting.cs b/Source/DafnyCore/Generic/Reporting.cs index 65f16076d1..10f9128ae6 100644 --- a/Source/DafnyCore/Generic/Reporting.cs +++ b/Source/DafnyCore/Generic/Reporting.cs @@ -1,10 +1,8 @@ // Copyright by the contributors to the Dafny Project // SPDX-License-Identifier: MIT -using System; using System.Collections.Generic; using System.CommandLine; -using System.IO; using System.Linq; namespace Microsoft.Dafny { @@ -21,72 +19,6 @@ public record DafnyDiagnostic(string ErrorId, IToken Token, string Message, MessageSource Source, ErrorLevel Level, IReadOnlyList RelatedInformation); - public class ConsoleErrorReporter : BatchErrorReporter { - private ConsoleColor ColorForLevel(ErrorLevel level) { - switch (level) { - case ErrorLevel.Error: - return ConsoleColor.Red; - case ErrorLevel.Warning: - return ConsoleColor.Yellow; - case ErrorLevel.Info: - return ConsoleColor.Green; - default: - throw new cce.UnreachableException(); - } - } - - protected override bool MessageCore(MessageSource source, ErrorLevel level, string errorId, IToken tok, string msg) { - if (base.MessageCore(source, level, errorId, tok, msg) && (Options is { PrintTooltips: true } || level != ErrorLevel.Info)) { - // Extra indent added to make it easier to distinguish multiline error messages for clients that rely on the CLI - msg = msg.Replace("\n", "\n "); - - ConsoleColor previousColor = Console.ForegroundColor; - if (Options.OutputWriter == Console.Out) { - Console.ForegroundColor = ColorForLevel(level); - } - var errorLine = ErrorToString(level, tok, msg); - while (tok is NestedToken nestedToken) { - tok = nestedToken.Inner; - if (tok.Filepath == nestedToken.Filepath && - tok.line == nestedToken.line && - tok.col == nestedToken.col) { - continue; - } - msg = nestedToken.Message ?? "[Related location]"; - errorLine += $" {msg} {tok.TokenToString(Options)}"; - } - - if (Options.Verbose && !String.IsNullOrEmpty(errorId) && errorId != "none") { - errorLine += " (ID: " + errorId + ")\n"; - var info = ErrorRegistry.GetDetail(errorId); - if (info != null) { - errorLine += info; // already ends with eol character - } - } else { - errorLine += "\n"; - } - - Options.OutputWriter.Write(errorLine); - - if (Options.Get(DafnyConsolePrinter.ShowSnippets) && tok.Uri != null) { - TextWriter tw = new StringWriter(); - new DafnyConsolePrinter(Options).WriteSourceCodeSnippet(tok.ToRange(), tw); - Options.OutputWriter.Write(tw.ToString()); - } - - if (Options.OutputWriter == Console.Out) { - Console.ForegroundColor = previousColor; - } - return true; - } - - return false; - } - - public ConsoleErrorReporter(DafnyOptions options) : base(options) { - } - } - public class ErrorReporterSink : ErrorReporter { public ErrorReporterSink(DafnyOptions options) : base(options) { } diff --git a/Source/DafnyCore/Options/DafnyCommands.cs b/Source/DafnyCore/Options/DafnyCommands.cs index 364b83921a..9f7f771f86 100644 --- a/Source/DafnyCore/Options/DafnyCommands.cs +++ b/Source/DafnyCore/Options/DafnyCommands.cs @@ -17,6 +17,7 @@ static DafnyCommands() { return r.Tokens.Where(t => !string.IsNullOrEmpty(t.Value)).Select(t => new FileInfo(t.Value)).ToList(); }, false, "Dafny input files and/or a Dafny project file"); } + public static IEnumerable