Merge branch 'master' into issue-3962

dafny-lang · May 8, 2023 · 9113f09 · 9113f09
2 parents 46bd5ad + a478a64
commit 9113f09
Show file tree

Hide file tree

Showing 4 changed files with 19 additions and 12 deletions.
diff --git a/Source/DafnyCore/Compilers/Dafny/DafnyBackend.cs b/Source/DafnyCore/Compilers/Dafny/DafnyBackend.cs
@@ -45,7 +45,7 @@ public class DafnyBackend : ExecutableBackend {
  string targetFilename, ReadOnlyCollection<string> otherFileNames, object compilationResult, TextWriter outputWriter) {
  Contract.Requires(targetFilename != null || otherFileNames.Count == 0);
 
- return RunTargetDafnyProgram(targetFilename, outputWriter);
+ return RunTargetDafnyProgram(targetFilename, outputWriter, false);
  }
 
  public DafnyBackend(DafnyOptions options) : base(options) {

diff --git a/Source/DafnyCore/Compilers/ExecutableBackend.cs b/Source/DafnyCore/Compilers/ExecutableBackend.cs
@@ -116,7 +116,7 @@ public abstract class ExecutableBackend : Plugins.IExecutableBackend {
  SinglePassCompiler.WriteFromStream(rd, outputWriter);
  }
 
- protected bool RunTargetDafnyProgram(string targetFilename, TextWriter outputWriter) {
+ protected bool RunTargetDafnyProgram(string targetFilename, TextWriter outputWriter, bool verify) {
 
  /*
  * In order to work for the continuous integration, we need to call the Dafny compiler using dotnet
@@ -128,15 +128,17 @@ public abstract class ExecutableBackend : Plugins.IExecutableBackend {
  var dafny = where + "/Dafny.dll";
 
  var opt = Options;
- var psi = PrepareProcessStartInfo("dotnet", opt.MainArgs
- .Prepend("/compileTarget:cs")
- .Prepend("/compile:4")
- .Prepend("/compileVerbose:0")
- .Prepend("/printVerifiedProceduresCount:0")
- .Prepend("/noVerify")
- .Prepend(targetFilename)
- .Prepend(dafny));
-
+ var args = opt.MainArgs
+ .Prepend(targetFilename);
+ if (!verify) {
+ args = args.Prepend("--no-verify");
+ }
+ args = args
+ .Prepend("--target:cs")
+ .Prepend("run")
+ .Prepend(dafny);
+ var psi = PrepareProcessStartInfo("dotnet", args);
+ Console.Out.WriteLine(string.Join(", ", psi.ArgumentList));
  /*
  * When this code was written, the Dafny compiler cannot be made completely silent.
  * This is a problem for this specific compiler and the integration tests because the second

diff --git a/Source/DafnyCore/Compilers/Library/LibraryBackend.cs b/Source/DafnyCore/Compilers/Library/LibraryBackend.cs
@@ -83,6 +83,6 @@ public class LibraryBackend : ExecutableBackend {
  ReadOnlyCollection<string> otherFileNames, object compilationResult, TextWriter outputWriter) {
 
  var dooPath = DooFilePath(dafnyProgramName);
- return RunTargetDafnyProgram(dooPath, outputWriter);
+ return RunTargetDafnyProgram(dooPath, outputWriter, true);
  }
 }
diff --git a/Source/DafnyCore/DooFile.cs b/Source/DafnyCore/DooFile.cs
@@ -113,6 +113,11 @@ public class ManifestData {
  }
 
  public bool Validate(string filePath, DafnyOptions options, Command currentCommand) {
+ if (currentCommand == null) {
+ options.Printer.ErrorWriteLine(Console.Out, $"Cannot load {filePath}: .doo files cannot be used with the legacy CLI");
+ return false;
+ }
+
  if (options.VersionNumber != Manifest.DafnyVersion) {
  options.Printer.ErrorWriteLine(Console.Out, $"Cannot load {filePath}: it was built with Dafny {Manifest.DafnyVersion}, which cannot be used by Dafny {options.VersionNumber}");
  return false;