Merge branch 'master' into fix-4823-general-traits-bug-extends

dafny-lang · Dec 27, 2023 · d9b6c7a · d9b6c7a
2 parents f319c0b + 968c13d
commit d9b6c7a
Show file tree

Hide file tree

Showing 36 changed files with 757 additions and 712 deletions.
diff --git 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!`)
 }
diff --git 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
@@ -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) {
+  }
+}
diff --git 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<DafnyRelatedInformation> 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
@@ -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<Option> FormatOptions => new Option[] {
     CommonOptionBag.Check,
     CommonOptionBag.FormatPrint,

diff --git a/Source/DafnyCore/Options/DafnyProject.cs b/Source/DafnyCore/Options/DafnyProject.cs
@@ -42,7 +42,7 @@ public class DafnyProject : IEquatable<DafnyProject> {
   public DafnyProject() {
   }
 
-  public static async Task<DafnyProject> Open(IFileSystem fileSystem, Uri uri) {
+  public static async Task<DafnyProject> Open(IFileSystem fileSystem, DafnyOptions dafnyOptions, Uri uri) {
 
     var emptyProject = new DafnyProject {
       Uri = uri
@@ -65,7 +65,8 @@ public static async Task<DafnyProject> 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/AuditCommand.cs b/Source/DafnyDriver/Commands/AuditCommand.cs
@@ -21,11 +21,11 @@ public static Command Create() {
       result.AddOption(option);
     }
 
-    DafnyCli.SetHandlerUsingDafnyOptionsContinuation(result, (options, _) => {
+    DafnyNewCli.SetHandlerUsingDafnyOptionsContinuation(result, (options, _) => {
       options.Compile = false;
       options.Verify = false;
       options.AuditProgram = true;
-      return CompilerDriver.RunCompiler(options);
+      return CompilerDriver.Run(options);
     });
     return result;
   }

diff --git a/Source/DafnyDriver/Commands/BuildCommand.cs b/Source/DafnyDriver/Commands/BuildCommand.cs
@@ -17,11 +17,11 @@ public static Command Create() {
                Concat(DafnyCommands.ResolverOptions)) {
       result.AddOption(option);
     }
-    DafnyCli.SetHandlerUsingDafnyOptionsContinuation(result, (options, _) => {
+    DafnyNewCli.SetHandlerUsingDafnyOptionsContinuation(result, (options, _) => {
       options.Compile = true;
       options.RunAfterCompile = false;
       options.ForceCompile = options.Get(BoogieOptionBag.NoVerify);
-      return CompilerDriver.RunCompiler(options);
+      return CompilerDriver.Run(options);
     });
     return result;
   }

diff --git a/Source/DafnyDriver/Commands/CoverageReportCommand.cs b/Source/DafnyDriver/Commands/CoverageReportCommand.cs
@@ -43,7 +43,7 @@ public static Command Create() {
       result.AddOption(option);
     }
 
-    DafnyCli.SetHandlerUsingDafnyOptionsContinuation(result, (options, _) => {
+    DafnyNewCli.SetHandlerUsingDafnyOptionsContinuation(result, (options, _) => {
       var coverageReporter = new CoverageReporter(options);
       coverageReporter.Merge(options.Get(ReportsArgument).ConvertAll(fileInfo => fileInfo.FullName),
         options.Get(OutDirArgument));