Use /tracePO instead of /trace in the server

This removes the need for special treatment of test input (/trace includes
timings in the output, which are not suitable for tests. /tracePO does not)

3 files changed, 10 insertions, 13 deletions

diff --git a/Source/DafnyServer/Server.cs b/Source/DafnyServer/Server.cs
index 0a9ce599..e524a9a3 100644
--- a/Source/DafnyServer/Server.cs
+++ b/Source/DafnyServer/Server.cs
@@ -11,7 +11,6 @@ using Microsoft.Boogie;
 

 namespace Microsoft.Dafny {

   class Server {

-    private bool trace;

     private bool running;

 

     static void Main(string[] args) {

@@ -25,7 +24,6 @@ namespace Microsoft.Dafny {
       } else if (hasArg && File.Exists(arg)) {

         Console.WriteLine("# Reading from {0}", Path.GetFileName(arg));

         Console.SetIn(new StreamReader(arg, Encoding.UTF8));

-        server.trace = false;

         server.Loop();

       } else {

         server.Loop();

@@ -40,7 +38,6 @@ namespace Microsoft.Dafny {
     }

 

     public Server() {

-      this.trace = true;

       this.running = true;

       ExecutionEngine.printer = new DafnyConsolePrinter();

       SetupConsole();

@@ -86,7 +83,7 @@ namespace Microsoft.Dafny {
         if (verb == "verify") {

           ServerUtils.checkArgs(command, 0);

           var payload = ReadPayload();

-          VerificationTask.ReadTask(payload).Run(trace);

+          VerificationTask.ReadTask(payload).Run();

         } else if (verb == "quit") {

           ServerUtils.checkArgs(command, 0);

           Exit();

diff --git a/Source/DafnyServer/Utilities.cs b/Source/DafnyServer/Utilities.cs
index 3bc334b3..d6654ac1 100644
--- a/Source/DafnyServer/Utilities.cs
+++ b/Source/DafnyServer/Utilities.cs
@@ -43,18 +43,18 @@ namespace Microsoft.Dafny {
       }

     }

 

-    internal static void ApplyArgs(string[] args, bool trace) {

+    internal static void ApplyArgs(string[] args) {

       Dafny.DafnyOptions.Install(new Dafny.DafnyOptions());

       Dafny.DafnyOptions.O.ProverKillTime = 10;

 

       if (CommandLineOptions.Clo.Parse(args)) {

         // Dafny.DafnyOptions.O.ErrorTrace = 0; //FIXME

         // Dafny.DafnyOptions.O.ModelViewFile = "-";

-        DafnyOptions.O.PrintTooltips = true;

-        DafnyOptions.O.UnicodeOutput = true;

-        DafnyOptions.O.VerifySnapshots = 2;

-        DafnyOptions.O.VcsCores = Math.Max(1, System.Environment.ProcessorCount - 1);

-        DafnyOptions.O.Trace = trace;

+        DafnyOptions.O.VerifySnapshots = 2; // Use caching

+        DafnyOptions.O.VcsCores = Math.Max(1, System.Environment.ProcessorCount - 1); //FIXME

+        DafnyOptions.O.PrintTooltips = true; // Dump tooptips (ErrorLevel.Info) to stdout

+        DafnyOptions.O.UnicodeOutput = true; // Use pretty warning signs

+        DafnyOptions.O.TraceProofObligations = true; // Show which method is being verified, but don't show duration of verification

       } else {

         throw new ServerException("Invalid command line options");

       }

diff --git a/Source/DafnyServer/VerificationTask.cs b/Source/DafnyServer/VerificationTask.cs
index dbafc781..a00688b1 100644
--- a/Source/DafnyServer/VerificationTask.cs
+++ b/Source/DafnyServer/VerificationTask.cs
@@ -44,15 +44,15 @@ namespace Microsoft.Dafny {
         source = "method selftest() { assert true; }"

       };

       try {

-        task.Run(false);

+        task.Run();

         Interaction.EOM(Interaction.SUCCESS, null);

       } catch (Exception ex) {

         Interaction.EOM(Interaction.FAILURE, ex);

       }

     }

 

-    internal void Run(bool trace = true) {

-      ServerUtils.ApplyArgs(args, trace);

+    internal void Run() {

+      ServerUtils.ApplyArgs(args);

       new DafnyHelper(filename, ProgramSource).Verify();

     }

   }