Merge functionality to filter out tests

.github/CONTRIBUTING.md

@@ -26,3 +26,14 @@ All other pull requests and issues can be submitted here.
 ## Code of Conduct
 
 See [`CODE_OF_CONDUCT.md`](./CODE_OF_CONDUCT.md).
+
+## FAQ
+
+### What to do if the nightly build failed but because of a "download failure"?
+
+If the test in a PR named `Build and Test / check-deep-tests / check-deep-tests` failed, clicking on its "details" reveals a view (view 1) in which you can see a failed run with the failure being something like "Error: Last run of deep-tests.yml did not succeed (some URL in parentheses).
+
+Clicking on this URL will reveal the deep tests that were run (view 2). If one of this test is just a "download failure", then one simply needs to re-run it (button on the top right).
+Once it succeeds, one has to go back to (view 1) and re-run the failed jobs, so that it will retrieve the latest successful deep tests.
+
+After doing these steps once, for other PRs, one only needs to re-run deep checks in (view 1)

RELEASE_NOTES.md

@@ -1,7 +1,9 @@
 # Upcoming
 
+- fix: Hovering over variables and methods inside cases of nested match statements work again (https://github.com/dafny-lang/dafny/pull/2334)
 - fix: Fix bug in translation of two-state predicates with heap labels. (https://github.com/dafny-lang/dafny/pull/2300)
 - fix: Check that arguments of 'unchanged' satisfy enclosing reads clause. (https://github.com/dafny-lang/dafny/pull/2302)
+- fix: Caching in the language server does not prevent gutter icons from being updated correctly. (https://github.com/dafny-lang/dafny/pull/2312)
 - fix: Correctly infer type of numeric arguments, where the type is a subset type of a newtype. (https://github.com/dafny-lang/dafny/pull/2314)
 
 # 3.7.1

Source/Dafny/Resolver.cs

@@ -11964,7 +11964,7 @@ private class RBranchStmt : RBranch {
  }
 
  public RBranchStmt(int branchid, NestedMatchCaseStmt x, Attributes attrs = null) : base(x.Tok, branchid, new List<ExtendedPattern>()) {
- this.Body = x.Body.ConvertAll((new Cloner()).CloneStmt);
+ this.Body = new List<Statement>(x.Body); // Resolving the body will insert new elements. 
  this.Attributes = attrs;
  this.Patterns.Add(x.Pat);
  }

Source/DafnyLanguageServer.Test/GutterStatus/CachedLinearVerificationGutterStatusTester.cs

@@ -0,0 +1,51 @@
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text.RegularExpressions;
+using System.Threading.Tasks;
+using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions;
+using Microsoft.Dafny.LanguageServer.IntegrationTest.Util;
+using Microsoft.Dafny.LanguageServer.Language;
+using Microsoft.Dafny.LanguageServer.Workspace;
+using Microsoft.Dafny.LanguageServer.Workspace.Notifications;
+using Microsoft.VisualStudio.TestTools.UnitTesting;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
+using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range;
+
+namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Diagnostics;
+
+[TestClass]
+public class CachedLinearVerificationGutterStatusTester : LinearVerificationGutterStatusTester {
+ private const int MaxTestExecutionTimeMs = 10000;
+
+
+
+ // To add a new test, just call VerifyTrace on a given program,
+ // the test will fail and give the correct output that can be use for the test
+ // Add '//Next<n>:' to edit a line multiple times
+
+ [TestMethod, Timeout(MaxTestExecutionTimeMs)]
+ public async Task EnsureCachingDoesNotMakeSquigglyLinesToRemain() {
+ await SetUp(new Dictionary<string, string>() {
+ { $"{VerifierOptions.Section}:{nameof(VerifierOptions.VerifySnapshots)}", "1" }
+ });
+ await VerifyTrace(@"
+ . S S | I $ | :method test() {
+ . S | | I $ | : assert true;
+ . S S | I $ | : //Next: 
+ . S S | I $ | :}");
+ }
+
+ [TestMethod, Timeout(MaxTestExecutionTimeMs)]
+ public async Task EnsureCachingDoesNotHideErrors() {
+ await SetUp(new Dictionary<string, string>() {
+ { $"{VerifierOptions.Section}:{nameof(VerifierOptions.VerifySnapshots)}", "1" }
+ });
+ await VerifyTrace(@"
+ . S [S][ ][I][S][S][ ]:method test() {
+ . S [O][O][o][Q][O][O]: assert true;
+ . S [=][=][-][~][=][=]: assert false;
+ . S [S][ ][I][S][S][ ]: //Next: 
+ . S [S][ ][I][S][S][ ]:}");
+ }
+}

Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs

@@ -427,5 +427,16 @@ function ToRelativeIndependent(): (p: Position)
 }
 ");
  }
+
+ [TestMethod]
+ public async Task HoveringVariablesInsideNestedMatchStmtWorks() {
+ await AssertHover(@"
+lemma dummy(e: int) {
+ match e {
+ case _ => var xx := 1;
+ ^[```dafny\nghost xx: int\n```]
+ }
+}");
+ }
  }
 }

Source/DafnyLanguageServer/Language/AssertionBatchCompletedObserver.cs

@@ -55,7 +55,7 @@ public class AssertionBatchCompletedObserver : OutputPrinter {
 
  public void ReportSplitResult(Split split, VCResult vcResult) {
  if (reportVerificationDiagnostics) {
- completedBatches.OnNext(new AssertionBatchResult(split, vcResult));
+ completedBatches.OnNext(new AssertionBatchResult(split.Implementation, vcResult));
  }
  }
 

Source/DafnyLanguageServer/Language/IProgramVerifier.cs

@@ -7,7 +7,7 @@
 using VC;
 
 namespace Microsoft.Dafny.LanguageServer.Language {
- public record AssertionBatchResult(Split Split, VCResult Result);
+ public record AssertionBatchResult(Implementation Implementation, VCResult Result);
 
  public record ProgramVerificationTasks(IReadOnlyList<IImplementationTask> Tasks);
 

Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs

@@ -134,7 +134,7 @@ VerifierOptions verifierOptions
  }
  var implementations = verificationTasks.Select(t => t.Implementation).ToHashSet();
  var subscription = verifier.BatchCompletions.Where(c =>
- implementations.Contains(c.Split.Implementation)).Subscribe(progressReporter.ReportAssertionBatchResult);
+ implementations.Contains(c.Implementation)).Subscribe(progressReporter.ReportAssertionBatchResult);
  cancellationToken.Register(() => subscription.Dispose());
  result.GutterProgressReporter = progressReporter;
  return result;
@@ -245,6 +245,12 @@ bool loadCanceled
 
  var statusUpdates = implementationTask.TryRun();
  if (statusUpdates == null) {
+ if (VerifierOptions.GutterStatus && implementationTask.CacheStatus is Completed completedCache) {
+ foreach (var result in completedCache.Result.VCResults) {
+ dafnyDocument.GutterProgressReporter!.ReportAssertionBatchResult(new AssertionBatchResult(implementationTask.Implementation, result));
+ }
+ dafnyDocument.GutterProgressReporter!.ReportEndVerifyImplementation(implementationTask.Implementation, completedCache.Result);
+ }
  return Observable.Empty<DafnyDocument>();
  }
 

Source/DafnyLanguageServer/Workspace/VerificationProgressReporter.cs

@@ -358,9 +358,8 @@ INotificationPublisher notificationPublisher
  return;
  }
  lock (LockProcessing) {
- var split = batchResult.Split;
+ var implementation = batchResult.Implementation;
  var result = batchResult.Result;
- var implementation = split.Implementation;
  // While there is no error, just add successful nodes.
  var targetMethodNode = GetTargetMethodTree(implementation, out var implementationNode);
  if (targetMethodNode == null) {

docs/OnlineTutorial/guide.md

@@ -2,11 +2,6 @@
 
 # Getting Started with Dafny: A Guide
 
-Be sure to follow along with the code examples by clicking the "load
-in editor" link in the
-corner. See what the tool says, try to fix programs on your own, and
-experiment!
-
 ## Introduction
 
 Dafny is a language that is designed to make it easy to