--show-snippets with default true and off in tests

Source/DafnyCore/DafnyConsolePrinter.cs

@@ -66,7 +66,7 @@ public void WriteSourceCodeSnippet(Boogie.IToken tok, TextWriter tw) {
     tw.WriteLine("");
   }
 
-  public static readonly Option<bool> ShowSnippets = new("--show-snippets",
+  public static readonly Option<bool> ShowSnippets = new("--show-snippets", () => true,
     "Show a source code snippet for each Dafny message.");
 
   static DafnyConsolePrinter() {

Source/DafnyCore/Generic/Reporting.cs

@@ -240,7 +240,7 @@ public override bool Message(MessageSource source, ErrorLevel level, string erro
           errorLine += "\n";
         }
 
-        if (Options.Get(DafnyConsolePrinter.ShowSnippets)) {
+        if (Options.Get(DafnyConsolePrinter.ShowSnippets) && tok != Token.NoToken) {
           TextWriter tw = new StringWriter();
           new DafnyConsolePrinter(Options).WriteSourceCodeSnippet(tok.ToRange(), tw);
           Options.OutputWriter.Write(tw.ToString());

Source/DafnyDriver/DafnyDriver.cs

@@ -83,7 +83,10 @@ static DafnyDriver() {
       "/compileVerbose:0",
 
       // Set a default time limit, to catch cases where verification time runs off the rails
-      "/timeLimit:300"
+      "/timeLimit:300",
+
+      // test results do not include source code snippets
+      "/showSnippets:0"
     };
 
     public static readonly string[] NewDefaultArgumentsForTesting = new[] {
@@ -94,7 +97,10 @@ static DafnyDriver() {
       "--use-basename-for-filename",
 
       // Set a default time limit, to catch cases where verification time runs off the rails
-      "--verification-time-limit=300"
+      "--verification-time-limit=300",
+
+      // test results do not include source code snippets
+      "--show-snippets:false"
     };
 
     public static int Main(string[] args) {

Source/IntegrationTests/LitTests.cs

@@ -57,15 +57,15 @@ IEnumerable<string> AddExtraArgs(IEnumerable<string> args, IEnumerable<string> l
         return (extraDafnyArguments is null ? args : args.Append(extraDafnyArguments)).Concat(local);
       }
 
-      string[] defaultResolveArgs = new[] { "resolve", "--use-basename-for-filename" };
-      string[] defaultVerifyArgs = new[] { "verify", "--use-basename-for-filename", "--cores:2", "--verification-time-limit:300" };
+      string[] defaultResolveArgs = new[] { "resolve", "--use-basename-for-filename", "--show-snippets:false" };
+      string[] defaultVerifyArgs = new[] { "verify", "--use-basename-for-filename", "--show-snippets:false", "--cores:2", "--verification-time-limit:300" };
       //string[] defaultTranslateArgs = new[] { "translate", "--use-basename-for-filename", "--cores:2", "--verification-time-limit:300" };
-      string[] defaultBuildArgs = new[] { "build", "--use-basename-for-filename", "--cores:2", "--verification-time-limit:300" };
-      string[] defaultRunArgs = new[] { "run", "--use-basename-for-filename", "--cores:2", "--verification-time-limit:300" };
+      string[] defaultBuildArgs = new[] { "build", "--use-basename-for-filename", "--show-snippets:false", "--cores:2", "--verification-time-limit:300" };
+      string[] defaultRunArgs = new[] { "run", "--use-basename-for-filename", "--show-snippets:false", "--cores:2", "--verification-time-limit:300" };
 
       var substitutions = new Dictionary<string, object> {
         { "%diff", "diff" },
-        { "%trargs", "--use-basename-for-filename --cores:2 --verification-time-limit:300" },
+        { "%trargs", "--use-basename-for-filename --show-snippets:false --cores:2 --verification-time-limit:300" },
         { "%binaryDir", "." },
         { "%z3", Path.Join("z3", "bin", $"z3-{DafnyOptions.DefaultZ3Version}") },
         { "%repositoryRoot", RepositoryRoot.Replace(@"\", "/") },

Test/cli/projectFile/dfyconfig.toml

@@ -2,4 +2,5 @@ includes = ["src/**/*"]
 excludes = ["**/excluded.dfy"]
 
 [options]
-warn-shadowing = true
+warn-shadowing = true
+show-snippets = false

Test/cli/projectFile/projectFile.dfy

@@ -1,34 +1,34 @@
 // A project file can specify input files and configure options
-// RUN: %baredafny resolve --use-basename-for-filename "%S/dfyconfig.toml" > "%t"
+// RUN: %baredafny resolve --show-snippets:false --use-basename-for-filename "%S/dfyconfig.toml" > "%t"
 
 // Test using a URL instead of a local file as a project file
-// RUN: ! %baredafny resolve --use-basename-for-filename "https://github.com/dafny-lang/dafny/blob/master/dfyconfig.toml"
+// RUN: ! %baredafny resolve --show-snippets:false --use-basename-for-filename "https://github.com/dafny-lang/dafny/blob/master/dfyconfig.toml"
 
 // Test option override behavior
-// RUN: %baredafny resolve --use-basename-for-filename "%S/dfyconfig.toml" --warn-shadowing=false >> "%t"
+// RUN: %baredafny resolve --show-snippets:false --use-basename-for-filename "%S/dfyconfig.toml" --warn-shadowing=false >> "%t"
 
 // Multiple project files are not allowed
-// RUN: ! %baredafny resolve --use-basename-for-filename "%S/dfyconfig.toml" "%S/broken/dfyconfig.toml"
+// RUN: ! %baredafny resolve --show-snippets:false --use-basename-for-filename "%S/dfyconfig.toml" "%S/broken/dfyconfig.toml"
 
 // Project files may not contain unknown properties
-// RUN: ! %baredafny resolve --use-basename-for-filename "%S/broken/dfyconfig.toml"
+// RUN: ! %baredafny resolve --show-snippets:false --use-basename-for-filename "%S/broken/dfyconfig.toml"
 
 // Warn if file contains options that don't exist
-// RUN: %baredafny resolve --use-basename-for-filename "%S/broken/invalidOption.toml" >> "%t"
+// RUN: %baredafny resolve --show-snippets:false --use-basename-for-filename "%S/broken/invalidOption.toml" >> "%t"
 
 // Project files must be files on disk.
-// RUN: ! %baredafny resolve --use-basename-for-filename "%S/doesNotExist/dfyconfig.toml"
+// RUN: ! %baredafny resolve --show-snippets:false --use-basename-for-filename "%S/doesNotExist/dfyconfig.toml"
 
 // Project file options must have the right type
-// RUN: ! %baredafny resolve --use-basename-for-filename "%S/badTypes/dfyconfig.toml" 2>> "%t"
+// RUN: ! %baredafny resolve --show-snippets:false --use-basename-for-filename "%S/badTypes/dfyconfig.toml" 2>> "%t"
 
 // A project file without includes will take all .dfy files as input
-// RUN: %baredafny resolve --use-basename-for-filename "%S/noIncludes/dfyconfig.toml" >> "%t"
+// RUN: %baredafny resolve --show-snippets:false --use-basename-for-filename "%S/noIncludes/dfyconfig.toml" >> "%t"
 
 // Files included by the project file and on the CLI, duplicate is ignored.
-// RUN: %baredafny resolve --use-basename-for-filename "%S/dfyconfig.toml" "%S/src/input.dfy" >> "%t"
+// RUN: %baredafny resolve --show-snippets:false --use-basename-for-filename "%S/dfyconfig.toml" "%S/src/input.dfy" >> "%t"
 
 // Files excluded by the project file and included on the CLI, are included
-// RUN: ! %baredafny resolve --use-basename-for-filename "%S/dfyconfig.toml" "%S/src/excluded.dfy" >> "%t"
+// RUN: ! %baredafny resolve --show-snippets:false --use-basename-for-filename "%S/dfyconfig.toml" "%S/src/excluded.dfy" >> "%t"
 
-// RUN: %diff "%s.expect" "%t"
+// RUN: %diff "%s.expect" "%t"

Test/cli/zeroCores.dfy

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

Test/dafny0/Stdin.dfy

@@ -1,4 +1,4 @@
-// RUN: %exits-with 0 %stdin "module A{}" %baredafny verify --stdin > "%t"
-// RUN: %exits-with 4 %stdin "method a() { assert false; }" %baredafny verify --stdin >> "%t"
+// RUN: %exits-with 0 %stdin "module A{}" %baredafny verify --show-snippets:false --stdin > "%t"
+// RUN: %exits-with 4 %stdin "method a() { assert false; }" %baredafny verify --show-snippets:false --stdin >> "%t"
 // RUN: %diff "%s.expect" "%t"
 

Test/dafny4/parse-errors.dfy

@@ -1,4 +1,4 @@
-// RUN: ! %baredafny resolve --use-basename-for-filename "%s" > "%t"
+// RUN: ! %baredafny resolve --show-snippets:false --use-basename-for-filename "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 datatype D = B | CCC | E { predicate IsFailure() { E? } function PropagateFailure(): D { E } }

Test/dafny4/parse-errors2.dfy

@@ -1,4 +1,4 @@
-// RUN: ! %baredafny resolve --use-basename-for-filename "%s" > "%t"
+// RUN: ! %baredafny resolve --use-basename-for-filename --show-snippets:false "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 datatype D = D(z: int, 2: int)

Test/git-issues/git-issue-1309.dfy

@@ -1,4 +1,4 @@
-// RUN: %exits-with 2 %baredafny verify --use-basename-for-filename "%s" > "%t"
+// RUN: %exits-with 2 %baredafny verify --show-snippets:false --use-basename-for-filename "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // Example for Issue 1309 -- not yet fixed

Test/git-issues/git-issue-1992.dfy

@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %baredafny verify --use-basename-for-filename "%s" > "%t"
+// RUN: %exits-with 4 %baredafny verify --use-basename-for-filename --show-snippets:false "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 function foo(x: int): int {

Test/git-issues/git-issue-2477.dfy

@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %baredafny verify --use-basename-for-filename --cores:2 --verification-time-limit:300 "%s" > "%t"
+// RUN: %exits-with 4 %baredafny verify --show-snippets:false --use-basename-for-filename --cores:2 --verification-time-limit:300 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 trait T {

Test/git-issues/git-issue-2507.dfy

@@ -1,4 +1,4 @@
-// RUN: %exits-with 2 %baredafny resolve --use-basename-for-filename "%s" > "%t"
+// RUN: %exits-with 2 %baredafny resolve --use-basename-for-filename --show-snippets:false "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method Test(i: int) {

Test/git-issues/git-issue-2959.dfy

@@ -1,4 +1,4 @@
-// RUN: %exits-with 3 %baredafny build --use-basename-for-filename --enforce-determinism "%s" > "%t"
+// RUN: %exits-with 3 %baredafny build --show-snippets:false --use-basename-for-filename --enforce-determinism "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method NondetIf() returns (x: int) {

Test/git-issues/git-issue-2959a.dfy

@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %baredafny build --use-basename-for-filename --enforce-determinism "%s" > "%t"
+// RUN: %exits-with 4 %baredafny build --show-snippets:false --use-basename-for-filename --enforce-determinism "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method AlsoNondetIf() returns (x: int) {

Test/git-issues/git-issue-2959b.dfy

@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %baredafny build --use-basename-for-filename "%s" > "%t"
+// RUN: %exits-with 4 %baredafny build --show-snippets:false --use-basename-for-filename "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method NondetIf() returns (x: int) {

Test/git-issues/git-issue-3288b.dfy

@@ -1,4 +1,4 @@
-// RUN: %exits-with 2 %baredafny verify --use-basename-for-filename "%s" > "%t"
+// RUN: %exits-with 2 %baredafny verify --show-snippets:false --use-basename-for-filename "%s" > "%t"
 // RUN: %diff "%s.expect" "%t" 
 
 module M {

Test/git-issues/git-issue-3366.dfy

@@ -1,4 +1,4 @@
-// RUN: %exits-with 2 %baredafny verify --use-basename-for-filename "%s" > "%t"
+// RUN: %exits-with 2 %baredafny verify --show-snippets:false --use-basename-for-filename "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 class C<T> {

Test/git-issues/git-issue-3370.dfy

@@ -1,5 +1,5 @@
-// RUN: %baredafny build --use-basename-for-filename "%s" > "%t"
-// RUN: %exits-with 4 %baredafny build --use-basename-for-filename --enforce-determinism "%s" >> "%t"
+// RUN: %baredafny build --use-basename-for-filename --show-snippets:false "%s" > "%t"
+// RUN: %exits-with 4 %baredafny build --use-basename-for-filename --show-snippets:false --enforce-determinism "%s" >> "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method m() {

Test/git-issues/git-issue-3377.dfy

@@ -1,4 +1,4 @@
-// RUN: %exits-with 2 %baredafny test --use-basename-for-filename "%s" > "%t"
+// RUN: %exits-with 2 %baredafny test --show-snippets:false --use-basename-for-filename "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method {:extern} {:test} m(i: int, ghost j: int) 

Test/git-issues/git-issue-3451/git-issue-3451.dfy

@@ -1,4 +1,4 @@
-// RUN: %exits-with 2 %baredafny resolve --use-basename-for-filename "%s" > "%t"
+// RUN: %exits-with 2 %baredafny resolve --show-snippets:false --use-basename-for-filename "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // The #line should no longer be special

Test/git-issues/git-issue-3451/git-issue-3451a.dfy

@@ -1,4 +1,4 @@
-// RUN: %exits-with 2 %baredafny resolve --use-basename-for-filename "%s" > "%t"
+// RUN: %exits-with 2 %baredafny resolve --use-basename-for-filename --show-snippets:false "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // The #line should no longer be special

Test/git-issues/git-issue-3513/git-issue-3513.dfy

@@ -1,8 +1,8 @@
-// RUN: %exits-with 2 %baredafny resolve --use-basename-for-filename "%s" > "%t"
-// RUN: %exits-with 2 %baredafny resolve --use-basename-for-filename --library:"%S/src/A.dfy" "%s" >> "%t"
-// RUN: %baredafny resolve --use-basename-for-filename --library:"%S/src/A.dfy,%S/src/sub/B.dfy" "%s" >> "%t"
-// RUN: %baredafny resolve --use-basename-for-filename --library:"%S/src/A.dfy , %S/src/sub/B.dfy" "%s" >> "%t"
-// RUN: %baredafny resolve --use-basename-for-filename --library:"%S/src" "%s" >> "%t"
+// RUN: %exits-with 2 %baredafny resolve --show-snippets:false --use-basename-for-filename "%s" > "%t"
+// RUN: %exits-with 2 %baredafny resolve --show-snippets:false --use-basename-for-filename --library:"%S/src/A.dfy" "%s" >> "%t"
+// RUN: %baredafny resolve --show-snippets:false --use-basename-for-filename --library:"%S/src/A.dfy,%S/src/sub/B.dfy" "%s" >> "%t"
+// RUN: %baredafny resolve --show-snippets:false --use-basename-for-filename --library:"%S/src/A.dfy , %S/src/sub/B.dfy" "%s" >> "%t"
+// RUN: %baredafny resolve --show-snippets:false --use-basename-for-filename --library:"%S/src" "%s" >> "%t"
 // RUN: %diff "%s.expect" "%t"
 
 module M {

Test/git-issues/git-issue-3757.dfy

@@ -1,4 +1,4 @@
-// RUN: %exits-with 2 %baredafny resolve --use-basename-for-filename "%s" > "%t"
+// RUN: %exits-with 2 %baredafny resolve --show-snippets:false --use-basename-for-filename "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 const

Test/git-issues/git-issue-3757a.dfy

@@ -1,4 +1,4 @@
-// RUN: %exits-with 2 %baredafny resolve --use-basename-for-filename "%s" > "%t"
+// RUN: %exits-with 2 %baredafny resolve --show-snippets:false --use-basename-for-filename "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 const +

Test/git-issues/git-issue-3839/git-issue-3839a.dfy

@@ -1,4 +1,4 @@
-// RUN: ! %baredafny test --use-basename-for-filename "%s" > "%t"
+// RUN: ! %baredafny test --use-basename-for-filename --show-snippets:false "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method {:test} M(x: int) returns (r: int)

Test/git-issues/git-issue-3855.dfy

@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %baredafny verify --warn-deprecation:false --use-basename-for-filename "%s" > "%t"
+// RUN: %exits-with 4 %baredafny verify --show-snippets:false --warn-deprecation:false --use-basename-for-filename "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 // Nearly verbatim copy of the text case given in the issue
 //SIMULADA 

Test/lit.site.cfg

@@ -114,6 +114,7 @@ config.suffixes.append('.transcript')
 dafnyArgs = [
     # We do not want absolute or relative paths in error messages, just the basename of the file
     'useBaseNameForFileName',
+    'showSnippets:0',
 
     # Try to verify 2 verification conditions at once
     'vcsCores:2',
@@ -155,7 +156,7 @@ def buildCmd(cmd, args):
 dafny = addParams(buildCmd(dafnyExecutable, dafnyArgs))
 boogie = buildCmd(boogieExecutable, boogieArgs)
 
-standardArguments = addParams(' '.join(["--use-basename-for-filename"]))
+standardArguments = addParams(' '.join(["--use-basename-for-filename", "--show-snippets"]))
 
 # Inform user what executable is being used
 lit_config.note(f'Using Dafny (%dafny): {dafny}\n')

Test/logger/TextLogger.dfy

@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %baredafny verify --log-format:text --isolate-assertions "%s" > "%t"
+// RUN: %exits-with 4 %baredafny verify --show-snippets:false --log-format:text --isolate-assertions "%s" > "%t"
 // RUN: %OutputCheck --file-to-check "%t" "%s"
 // CHECK: Overall outcome: Errors
 // CHECK: Overall time: .*

Test/logger/TextLoggerBatch.dfy

@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %baredafny verify --log-format:text "%s" > "%t"
+// RUN: %exits-with 4 %baredafny verify --show-snippets:false --log-format:text "%s" > "%t"
 // RUN: %OutputCheck --file-to-check "%t" "%s"
 // CHECK: Overall outcome: Errors
 // CHECK: Overall time: .*

docs/HowToFAQ/Errors-CommandLine.md

@@ -235,7 +235,7 @@ The `printIncludes` option has these alternatives: None, Immediate, Transitive.
 
 <!-- %no-check TODO: Outputs the help document  -->
 ```bash 
-dafny resolve --quantifier-syntax:2 null.dfy
+dafny resolve --show-snippets:false --quantifier-syntax:2 null.dfy
 ```
 
 This is a generic error message about command-line arguments,

docs/OnlineTutorial/Lemmas.md

@@ -29,7 +29,7 @@ for zero in an array. What makes this problem interesting is that the array we a
 searching in has two special properties: all elements are non-negative, and each successive
 element decreases by at most one from the previous element. In code:
 
-<!-- %check-verify Lemmas.1.expect -->
+<!-- %check-verify Lemmas.1.expect %options -->
 ```dafny
 method FindZero(a: array<int>) returns (index: int)
   requires forall i :: 0 <= i < a.Length ==> 0 <= a[i]

docs/check-examples

@@ -120,8 +120,9 @@ dafny="$dafnydir/dafny"
 outdir="$dir/../Test/docexamples"
 
 coverage=0
+permOptions="--show-snippets:false "
 defOptions="--function-syntax:4 --use-basename-for-filename --unicode-char:false"
-legacyOptions="-functionSyntax:4 -useBaseNameForFileName"
+legacyOptions="-functionSyntax:4 -useBaseNameForFileName -showSnippets:0"
 
 while getopts 'c' opt; do
   case "$opt" in
@@ -366,7 +367,7 @@ do
         if [ "$coverage" == "1" ] ; then
           f=$outdir/$(basename $file)_${n}.dfy
           if  [ "$command" == "%check-legacy" ]; then
-            echo "// RUN: %exits-with" $expectedExit "%baredafny" $verb $dOptions ${options[@]} '"%s" > "%t"' > "$f"
+            echo "// RUN: %exits-with" $expectedExit "%baredafny" "/showSnippets:0" $verb $dOptions ${options[@]} '"%s" > "%t"' > "$f"
             echo " " >> $f
             cat $text >> $f
           elif [ "$command" == "%check-cli" ]; then
@@ -379,11 +380,11 @@ do
         else
           if [ "$command" == "%check-legacy" ]; then
             isverbose=-compileVerbose:$checkIds
-            (cd "$dir"; "$dafny" $verb $dOptions $isverbose ${options[@]} $text   ) > "$actualOut" 2> "$actualError"
+            (cd "$dir"; "$dafny" /showSnippets:0 $dOptions $isverbose ${options[@]} $text   ) > "$actualOut" 2> "$actualError"
           else
             isverbose=
             if [ "$checkIds" == "1" ]; then isverbose="--verbose" ; fi
-            ( cd "$dir" ; "$dafny" $verb $isverbose $dOptions ${options[@]} $text ) > "$actualOut" 2> "$actualError"
+            ( cd "$dir" ; "$dafny" $verb $isverbose $permOptions $dOptions ${options[@]} $text ) > "$actualOut" 2> "$actualError"
           fi
           actualExit=$?
           if [ "$useHeadings" == "1" ]; then

docs/dev/news/4087.feat

@@ -0,0 +1 @@
+errors issued in command-line mode now show source code context by default; this behavior can be disabled using the option --show-snippets:false.