Enable passing a percentage as a value for --cores

Source/DafnyCore/Options/BoogieOptionBag.cs

@@ -1,6 +1,8 @@
+using System;
 using System.Collections.Generic;
 using System.CommandLine;
 using System.Linq;
+using System.Transactions;
 using Microsoft.Boogie;
 
 namespace Microsoft.Dafny;
@@ -17,8 +19,34 @@ public static class BoogieOptionBag {
     ArgumentHelpName = "arguments",
   };
 
-  public static readonly Option<uint> Cores = new("--cores", () => 0,
-    "Run the Dafny CLI using <n> cores. Specifying 0 will use half of the available processor cores.") {
+  public static readonly Option<uint> Cores = new("--cores", result => {
+    if (result.Tokens.Count != 1) {
+      result.ErrorMessage = $"Expected only one value for option {Cores.Name}";
+      return 1;
+    }
+
+    var value = result.Tokens[0].Value;
+    if (value.EndsWith('%')) {
+      if (double.TryParse(value.Substring(0, value.Length - 1), out var percentage)) {
+        return Math.Max(1U, (uint)(percentage / 100.0 * Environment.ProcessorCount));
+      }
+
+      result.ErrorMessage = $"Could not parse percentage {value}";
+      return 1;
+    }
+
+    if (uint.TryParse(value, out var number)) {
+      if (number > 0) {
+        return number;
+      }
+
+      result.ErrorMessage = $"Number of cores to use must be greater than 0";
+      return 1;
+    }
+    result.ErrorMessage = $"Could not parse number {value}";
+    return 1;
+  }, true,
+    "Run the Dafny verifier using <n> cores, or using <XX%> of the machine's logical cores.") {
     ArgumentHelpName = "count"
   };
 
@@ -33,6 +61,8 @@ public static class BoogieOptionBag {
   };
 
   static BoogieOptionBag() {
+    Cores.SetDefaultValue((uint)((Environment.ProcessorCount + 1) / 2));
+
     DafnyOptions.RegisterLegacyBinding(BoogieFilter, (o, f) => o.ProcsToCheck.AddRange(f));
     DafnyOptions.RegisterLegacyBinding(BoogieArguments, (o, boogieOptions) => {
 

Source/XUnitExtensions/Lit/LitCommandWithRedirection.cs

@@ -38,6 +38,12 @@ public static LitCommandWithRedirection Parse(string[] tokens, LitTestConfigurat
         errorFile = config.ApplySubstitutions(argumentsList[redirectErrorIndex + 1]).Single();
         argumentsList.RemoveRange(redirectErrorIndex, 2);
       }
+      var redirectErrorAppendIndex = argumentsList.IndexOf("2>>");
+      if (redirectErrorAppendIndex >= 0) {
+        errorFile = config.ApplySubstitutions(argumentsList[redirectErrorAppendIndex + 1]).Single();
+        appendOutput = true;
+        argumentsList.RemoveRange(redirectErrorAppendIndex, 2);
+      }
 
       var arguments = argumentsList.SelectMany(config.ApplySubstitutions);
 
@@ -69,7 +75,7 @@ public LitCommandWithRedirection(ILitCommand command, string? inputFile, string?
     public (int, string, string) Execute(ITestOutputHelper? outputHelper, TextReader? inReader, TextWriter? outWriter, TextWriter? errWriter) {
       var inputReader = inputFile != null ? new StreamReader(inputFile) : null;
       var outputWriter = outputFile != null ? new StreamWriter(outputFile, append) : null;
-      var errorWriter = errorFile != null ? new StreamWriter(errorFile, false) : null;
+      var errorWriter = errorFile != null ? new StreamWriter(errorFile, append) : null;
       var result = command.Execute(outputHelper, inputReader, outputWriter, errorWriter);
       inputReader?.Close();
       outputWriter?.Close();
@@ -95,4 +101,4 @@ public override string ToString() {
       return builder.ToString();
     }
   }
-}
+}

Test/cli/zeroCores.dfy

@@ -1,4 +1,10 @@
-// RUN: ! %baredafny verify --use-basename-for-filename --cores=0 "%s" > "%t"
+// RUN: ! %baredafny verify --use-basename-for-filename --cores=0 "%s" 2> "%t"
+// RUN: ! %baredafny verify --use-basename-for-filename --cores=earga "%s" 2>> "%t"
+// RUN: ! %baredafny verify --use-basename-for-filename --cores=earga% "%s" 2>> "%t"
+// RUN: ! %baredafny verify --use-basename-for-filename "%s" >> "%t"
+// RUN: ! %baredafny verify --use-basename-for-filename --cores=1 "%s" >> "%t"
+// RUN: ! %baredafny verify --use-basename-for-filename --cores=0% "%s" >> "%t"
+// RUN: ! %baredafny verify --use-basename-for-filename --cores=50% "%s" >> "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method Foo() ensures false {

Test/cli/zeroCores.dfy.expect

@@ -1,4 +1,22 @@
-zeroCores.dfy(4,27): Error: A postcondition might not hold on this return path.
-zeroCores.dfy(4,21): Related location: This is the postcondition that might not hold.
+Number of cores to use must be greater than 0
+
+Could not parse number earga
+
+Could not parse percentage earga%
+
+zeroCores.dfy(10,27): Error: A postcondition might not hold on this return path.
+zeroCores.dfy(10,21): Related location: This is the postcondition that might not hold.
+
+Dafny program verifier finished with 0 verified, 1 error
+zeroCores.dfy(10,27): Error: A postcondition might not hold on this return path.
+zeroCores.dfy(10,21): Related location: This is the postcondition that might not hold.
+
+Dafny program verifier finished with 0 verified, 1 error
+zeroCores.dfy(10,27): Error: A postcondition might not hold on this return path.
+zeroCores.dfy(10,21): Related location: This is the postcondition that might not hold.
+
+Dafny program verifier finished with 0 verified, 1 error
+zeroCores.dfy(10,27): Error: A postcondition might not hold on this return path.
+zeroCores.dfy(10,21): Related location: This is the postcondition that might not hold.
 
 Dafny program verifier finished with 0 verified, 1 error

docs/dev/news/3328.feat

@@ -0,0 +1 @@
+Enable passing a percentage value to the --cores option, to use a percentage of the total number of logical cores on the machine for verification.