Allow using project files together with --library

Source/DafnyCore/AST/Grammar/ProgramParser.cs

@@ -4,6 +4,7 @@
 using System.Diagnostics.Contracts;
 using System.IO;
 using System.Linq;
+using System.Runtime.CompilerServices;
 using System.Text;
 using System.Threading;
 using System.Threading.Tasks;
@@ -62,7 +63,7 @@ public virtual async Task<Program> ParseFiles(string programName, IReadOnlyList<
       }
 
       var parseResult = ParseFileWithErrorHandling(
-        dafnyFile.ParseOptions,
+        dafnyFile.FileOptions,
         dafnyFile.GetContent,
         dafnyFile.Origin,
         dafnyFile.Uri,
@@ -96,7 +97,7 @@ public virtual async Task<Program> ParseFiles(string programName, IReadOnlyList<
       // if we're building a .doo file.
       // See comment on LibraryBackend.DooFile.
       if (program.Options.Backend is LibraryBackend libBackend) {
-        libBackend.ProgramAfterParsing = new Program(new Cloner(true), program);
+        program.AfterParsingClone = new Program(new Cloner(true), program);
       }
     }
 
@@ -220,7 +221,7 @@ CancellationToken cancellationToken
     }
 
     foreach (var root in roots) {
-      var dafnyFile = await IncludeToDafnyFile(systemModuleManager, errorReporter, root);
+      var dafnyFile = await IncludeToDafnyFile(errorReporter, root);
       if (dafnyFile != null) {
         stack.Push(dafnyFile);
       }
@@ -234,15 +235,15 @@ CancellationToken cancellationToken
 
       cancellationToken.ThrowIfCancellationRequested();
       var parseIncludeResult = ParseFileWithErrorHandling(
-        errorReporter.Options,
+        top.FileOptions,
         top.GetContent,
         top.Origin,
         top.Uri,
         cancellationToken);
       result.Add(parseIncludeResult);
 
       foreach (var include in parseIncludeResult.Module.Includes) {
-        var dafnyFile = await IncludeToDafnyFile(systemModuleManager, errorReporter, include);
+        var dafnyFile = await IncludeToDafnyFile(errorReporter, include);
         if (dafnyFile != null) {
           stack.Push(dafnyFile);
         }
@@ -252,8 +253,8 @@ CancellationToken cancellationToken
     return result;
   }
 
-  private Task<DafnyFile> IncludeToDafnyFile(SystemModuleManager systemModuleManager, ErrorReporter errorReporter, Include include) {
-    return DafnyFile.CreateAndValidate(errorReporter, fileSystem, systemModuleManager.Options, include.IncludedFilename, include.tok);
+  private async Task<DafnyFile> IncludeToDafnyFile(ErrorReporter errorReporter, Include include) {
+    return await DafnyFile.CreateAndValidate(errorReporter, fileSystem, include.ParseOptions, include.IncludedFilename, include.tok);
   }
 
   ///<summary>

Source/DafnyCore/AST/Include.cs

@@ -5,14 +5,16 @@
 namespace Microsoft.Dafny;
 
 public class Include : TokenNode, IComparable {
+  public DafnyOptions ParseOptions { get; }
   public Uri IncluderFilename { get; }
   public Uri IncludedFilename { get; }
   public string CanonicalPath { get; }
 
-  public Include(IToken tok, Uri includer, Uri theFilename) {
+  public Include(IToken tok, Uri includer, Uri theFilename, DafnyOptions parseOptions) {
     this.tok = tok;
     this.IncluderFilename = includer;
     this.IncludedFilename = theFilename;
+    ParseOptions = parseOptions;
     this.CanonicalPath = DafnyFile.Canonicalize(theFilename.LocalPath).LocalPath;
   }
 

Source/DafnyCore/AST/Members/Function.cs

@@ -315,7 +315,6 @@ static Function() {
     DafnyOptions.RegisterLegacyBinding(FunctionSyntaxOption, (options, value) => {
       options.FunctionSyntax = functionSyntaxOptionsMap[value];
     });
-
     DooFile.RegisterNoChecksNeeded(FunctionSyntaxOption);
   }
 

Source/DafnyCore/AST/Members/Method.cs

@@ -1,14 +1,28 @@
 using System.Collections.Generic;
+using System.CommandLine;
 using System.Diagnostics.Contracts;
 using System.Linq;
 using System.Numerics;
+using DafnyCore;
 using Microsoft.Dafny.Auditor;
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 
 namespace Microsoft.Dafny;
 
 public class Method : MethodOrFunction, TypeParameter.ParentType,
   IMethodCodeContext, ICanFormat, IHasDocstring, IHasSymbolChildren, ICanAutoRevealDependencies, ICanVerify {
+
+  public static readonly Option<bool> ReadsClausesOnMethods = new("--reads-clauses-on-methods",
+    "Allows reads clauses on methods (with a default of 'reads *') as well as functions."
+  );
+
+  static Method() {
+    DafnyOptions.RegisterLegacyUi(ReadsClausesOnMethods, DafnyOptions.ParseBoolean, "Language feature selection", "readsClausesOnMethods", @"
+0 (default) - Reads clauses on methods are forbidden.
+1 - Reads clauses on methods are permitted (with a default of 'reads *').".TrimStart(), defaultValue: false);
+    DooFile.RegisterLibraryCheck(ReadsClausesOnMethods, DooFile.CheckOptionLocalImpliesLibrary);
+  }
+
   public override IEnumerable<INode> Children => new Node[] { Body, Decreases }.Where(x => x != null).
     Concat(Ins).Concat(Outs).Concat<Node>(TypeArgs).
     Concat(Req).Concat(Ens).Concat(Reads.Expressions).Concat(Mod.Expressions);

Source/DafnyCore/AST/Program.cs

@@ -39,6 +39,24 @@ void ObjectInvariant() {
 
   public ProofDependencyManager ProofDependencyManager { get; set; } = new();
 
+  /// <summary>
+  /// Serializing the state of the Program passed to this backend,
+  /// after resolution, can be problematic.
+  /// If nothing else, very early on in the resolution process
+  /// we create explicit module definitions for implicit ones appearing
+  /// in qualified names such as `module A.B.C { ... }`,
+  /// and this means that multiple .doo files would then not be able to
+  /// share these prefixes without hitting duplicate name errors.
+  ///
+  /// Instead we serialize the state of the program immediately after parsing.
+  /// See also ProgramParser.ParseFiles().
+  /// 
+  /// This could be captured somewhere else, such as on the Program itself,
+  /// if having this state here hampers reuse in the future,
+  /// especially parallel processing.
+  /// </summary>
+  public Program AfterParsingClone { get; set; }
+
   public Program(string name, [Captured] LiteralModuleDecl module, [Captured] SystemModuleManager systemModuleManager, ErrorReporter reporter,
     CompilationData compilation) {
     Contract.Requires(name != null);

Source/DafnyCore/Backends/Library/LibraryBackend.cs

@@ -36,24 +36,6 @@ public override string TargetBaseDir(string dafnyProgramName) =>
   // Necessary since Compiler is null
   public override string ModuleSeparator => ".";
 
-  /// <summary>
-  /// Serializing the state of the Program passed to this backend,
-  /// after resolution, can be problematic.
-  /// If nothing else, very early on in the resolution process
-  /// we create explicit module definitions for implicit ones appearing
-  /// in qualified names such as `module A.B.C { ... }`,
-  /// and this means that multiple .doo files would then not be able to
-  /// share these prefixes without hitting duplicate name errors.
-  ///
-  /// Instead we serialize the state of the program immediately after parsing.
-  /// See also ProgramParser.ParseFiles().
-  /// 
-  /// This could be captured somewhere else, such as on the Program itself,
-  /// if having this state here hampers reuse in the future,
-  /// especially parallel processing.
-  /// </summary>
-  internal Program ProgramAfterParsing { get; set; }
-
   protected override SinglePassCodeGenerator CreateCodeGenerator() {
     return null;
   }
@@ -72,7 +54,7 @@ public override void Compile(Program dafnyProgram, ConcreteSyntaxTree output) {
       throw new UnsupportedFeatureException(dafnyProgram.GetStartOfFirstFileToken(), Feature.LegacyCLI);
     }
 
-    var dooFile = new DooFile(ProgramAfterParsing);
+    var dooFile = new DooFile(dafnyProgram.AfterParsingClone);
     dooFile.Write(output);
   }
 
@@ -81,10 +63,10 @@ public override void EmitCallToMain(Method mainMethod, string baseName, Concrete
   }
 
   private string DooFilePath(string dafnyProgramName) {
-    return Path.GetFullPath(Path.ChangeExtension(dafnyProgramName, ".doo"));
+    return Path.GetFullPath(Path.ChangeExtension(dafnyProgramName, DooFile.Extension));
   }
 
-  public override Task<(bool Success, object CompilationResult)> CompileTargetProgram(string dafnyProgramName,
+  public override async Task<(bool Success, object CompilationResult)> CompileTargetProgram(string dafnyProgramName,
     string targetProgramText, string callToMain,
     string targetFilename,
     ReadOnlyCollection<string> otherFileNames, bool runAfterCompile, TextWriter outputWriter) {
@@ -94,8 +76,11 @@ private string DooFilePath(string dafnyProgramName) {
 
     File.Delete(dooPath);
     ZipFile.CreateFromDirectory(targetDirectory, dooPath);
+    if (Options.Verbose) {
+      await outputWriter.WriteLineAsync($"Wrote Dafny library to {dooPath}");
+    }
 
-    return Task.FromResult((true, (object)null));
+    return (true, null);
   }
 
   public override Task<bool> RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain,

Source/DafnyCore/Dafny.atg

@@ -223,7 +223,7 @@ Dafny
                                    string basePath = parsedFile.Scheme == "stdin" ? "" : Path.GetDirectoryName(parsedFile.LocalPath);
                                    includedFile = Path.Combine(basePath, includedFile);
                                  }
-                                 var oneInclude = new Include(t, parsedFile, new Uri(Path.GetFullPath(includedFile)));
+                                 var oneInclude = new Include(t, parsedFile, new Uri(Path.GetFullPath(includedFile)), theOptions);
                                  oneInclude.RangeToken = new RangeToken(includeStartToken, t);
                                  theModule.Includes.Add(oneInclude);
                                }