Merge branch 'master' into alexchew/publish-py-runtime

.github/workflows/doc-tests.yml

@@ -10,6 +10,8 @@ on:
   workflow_dispatch:
   pull_request:
     branches: [ master, main-* ]
+  merge_group:
+    branches: [ master, main-* ]
 
 concurrency:
   group: ${{ github.workflow }}-${{ github.ref }}

.github/workflows/jekyll.yml

@@ -37,7 +37,7 @@ jobs:
           working-directory: 'docs'
       - name: Setup Pages
         id: pages
-        uses: actions/configure-pages@v4
+        uses: actions/configure-pages@v5
       - name: Build with Jekyll
         # Outputs to the './_site' directory by default
         run: (cd docs; bundle exec jekyll build --baseurl "${{ steps.pages.outputs.base_path }}"  --destination ../_site)

.github/workflows/msbuild.yml

@@ -4,6 +4,8 @@ on:
   workflow_dispatch:
   pull_request:
     branches: [ master, main-* ]
+  merge_group:
+    branches: [ master, main-* ]
 
 concurrency:
   group: ${{ github.workflow }}-${{ github.ref }}

.github/workflows/refman.yml

@@ -4,6 +4,8 @@ on:
   workflow_dispatch:
   pull_request:
     branches: [ master, main-* ]
+  merge_group:
+    branches: [ master, main-* ]
 
 concurrency:
   group: ${{ github.workflow }}-${{ github.ref }}

.github/workflows/runtime-tests.yml

@@ -4,6 +4,8 @@ on:
   workflow_dispatch:
   pull_request:
     branches: [ master, main-* ]
+  merge_group:
+    branches: [ master, main-* ]
 
 concurrency:
   group: ${{ github.workflow }}-${{ github.ref }}

.github/workflows/standard-libraries.yml

@@ -4,6 +4,8 @@ on:
   workflow_dispatch:
   pull_request:
     branches: [ master, main-* ]
+  merge_group:
+    branches: [ master, main-* ]
 
 concurrency:
   group: ${{ github.workflow }}-${{ github.ref }}

.gitignore

@@ -79,3 +79,5 @@ Source/IntegrationTests/TestFiles/LitTests/LitTest/server/*.bvd
 /Source/IntegrationTests/TestFiles/LitTests/LitTest/separate-verification/assumptions-lib
 /Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/log.smt2
 /Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/model
+Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/*.html
+Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/*.html

CONTRIBUTING.md

@@ -74,7 +74,7 @@ After doing these steps once, for other PRs, one only needs to re-run deep check
 - If some required tests fail, investigate and push more commits, but know that each CI run takes a lot of time, so try to fix the problem with as few commits as possible (ideally 1)
   It is also possible you find some tests that fail randomly, in that case, re-run them and report to the team. Avoid using the re-run all failed jobs here, because it will re-run _all_ jobs, so select them individually instead.
 - Have someone approve the PR and merge it (or auto-merge).
-- Once the PR with the fix to the CI is merged to master, go to https://github.com/dafny-lang/dafny/actions/workflows/deep-tests.yml
+- Once the PR with the fix to the CI is merged to master, go to https://github.com/dafny-lang/dafny/actions/workflows/nightly-build.yml
 - Select "Run workflow..."
 - Select master
 - Wait for this new run to succeed.
@@ -106,4 +106,4 @@ You can find a description of the release process in [docs/dev/RELEASE.md](https
 
 Dafny is still changing and backwards incompatible changes may be made. Any backwards compatibility breaking change must be easy to adapt to, such as by adding a command line option. In the future, we plan to add a `dafny migrate` command which should support migrating any Dafny codebase from the previous to the current CLI version. 
 
-As rule, Dafny features must be marked as deprecated, including migration instructions, at least one release before they are removed.
+As rule, Dafny features must be marked as deprecated, including migration instructions, at least one release before they are removed.

Source/DafnyCore/AST/Expressions/Comprehensions/LambdaExpr.cs

@@ -3,7 +3,7 @@
 
 namespace Microsoft.Dafny;
 
-public class LambdaExpr : ComprehensionExpr, ICloneable<LambdaExpr> {
+public class LambdaExpr : ComprehensionExpr, ICloneable<LambdaExpr>, IFrameScope {
   public override string WhatKind => Reads.Expressions.Count != 0 ? "lambda" : Range != null ? "partial lambda" : "total lambda";
 
   public Expression Body => Term;
@@ -84,4 +84,6 @@ public override bool SetIndent(int indentBefore, TokenNewIndentCollector formatt
 
     return true;
   }
+
+  public string Designator => "lambda";
 }

Source/DafnyCore/AST/IHasUsages.cs

@@ -28,6 +28,10 @@ public interface ICanVerify : ISymbol {
   string FullDafnyName { get; }
 }
 
+public interface IFrameScope {
+  string Designator { get; } // "lambda expression", "method", "function"...
+}
+
 public static class AstExtensions {
 
   public static string GetMemberQualification(MemberDecl memberDecl) {

Source/DafnyCore/AST/Members/ConstantField.cs

@@ -65,4 +65,5 @@ public void AutoRevealDependencies(AutoRevealFunctionDependencies Rewriter, Dafn
         AutoRevealFunctionDependencies.GenerateMessage(addedReveals.ToList()));
     }
   }
+  public string Designator => WhatKind;
 }

Source/DafnyCore/AST/Members/Function.cs

@@ -564,4 +564,5 @@ public void AutoRevealDependencies(AutoRevealFunctionDependencies Rewriter, Dafn
         AutoRevealFunctionDependencies.GenerateMessage(addedReveals, autoRevealDepth));
     }
   }
+  public string Designator => WhatKind;
 }

Source/DafnyCore/AST/Members/ICodeContext.cs

@@ -50,7 +50,7 @@ public static ICodeContext Unwrap(ICodeContext codeContext) {
 /// <summary>
 /// An ICallable is a Function, Method, IteratorDecl, or (less fitting for the name ICallable) RedirectingTypeDecl or DatatypeDecl.
 /// </summary>
-public interface ICallable : ICodeContext, ISymbol {
+public interface ICallable : ICodeContext, ISymbol, IFrameScope {
   string WhatKind { get; }
   string NameRelativeToModule { get; }
   Specification<Expression> Decreases { get; }
@@ -98,6 +98,8 @@ public bool InferredDecreases {
   public string GetDescription(DafnyOptions options) {
     return CwInner.GetDescription(options);
   }
+
+  public string Designator => WhatKind;
 }
 
 
@@ -132,6 +134,7 @@ public IEnumerable<INode> GetConcreteChildren() {
   public string GetDescription(DafnyOptions options) {
     throw new cce.UnreachableException();
   }
+  public string Designator => WhatKind;
 }
 
 /// <summary>

Source/DafnyCore/AST/Members/Method.cs

@@ -472,4 +472,5 @@ public void AutoRevealDependencies(AutoRevealFunctionDependencies Rewriter, Dafn
         AutoRevealFunctionDependencies.GenerateMessage(addedReveals, autoRevealDepth));
     }
   }
+  public string Designator => WhatKind;
 }

Source/DafnyCore/AST/TypeDeclarations/DatatypeDecl.cs

@@ -196,4 +196,5 @@ public void AutoRevealDependencies(AutoRevealFunctionDependencies Rewriter, Dafn
       }
     }
   }
+  public string Designator => WhatKind;
 }

Source/DafnyCore/AST/TypeDeclarations/IteratorDecl.cs

@@ -513,4 +513,5 @@ public override string GetTriviaContainingDocstring() {
   }
   public bool ShouldVerify => true; // This could be made more accurate
   public ModuleDefinition ContainingModule => EnclosingModuleDefinition;
+  public string Designator => WhatKind;
 }

Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs

@@ -166,6 +166,7 @@ public string GetTriviaContainingDocstring() {
 
   public ModuleDefinition ContainingModule => EnclosingModuleDefinition;
   public bool ShouldVerify => true; // This could be made more accurate
+  public string Designator => WhatKind;
 }
 
 public class NativeType {

Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs

@@ -125,4 +125,5 @@ public string GetTriviaContainingDocstring() {
 
   public abstract SymbolKind Kind { get; }
   public abstract string GetDescription(DafnyOptions options);
+  public string Designator => WhatKind;
 }

Source/DafnyCore/AST/Types/UserDefinedType.cs

@@ -12,7 +12,7 @@ void ObjectInvariant() {
     Contract.Invariant(tok != null);
     Contract.Invariant(Name != null);
     Contract.Invariant(cce.NonNullElements(TypeArgs));
-    Contract.Invariant(NamePath is NameSegment || NamePath is ExprDotName);
+    Contract.Invariant(NamePath is NameSegment or ExprDotName);
     Contract.Invariant(!ArrowType.IsArrowTypeName(Name) || this is ArrowType);
   }
 

Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs

@@ -110,8 +110,8 @@ void EmitImports(ConcreteSyntaxTree wr, out ConcreteSyntaxTree importWriter, out
       }
     }
 
-    public static string TransformToClassName(string baseName) =>
-      Regex.Replace(baseName, "[^_A-Za-z0-9$]", "_");
+    public string TransformToClassName(string baseName) =>
+      IdProtect(Regex.Replace(baseName, "[^_A-Za-z0-9$]", "_"));
 
     public override void EmitCallToMain(Method mainMethod, string baseName, ConcreteSyntaxTree wr) {
       var companion = TypeName_Companion(UserDefinedType.FromTopLevelDeclWithAllBooleanTypeParameters(mainMethod.EnclosingClass), wr, mainMethod.tok, mainMethod);
@@ -167,11 +167,11 @@ protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDef
         return wr;
       }
 
-      var import = CreateImport(moduleName, isDefault, externModule, libraryName);
+      ModuleName = PublicModuleIdProtect(moduleName);
+      var import = CreateImport(ModuleName, isDefault, externModule, libraryName);
 
       var filename = string.Format("{0}/{0}.go", import.Path);
       var w = wr.NewFile(filename);
-      ModuleName = moduleName;
       EmitModuleHeader(w);
 
       AddImport(import);
@@ -2519,6 +2519,14 @@ public override string PublicIdProtect(string name) {
       }
     }
 
+    public string PublicModuleIdProtect(string name) {
+      if (name == "C") {
+        return "_C";
+      } else {
+        return name;
+      }
+    }
+
     protected override string FullTypeName(UserDefinedType udt, MemberDecl/*?*/ member = null) {
       return UserDefinedTypeName(udt, full: true, member: member);
     }
@@ -2541,28 +2549,30 @@ private string UserDefinedTypeName(UserDefinedType udt, bool full, MemberDecl/*?
     }
 
     private string UserDefinedTypeName(TopLevelDecl cl, bool full, MemberDecl/*?*/ member = null) {
+      var enclosingModuleDefinitionId = PublicModuleIdProtect(cl.EnclosingModuleDefinition.GetCompileName(Options));
       if (IsExternMemberOfExternModule(member, cl)) {
         // omit the default class name ("_default") in extern modules, when the class is used to qualify an extern member
         Contract.Assert(!cl.EnclosingModuleDefinition.IsDefaultModule);  // default module is not marked ":extern"
-        return IdProtect(cl.EnclosingModuleDefinition.GetCompileName(Options));
+        return enclosingModuleDefinitionId;
       } else {
         if (cl.IsExtern(Options, out var qual, out _)) {
           // No need to take into account the second argument to extern, since
           // it'll already be cl.CompileName
           if (qual == null) {
-            if (this.ModuleName == cl.EnclosingModuleDefinition.GetCompileName(Options)) {
+            if (this.ModuleName == enclosingModuleDefinitionId) {
               qual = "";
             } else {
-              qual = cl.EnclosingModuleDefinition.GetCompileName(Options);
+              qual = enclosingModuleDefinitionId;
             }
           }
           // Don't use IdName since that'll capitalize, which is unhelpful for
           // built-in types
           return qual + (qual == "" ? "" : ".") + cl.GetCompileName(Options);
-        } else if (!full || cl.EnclosingModuleDefinition.TryToAvoidName || this.ModuleName == cl.EnclosingModuleDefinition.GetCompileName(Options)) {
+
+        } else if (!full || cl.EnclosingModuleDefinition.TryToAvoidName || this.ModuleName == enclosingModuleDefinitionId) {
           return IdName(cl);
         } else {
-          return cl.EnclosingModuleDefinition.GetCompileName(Options) + "." + IdName(cl);
+          return enclosingModuleDefinitionId + "." + IdName(cl);
         }
       }
     }

Source/DafnyCore/Backends/SinglePassCodeGenerator.cs

@@ -5571,6 +5571,7 @@ void EmitExpr(Expression e2, ConcreteSyntaxTree wr2, bool inLetExpr, ConcreteSyn
         var collectionName = ProtectedFreshId("_coll");
         var setType = e.Type.NormalizeToAncestorType().AsSetType;
         var bwr = CreateIIFE0(setType, e.tok, wr, wStmts);
+        wStmts = bwr.Fork();
         wr = bwr;
         EmitSetBuilder_New(wr, e, collectionName);
         var n = e.BoundVars.Count;
@@ -5617,6 +5618,7 @@ void EmitExpr(Expression e2, ConcreteSyntaxTree wr2, bool inLetExpr, ConcreteSyn
         var rantypeName = TypeName(mapType.Range, wr, e.tok);
         var collection_name = ProtectedFreshId("_coll");
         var bwr = CreateIIFE0(mapType, e.tok, wr, wStmts);
+        wStmts = bwr.Fork();
         wr = bwr;
         EmitMapBuilder_New(wr, e, collection_name);
         var n = e.BoundVars.Count;

Source/DafnyCore/DooFile.cs

@@ -54,7 +54,7 @@ public static ManifestData Read(TextReader reader) {
     }
 
     public void Write(TextWriter writer) {
-      writer.Write(Toml.FromModel(this, new TomlModelOptions()));
+      writer.Write(Toml.FromModel(this, new TomlModelOptions()).Replace("\r\n", "\n"));
     }
   }
 
@@ -103,7 +103,9 @@ private static DooFile Read(ZipArchive archive) {
   }
 
   public DooFile(Program dafnyProgram) {
-    var tw = new StringWriter();
+    var tw = new StringWriter {
+      NewLine = "\n"
+    };
     var pr = new Printer(tw, ProgramSerializationOptions, PrintModes.Serialization);
     // afterResolver is false because we don't yet have a way to safely skip resolution
     // when reading the program back into memory.
@@ -191,7 +193,7 @@ public void Write(ConcreteSyntaxTree wr) {
     var manifestWr = wr.NewFile(ManifestFileEntry);
     using var manifestWriter = new StringWriter();
     Manifest.Write(manifestWriter);
-    manifestWr.Write(manifestWriter.ToString());
+    manifestWr.Write(manifestWriter.ToString().Replace("\r\n", "\n"));
 
     var programTextWr = wr.NewFile(ProgramFileEntry);
     programTextWr.Write(ProgramText);

Source/DafnyCore/Resolver/CheckTypeCharacteristics_Visitor.cs

@@ -257,6 +257,7 @@ bool VisitPattern(CasePattern<BoundVar> pat, bool patternGhostContext) {
       return false;  // we've done what there is to be done
     } else if (expr is DatatypeValue) {
       var e = (DatatypeValue)expr;
+      VisitType(expr.tok, expr.Type, inGhostContext);
       // recursively visit all subexpressions (all actual parameters), noting which ones correspond to ghost formal parameters
       Contract.Assert(e.Arguments.Count == e.Ctor.Formals.Count);
       for (var i = 0; i < e.Arguments.Count; i++) {

Source/DafnyCore/Resolver/PreType/Flows.cs

@@ -230,15 +230,14 @@ Type JoinChildren(UserDefinedType udtA, UserDefinedType udtB) {
     var bTypeSubstMap = TypeParameter.SubstitutionMap(bDecl.TypeArgs, b.TypeArgs);
     (bDecl as TopLevelDeclWithMembers)?.AddParentTypeParameterSubstitutions(bTypeSubstMap);
 
-    a = UserDefinedType.FromTopLevelDecl(commonSupertypeDecl.tok, commonSupertypeDecl).Subst(aTypeSubstMap);
-    b = UserDefinedType.FromTopLevelDecl(commonSupertypeDecl.tok, commonSupertypeDecl).Subst(bTypeSubstMap);
+    var aSubst = UserDefinedType.FromTopLevelDecl(commonSupertypeDecl.tok, commonSupertypeDecl).Subst(aTypeSubstMap);
+    var bSubst = UserDefinedType.FromTopLevelDecl(commonSupertypeDecl.tok, commonSupertypeDecl).Subst(bTypeSubstMap);
 
-    var joinedTypeArgs = Joins(TypeParameter.Variances(commonSupertypeDecl.TypeArgs), a.TypeArgs, b.TypeArgs, context);
+    var joinedTypeArgs = Joins(TypeParameter.Variances(commonSupertypeDecl.TypeArgs), aSubst.TypeArgs, bSubst.TypeArgs, context);
     if (joinedTypeArgs == null) {
       return null;
     }
-    var udt = (UserDefinedType)a;
-    var result = UserDefinedType.FromTopLevelDecl(udt.tok, commonSupertypeDecl, joinedTypeArgs);
+    var result = UserDefinedType.FromTopLevelDecl(a.tok, commonSupertypeDecl, joinedTypeArgs);
     return abNonNullTypes && result.IsRefType ? UserDefinedType.CreateNonNullType(result) : result;
   }