diff --git a/Source/DafnyCore/AST/Grammar/IFileSystem.cs b/Source/DafnyCore/AST/Grammar/IFileSystem.cs
index 5af553b872d..99b9f56ec8c 100644
--- a/Source/DafnyCore/AST/Grammar/IFileSystem.cs
+++ b/Source/DafnyCore/AST/Grammar/IFileSystem.cs
@@ -1,5 +1,9 @@
 using System;
+using System.Collections.Generic;
 using System.IO;
+using System.Linq;
+using DafnyCore.Options;
+using Microsoft.Dafny.LanguageServer.Workspace;
 using Microsoft.Extensions.FileSystemGlobbing.Abstractions;
 
 namespace Microsoft.Dafny;
@@ -11,6 +15,32 @@ public interface IFileSystem {
   DirectoryInfoBase GetDirectoryInfoBase(string root);
 }
 
+public class InMemoryFileSystem : IFileSystem {
+  private readonly IReadOnlyDictionary<Uri, string> files;
+
+  public InMemoryFileSystem(IReadOnlyDictionary<Uri, string> files) {
+    this.files = files;
+  }
+
+  public TextReader ReadFile(Uri uri) {
+    if (files.TryGetValue(uri, out var entry)) {
+      return new StringReader(entry);
+    }
+
+    return OnDiskFileSystem.Instance.ReadFile(uri);
+  }
+
+  public bool Exists(Uri path) {
+    return files.ContainsKey(path) || OnDiskFileSystem.Instance.Exists(path);
+  }
+
+  public DirectoryInfoBase GetDirectoryInfoBase(string root) {
+    var inMemoryFiles = files.Keys.Select(openFileUri => openFileUri.LocalPath);
+    var inMemory = new InMemoryDirectoryInfoFromDotNet8(root, inMemoryFiles);
+    return new CombinedDirectoryInfo(new[] { inMemory, OnDiskFileSystem.Instance.GetDirectoryInfoBase(root) });
+  }
+}
+
 public class OnDiskFileSystem : IFileSystem {
   public static readonly IFileSystem Instance = new OnDiskFileSystem();
 
diff --git a/Source/DafnyCore/AST/Grammar/ProgramParser.cs b/Source/DafnyCore/AST/Grammar/ProgramParser.cs
index eeb69d5ea44..a8a63493001 100644
--- a/Source/DafnyCore/AST/Grammar/ProgramParser.cs
+++ b/Source/DafnyCore/AST/Grammar/ProgramParser.cs
@@ -1,5 +1,6 @@
 using System;
 using System.Collections.Generic;
+using System.Collections.Immutable;
 using System.Diagnostics.Contracts;
 using System.IO;
 using System.Linq;
@@ -255,14 +256,7 @@ CancellationToken cancellationToken
   }
 
   private DafnyFile IncludeToDafnyFile(SystemModuleManager systemModuleManager, ErrorReporter errorReporter, Include include) {
-    try {
-      return new DafnyFile(systemModuleManager.Options, include.IncludedFilename, include.tok,
-        () => fileSystem.ReadFile(include.IncludedFilename));
-    } catch (IllegalDafnyFile) {
-      errorReporter.Error(MessageSource.Parser, include.tok,
-        $"Unable to open the include {include.IncludedFilename}.");
-      return null;
-    }
+    return DafnyFile.CreateAndValidate(errorReporter, fileSystem, systemModuleManager.Options, include.IncludedFilename, include.tok);
   }
 
   ///<summary>
@@ -317,7 +311,9 @@ private static Parser SetupParser(bool parseAsDooFile, string s /*!*/, Uri uri /
   }
 
   public Program Parse(string source, Uri uri, ErrorReporter reporter) {
-    var files = new[] { new DafnyFile(reporter.Options, uri, null, () => new StringReader(source)) };
+    var fs = new InMemoryFileSystem(ImmutableDictionary<Uri, string>.Empty.Add(uri, source));
+    var file = DafnyFile.CreateAndValidate(reporter, fs, reporter.Options, uri, Token.NoToken);
+    var files = file == null ? Array.Empty<DafnyFile>() : new[] { file };
     return ParseFiles(uri.ToString(), files, reporter, CancellationToken.None);
   }
 }
diff --git a/Source/DafnyCore/AST/Tokens.cs b/Source/DafnyCore/AST/Tokens.cs
index fd014c323ca..d268539e3d9 100644
--- a/Source/DafnyCore/AST/Tokens.cs
+++ b/Source/DafnyCore/AST/Tokens.cs
@@ -57,6 +57,7 @@ public class Token : IToken {
 
   public Token peekedTokens; // Used only internally by Coco when the scanner "peeks" tokens. Normally null at the end of parsing
   public static readonly Token NoToken = new Token();
+  public static readonly Token Cli = new Token();
   public Token() : this(0, 0) { }
 
   public Token(int linenum, int colnum) {
@@ -193,6 +194,10 @@ public int CompareTo(IToken other) {
 public static class TokenExtensions {
 
   public static string TokenToString(this IToken tok, DafnyOptions options) {
+    if (tok == Token.Cli) {
+      return "CLI";
+    }
+
     if (tok.Uri == null) {
       return $"({tok.line},{tok.col - 1})";
     }
diff --git a/Source/DafnyCore/DafnyConsolePrinter.cs b/Source/DafnyCore/DafnyConsolePrinter.cs
index 87744bb3028..36bb9f21513 100644
--- a/Source/DafnyCore/DafnyConsolePrinter.cs
+++ b/Source/DafnyCore/DafnyConsolePrinter.cs
@@ -68,7 +68,8 @@ private string GetFileLine(Uri uri, int lineIndex) {
       try {
         // Note: This is not guaranteed to be the same file that Dafny parsed. To ensure that, Dafny should keep
         // an in-memory version of each file it parses.
-        var reader = new DafnyFile(options, uri).GetContent();
+        var file = DafnyFile.CreateAndValidate(new ErrorReporterSink(options), OnDiskFileSystem.Instance, options, uri, Token.NoToken);
+        var reader = file.GetContent();
         lines = Util.Lines(reader).ToList();
       } catch (Exception) {
         lines = new List<string>();
diff --git a/Source/DafnyCore/DafnyFile.cs b/Source/DafnyCore/DafnyFile.cs
index 0aecd6cacbd..86fd840876e 100644
--- a/Source/DafnyCore/DafnyFile.cs
+++ b/Source/DafnyCore/DafnyFile.cs
@@ -10,9 +10,9 @@
 namespace Microsoft.Dafny;
 
 public class DafnyFile {
-  public string FilePath { get; private set; }
+  public string FilePath => CanonicalPath;
   public string Extension { get; private set; }
-  public string CanonicalPath { get; private set; }
+  public string CanonicalPath { get; }
   public string BaseName { get; private set; }
   public bool IsPreverified { get; set; }
   public bool IsPrecompiled { get; set; }
@@ -21,56 +21,62 @@ public class DafnyFile {
   public Uri Uri { get; }
   [CanBeNull] public IToken Origin { get; }
 
-  public DafnyFile(DafnyOptions options, Uri uri, [CanBeNull] IToken origin = null, Func<TextReader> getContentOverride = null) {
-    Uri = uri;
-    Origin = origin;
+  public static DafnyFile CreateAndValidate(ErrorReporter reporter, IFileSystem fileSystem,
+    DafnyOptions options, Uri uri, IToken origin) {
     var filePath = uri.LocalPath;
 
-    Extension = ".dfy";
+    origin ??= Token.NoToken;
+
+    string canonicalPath;
+    string baseName;
+    Func<TextReader> getContent = null;
+    bool isPreverified;
+    bool isPrecompiled;
+    var isPrerefined = false;
+    var extension = ".dfy";
     if (uri.IsFile) {
-      Extension = Path.GetExtension(uri.LocalPath).ToLower();
-      BaseName = Path.GetFileName(uri.LocalPath);
+      extension = Path.GetExtension(uri.LocalPath).ToLower();
+      baseName = Path.GetFileName(uri.LocalPath);
       // Normalizing symbolic links appears to be not
       // supported in .Net APIs, because it is very difficult in general
       // So we will just use the absolute path, lowercased for all file systems.
       // cf. IncludeComparer.CompareTo
-      CanonicalPath = Canonicalize(filePath).LocalPath;
+      canonicalPath = Canonicalize(filePath).LocalPath;
     } else if (uri.Scheme == "stdin") {
-      getContentOverride = () => options.Input;
-      BaseName = "<stdin>";
-      CanonicalPath = "<stdin>";
+      getContent = () => options.Input;
+      baseName = "<stdin>";
+      canonicalPath = "<stdin>";
     } else if (uri.Scheme == "dllresource") {
-      Extension = Path.GetExtension(uri.LocalPath).ToLower();
-      BaseName = uri.LocalPath;
-      CanonicalPath = uri.ToString();
+      extension = Path.GetExtension(uri.LocalPath).ToLower();
+      baseName = uri.LocalPath;
+      canonicalPath = uri.ToString();
+    } else {
+      canonicalPath = "";
+      baseName = "";
     }
 
-    FilePath = CanonicalPath;
-
     var filePathForErrors = options.UseBaseNameForFileName ? Path.GetFileName(filePath) : filePath;
-    if (getContentOverride != null) {
-      IsPreverified = false;
-      IsPrecompiled = false;
-      GetContent = getContentOverride;
-    } else if (Extension == ".dfy" || Extension == ".dfyi") {
-      IsPreverified = false;
-      IsPrecompiled = false;
-      if (!File.Exists(filePath)) {
+    if (getContent != null) {
+      isPreverified = false;
+      isPrecompiled = false;
+    } else if (uri.Scheme == "untitled" || extension == ".dfy" || extension == ".dfyi") {
+      isPreverified = false;
+      isPrecompiled = false;
+      if (!fileSystem.Exists(uri)) {
         if (0 < options.VerifySnapshots) {
           // For snapshots, we first create broken DafnyFile without content,
           // then look for the real files and create DafnuFiles for them.
-          // TODO prevent creating the broken DafnyFiles for snapshots
-          return;
+          return new DafnyFile(extension, canonicalPath, baseName, null, uri, origin);
         }
 
-        options.Printer.ErrorWriteLine(options.OutputWriter, $"*** Error: file {filePathForErrors} not found");
-        throw new IllegalDafnyFile(true);
-      } else {
-        GetContent = () => new StreamReader(filePath);
+        reporter.Error(MessageSource.Project, origin, $"file {filePathForErrors} not found");
+        return null;
       }
-    } else if (Extension == ".doo") {
-      IsPreverified = true;
-      IsPrecompiled = false;
+
+      getContent = () => fileSystem.ReadFile(uri);
+    } else if (extension == ".doo") {
+      isPreverified = true;
+      isPrecompiled = false;
 
       DooFile dooFile;
       if (uri.Scheme == "dllresource") {
@@ -84,16 +90,16 @@ public DafnyFile(DafnyOptions options, Uri uri, [CanBeNull] IToken origin = null
 
         dooFile = DooFile.Read(stream);
       } else {
-        if (!File.Exists(filePath)) {
-          options.Printer.ErrorWriteLine(options.OutputWriter, $"*** Error: file {filePathForErrors} not found");
-          throw new IllegalDafnyFile(true);
+        if (!fileSystem.Exists(uri)) {
+          reporter.Error(MessageSource.Project, origin, $"file {filePathForErrors} not found");
+          return null;
         }
 
         dooFile = DooFile.Read(filePath);
       }
 
-      if (!dooFile.Validate(filePathForErrors, options, options.CurrentCommand)) {
-        throw new IllegalDafnyFile(true);
+      if (!dooFile.Validate(reporter, filePathForErrors, options, options.CurrentCommand, origin)) {
+        return null;
       }
 
       // For now it's simpler to let the rest of the pipeline parse the
@@ -102,19 +108,37 @@ public DafnyFile(DafnyOptions options, Uri uri, [CanBeNull] IToken origin = null
       // more efficiently inside a .doo file, at which point
       // the DooFile class should encapsulate the serialization logic better
       // and expose a Program instead of the program text.
-      GetContent = () => new StringReader(dooFile.ProgramText);
-      IsPrerefined = true;
-    } else if (Extension == ".dll") {
-      IsPreverified = true;
+      getContent = () => new StringReader(dooFile.ProgramText);
+      isPrerefined = true;
+    } else if (extension == ".dll") {
+      isPreverified = true;
       // Technically only for C#, this is for backwards compatability
-      IsPrecompiled = true;
+      isPrecompiled = true;
 
       var sourceText = GetDafnySourceAttributeText(filePath);
-      if (sourceText == null) { throw new IllegalDafnyFile(); }
-      GetContent = () => new StringReader(sourceText);
+      if (sourceText == null) {
+        return null;
+      }
+      getContent = () => new StringReader(sourceText);
     } else {
-      throw new IllegalDafnyFile();
+      return null;
     }
+
+    return new DafnyFile(extension, canonicalPath, baseName, getContent, uri, origin) {
+      IsPrecompiled = isPrecompiled,
+      IsPreverified = isPreverified,
+      IsPrerefined = isPrerefined
+    };
+  }
+
+  protected DafnyFile(string extension, string canonicalPath, string baseName,
+    Func<TextReader> getContent, Uri uri, [CanBeNull] IToken origin) {
+    Extension = extension;
+    CanonicalPath = canonicalPath;
+    BaseName = baseName;
+    GetContent = getContent;
+    Uri = uri;
+    Origin = origin;
   }
 
   // Returns a canonical string for the given file path, namely one which is the same
@@ -155,7 +179,7 @@ public static List<string> FileNames(IReadOnlyList<DafnyFile> dafnyFiles) {
 
   private static string GetDafnySourceAttributeText(string dllPath) {
     if (!File.Exists(dllPath)) {
-      throw new IllegalDafnyFile();
+      return null;
     }
     using var dllFs = new FileStream(dllPath, FileMode.Open, FileAccess.Read, FileShare.ReadWrite);
     using var dllPeReader = new PEReader(dllFs);
diff --git a/Source/DafnyCore/DafnyMain.cs b/Source/DafnyCore/DafnyMain.cs
index cb1041961c4..e29a5bbb703 100644
--- a/Source/DafnyCore/DafnyMain.cs
+++ b/Source/DafnyCore/DafnyMain.cs
@@ -21,15 +21,10 @@
 
 namespace Microsoft.Dafny {
 
-  public class IllegalDafnyFile : Exception {
-    public bool ProcessingError { get; }
-
-    public IllegalDafnyFile(bool processingError = false) {
-      this.ProcessingError = processingError;
-    }
-  }
-
   public class DafnyMain {
+    public static readonly string StandardLibrariesDooUriBase = "dllresource://DafnyPipeline/DafnyStandardLibraries";
+    public static readonly Uri StandardLibrariesDooUri = new("dllresource://DafnyPipeline/DafnyStandardLibraries.doo");
+    public static readonly Uri StandardLibrariesArithmeticDooUri = new("dllresource://DafnyPipeline/DafnyStandardLibraries-arithmetic.doo");
 
     public static void MaybePrintProgram(Program program, string filename, bool afterResolver) {
       if (filename == null) {
diff --git a/Source/DafnyCore/DooFile.cs b/Source/DafnyCore/DooFile.cs
index b4f05dd9a53..05859951a44 100644
--- a/Source/DafnyCore/DooFile.cs
+++ b/Source/DafnyCore/DooFile.cs
@@ -116,14 +116,17 @@ public DooFile(Program dafnyProgram) {
   private DooFile() {
   }
 
-  public bool Validate(string filePath, DafnyOptions options, Command currentCommand) {
+  public bool Validate(ErrorReporter reporter, string filePath, DafnyOptions options, Command currentCommand,
+    IToken origin) {
     if (currentCommand == null) {
-      options.Printer.ErrorWriteLine(Console.Out, $"Cannot load {filePath}: .doo files cannot be used with the legacy CLI");
+      reporter.Error(MessageSource.Project, origin,
+        $"Cannot load {filePath}: .doo files cannot be used with the legacy CLI");
       return false;
     }
 
     if (options.VersionNumber != Manifest.DafnyVersion) {
-      options.Printer.ErrorWriteLine(Console.Out, $"Cannot load {filePath}: it was built with Dafny {Manifest.DafnyVersion}, which cannot be used by Dafny {options.VersionNumber}");
+      reporter.Error(MessageSource.Project, origin,
+        $"cannot load {filePath}: it was built with Dafny {Manifest.DafnyVersion}, which cannot be used by Dafny {options.VersionNumber}");
       return false;
     }
 
@@ -141,7 +144,7 @@ public bool Validate(string filePath, DafnyOptions options, Command currentComma
 
       object libraryValue = null;
       if (Manifest.Options.TryGetValue(option.Name, out var manifestValue)) {
-        if (!TomlUtil.TryGetValueFromToml(Console.Out, null,
+        if (!TomlUtil.TryGetValueFromToml(reporter, origin, null,
               option.Name, option.ValueType, manifestValue, out libraryValue)) {
           return false;
         }
@@ -149,7 +152,7 @@ public bool Validate(string filePath, DafnyOptions options, Command currentComma
         // This can happen because Tomlyn will drop aggregate properties with no values.
         libraryValue = Array.Empty<string>();
       }
-      success = success && check(options, option, localValue, filePath, libraryValue);
+      success = success && check(reporter, origin, option, localValue, filePath, libraryValue);
     }
     return success;
   }
@@ -208,40 +211,39 @@ public void Write(string path) {
   // more difficult to completely categorize, which is the main reason the LibraryBackend
   // is restricted to only the new CLI.
 
-  public delegate bool OptionCheck(DafnyOptions options, Option option, object localValue, string libraryFile, object libraryValue);
+  public delegate bool OptionCheck(ErrorReporter reporter, IToken origin, Option option, object localValue, string libraryFile, object libraryValue);
   private static readonly Dictionary<Option, OptionCheck> OptionChecks = new();
   private static readonly HashSet<Option> NoChecksNeeded = new();
 
-  public static bool CheckOptionMatches(DafnyOptions options, Option option, object localValue, string libraryFile, object libraryValue) {
+  public static bool CheckOptionMatches(ErrorReporter reporter, IToken origin, Option option, object localValue, string libraryFile, object libraryValue) {
     if (OptionValuesEqual(option, localValue, libraryValue)) {
       return true;
     }
 
-    options.Printer.ErrorWriteLine(options.OutputWriter, $"*** Error: Cannot load {libraryFile}: --{option.Name} is set locally to {OptionValueToString(option, localValue)}, but the library was built with {OptionValueToString(option, libraryValue)}");
+    reporter.Error(MessageSource.Project, origin, $"cannot load {libraryFile}: --{option.Name} is set locally to {OptionValueToString(option, localValue)}, but the library was built with {OptionValueToString(option, libraryValue)}");
     return false;
   }
 
   /// Checks that the library option ==> the local option.
   /// E.g. --no-verify: the only incompatibility is if it's on in the library but not locally.
   /// Generally the right check for options that weaken guarantees.
-  public static bool CheckOptionLibraryImpliesLocal(DafnyOptions options, Option option, object localValue, string libraryFile, object libraryValue) {
+  public static bool CheckOptionLibraryImpliesLocal(ErrorReporter reporter, IToken origin, Option option, object localValue, string libraryFile, object libraryValue) {
     if (OptionValuesImplied(option, libraryValue, localValue)) {
       return true;
     }
 
-    options.Printer.ErrorWriteLine(options.OutputWriter, $"*** Error: Cannot load {libraryFile}: --{option.Name} is set locally to {OptionValueToString(option, localValue)}, but the library was built with {OptionValueToString(option, libraryValue)}");
+    reporter.Error(MessageSource.Project, origin, $"cannot load {libraryFile}: --{option.Name} is set locally to {OptionValueToString(option, localValue)}, but the library was built with {OptionValueToString(option, libraryValue)}");
     return false;
   }
 
   /// Checks that the local option ==> the library option.
   /// E.g. --track-print-effects: the only incompatibility is if it's on locally but not in the library.
   /// Generally the right check for options that strengthen guarantees.
-  public static bool CheckOptionLocalImpliesLibrary(DafnyOptions options, Option option, object localValue, string libraryFile, object libraryValue) {
+  public static bool CheckOptionLocalImpliesLibrary(ErrorReporter reporter, IToken origin, Option option, object localValue, string libraryFile, object libraryValue) {
     if (OptionValuesImplied(option, localValue, libraryValue)) {
       return true;
     }
-
-    options.Printer.ErrorWriteLine(options.OutputWriter, $"*** Error: Cannot load {libraryFile}: --{option.Name} is set locally to {OptionValueToString(option, localValue)}, but the library was built with {OptionValueToString(option, libraryValue)}");
+    reporter.Error(MessageSource.Project, origin, $"cannot load {libraryFile}: --{option.Name} is set locally to {OptionValueToString(option, localValue)}, but the library was built with {OptionValueToString(option, libraryValue)}");
     return false;
   }
 
diff --git a/Source/DafnyLanguageServer/Workspace/CombinedDirectoryInfo.cs b/Source/DafnyCore/Generic/CombinedDirectoryInfo.cs
similarity index 96%
rename from Source/DafnyLanguageServer/Workspace/CombinedDirectoryInfo.cs
rename to Source/DafnyCore/Generic/CombinedDirectoryInfo.cs
index 21e17eb25f1..a5e89877746 100644
--- a/Source/DafnyLanguageServer/Workspace/CombinedDirectoryInfo.cs
+++ b/Source/DafnyCore/Generic/CombinedDirectoryInfo.cs
@@ -1,3 +1,4 @@
+#nullable enable
 using System;
 using System.Collections.Generic;
 using System.IO;
@@ -11,7 +12,7 @@ namespace Microsoft.Dafny.LanguageServer.Workspace;
 /// The order in which the filesystems are given matters,
 /// when multiple filesystem contain the same file, the first containing filesystem returns it.
 /// </summary>
-class CombinedDirectoryInfo : DirectoryInfoBase {
+public class CombinedDirectoryInfo : DirectoryInfoBase {
   public DirectoryInfoBase[] Parts { get; }
 
   public CombinedDirectoryInfo(DirectoryInfoBase[] parts) {
diff --git a/Source/DafnyCore/Generic/Reporting.cs b/Source/DafnyCore/Generic/Reporting.cs
index 3f31bd655f8..858e4253a7e 100644
--- a/Source/DafnyCore/Generic/Reporting.cs
+++ b/Source/DafnyCore/Generic/Reporting.cs
@@ -13,7 +13,7 @@ public enum ErrorLevel {
   }
 
   public enum MessageSource {
-    Parser, Cloner, RefinementTransformer, Rewriter, Resolver, Translator, Verifier, Compiler, Documentation, TestGeneration
+    Project, Parser, Cloner, RefinementTransformer, Rewriter, Resolver, Translator, Verifier, Compiler, Documentation, TestGeneration
   }
 
   public record DafnyRelatedInformation(IToken Token, string Message);
diff --git a/Source/DafnyCore/Generic/TomlUtil.cs b/Source/DafnyCore/Generic/TomlUtil.cs
index c3f4fbf9e6b..b5cf6f8dab0 100644
--- a/Source/DafnyCore/Generic/TomlUtil.cs
+++ b/Source/DafnyCore/Generic/TomlUtil.cs
@@ -2,23 +2,26 @@
 using System.Collections.Generic;
 using System.IO;
 using System.Linq;
+using Microsoft.Dafny;
 using Tomlyn.Model;
+using Type = System.Type;
 
 namespace DafnyCore.Generic;
 
 public static class TomlUtil {
 
-  public static bool TryGetValueFromToml(TextWriter errorWriter, string sourceDir, string tomlPath, Type type, object tomlValue, out object value) {
+  public static bool TryGetValueFromToml(ErrorReporter reporter, IToken origin, string sourceDir, string tomlPath,
+    Type type, object tomlValue, out object value) {
     if (tomlValue == null) {
       value = null;
       return false;
     }
 
     if (type.IsAssignableFrom(typeof(List<string>))) {
-      return TryGetListValueFromToml<string>(errorWriter, sourceDir, tomlPath, (TomlArray)tomlValue, out value);
+      return TryGetListValueFromToml<string>(reporter, origin, sourceDir, tomlPath, (TomlArray)tomlValue, out value);
     }
     if (type.IsAssignableFrom(typeof(List<FileInfo>))) {
-      return TryGetListValueFromToml<FileInfo>(errorWriter, sourceDir, tomlPath, (TomlArray)tomlValue, out value);
+      return TryGetListValueFromToml<FileInfo>(reporter, origin, sourceDir, tomlPath, (TomlArray)tomlValue, out value);
     }
 
     if (tomlValue is string tomlString) {
@@ -46,8 +49,7 @@ public static bool TryGetValueFromToml(TextWriter errorWriter, string sourceDir,
         value = tomlValue.ToString();
         return true;
       }
-      errorWriter.WriteLine(
-        $"Error: property '{tomlPath}' is of type '{tomlValue.GetType()}' but should be of type '{type}'");
+      reporter.Error(MessageSource.Project, origin, $"property '{tomlPath}' is of type '{tomlValue.GetType()}' but should be of type '{type}'");
       value = null;
       return false;
     }
@@ -56,10 +58,10 @@ public static bool TryGetValueFromToml(TextWriter errorWriter, string sourceDir,
     return true;
   }
 
-  private static bool TryGetListValueFromToml<T>(TextWriter errorWriter, string sourceDir, string tomlPath, TomlArray tomlValue, out object value) {
+  private static bool TryGetListValueFromToml<T>(ErrorReporter reporter, IToken origin, string sourceDir, string tomlPath, TomlArray tomlValue, out object value) {
     var success = true;
     value = tomlValue.Select((e, i) => {
-      if (TryGetValueFromToml(errorWriter, sourceDir, $"{tomlPath}[{i}]", typeof(T), e, out var elementValue)) {
+      if (TryGetValueFromToml(reporter, origin, sourceDir, $"{tomlPath}[{i}]", typeof(T), e, out var elementValue)) {
         return (T)elementValue;
       }
       success = false;
diff --git a/Source/DafnyDriver/Commands/DafnyCli.cs b/Source/DafnyDriver/Commands/DafnyCli.cs
index a8da490ff95..893e429eb41 100644
--- a/Source/DafnyDriver/Commands/DafnyCli.cs
+++ b/Source/DafnyDriver/Commands/DafnyCli.cs
@@ -31,10 +31,6 @@ public static class DafnyCli {
   private const string ToolchainDebuggingHelpName = "--help-internal";
   private static readonly RootCommand RootCommand = new("The Dafny CLI enables working with Dafny, a verification-aware programming language. Use 'dafny -?' to see help for the previous CLI format.");
 
-  private static readonly string StandardLibrariesDooUriBase = "dllresource://DafnyPipeline/DafnyStandardLibraries";
-  private static readonly Uri StandardLibrariesDooUri = new("dllresource://DafnyPipeline/DafnyStandardLibraries.doo");
-  private static readonly Uri StandardLibrariesArithmeticDooUri = new("dllresource://DafnyPipeline/DafnyStandardLibraries-arithmetic.doo");
-
   public static int Main(string[] args) {
     return MainWithWriters(Console.Out, Console.Error, Console.In, args);
   }
@@ -388,7 +384,7 @@ public static ExitValue GetDafnyFiles(DafnyOptions options,
     if (options.UseStdin) {
       var uri = new Uri("stdin:///");
       options.CliRootSourceUris.Add(uri);
-      dafnyFiles.Add(new DafnyFile(options, uri));
+      dafnyFiles.Add(DafnyFile.CreateAndValidate(new ConsoleErrorReporter(options), OnDiskFileSystem.Instance, options, uri, Token.NoToken));
     } else if (options.CliRootSourceUris.Count == 0) {
       options.Printer.ErrorWriteLine(options.ErrorWriter, "*** Error: No input files were specified in command-line. " + options.Environment);
       return ExitValue.PREPROCESSING_ERROR;
@@ -417,24 +413,26 @@ public static ExitValue GetDafnyFiles(DafnyOptions options,
       var nameToShow = useRelative ? relative
         : Path.GetRelativePath(Directory.GetCurrentDirectory(), file);
       try {
-        var df = new DafnyFile(options, new Uri(Path.GetFullPath(file)));
-        if (options.LibraryFiles.Contains(file)) {
-          df.IsPreverified = true;
-          df.IsPrecompiled = true;
-        }
-        if (!filesSeen.Add(df.CanonicalPath)) {
-          continue; // silently ignore duplicate
+        var consoleErrorReporter = new ConsoleErrorReporter(options);
+        var df = DafnyFile.CreateAndValidate(consoleErrorReporter, OnDiskFileSystem.Instance, options, new Uri(Path.GetFullPath(file)), Token.Cli);
+        if (df == null) {
+          if (consoleErrorReporter.HasErrors) {
+            return ExitValue.PREPROCESSING_ERROR;
+          }
+        } else {
+          if (options.LibraryFiles.Contains(file)) {
+            df.IsPreverified = true;
+            df.IsPrecompiled = true;
+          }
+          if (!filesSeen.Add(df.CanonicalPath)) {
+            continue; // silently ignore duplicate
+          }
+          dafnyFiles.Add(df);
+          isDafnyFile = true;
         }
-        dafnyFiles.Add(df);
-        isDafnyFile = true;
       } catch (ArgumentException e) {
         options.Printer.ErrorWriteLine(options.ErrorWriter, "*** Error: {0}: ", nameToShow, e.Message);
         return ExitValue.PREPROCESSING_ERROR;
-      } catch (IllegalDafnyFile e) {
-        if (e.ProcessingError) {
-          return ExitValue.PREPROCESSING_ERROR;
-        }
-        // Fall through and try to handle the file as an "other file"
       } catch (Exception e) {
         options.Printer.ErrorWriteLine(options.ErrorWriter, "*** Error: {0}: {1}", nameToShow, e.Message);
         return ExitValue.PREPROCESSING_ERROR;
@@ -489,18 +487,19 @@ public static ExitValue GetDafnyFiles(DafnyOptions options,
     // only because if they are added first, one might be used as the program name,
     // which is not handled well.
     if (options.Get(CommonOptionBag.UseStandardLibraries)) {
+      var reporter = new ConsoleErrorReporter(options);
       if (options.CompilerName is null or "cs" or "java" or "go" or "py" or "js") {
         var targetName = options.CompilerName ?? "notarget";
-        var stdlibDooUri = new Uri($"{StandardLibrariesDooUriBase}-{targetName}.doo");
+        var stdlibDooUri = new Uri($"{DafnyMain.StandardLibrariesDooUriBase}-{targetName}.doo");
         options.CliRootSourceUris.Add(stdlibDooUri);
-        dafnyFiles.Add(new DafnyFile(options, stdlibDooUri));
+        dafnyFiles.Add(DafnyFile.CreateAndValidate(reporter, OnDiskFileSystem.Instance, options, stdlibDooUri, Token.Cli));
       }
 
-      options.CliRootSourceUris.Add(StandardLibrariesDooUri);
-      dafnyFiles.Add(new DafnyFile(options, StandardLibrariesDooUri));
+      options.CliRootSourceUris.Add(DafnyMain.StandardLibrariesDooUri);
+      dafnyFiles.Add(DafnyFile.CreateAndValidate(reporter, OnDiskFileSystem.Instance, options, DafnyMain.StandardLibrariesDooUri, Token.Cli));
 
-      options.CliRootSourceUris.Add(StandardLibrariesArithmeticDooUri);
-      dafnyFiles.Add(new DafnyFile(options, StandardLibrariesArithmeticDooUri));
+      options.CliRootSourceUris.Add(DafnyMain.StandardLibrariesArithmeticDooUri);
+      dafnyFiles.Add(DafnyFile.CreateAndValidate(reporter, OnDiskFileSystem.Instance, options, DafnyMain.StandardLibrariesArithmeticDooUri, Token.Cli));
     }
 
     return ExitValue.SUCCESS;
diff --git a/Source/DafnyDriver/Commands/FormatCommand.cs b/Source/DafnyDriver/Commands/FormatCommand.cs
index 41c5db82295..873ea6b6516 100644
--- a/Source/DafnyDriver/Commands/FormatCommand.cs
+++ b/Source/DafnyDriver/Commands/FormatCommand.cs
@@ -43,10 +43,7 @@ public static async Task<ExitValue> DoFormatting(DafnyOptions options) {
 
     var exitValue = ExitValue.SUCCESS;
     Contract.Assert(dafnyFiles.Count > 0 || options.SourceFolders.Count > 0);
-    dafnyFiles = dafnyFiles.Concat(options.SourceFolders.SelectMany(folderPath => {
-      return Directory.GetFiles(folderPath, "*.dfy", SearchOption.AllDirectories)
-          .Select(name => new DafnyFile(options, new Uri(name))).ToList();
-    })).ToList();
+    dafnyFiles = dafnyFiles.Concat(options.SourceFolders.SelectMany(folderPath => GetFilesForFolder(options, folderPath))).ToList();
 
     var failedToParseFiles = new List<string>();
     var emptyFiles = new List<string>();
@@ -71,7 +68,8 @@ public static async Task<ExitValue> DoFormatting(DafnyOptions options) {
       if (dafnyFile.Uri.Scheme == "stdin") {
         tempFileName = Path.GetTempFileName() + ".dfy";
         CompilerDriver.WriteFile(tempFileName, await Console.In.ReadToEndAsync());
-        dafnyFile = new DafnyFile(options, new Uri(tempFileName));
+        dafnyFile = DafnyFile.CreateAndValidate(new ConsoleErrorReporter(options),
+          OnDiskFileSystem.Instance, options, new Uri(tempFileName), Token.NoToken);
       }
 
       using var content = dafnyFile.GetContent();
@@ -155,4 +153,10 @@ await options.OutputWriter.WriteLineAsync(neededFormatting > 0
 
     return exitValue;
   }
+
+  public static IEnumerable<DafnyFile> GetFilesForFolder(DafnyOptions options, string folderPath) {
+    return Directory.GetFiles(folderPath, "*.dfy", SearchOption.AllDirectories)
+      .Select(name => DafnyFile.CreateAndValidate(new ConsoleErrorReporter(options), OnDiskFileSystem.Instance,
+        options, new Uri(name), Token.Cli));
+  }
 }
diff --git a/Source/DafnyDriver/CompilerDriver.cs b/Source/DafnyDriver/CompilerDriver.cs
index ac06e8fea31..c8c38c1e3d5 100644
--- a/Source/DafnyDriver/CompilerDriver.cs
+++ b/Source/DafnyDriver/CompilerDriver.cs
@@ -129,7 +129,7 @@ private async Task<ExitValue> ProcessFilesAsync(IReadOnlyList<DafnyFile/*!*/>/*!
           var snapshots = new List<DafnyFile>();
           foreach (var f in s) {
             var uri = new Uri(Path.GetFullPath(f));
-            snapshots.Add(new DafnyFile(options, uri));
+            snapshots.Add(DafnyFile.CreateAndValidate(new ConsoleErrorReporter(options), OnDiskFileSystem.Instance, options, uri, Token.Cli));
             options.CliRootSourceUris.Add(uri);
           }
           var ev = await ProcessFilesAsync(snapshots, new List<string>().AsReadOnly(), options, depManager, false, programId);
diff --git a/Source/DafnyDriver/CoverageReporter.cs b/Source/DafnyDriver/CoverageReporter.cs
index 7f176264c4a..fca297cb4b7 100644
--- a/Source/DafnyDriver/CoverageReporter.cs
+++ b/Source/DafnyDriver/CoverageReporter.cs
@@ -317,7 +317,7 @@ private void CopyStyleFiles(string baseDirectory) {
   }
 
   private string HtmlReportForFile(CoverageReport report, Uri uri, string baseDirectory, string linksToOtherReports) {
-    var dafnyFile = new DafnyFile(options, uri);
+    var dafnyFile = DafnyFile.CreateAndValidate(new ConsoleErrorReporter(options), OnDiskFileSystem.Instance, options, uri, Token.Cli);
     var source = dafnyFile.GetContent().ReadToEnd();
     var lines = source.Split(new[] { Environment.NewLine }, StringSplitOptions.None);
     var characterLabels = new CoverageLabel[lines.Length][];
diff --git a/Source/DafnyDriver/DafnyDoc.cs b/Source/DafnyDriver/DafnyDoc.cs
index 57beaddc438..1b7e470b215 100644
--- a/Source/DafnyDriver/DafnyDoc.cs
+++ b/Source/DafnyDriver/DafnyDoc.cs
@@ -59,10 +59,8 @@ public static async Task<ExitValue> DoDocumenting(DafnyOptions options) {
 
     // Collect all the dafny files; dafnyFiles already includes files from a .toml project file
     var exitValue = ExitValue.SUCCESS;
-    dafnyFiles = dafnyFiles.Concat(dafnyFolders.SelectMany(folderPath => {
-      return Directory.GetFiles(folderPath, "*.dfy", SearchOption.AllDirectories)
-          .Select(name => new DafnyFile(options, new Uri(Path.GetFullPath(name)))).ToList();
-    })).ToList();
+    dafnyFiles = dafnyFiles.Concat(dafnyFolders.SelectMany(folderPath =>
+      FormatCommand.GetFilesForFolder(options, folderPath))).ToList();
     await Console.Out.WriteAsync($"Documenting {dafnyFiles.Count} files from {dafnyFolders.Count} folders\n");
     if (dafnyFiles.Count == 0) {
       return exitValue;
diff --git a/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs b/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs
index e48570e2a1b..4404a095232 100644
--- a/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs
+++ b/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs
@@ -137,18 +137,25 @@ private static void ApplyDefaultOptionValues(DafnyOptions dafnyOptions) {
     }
 
     protected static TextDocumentItem CreateTestDocument(string source, string filePath = null, int version = 1) {
+      DocumentUri uri;
       if (filePath == null) {
         var index = Interlocked.Increment(ref fileIndex);
         filePath = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName(), $"testFile{index}.dfy");
       }
-      if (string.IsNullOrEmpty(Path.GetDirectoryName(filePath))) {
-        filePath = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName(), filePath);
+
+      if (filePath.StartsWith("untitled:")) {
+        uri = DocumentUri.Parse(filePath);
+      } else {
+        if (string.IsNullOrEmpty(Path.GetDirectoryName(filePath))) {
+          filePath = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName(), filePath);
+        }
+        filePath = Path.GetFullPath(filePath);
+        uri = DocumentUri.FromFileSystemPath(filePath);
       }
-      filePath = Path.GetFullPath(filePath);
       return new TextDocumentItem {
         LanguageId = LanguageId,
         Text = source,
-        Uri = filePath.StartsWith("untitled:") ? DocumentUri.Parse(filePath) : DocumentUri.FromFileSystemPath(filePath),
+        Uri = uri,
         Version = version
       };
     }
diff --git a/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs b/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs
index 921b76b22fb..3e90f7188db 100644
--- a/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs
+++ b/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs
@@ -718,7 +718,7 @@ public async Task OpeningDocumentThatIncludesNonExistentDocumentReportsParserErr
       await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
       var diagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken);
       Assert.Single(diagnostics);
-      Assert.Equal("Parser", diagnostics[0].Source);
+      Assert.Equal("Project", diagnostics[0].Source);
       Assert.Equal(DiagnosticSeverity.Error, diagnostics[0].Severity);
       Assert.Equal(new Range((0, 8), (0, 26)), diagnostics[0].Range);
       await AssertNoDiagnosticsAreComing(CancellationToken);
diff --git a/Source/DafnyLanguageServer.Test/Diagnostics/ProjectFileDiagnosticsTest.cs b/Source/DafnyLanguageServer.Test/Diagnostics/ProjectFileDiagnosticsTest.cs
new file mode 100644
index 00000000000..23fce2cb9ef
--- /dev/null
+++ b/Source/DafnyLanguageServer.Test/Diagnostics/ProjectFileDiagnosticsTest.cs
@@ -0,0 +1,71 @@
+using System;
+using System.IO;
+using System.Linq;
+using System.Threading.Tasks;
+using Microsoft.Dafny.LanguageServer.IntegrationTest.Util;
+using Microsoft.Extensions.Logging;
+using OmniSharp.Extensions.LanguageServer.Protocol;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
+using Xunit;
+using Xunit.Abstractions;
+using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range;
+
+namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization;
+
+public class ProjectFileDiagnosticsTest : ClientBasedLanguageServerTest {
+
+  [Fact]
+  public async Task ProjectFileErrorIsShown() {
+    var projectFileSource = @"includes = [stringWithoutQuotes]";
+    var projectFile = await CreateOpenAndWaitForResolve(projectFileSource, DafnyProject.FileName);
+    var diagnostics = await GetLastDiagnostics(projectFile, DiagnosticSeverity.Error);
+    Assert.Single(diagnostics);
+    Assert.Equal(new Range(0, 0, 0, 0), diagnostics.First().Range);
+    Assert.Contains("contains the following errors", diagnostics.First().Message);
+  }
+
+  [Fact]
+  public async Task ProjectFileErrorIsShownFromDafnyFile() {
+    var projectFileSource = @"includes = [stringWithoutQuotes]";
+    var directory = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName());
+    Directory.CreateDirectory(directory);
+    var projectFilePath = Path.Combine(directory, DafnyProject.FileName);
+    await File.WriteAllTextAsync(projectFilePath, projectFileSource);
+    await CreateOpenAndWaitForResolve("method Foo() { }", Path.Combine(directory, "ProjectFileErrorIsShownFromDafnyFile.dfy"));
+    var diagnostics = await diagnosticsReceiver.AwaitNextNotificationAsync(CancellationToken);
+    Assert.Equal(DocumentUri.File(projectFilePath), diagnostics.Uri.GetFileSystemPath());
+    Assert.Equal(2, diagnostics.Diagnostics.Count());
+    Assert.Equal(new Range(0, 0, 0, 0), diagnostics.Diagnostics.First().Range);
+    Assert.Contains(diagnostics.Diagnostics, d => d.Message.Contains("contains the following errors"));
+    Assert.Contains(diagnostics.Diagnostics, d => d.Message.Contains($"Files referenced by project are:{Environment.NewLine}ProjectFileErrorIsShownFromDafnyFile.dfy"));
+  }
+
+  [Fact]
+  public async Task IncludeNotFound() {
+    var projectFile = @"
+includes = [""doesNotExist.dfy""]
+".TrimStart();
+
+    var project = CreateAndOpenTestDocument(projectFile, DafnyProject.FileName);
+    var diagnostics = await GetLastDiagnostics(project);
+    Assert.Single(diagnostics);
+    Assert.Contains("references no files", diagnostics[0].Message);
+  }
+
+  [Fact]
+  public async Task LibraryNotFound() {
+    var projectFile = @"
+[options]
+library = [""doesNotExist.dfy""]
+".TrimStart();
+
+    var project = CreateAndOpenTestDocument(projectFile, DafnyProject.FileName);
+    var diagnostics = await GetLastDiagnostics(project, DiagnosticSeverity.Error);
+    Assert.Single(diagnostics);
+    Assert.Contains("not found", diagnostics[0].Message);
+  }
+
+  public ProjectFileDiagnosticsTest(ITestOutputHelper output, LogLevel dafnyLogLevel = LogLevel.Information)
+    : base(output, dafnyLogLevel) {
+  }
+}
\ No newline at end of file
diff --git a/Source/DafnyLanguageServer.Test/MultipleFilesNoProjectTest.cs b/Source/DafnyLanguageServer.Test/MultipleFilesNoProjectTest.cs
index b0871e9762c..2a0f808fdec 100644
--- a/Source/DafnyLanguageServer.Test/MultipleFilesNoProjectTest.cs
+++ b/Source/DafnyLanguageServer.Test/MultipleFilesNoProjectTest.cs
@@ -48,7 +48,7 @@ method Bar() {
     await client.OpenDocumentAndWaitAsync(consumer3, CancellationToken);
     var consumer3Diagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken, consumer3);
     Assert.Single(consumer3Diagnostics);
-    Assert.Contains("Unable to open", consumer3Diagnostics[0].Message);
+    Assert.Contains("not found", consumer3Diagnostics[0].Message);
   }
 
   public MultipleFilesNoProjectTest(ITestOutputHelper output) : base(output) {
diff --git a/Source/DafnyLanguageServer.Test/ProjectFiles/MultipleFilesProjectTest.cs b/Source/DafnyLanguageServer.Test/ProjectFiles/MultipleFilesProjectTest.cs
index a60069e0792..a7003bfdddd 100644
--- a/Source/DafnyLanguageServer.Test/ProjectFiles/MultipleFilesProjectTest.cs
+++ b/Source/DafnyLanguageServer.Test/ProjectFiles/MultipleFilesProjectTest.cs
@@ -330,7 +330,7 @@ method Bar() {
     var consumer3 = await CreateOpenAndWaitForResolve(consumerSource, Path.Combine(Directory.GetCurrentDirectory(), "consumer3.dfy"));
     var consumer3Diagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken, consumer3);
     Assert.Single(consumer3Diagnostics);
-    Assert.Contains("Unable to open", consumer3Diagnostics[0].Message);
+    Assert.Contains("not found", consumer3Diagnostics[0].Message);
   }
 
   public MultipleFilesProjectTest(ITestOutputHelper output) : base(output) {
diff --git a/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs b/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs
index fa835d40b0e..6b748c9ccd4 100644
--- a/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs
+++ b/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs
@@ -1,11 +1,9 @@
-using System;
 using System.IO;
 using System.Linq;
 using System.Threading.Tasks;
 using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions;
 using Microsoft.Dafny.LanguageServer.IntegrationTest.Util;
 using Microsoft.Dafny.LanguageServer.Workspace;
-using OmniSharp.Extensions.LanguageServer.Protocol;
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 using Xunit;
 using Xunit.Abstractions;
@@ -16,29 +14,32 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest;
 public class ProjectFilesTest : ClientBasedLanguageServerTest {
 
   [Fact]
-  public async Task ProjectFileErrorIsShown() {
-    var projectFileSource = @"includes = [stringWithoutQuotes]";
-    var projectFile = await CreateOpenAndWaitForResolve(projectFileSource, DafnyProject.FileName);
-    var diagnostics = await GetLastDiagnostics(projectFile, DiagnosticSeverity.Error);
-    Assert.Single(diagnostics);
-    Assert.Equal(new Range(0, 0, 0, 0), diagnostics.First().Range);
-    Assert.Contains("contains the following errors", diagnostics.First().Message);
-  }
+  public async Task ProducerLibrary() {
+    var libraryDirectory = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName());
+    var producerSource = @"
+module Producer {
+  const x := 3
+}".TrimStart();
+    Directory.CreateDirectory(libraryDirectory);
+    var producerPath = Path.Combine(libraryDirectory, "producer.dfy").Replace("\\", "/");
+    await File.WriteAllTextAsync(producerPath, producerSource);
+    var consumerSource = @"
+module Consumer {
+  import opened Producer
+  const y := x + 2
+}".TrimStart();
 
-  [Fact]
-  public async Task ProjectFileErrorIsShownFromDafnyFile() {
-    var projectFileSource = @"includes = [stringWithoutQuotes]";
-    var directory = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName());
-    Directory.CreateDirectory(directory);
-    var projectFilePath = Path.Combine(directory, DafnyProject.FileName);
-    await File.WriteAllTextAsync(projectFilePath, projectFileSource);
-    await CreateOpenAndWaitForResolve("method Foo() { }", Path.Combine(directory, "ProjectFileErrorIsShownFromDafnyFile.dfy"));
-    var diagnostics = await diagnosticsReceiver.AwaitNextNotificationAsync(CancellationToken);
-    Assert.Equal(DocumentUri.File(projectFilePath), diagnostics.Uri.GetFileSystemPath());
-    Assert.Equal(2, diagnostics.Diagnostics.Count());
-    Assert.Equal(new Range(0, 0, 0, 0), diagnostics.Diagnostics.First().Range);
-    Assert.Contains(diagnostics.Diagnostics, d => d.Message.Contains("contains the following errors"));
-    Assert.Contains(diagnostics.Diagnostics, d => d.Message.Contains($"Files referenced by project are:{Environment.NewLine}ProjectFileErrorIsShownFromDafnyFile.dfy"));
+    var projectFileSource = $@"
+[options]
+library = [""{producerPath}""]".TrimStart();
+
+    var consumerDirectory = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName());
+    Directory.CreateDirectory(consumerDirectory);
+    await File.WriteAllTextAsync(Path.Combine(consumerDirectory, "consumer.dfy"), consumerSource);
+    var projectFile = await CreateOpenAndWaitForResolve(projectFileSource, Path.Combine(consumerDirectory, DafnyProject.FileName));
+    await Task.Delay(ProjectManagerDatabase.ProjectFileCacheExpiryTime);
+
+    await AssertNoDiagnosticsAreComing(CancellationToken);
   }
 
   /// <summary>
diff --git a/Source/DafnyLanguageServer.Test/Unit/CompilationManagerTest.cs b/Source/DafnyLanguageServer.Test/Unit/CompilationManagerTest.cs
index 85d59dd6f73..967c98b12ab 100644
--- a/Source/DafnyLanguageServer.Test/Unit/CompilationManagerTest.cs
+++ b/Source/DafnyLanguageServer.Test/Unit/CompilationManagerTest.cs
@@ -14,10 +14,11 @@ public class CompilationManagerTest {
   public async Task CancelUnstartedCompilationLeadsToCancelledTasks() {
     var dafnyOptions = DafnyOptions.Create(TextWriter.Null, TextReader.Null);
     var compilationManager = new Compilation(new Mock<ILogger<Compilation>>().Object,
+      new Mock<IFileSystem>().Object,
       new Mock<ITextDocumentLoader>().Object,
       new Mock<IProgramVerifier>().Object,
-      dafnyOptions,
-      null, new CompilationInput(dafnyOptions, 0, new DafnyProject() { Uri = new Uri(Directory.GetCurrentDirectory()) }, new Uri[] { }));
+      null, new CompilationInput(dafnyOptions, 0,
+        new DafnyProject() { Uri = new Uri(Directory.GetCurrentDirectory()) }));
     compilationManager.CancelPendingUpdates();
     await Assert.ThrowsAsync<TaskCanceledException>(() => compilationManager.Program);
   }
diff --git a/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs b/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs
index f58ef32cd22..ec10c4c2a2b 100644
--- a/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs
+++ b/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs
@@ -4,10 +4,12 @@
 using Moq;
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 using System;
+using System.Collections.Immutable;
 using System.IO;
 using System.Threading;
 using System.Threading.Tasks;
 using DafnyCore.Test;
+using Microsoft.Boogie;
 using Microsoft.Extensions.Logging;
 using OmniSharp.Extensions.LanguageServer.Protocol;
 using Xunit;
@@ -62,11 +64,10 @@ private static DocumentTextBuffer CreateTestDocument() {
     public async Task LoadReturnsCanceledTaskIfOperationIsCanceled() {
       var source = new CancellationTokenSource();
       parser.Setup(p => p.Parse(
-          It.IsAny<CompilationInput>(),
-          It.IsAny<ErrorReporter>(),
+          It.IsAny<Compilation>(),
           It.IsAny<CancellationToken>())).Callback(() => source.Cancel())
         .Throws<TaskCanceledException>();
-      var task = textDocumentLoader.ParseAsync(new ErrorReporterSink(DafnyOptions.Default), GetCompilation(), source.Token);
+      var task = textDocumentLoader.ParseAsync(GetCompilation(), source.Token);
       try {
         await task;
         Assert.Fail("document load was not cancelled");
@@ -77,19 +78,27 @@ public async Task LoadReturnsCanceledTaskIfOperationIsCanceled() {
       }
     }
 
-    private static CompilationInput GetCompilation() {
+    private Compilation GetCompilation() {
       var versionedTextDocumentIdentifier = CreateTestDocumentId();
-      var compilation = new CompilationInput(DafnyOptions.Default, 0, ProjectManagerDatabase.ImplicitProject(versionedTextDocumentIdentifier.Uri.ToUri()), new[] { versionedTextDocumentIdentifier.Uri.ToUri() });
+      var uri = versionedTextDocumentIdentifier.Uri.ToUri();
+      var fs = new InMemoryFileSystem(ImmutableDictionary<Uri, string>.Empty.Add(uri, ""));
+      var file = DafnyFile.CreateAndValidate(new ErrorReporterSink(DafnyOptions.Default), fs, DafnyOptions.Default, uri, Token.NoToken);
+      var input = new CompilationInput(DafnyOptions.Default, 0,
+        ProjectManagerDatabase.ImplicitProject(uri));
+      var engine = new ExecutionEngine(DafnyOptions.Default, new VerificationResultCache(),
+        CustomStackSizePoolTaskScheduler.Create(0, 0));
+      var compilation = new Compilation(new Mock<ILogger<Compilation>>().Object, new Mock<IFileSystem>().Object, textDocumentLoader,
+        new Mock<IProgramVerifier>().Object, engine, input);
+      compilation.RootFiles = new[] { file };
       return compilation;
     }
 
     [Fact]
     public async Task LoadReturnsFaultedTaskIfAnyExceptionOccured() {
-      parser.Setup(p => p.Parse(It.IsAny<CompilationInput>(),
-          It.IsAny<ErrorReporter>(),
+      parser.Setup(p => p.Parse(It.IsAny<Compilation>(),
           It.IsAny<CancellationToken>()))
         .Throws<InvalidOperationException>();
-      var task = textDocumentLoader.ParseAsync(new ErrorReporterSink(DafnyOptions.Default), GetCompilation(), default);
+      var task = textDocumentLoader.ParseAsync(GetCompilation(), default);
       try {
         await task;
         Assert.Fail("document load did not fail");
diff --git a/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs b/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs
index 8298c0f4875..1e7a492828a 100644
--- a/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs
+++ b/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs
@@ -298,7 +298,7 @@ protected void ApplyChanges(ref TextDocumentItem documentItem, List<Change> chan
   }
 
   protected async Task AssertNoVerificationStatusIsComing(TextDocumentItem documentItem, CancellationToken cancellationToken) {
-    var verificationDocumentItem = CreateTestDocument("method Foo() { assert false; }", $"verification{fileIndex++}.dfy");
+    var verificationDocumentItem = CreateTestDocument("method Foo() { assert false; }", $"verificationStatus{fileIndex++}.dfy");
     await client.OpenDocumentAndWaitAsync(verificationDocumentItem, cancellationToken);
     var statusReport = await verificationStatusReceiver.AwaitNextNotificationAsync(cancellationToken);
     try {
diff --git a/Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs b/Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs
index f469726284c..4ff9d1db531 100644
--- a/Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs
+++ b/Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs
@@ -214,7 +214,7 @@ public async Task DocumentWithOnlyConfiguredVerifierTimeoutSendsCompilationSucce
       await WaitForStatus(null, PublishedVerificationStatus.Error, CancellationToken, documentItem);
     }
 
-    [Fact(Timeout = MaxTestExecutionTimeMs)]
+    [Fact]
     public async Task DocumentLoadWithOnSaveVerificationDoesNotSendVerificationStatuses() {
       var source = @"
 method Abs(x: int) returns (y: int)
@@ -232,14 +232,14 @@ method Abs(x: int) returns (y: int)
       await AssertProgress(documentItem1, CompilationStatus.ResolutionStarted);
       await AssertProgress(documentItem1, CompilationStatus.ResolutionSucceeded);
       await WaitForStatus(null, PublishedVerificationStatus.Stale, CancellationToken, documentItem1);
-      var documentItem2 = CreateTestDocument(source, "test_2dfy");
+      var documentItem2 = CreateTestDocument(source, "test_2.dfy");
       await client.OpenDocumentAndWaitAsync(documentItem2, CancellationToken);
       await AssertProgress(documentItem2, CompilationStatus.ResolutionStarted);
       await AssertProgress(documentItem2, CompilationStatus.ResolutionSucceeded);
       await WaitForStatus(null, PublishedVerificationStatus.Stale, CancellationToken, documentItem2);
     }
 
-    [Fact(Timeout = MaxTestExecutionTimeMs)]
+    [Fact]
     public async Task DocumentLoadAndSaveWithNeverVerifySendsNoVerificationStatuses() {
       var source = @"
 method Abs(x: int) returns (y: int)
@@ -258,7 +258,7 @@ method Abs(x: int) returns (y: int)
       await AssertProgress(documentItem1, CompilationStatus.ResolutionStarted);
       await AssertProgress(documentItem1, CompilationStatus.ResolutionSucceeded);
       await WaitForStatus(null, PublishedVerificationStatus.Stale, CancellationToken, documentItem1);
-      var documentItem2 = CreateTestDocument(source, "test_2dfy");
+      var documentItem2 = CreateTestDocument(source, "test_2.dfy");
       await client.OpenDocumentAndWaitAsync(documentItem2, CancellationToken);
       await client.SaveDocumentAndWaitAsync(documentItem2, CancellationToken);
       await AssertProgress(documentItem2, CompilationStatus.ResolutionStarted);
diff --git a/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs b/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs
index 62a5af7fec7..8e0a8bd0727 100644
--- a/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs
+++ b/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs
@@ -117,8 +117,8 @@ public CrashingLoader(ExceptionTests tests, TextDocumentLoader loader) {
       this.loader = loader;
     }
 
-    public Task<Program> ParseAsync(ErrorReporter reporter, CompilationInput compilation, CancellationToken cancellationToken) {
-      return loader.ParseAsync(reporter, compilation, cancellationToken);
+    public Task<Program> ParseAsync(Compilation compilation, CancellationToken cancellationToken) {
+      return loader.ParseAsync(compilation, cancellationToken);
     }
 
     public Task<ResolutionResult> ResolveAsync(CompilationInput input,
diff --git a/Source/DafnyLanguageServer.Test/Various/StandardLibrary.cs b/Source/DafnyLanguageServer.Test/Various/StandardLibrary.cs
new file mode 100644
index 00000000000..9d5b144ae02
--- /dev/null
+++ b/Source/DafnyLanguageServer.Test/Various/StandardLibrary.cs
@@ -0,0 +1,37 @@
+using System.IO;
+using System.Threading.Tasks;
+using Microsoft.Dafny.LanguageServer.IntegrationTest.Util;
+using Microsoft.Extensions.Logging;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
+using Xunit;
+using Xunit.Abstractions;
+
+namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various;
+
+public class StandardLibrary : ClientBasedLanguageServerTest {
+  [Fact]
+  public async Task CanUseWrappers() {
+    var source = @"
+import opened DafnyStdLibs.Wrappers
+
+method Foo() returns (s: Option<int>) { 
+  return Some(3); 
+}".TrimStart();
+
+    var projectSource = @"
+[options]
+standard-libraries = true";
+
+    var withoutStandardLibraries = CreateAndOpenTestDocument(source);
+    var diagnostics1 = await GetLastDiagnostics(withoutStandardLibraries);
+    Assert.Single(diagnostics1);
+
+    var directory = Path.GetTempFileName();
+    CreateAndOpenTestDocument(projectSource, Path.Combine(directory, DafnyProject.FileName));
+    CreateAndOpenTestDocument(source, Path.Combine(directory, "document.dfy"));
+    await AssertNoDiagnosticsAreComing(CancellationToken);
+  }
+
+  public StandardLibrary(ITestOutputHelper output, LogLevel dafnyLogLevel = LogLevel.Information) : base(output, dafnyLogLevel) {
+  }
+}
\ No newline at end of file
diff --git a/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs b/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs
index 77472ea225b..98dace07a08 100644
--- a/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs
+++ b/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs
@@ -35,7 +35,7 @@ public async Task<CounterExampleList> Handle(CounterExampleParams request, Cance
           var uri = request.TextDocument.Uri.ToUri();
           await projectManager.VerifyEverythingAsync(uri);
 
-          var state = await projectManager.States.Select(s => s.Value).
+          var state = await projectManager.States.
             Where(s => FinishedVerifyingUri(s, uri)).FirstAsync();
           logger.LogDebug($"counter-example handler retrieved IDE state, " +
                           $"canVerify count: {state.VerificationResults[uri].Count}, " +
diff --git a/Source/DafnyLanguageServer/Language/DafnyLangParser.cs b/Source/DafnyLanguageServer/Language/DafnyLangParser.cs
index 5949a7c1448..106bafce449 100644
--- a/Source/DafnyLanguageServer/Language/DafnyLangParser.cs
+++ b/Source/DafnyLanguageServer/Language/DafnyLangParser.cs
@@ -1,11 +1,8 @@
 using Microsoft.Extensions.Logging;
 using System;
 using System.Collections.Generic;
-using System.Diagnostics;
 using System.IO;
-using System.Linq;
 using System.Threading;
-using System.Threading.Tasks;
 using Microsoft.Dafny.LanguageServer.Language.Symbols;
 using Microsoft.Dafny.LanguageServer.Workspace;
 
@@ -37,25 +34,25 @@ public DafnyLangParser(DafnyOptions options, IFileSystem fileSystem, ITelemetryP
         : new ProgramParser(innerParserLogger, fileSystem);
     }
 
-    public Program Parse(CompilationInput compilation, ErrorReporter reporter, CancellationToken cancellationToken) {
+    public Program Parse(Compilation compilation, CancellationToken cancellationToken) {
       mutex.Wait(cancellationToken);
 
       var beforeParsing = DateTime.Now;
       try {
-        var rootSourceUris = compilation.RootUris;
+        var rootFiles = compilation.RootFiles!;
         List<DafnyFile> dafnyFiles = new();
-        foreach (var rootSourceUri in rootSourceUris) {
+        foreach (var rootFile in rootFiles) {
           try {
-            dafnyFiles.Add(new DafnyFile(reporter.Options, rootSourceUri, null, () => fileSystem.ReadFile(rootSourceUri)));
+            dafnyFiles.Add(rootFile);
             if (logger.IsEnabled(LogLevel.Trace)) {
-              logger.LogTrace($"Parsing file with uri {rootSourceUri} and content\n{fileSystem.ReadFile(rootSourceUri).ReadToEnd()}");
+              logger.LogTrace($"Parsing file with uri {rootFile.Uri} and content\n{rootFile.GetContent().ReadToEnd()}");
             }
           } catch (IOException) {
-            logger.LogError($"Tried to parse file {rootSourceUri} that could not be found");
+            logger.LogError($"Tried to parse file {rootFile} that could not be found");
           }
         }
 
-        return programParser.ParseFiles(compilation.Project.ProjectName, dafnyFiles, reporter, cancellationToken);
+        return programParser.ParseFiles(compilation.Project.ProjectName, dafnyFiles, compilation.Reporter, cancellationToken);
       }
       finally {
         telemetryPublisher.PublishTime("Parse", compilation.Project.Uri.ToString(), DateTime.Now - beforeParsing);
diff --git a/Source/DafnyLanguageServer/Language/IDafnyParser.cs b/Source/DafnyLanguageServer/Language/IDafnyParser.cs
index c296e4c0a4e..0b091b50419 100644
--- a/Source/DafnyLanguageServer/Language/IDafnyParser.cs
+++ b/Source/DafnyLanguageServer/Language/IDafnyParser.cs
@@ -11,7 +11,6 @@ namespace Microsoft.Dafny.LanguageServer.Language {
   /// Any implementation has to guarantee thread-safety of its public members.
   /// </remarks>
   public interface IDafnyParser {
-    Program Parse(CompilationInput compilation, ErrorReporter reporter,
-      CancellationToken cancellationToken);
+    Program Parse(Compilation compilation, CancellationToken cancellationToken);
   }
 }
diff --git a/Source/DafnyLanguageServer/Language/LanguageServerExtensions.cs b/Source/DafnyLanguageServer/Language/LanguageServerExtensions.cs
index 5b346d0b9de..9927349211a 100644
--- a/Source/DafnyLanguageServer/Language/LanguageServerExtensions.cs
+++ b/Source/DafnyLanguageServer/Language/LanguageServerExtensions.cs
@@ -40,11 +40,12 @@ private static IServiceCollection WithDafnyLanguage(this IServiceCollection serv
             serviceProvider.GetRequiredService<INotificationPublisher>(),
             compilation))
         .AddSingleton(CreateVerifier)
-        .AddSingleton<CreateCompilation>(serviceProvider => (options, engine, compilation) => new Compilation(
+        .AddSingleton<CreateCompilation>(serviceProvider => (engine, compilation) => new Compilation(
           serviceProvider.GetRequiredService<ILogger<Compilation>>(),
+          serviceProvider.GetRequiredService<IFileSystem>(),
           serviceProvider.GetRequiredService<ITextDocumentLoader>(),
           serviceProvider.GetRequiredService<IProgramVerifier>(),
-          options, engine, compilation
+          engine, compilation
           ))
         .AddSingleton<ISymbolTableFactory, SymbolTableFactory>()
         .AddSingleton<IGhostStateDiagnosticCollector, GhostStateDiagnosticCollector>();
diff --git a/Source/DafnyLanguageServer/Workspace/BoogieUpdate.cs b/Source/DafnyLanguageServer/Workspace/BoogieUpdate.cs
index f72c88cfacf..e8b2b6f5d95 100644
--- a/Source/DafnyLanguageServer/Workspace/BoogieUpdate.cs
+++ b/Source/DafnyLanguageServer/Workspace/BoogieUpdate.cs
@@ -3,6 +3,7 @@
 using System.Collections.Immutable;
 using System.IO;
 using System.Linq;
+using System.Threading.Tasks;
 using Microsoft.Boogie;
 using Microsoft.Dafny.LanguageServer.Language;
 using Microsoft.Extensions.Logging;
@@ -11,12 +12,13 @@
 
 namespace Microsoft.Dafny.LanguageServer.Workspace;
 
-record BoogieUpdate(ICanVerify CanVerify, IImplementationTask Task, IVerificationStatus BoogieStatus)
+record BoogieUpdate(ICanVerify CanVerify, IImplementationTask ImplementationTask, IVerificationStatus BoogieStatus)
   : ICompilationEvent {
-  public IdeState UpdateState(DafnyOptions options, ILogger logger, IdeState previousState) {
+  public Task<IdeState> UpdateState(DafnyOptions options, ILogger logger, IProjectDatabase projectDatabase,
+    IdeState previousState) {
     UpdateGutterIconTrees(options, logger, previousState);
 
-    var name = Compilation.GetImplementationName(Task.Implementation);
+    var name = Compilation.GetImplementationName(ImplementationTask.Implementation);
     var status = StatusFromBoogieStatus(BoogieStatus);
     var uri = CanVerify.Tok.Uri;
     var range = CanVerify.NameToken.GetLspRange();
@@ -35,32 +37,32 @@ public IdeState UpdateState(DafnyOptions options, ILogger logger, IdeState previ
     if (BoogieStatus is BatchCompleted batchCompleted) {
       counterExamples = counterExamples.Concat(batchCompleted.VcResult.counterExamples);
       hitErrorLimit |= batchCompleted.VcResult.maxCounterExamples == batchCompleted.VcResult.counterExamples.Count;
-      var newDiagnostics = GetDiagnosticsFromResult(options, previousState, Task, batchCompleted.VcResult).ToArray();
+      var newDiagnostics = GetDiagnosticsFromResult(options, previousState, ImplementationTask, batchCompleted.VcResult).ToArray();
       diagnostics = diagnostics.Concat(newDiagnostics.Select(d => d.ToLspDiagnostic())).ToList();
       logger.LogTrace($"BatchCompleted received for {previousState.Input} and found #{newDiagnostics.Length} new diagnostics.");
     }
     var view = new IdeImplementationView(range, status, diagnostics.ToList(), previousView.HitErrorLimit || hitErrorLimit);
-    return previousState with {
+    return Task.FromResult(previousState with {
       Counterexamples = counterExamples,
       VerificationResults = previousState.VerificationResults.SetItem(uri, previousState.VerificationResults[uri].SetItem(range, previousVerificationResult with {
         Implementations = previousVerificationResult.Implementations.SetItem(name, view)
       }))
-    };
+    });
   }
 
   private void UpdateGutterIconTrees(DafnyOptions options, ILogger logger, IdeState previousState) {
     var gutterIconManager = new GutterIconAndHoverVerificationDetailsManager(logger);
     if (BoogieStatus is Running) {
-      gutterIconManager.ReportVerifyImplementationRunning(previousState, Task.Implementation);
+      gutterIconManager.ReportVerifyImplementationRunning(previousState, ImplementationTask.Implementation);
     }
 
     if (BoogieStatus is BatchCompleted batchCompleted) {
       gutterIconManager.ReportAssertionBatchResult(previousState,
-        new AssertionBatchResult(Task.Implementation, batchCompleted.VcResult));
+        new AssertionBatchResult(ImplementationTask.Implementation, batchCompleted.VcResult));
     }
 
     if (BoogieStatus is Completed completed) {
-      var tokenString = BoogieGenerator.ToDafnyToken(true, Task.Implementation.tok).TokenToString(options);
+      var tokenString = BoogieGenerator.ToDafnyToken(true, ImplementationTask.Implementation.tok).TokenToString(options);
       var verificationResult = completed.Result;
       // Sometimes, the boogie status is set as Completed
       // but the assertion batches were not reported yet.
@@ -71,10 +73,10 @@ private void UpdateGutterIconTrees(DafnyOptions options, ILogger logger, IdeStat
         logger.LogDebug(
           $"Possibly duplicate reporting assertion batch {result.vcNum} as completed in {tokenString}, version {previousState.Version}");
         gutterIconManager.ReportAssertionBatchResult(previousState,
-          new AssertionBatchResult(Task.Implementation, result));
+          new AssertionBatchResult(ImplementationTask.Implementation, result));
       }
 
-      gutterIconManager.ReportEndVerifyImplementation(previousState, Task.Implementation, verificationResult);
+      gutterIconManager.ReportEndVerifyImplementation(previousState, ImplementationTask.Implementation, verificationResult);
     }
   }
 
diff --git a/Source/DafnyLanguageServer/Workspace/CanVerifyPartsIdentified.cs b/Source/DafnyLanguageServer/Workspace/CanVerifyPartsIdentified.cs
index 73d284f57e1..ae17ee81f61 100644
--- a/Source/DafnyLanguageServer/Workspace/CanVerifyPartsIdentified.cs
+++ b/Source/DafnyLanguageServer/Workspace/CanVerifyPartsIdentified.cs
@@ -2,6 +2,7 @@
 using System.Collections.Generic;
 using System.Collections.Immutable;
 using System.Linq;
+using System.Threading.Tasks;
 using Microsoft.Boogie;
 using Microsoft.Dafny.LanguageServer.Language;
 using Microsoft.Dafny.LanguageServer.Workspace.Notifications;
@@ -11,7 +12,8 @@
 namespace Microsoft.Dafny.LanguageServer.Workspace;
 
 record CanVerifyPartsIdentified(ICanVerify CanVerify, IReadOnlyList<IImplementationTask> Parts) : ICompilationEvent {
-  public IdeState UpdateState(DafnyOptions options, ILogger logger, IdeState previousState) {
+  public Task<IdeState> UpdateState(DafnyOptions options, ILogger logger, IProjectDatabase projectDatabase,
+    IdeState previousState) {
     var implementations = Parts.Select(t => t.Implementation);
     var gutterIconManager = new GutterIconAndHoverVerificationDetailsManager(logger);
 
@@ -30,8 +32,8 @@ public IdeState UpdateState(DafnyOptions options, ILogger logger, IdeState previ
             previous?.Diagnostics ?? Array.Empty<Diagnostic>(),
             previous?.HitErrorLimit ?? false);
         }));
-    return previousState with {
+    return Task.FromResult(previousState with {
       VerificationResults = previousState.VerificationResults.SetItem(uri, previousState.VerificationResults[uri].SetItem(range, verificationResult))
-    };
+    });
   }
 }
\ No newline at end of file
diff --git a/Source/DafnyLanguageServer/Workspace/Compilation.cs b/Source/DafnyLanguageServer/Workspace/Compilation.cs
index df520666a40..271599edb69 100644
--- a/Source/DafnyLanguageServer/Workspace/Compilation.cs
+++ b/Source/DafnyLanguageServer/Workspace/Compilation.cs
@@ -2,6 +2,7 @@
 using System.Collections.Concurrent;
 using System.Collections.Generic;
 using System.Collections.Immutable;
+using System.IO;
 using System.Linq;
 using System.Reactive;
 using System.Reactive.Disposables;
@@ -9,9 +10,9 @@
 using System.Threading;
 using System.Threading.Tasks;
 using Microsoft.Boogie;
+using Microsoft.Dafny.Compilers;
 using Microsoft.Dafny.LanguageServer.Language;
 using Microsoft.Dafny.LanguageServer.Util;
-using Microsoft.Dafny.LanguageServer.Workspace.Notifications;
 using Microsoft.Extensions.Logging;
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range;
@@ -19,22 +20,19 @@
 namespace Microsoft.Dafny.LanguageServer.Workspace;
 
 public delegate Compilation CreateCompilation(
-  DafnyOptions options,
   ExecutionEngine boogieEngine,
   CompilationInput compilation);
 
 /// <summary>
-/// The compilation of a single document version.
-/// The document will be parsed, resolved, translated to Boogie and verified.
+/// The compilation of a single version of a program
+/// After calling Start, the document will be parsed and resolved.
 ///
-/// Compilation may be configured to pause after translation,
-/// requiring a call to Compilation.VerifySymbol for the document to be verified.
-///
-/// Compilation is agnostic to document updates, it does not handle the migration of old document state.
+/// To verify a symbol, VerifySymbol must be called.
 /// </summary>
 public class Compilation : IDisposable {
 
   private readonly ILogger logger;
+  private readonly IFileSystem fileSystem;
   private readonly ITextDocumentLoader documentLoader;
   private readonly IProgramVerifier verifier;
 
@@ -53,8 +51,9 @@ public DafnyDiagnostic[] GetDiagnosticsForUri(Uri uri) =>
   private readonly ConcurrentDictionary<ICanVerify, Unit> verifyingOrVerifiedSymbols = new();
   private readonly LazyConcurrentDictionary<ICanVerify, Dictionary<string, IImplementationTask>> implementationsPerVerifiable = new();
 
-  private readonly DafnyOptions options;
+  private DafnyOptions Options => Input.Options;
   public CompilationInput Input { get; }
+  public DafnyProject Project => Input.Project;
   private readonly ExecutionEngine boogieEngine;
 
   private readonly Subject<ICompilationEvent> updates = new();
@@ -62,26 +61,36 @@ public DafnyDiagnostic[] GetDiagnosticsForUri(Uri uri) =>
 
   private Program? programAfterParsing;
   private Program? transformedProgram;
-  private IDisposable staticDiagnosticsSubscription = Disposable.Empty;
+  private readonly IDisposable staticDiagnosticsSubscription;
 
   public Task<Program> Program { get; }
   public Task<ResolutionResult> Resolution { get; }
 
+  public ErrorReporter Reporter => errorReporter;
+
+  public IReadOnlyList<DafnyFile>? RootFiles { get; set; }
+
   public Compilation(
     ILogger<Compilation> logger,
+    IFileSystem fileSystem,
     ITextDocumentLoader documentLoader,
     IProgramVerifier verifier,
-    DafnyOptions options,
     ExecutionEngine boogieEngine,
     CompilationInput input
     ) {
-    this.options = options;
     Input = input;
     this.boogieEngine = boogieEngine;
 
     this.documentLoader = documentLoader;
     this.logger = logger;
+    this.fileSystem = fileSystem;
     this.verifier = verifier;
+
+    errorReporter = new ObservableErrorReporter(Options, Project.Uri);
+    errorReporter.Updates.Subscribe(updates);
+    staticDiagnosticsSubscription = errorReporter.Updates.Subscribe(newDiagnostic =>
+      staticDiagnostics.GetOrAdd(newDiagnostic.Uri, _ => new()).Push(newDiagnostic.Diagnostic));
+
     cancellationSource = new();
     cancellationSource.Token.Register(() => started.TrySetCanceled(cancellationSource.Token));
 
@@ -92,25 +101,78 @@ CompilationInput input
   }
 
   public void Start() {
+    Project.Errors.CopyDiagnostics(errorReporter);
+    RootFiles = DetermineRootFiles();
+    updates.OnNext(new DeterminedRootFiles(Project, RootFiles!, GetDiagnosticsCopy()));
     started.TrySetResult();
   }
 
+  private ImmutableDictionary<Uri, ImmutableList<Diagnostic>> GetDiagnosticsCopy() {
+    return staticDiagnostics.ToImmutableDictionary(k => k.Key,
+      kv => kv.Value.Select(d => d.ToLspDiagnostic()).ToImmutableList());
+  }
+
+  private IReadOnlyList<DafnyFile> DetermineRootFiles() {
+    var result = new List<DafnyFile>();
+
+    foreach (var uri in Input.Project.GetRootSourceUris(fileSystem)) {
+      var file = DafnyFile.CreateAndValidate(errorReporter, fileSystem, Options, uri, Project.StartingToken);
+      if (file != null) {
+        result.Add(file);
+      }
+    }
+
+    foreach (var uri in Options.CliRootSourceUris) {
+      var file = DafnyFile.CreateAndValidate(errorReporter, fileSystem, Options, uri, Token.Cli);
+      if (file != null) {
+        result.Add(file);
+      }
+    }
+
+    if (Options.Get(CommonOptionBag.UseStandardLibraries)) {
+      if (Options.CompilerName is null or "cs" or "java" or "go" or "py" or "js") {
+        var targetName = Options.CompilerName ?? "notarget";
+        var stdlibDooUri = new Uri($"{DafnyMain.StandardLibrariesDooUriBase}-{targetName}.doo");
+        Options.CliRootSourceUris.Add(stdlibDooUri);
+        result.Add(DafnyFile.CreateAndValidate(errorReporter, OnDiskFileSystem.Instance, Options, stdlibDooUri, Project.StartingToken));
+      }
+
+      result.Add(DafnyFile.CreateAndValidate(errorReporter, fileSystem, Options, DafnyMain.StandardLibrariesDooUri, Project.StartingToken));
+      result.Add(DafnyFile.CreateAndValidate(errorReporter, fileSystem, Options, DafnyMain.StandardLibrariesArithmeticDooUri, Project.StartingToken));
+    }
+
+    foreach (var library in Options.Get(CommonOptionBag.Libraries)) {
+      var file = DafnyFile.CreateAndValidate(errorReporter, fileSystem, Options, new Uri(library.FullName), Project.StartingToken);
+      if (file != null) {
+        file.IsPreverified = true;
+        file.IsPrecompiled = true;
+        result.Add(file);
+      }
+    }
+
+    var projectPath = Project.Uri.LocalPath;
+    if (projectPath.EndsWith(DafnyProject.FileName)) {
+      var projectDirectory = Path.GetDirectoryName(projectPath)!;
+      var filesMessage = string.Join("\n", result.Select(uri => Path.GetRelativePath(projectDirectory, uri.Uri.LocalPath)));
+      if (filesMessage.Any()) {
+        errorReporter.Info(MessageSource.Parser, Project.StartingToken, "Files referenced by project are:" + Environment.NewLine + filesMessage);
+      } else {
+        errorReporter.Warning(MessageSource.Parser, CompilerErrors.ErrorId.None, Project.StartingToken, "Project references no files");
+      }
+    }
+
+    return result;
+  }
+
   private async Task<Program> ParseAsync() {
     try {
       await started.Task;
-      var uri = Input.Uri.ToUri();
-      var errorReporter = new ObservableErrorReporter(options, uri);
-      errorReporter.Updates.Subscribe(updates);
-      staticDiagnosticsSubscription = errorReporter.Updates.Subscribe(newDiagnostic =>
-        staticDiagnostics.GetOrAdd(newDiagnostic.Uri, _ => new()).Push(newDiagnostic.Diagnostic));
-      transformedProgram = await documentLoader.ParseAsync(errorReporter, Input, cancellationSource.Token);
+      transformedProgram = await documentLoader.ParseAsync(this, cancellationSource.Token);
 
       var cloner = new Cloner(true, false);
       programAfterParsing = new Program(cloner, transformedProgram);
 
-      var diagnosticsCopy = staticDiagnostics.ToImmutableDictionary(k => k.Key,
-        kv => kv.Value.Select(d => d.ToLspDiagnostic()).ToImmutableList());
-      updates.OnNext(new FinishedParsing(programAfterParsing, diagnosticsCopy));
+      updates.OnNext(new FinishedParsing(programAfterParsing, GetDiagnosticsCopy()));
       logger.LogDebug(
         $"Passed parsedCompilation to documentUpdates.OnNext, resolving ParsedCompilation task for version {Input.Version}.");
       return programAfterParsing;
@@ -320,7 +382,7 @@ public async Task Cancel(FilePosition filePosition) {
   }
 
   private void HandleStatusUpdate(ICanVerify canVerify, IImplementationTask implementationTask, IVerificationStatus boogieStatus) {
-    var tokenString = BoogieGenerator.ToDafnyToken(true, implementationTask.Implementation.tok).TokenToString(options);
+    var tokenString = BoogieGenerator.ToDafnyToken(true, implementationTask.Implementation.tok).TokenToString(Options);
     logger.LogDebug($"Received Boogie status {boogieStatus} for {tokenString}, version {Input.Version}");
 
     if (boogieStatus is Completed completed) {
@@ -377,6 +439,7 @@ public void CancelPendingUpdates() {
   }
 
   private bool disposed;
+  private readonly ObservableErrorReporter errorReporter;
 
   public void Dispose() {
     if (disposed) {
diff --git a/Source/DafnyLanguageServer/Workspace/CompilationInput.cs b/Source/DafnyLanguageServer/Workspace/CompilationInput.cs
index ca5430955b2..c1e953de5ea 100644
--- a/Source/DafnyLanguageServer/Workspace/CompilationInput.cs
+++ b/Source/DafnyLanguageServer/Workspace/CompilationInput.cs
@@ -3,7 +3,6 @@
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 using System.Collections.Generic;
 using System.Collections.Immutable;
-using System.Dynamic;
 using System.Linq;
 using Microsoft.Boogie;
 using Microsoft.Dafny.LanguageServer.Language.Symbols;
@@ -12,34 +11,21 @@
 
 namespace Microsoft.Dafny.LanguageServer.Workspace {
 
-
   /// <summary>
-  /// Internal representation of a specific version of a Dafny document.
-  ///
-  /// Only one instance should exist of a specific version.
-  /// Asynchronous compilation tasks use this instance to synchronise on.
-  ///
-  /// When verification starts, no new instances of Compilation will be created for this version.
-  /// There can be different verification threads that update the state of this object.
+  /// Contains all the inputs of a Compilation
   /// </summary>
   public class CompilationInput {
-    /// <summary>
-    /// These do not have to be owned
-    /// </summary>
-    public IReadOnlyList<Uri> RootUris { get; }
 
     public override string ToString() {
       return $"URI: {Uri}, Version: {Version}";
     }
 
-    public IEnumerable<Uri> RootAndProjectUris => RootUris.Concat(new[] { Project.Uri }).Distinct();
     public int Version { get; }
     public DafnyOptions Options { get; }
     public DafnyProject Project { get; }
     public DocumentUri Uri => Project.Uri;
 
-    public CompilationInput(DafnyOptions options, int version, DafnyProject project, IReadOnlyList<Uri> rootUris) {
-      RootUris = rootUris;
+    public CompilationInput(DafnyOptions options, int version, DafnyProject project) {
       Options = options;
       Version = version;
       Project = project;
@@ -47,7 +33,8 @@ public CompilationInput(DafnyOptions options, int version, DafnyProject project,
 
     public IdeState InitialIdeState(DafnyOptions options) {
       var program = new EmptyNode();
-      return new IdeState(Version, this, CompilationStatus.Parsing,
+      return new IdeState(Version, ImmutableHashSet<Uri>.Empty,
+        this, CompilationStatus.Parsing,
         program,
         ImmutableDictionary<Uri, ImmutableList<Diagnostic>>.Empty,
         program,
@@ -55,7 +42,7 @@ public IdeState InitialIdeState(DafnyOptions options) {
         LegacySignatureAndCompletionTable.Empty(options, Project), ImmutableDictionary<Uri, ImmutableDictionary<Range, IdeVerificationResult>>.Empty,
         Array.Empty<Counterexample>(),
         ImmutableDictionary<Uri, IReadOnlyList<Range>>.Empty,
-        RootUris.ToImmutableDictionary(uri => uri, uri => new DocumentVerificationTree(program, uri))
+        ImmutableDictionary<Uri, DocumentVerificationTree>.Empty
       );
     }
   }
diff --git a/Source/DafnyLanguageServer/Workspace/DeterminedRootFiles.cs b/Source/DafnyLanguageServer/Workspace/DeterminedRootFiles.cs
new file mode 100644
index 00000000000..96506aae83c
--- /dev/null
+++ b/Source/DafnyLanguageServer/Workspace/DeterminedRootFiles.cs
@@ -0,0 +1,44 @@
+using System;
+using System.Collections.Generic;
+using System.Collections.Immutable;
+using System.Linq;
+using System.Threading.Tasks;
+using Microsoft.Dafny.LanguageServer.Workspace.Notifications;
+using Microsoft.Extensions.Logging;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
+
+namespace Microsoft.Dafny.LanguageServer.Workspace;
+
+record DeterminedRootFiles(
+  DafnyProject Project,
+  IReadOnlyList<DafnyFile> Roots,
+  ImmutableDictionary<Uri, ImmutableList<Diagnostic>> Diagnostics) : ICompilationEvent {
+  public async Task<IdeState> UpdateState(DafnyOptions options,
+    ILogger logger,
+    IProjectDatabase projectDatabase,
+    IdeState previousState) {
+    var errors = Diagnostics.Values.SelectMany(x => x).
+      Where(d => d.Severity == DiagnosticSeverity.Error);
+    var status = errors.Any() ? CompilationStatus.ParsingFailed : previousState.Status;
+
+    var ownedUris = new HashSet<Uri>();
+    foreach (var file in Roots) {
+      var uriProject = await projectDatabase.GetProject(file.Uri);
+      var ownedUri = uriProject.Equals(Project);
+      if (ownedUri) {
+        ownedUris.Add(file.Uri);
+      }
+    }
+    ownedUris.Add(Project.Uri);
+
+    return previousState with {
+      OwnedUris = ownedUris,
+      StaticDiagnostics = status == CompilationStatus.ParsingFailed ? Diagnostics : previousState.StaticDiagnostics,
+      Status = status,
+      VerificationTrees = Roots.ToImmutableDictionary(
+        file => file.Uri,
+        file => previousState.VerificationTrees.GetValueOrDefault(file.Uri) ??
+                new DocumentVerificationTree(previousState.Program, file.Uri))
+    };
+  }
+}
\ No newline at end of file
diff --git a/Source/DafnyLanguageServer/Workspace/FinishedParsing.cs b/Source/DafnyLanguageServer/Workspace/FinishedParsing.cs
index 9d2bf77d103..e262633bd59 100644
--- a/Source/DafnyLanguageServer/Workspace/FinishedParsing.cs
+++ b/Source/DafnyLanguageServer/Workspace/FinishedParsing.cs
@@ -1,6 +1,7 @@
 using System;
 using System.Collections.Immutable;
 using System.Linq;
+using System.Threading.Tasks;
 using Microsoft.Dafny.LanguageServer.Workspace.Notifications;
 using Microsoft.Extensions.Logging;
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
@@ -10,7 +11,8 @@ namespace Microsoft.Dafny.LanguageServer.Workspace;
 record FinishedParsing(
   Program Program,
   ImmutableDictionary<Uri, ImmutableList<Diagnostic>> Diagnostics) : ICompilationEvent {
-  public IdeState UpdateState(DafnyOptions options, ILogger logger, IdeState previousState) {
+  public Task<IdeState> UpdateState(DafnyOptions options, ILogger logger, IProjectDatabase projectDatabase,
+    IdeState previousState) {
 
     var trees = previousState.VerificationTrees;
     foreach (var uri in trees.Keys) {
@@ -24,11 +26,11 @@ public IdeState UpdateState(DafnyOptions options, ILogger logger, IdeState previ
       Where(d => d.Severity == DiagnosticSeverity.Error);
     var status = errors.Any() ? CompilationStatus.ParsingFailed : CompilationStatus.ResolutionStarted;
 
-    return previousState with {
+    return Task.FromResult(previousState with {
       Program = Program,
       StaticDiagnostics = status == CompilationStatus.ParsingFailed ? Diagnostics : previousState.StaticDiagnostics,
       Status = status,
       VerificationTrees = trees
-    };
+    });
   }
 }
\ No newline at end of file
diff --git a/Source/DafnyLanguageServer/Workspace/FinishedResolution.cs b/Source/DafnyLanguageServer/Workspace/FinishedResolution.cs
index 4077cc2911c..9e53067a01f 100644
--- a/Source/DafnyLanguageServer/Workspace/FinishedResolution.cs
+++ b/Source/DafnyLanguageServer/Workspace/FinishedResolution.cs
@@ -2,6 +2,7 @@
 using System.Collections.Generic;
 using System.Collections.Immutable;
 using System.Linq;
+using System.Threading.Tasks;
 using Microsoft.Boogie;
 using Microsoft.Dafny.LanguageServer.Language;
 using Microsoft.Dafny.LanguageServer.Language.Symbols;
@@ -19,7 +20,8 @@ record FinishedResolution(
   LegacySignatureAndCompletionTable LegacySignatureAndCompletionTable,
   IReadOnlyDictionary<Uri, IReadOnlyList<Range>> GhostRanges,
   IReadOnlyList<ICanVerify>? CanVerifies) : ICompilationEvent {
-  public IdeState UpdateState(DafnyOptions options, ILogger logger, IdeState previousState) {
+  public Task<IdeState> UpdateState(DafnyOptions options, ILogger logger, IProjectDatabase projectDatabase,
+    IdeState previousState) {
     var errors = Diagnostics.Values.SelectMany(x => x).
       Where(d => d.Severity == DiagnosticSeverity.Error && d.Source != MessageSource.Compiler.ToString()).ToList();
     var status = errors.Any() ? CompilationStatus.ResolutionFailed : CompilationStatus.ResolutionSucceeded;
@@ -41,7 +43,7 @@ public IdeState UpdateState(DafnyOptions options, ILogger logger, IdeState previ
           l => MergeResults(l.Select(canVerify => MergeVerifiable(previousState, canVerify)))));
     var signatureAndCompletionTable = LegacySignatureAndCompletionTable.Resolved ? LegacySignatureAndCompletionTable : previousState.SignatureAndCompletionTable;
 
-    return previousState with {
+    return Task.FromResult(previousState with {
       StaticDiagnostics = Diagnostics,
       Status = status,
       ResolvedProgram = ResolvedProgram,
@@ -51,7 +53,7 @@ public IdeState UpdateState(DafnyOptions options, ILogger logger, IdeState previ
       Counterexamples = new List<Counterexample>(),
       VerificationResults = verificationResults,
       VerificationTrees = trees
-    };
+    });
   }
 
   private static IdeVerificationResult MergeResults(IEnumerable<IdeVerificationResult> results) {
diff --git a/Source/DafnyLanguageServer/Workspace/ICompilationEvent.cs b/Source/DafnyLanguageServer/Workspace/ICompilationEvent.cs
index 845d59dbb5b..0551737bd40 100644
--- a/Source/DafnyLanguageServer/Workspace/ICompilationEvent.cs
+++ b/Source/DafnyLanguageServer/Workspace/ICompilationEvent.cs
@@ -1,7 +1,9 @@
+using System.Threading.Tasks;
 using Microsoft.Extensions.Logging;
 
 namespace Microsoft.Dafny.LanguageServer.Workspace;
 
 public interface ICompilationEvent {
-  public IdeState UpdateState(DafnyOptions options, ILogger logger, IdeState previousState);
+  public Task<IdeState> UpdateState(DafnyOptions options, ILogger logger, IProjectDatabase projectDatabase,
+    IdeState previousState);
 }
\ No newline at end of file
diff --git a/Source/DafnyLanguageServer/Workspace/INotificationPublisher.cs b/Source/DafnyLanguageServer/Workspace/INotificationPublisher.cs
index 1526f62c81e..8944daba34d 100644
--- a/Source/DafnyLanguageServer/Workspace/INotificationPublisher.cs
+++ b/Source/DafnyLanguageServer/Workspace/INotificationPublisher.cs
@@ -11,6 +11,6 @@ public interface INotificationPublisher {
     /// Publishes the diagnostics of the specified dafny document to the connected LSP client.
     /// </summary>
     /// <param name="state">The document whose diagnostics should be published.</param>
-    Task PublishNotifications(IdeState previousState, IdeState state);
+    void PublishNotifications(IdeState previousState, IdeState state);
   }
 }
diff --git a/Source/DafnyLanguageServer/Workspace/ITextDocumentLoader.cs b/Source/DafnyLanguageServer/Workspace/ITextDocumentLoader.cs
index 17646089821..c826dff0427 100644
--- a/Source/DafnyLanguageServer/Workspace/ITextDocumentLoader.cs
+++ b/Source/DafnyLanguageServer/Workspace/ITextDocumentLoader.cs
@@ -10,7 +10,7 @@ namespace Microsoft.Dafny.LanguageServer.Workspace {
   /// </summary>
   public interface ITextDocumentLoader {
 
-    Task<Program> ParseAsync(ErrorReporter reporter, CompilationInput compilation, CancellationToken cancellationToken);
+    Task<Program> ParseAsync(Compilation compilation, CancellationToken cancellationToken);
 
     Task<ResolutionResult> ResolveAsync(CompilationInput input,
       Program program,
diff --git a/Source/DafnyLanguageServer/Workspace/IdeState.cs b/Source/DafnyLanguageServer/Workspace/IdeState.cs
index 306a2526ed2..db07c4d77ea 100644
--- a/Source/DafnyLanguageServer/Workspace/IdeState.cs
+++ b/Source/DafnyLanguageServer/Workspace/IdeState.cs
@@ -25,6 +25,7 @@ public record IdeVerificationResult(VerificationPreparationState PreparationProg
 /// </summary>
 public record IdeState(
   int Version,
+  ISet<Uri> OwnedUris,
   CompilationInput Input,
   CompilationStatus Status,
   Node Program,
diff --git a/Source/DafnyLanguageServer/Workspace/IdeStateObserver.cs b/Source/DafnyLanguageServer/Workspace/IdeStateObserver.cs
index 91b470e565f..408ea351c78 100644
--- a/Source/DafnyLanguageServer/Workspace/IdeStateObserver.cs
+++ b/Source/DafnyLanguageServer/Workspace/IdeStateObserver.cs
@@ -37,9 +37,7 @@ public void OnCompleted() {
     var ideState = initialState with {
       Version = LastPublishedState.Version + 1
     };
-#pragma warning disable VSTHRD002
-    notificationPublisher.PublishNotifications(LastPublishedState, ideState).Wait();
-#pragma warning restore VSTHRD002
+    notificationPublisher.PublishNotifications(LastPublishedState, ideState);
     telemetryPublisher.PublishUpdateComplete();
   }
 
@@ -52,11 +50,7 @@ public void OnNext(IdeState snapshot) {
         return;
       }
 
-      // To prevent older updates from being sent after newer ones, we can only run one PublishNotifications at a time.
-      // So we wait for it here to finish, and the lock in this method prevents more than one from running at a time.
-#pragma warning disable VSTHRD002
-      notificationPublisher.PublishNotifications(LastPublishedState, snapshot).Wait();
-#pragma warning restore VSTHRD002
+      notificationPublisher.PublishNotifications(LastPublishedState, snapshot);
       LastPublishedState = snapshot;
       logger.LogDebug($"Updated LastPublishedState to version {snapshot.Version}, uri {initialState.Input.Uri.ToUri()}");
     }
diff --git a/Source/DafnyLanguageServer/Workspace/InternalCompilationException.cs b/Source/DafnyLanguageServer/Workspace/InternalCompilationException.cs
index 95f20ae706d..2ce2c5c8a6c 100644
--- a/Source/DafnyLanguageServer/Workspace/InternalCompilationException.cs
+++ b/Source/DafnyLanguageServer/Workspace/InternalCompilationException.cs
@@ -1,6 +1,7 @@
 
 using System;
 using System.Collections.Immutable;
+using System.Threading.Tasks;
 using Microsoft.Dafny.LanguageServer.Workspace.Notifications;
 using Microsoft.Extensions.Logging;
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
@@ -9,7 +10,8 @@
 namespace Microsoft.Dafny.LanguageServer.Workspace;
 
 record InternalCompilationException(Exception Exception) : ICompilationEvent {
-  public IdeState UpdateState(DafnyOptions options, ILogger logger, IdeState previousState) {
+  public Task<IdeState> UpdateState(DafnyOptions options, ILogger logger, IProjectDatabase projectDatabase,
+    IdeState previousState) {
     var internalErrorDiagnostic = new Diagnostic {
       Message =
         "Dafny encountered an internal error. Please report it at <https://github.com/dafny-lang/dafny/issues>.\n" +
@@ -17,9 +19,9 @@ public IdeState UpdateState(DafnyOptions options, ILogger logger, IdeState previ
       Severity = DiagnosticSeverity.Error,
       Range = new Range(0, 0, 0, 1)
     };
-    return previousState with {
+    return Task.FromResult(previousState with {
       Status = CompilationStatus.InternalException,
       StaticDiagnostics = ImmutableDictionary<Uri, ImmutableList<Diagnostic>>.Empty.Add(previousState.Input.Uri.ToUri(), ImmutableList.Create(internalErrorDiagnostic))
-    };
+    });
   }
 }
\ No newline at end of file
diff --git a/Source/DafnyLanguageServer/Workspace/LanguageServerExtensions.cs b/Source/DafnyLanguageServer/Workspace/LanguageServerExtensions.cs
index 5f6bbe0e520..a748ee6f88a 100644
--- a/Source/DafnyLanguageServer/Workspace/LanguageServerExtensions.cs
+++ b/Source/DafnyLanguageServer/Workspace/LanguageServerExtensions.cs
@@ -29,6 +29,7 @@ private static IServiceCollection WithDafnyWorkspace(this IServiceCollection ser
           provider.GetRequiredService<CreateMigrator>(),
           provider.GetRequiredService<IFileSystem>(),
           provider.GetRequiredService<ITelemetryPublisher>(),
+          provider.GetRequiredService<IProjectDatabase>(),
           provider.GetRequiredService<CreateCompilation>(),
           provider.GetRequiredService<CreateIdeStateObserver>(),
           scheduler,
diff --git a/Source/DafnyLanguageServer/Workspace/NewDiagnostic.cs b/Source/DafnyLanguageServer/Workspace/NewDiagnostic.cs
index 8b457375b90..89a99a9b9ff 100644
--- a/Source/DafnyLanguageServer/Workspace/NewDiagnostic.cs
+++ b/Source/DafnyLanguageServer/Workspace/NewDiagnostic.cs
@@ -1,5 +1,6 @@
 using System;
 using System.Collections.Immutable;
+using System.Threading.Tasks;
 using Microsoft.Dafny.LanguageServer.Workspace.Notifications;
 using Microsoft.Extensions.Logging;
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
@@ -7,17 +8,18 @@
 namespace Microsoft.Dafny.LanguageServer.Workspace;
 
 public record NewDiagnostic(Uri Uri, DafnyDiagnostic Diagnostic) : ICompilationEvent {
-  public IdeState UpdateState(DafnyOptions options, ILogger logger, IdeState previousState) {
+  public Task<IdeState> UpdateState(DafnyOptions options, ILogger logger, IProjectDatabase projectDatabase,
+    IdeState previousState) {
     // Until resolution is finished, keep showing the old diagnostics. 
     if (previousState.Status > CompilationStatus.ResolutionStarted) {
       var diagnostics = previousState.StaticDiagnostics.GetValueOrDefault(Uri, ImmutableList<Diagnostic>.Empty);
       var newDiagnostics = diagnostics.Add(Diagnostic.ToLspDiagnostic());
-      return previousState with {
+      return Task.FromResult(previousState with {
         StaticDiagnostics = previousState.StaticDiagnostics.SetItem(Uri, newDiagnostics)
-      };
+      });
     }
 
-    return previousState;
+    return Task.FromResult(previousState);
 
   }
 }
\ No newline at end of file
diff --git a/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs b/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs
index 719fadb7edf..63b6150bf40 100644
--- a/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs
+++ b/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs
@@ -18,28 +18,27 @@ public class NotificationPublisher : INotificationPublisher {
     private readonly ILogger<NotificationPublisher> logger;
     private readonly LanguageServerFilesystem filesystem;
     private readonly ILanguageServerFacade languageServer;
-    private readonly IProjectDatabase projectManagerDatabase;
     private readonly DafnyOptions options;
 
-    public NotificationPublisher(ILogger<NotificationPublisher> logger, ILanguageServerFacade languageServer,
-      IProjectDatabase projectManagerDatabase,
+    public NotificationPublisher(
+      ILogger<NotificationPublisher> logger,
+      ILanguageServerFacade languageServer,
       DafnyOptions options, LanguageServerFilesystem filesystem) {
       this.logger = logger;
       this.languageServer = languageServer;
-      this.projectManagerDatabase = projectManagerDatabase;
       this.options = options;
       this.filesystem = filesystem;
     }
 
-    public async Task PublishNotifications(IdeState previousState, IdeState state) {
+    public void PublishNotifications(IdeState previousState, IdeState state) {
       if (state.Version < previousState.Version) {
         return;
       }
 
-      await PublishDiagnostics(state);
+      PublishDiagnostics(state);
       PublishProgress(previousState, state);
       PublishGhostness(previousState, state);
-      foreach (var uri in state.Input.RootUris) {
+      foreach (var uri in state.OwnedUris) {
         PublishGutterIcons(uri, state);
       }
     }
@@ -58,7 +57,7 @@ private void PublishProgress(IdeState previousState, IdeState state) {
     }
 
     private void PublishSymbolProgress(IdeState previousState, IdeState state) {
-      foreach (var uri in state.Input.RootUris) {
+      foreach (var uri in state.OwnedUris.Concat(previousState.OwnedUris).Distinct()) {
         var previous = GetFileVerificationStatus(previousState, uri);
         var current = GetFileVerificationStatus(state, uri);
 
@@ -71,8 +70,7 @@ private void PublishSymbolProgress(IdeState previousState, IdeState state) {
     }
 
     private void PublishGlobalProgress(IdeState previousState, IdeState state) {
-      foreach (var uri in state.Input.RootAndProjectUris) {
-        // TODO, still have to check for ownedness
+      foreach (var uri in state.OwnedUris) {
 
         var current = state.Status;
         var previous = previousState.Status;
@@ -118,15 +116,14 @@ public static PublishedVerificationStatus Combine(PublishedVerificationStatus fi
 
     private readonly ConcurrentDictionary<Uri, IList<Diagnostic>> publishedDiagnostics = new();
 
-    private async Task PublishDiagnostics(IdeState state) {
+    private void PublishDiagnostics(IdeState state) {
       // All root uris are added because we may have to publish empty diagnostics for owned uris.
-      var sources = state.GetDiagnosticUris().Concat(state.Input.RootUris).Distinct();
+      var sources = state.GetDiagnosticUris().Concat(state.OwnedUris).Distinct();
 
       var projectDiagnostics = new List<Diagnostic>();
       foreach (var uri in sources) {
         var current = state.GetDiagnosticsForUri(uri);
-        var uriProject = await projectManagerDatabase.GetProject(uri);
-        var ownedUri = uriProject.Equals(state.Input.Project);
+        var ownedUri = state.OwnedUris.Contains(uri);
         if (ownedUri) {
           if (uri == state.Input.Project.Uri) {
             // Delay publication of project diagnostics,
@@ -187,7 +184,10 @@ private void PublishGutterIcons(Uri uri, IdeState state) {
 
       var errors = state.StaticDiagnostics.GetOrDefault(uri, Enumerable.Empty<Diagnostic>).
         Where(x => x.Severity == DiagnosticSeverity.Error).ToList();
-      var tree = state.VerificationTrees[uri];
+      var tree = state.VerificationTrees.GetValueOrDefault(uri);
+      if (tree == null) {
+        return;
+      }
 
       var linesCount = tree.Range.End.Line + 1;
       var fileVersion = filesystem.GetVersion(uri);
diff --git a/Source/DafnyLanguageServer/Workspace/ProjectManager.cs b/Source/DafnyLanguageServer/Workspace/ProjectManager.cs
index 094a9566683..64cc4b4954e 100644
--- a/Source/DafnyLanguageServer/Workspace/ProjectManager.cs
+++ b/Source/DafnyLanguageServer/Workspace/ProjectManager.cs
@@ -19,6 +19,7 @@
 using Microsoft.Dafny.LanguageServer.Workspace.Notifications;
 using Microsoft.Extensions.Logging;
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
+using Location = OmniSharp.Extensions.LanguageServer.Protocol.Models.Location;
 
 namespace Microsoft.Dafny.LanguageServer.Workspace;
 
@@ -77,9 +78,10 @@ public class ProjectManager : IDisposable {
   private readonly ExecutionEngine boogieEngine;
   private readonly IFileSystem fileSystem;
   private readonly ITelemetryPublisher telemetryPublisher;
-  private Lazy<IdeState> latestIdeState;
-  private ReplaySubject<Lazy<IdeState>> states = new(1);
-  public IObservable<Lazy<IdeState>> States => states;
+  private readonly IProjectDatabase projectDatabase;
+  private IdeState latestIdeState;
+  private ReplaySubject<IdeState> states = new(1);
+  public IObservable<IdeState> States => states;
 
   public ProjectManager(
     DafnyOptions serverOptions,
@@ -87,6 +89,7 @@ public ProjectManager(
     CreateMigrator createMigrator,
     IFileSystem fileSystem,
     ITelemetryPublisher telemetryPublisher,
+    IProjectDatabase projectDatabase,
     CreateCompilation createCompilation,
     CreateIdeStateObserver createIdeStateObserver,
     CustomStackSizePoolTaskScheduler scheduler,
@@ -94,6 +97,7 @@ public ProjectManager(
     DafnyProject project) {
     Project = project;
     this.telemetryPublisher = telemetryPublisher;
+    this.projectDatabase = projectDatabase;
     this.serverOptions = serverOptions;
     this.fileSystem = fileSystem;
     this.createCompilation = createCompilation;
@@ -103,33 +107,25 @@ public ProjectManager(
     options = DetermineProjectOptions(project, serverOptions);
     options.Printer = new OutputLogger(logger);
     boogieEngine = new ExecutionEngine(options, cache, scheduler);
-    var initialCompilation = GetCompilationInput();
-    var initialIdeState = initialCompilation.InitialIdeState(options);
-    latestIdeState = new Lazy<IdeState>(initialIdeState);
+    var compilationInput = new CompilationInput(options, version, Project);
+    var initialIdeState = compilationInput.InitialIdeState(options);
+    latestIdeState = initialIdeState;
 
     observer = createIdeStateObserver(initialIdeState);
-    Compilation = createCompilation(options, boogieEngine, initialCompilation);
+    Compilation = createCompilation(boogieEngine, compilationInput);
 
     observerSubscription = Disposable.Empty;
   }
 
-  private CompilationInput GetCompilationInput() {
-    var rootUris = Project.GetRootSourceUris(fileSystem).Concat(options.CliRootSourceUris).ToList();
-    return new CompilationInput(options, version, Project, rootUris);
-  }
-
   private const int MaxRememberedChanges = 100;
-  private const int MaxRememberedChangedVerifiables = 5;
 
   public void UpdateDocument(DidChangeTextDocumentParams documentChange) {
     var migrator = createMigrator(documentChange, CancellationToken.None);
-    Lazy<IdeState> lazyPreviousCompilationLastIdeState = latestIdeState;
+
     var upcomingVersion = version + 1;
-    latestIdeState = new Lazy<IdeState>(() => {
-      // If we migrate the observer before accessing latestIdeState, we can be sure it's migrated before it receives new events.
-      observer.Migrate(options, migrator, upcomingVersion);
-      return lazyPreviousCompilationLastIdeState.Value.Migrate(options, migrator, upcomingVersion, false);
-    });
+    // If we migrate the observer before accessing latestIdeState, we can be sure it's migrated before it receives new events.
+    observer.Migrate(options, migrator, upcomingVersion);
+    latestIdeState = latestIdeState.Migrate(options, migrator, upcomingVersion, false);
     StartNewCompilation();
 
     lock (RecentChanges) {
@@ -164,46 +160,39 @@ private void StartNewCompilation() {
     observerSubscription.Dispose();
 
     Compilation.Dispose();
-    var input = GetCompilationInput();
-    Compilation = createCompilation(
-      options,
-      boogieEngine,
-      input);
+    var input = new CompilationInput(options, version, Project);
+    Compilation = createCompilation(boogieEngine, input);
     var migratedUpdates = GetStates(Compilation);
-    states = new ReplaySubject<Lazy<IdeState>>(1);
+    states = new ReplaySubject<IdeState>(1);
     var statesSubscription = observerSubscription =
       migratedUpdates.Do(s => latestIdeState = s).Subscribe(states);
 
     var throttleTime = options.Get(UpdateThrottling);
     var throttledUpdates = throttleTime == 0 ? States : States.Sample(TimeSpan.FromMilliseconds(throttleTime));
-    var throttledSubscription = throttledUpdates.
-      Select(x => x.Value).Subscribe(observer);
+    var throttledSubscription = throttledUpdates.Subscribe(observer);
     observerSubscription = new CompositeDisposable(statesSubscription, throttledSubscription);
 
     Compilation.Start();
   }
 
-  private IObservable<Lazy<IdeState>> GetStates(Compilation compilation) {
+  private IObservable<IdeState> GetStates(Compilation compilation) {
     var initialState = latestIdeState;
-    var latestCompilationState = new Lazy<IdeState>(() => {
-      var value = initialState.Value;
-      return value with {
-        Input = compilation.Input,
-        VerificationTrees = compilation.Input.RootUris.ToImmutableDictionary(uri => uri,
-          uri => value.VerificationTrees.GetValueOrDefault(uri) ??
-                 new DocumentVerificationTree(new EmptyNode(), uri))
-      };
-    });
-
-    return compilation.Updates.ObserveOn(ideStateUpdateScheduler).Select(ev => {
-      var previousState = latestCompilationState.Value;
+    var latestCompilationState = initialState with {
+      Input = compilation.Input,
+    };
+
+    async Task<IdeState> Update(ICompilationEvent ev) {
       if (ev is InternalCompilationException compilationException) {
         logger.LogError(compilationException.Exception, "error while handling document event");
         telemetryPublisher.PublishUnhandledException(compilationException.Exception);
       }
-      latestCompilationState = new Lazy<IdeState>(() => ev.UpdateState(options, logger, previousState));
-      return latestCompilationState;
-    });
+
+      var newState = await ev.UpdateState(options, logger, projectDatabase, latestCompilationState);
+      latestCompilationState = newState;
+      return newState;
+    }
+
+    return compilation.Updates.ObserveOn(ideStateUpdateScheduler).SelectMany(ev => Update(ev).ToObservable());
   }
 
   private void TriggerVerificationForFile(Uri triggeringFile) {
@@ -264,12 +253,11 @@ public void CloseAsync() {
   }
 
   public Task<IdeState> GetStateAfterParsingAsync() {
-    return States.Select(l => l.Value).Where(s => s.Status > CompilationStatus.Parsing).FirstAsync().ToTask();
+    return States.Where(s => s.Status > CompilationStatus.Parsing).FirstAsync().ToTask();
   }
 
   public Task<IdeState> GetStateAfterResolutionAsync() {
-    return States.Select(l => l.Value).
-      Where(s => s.Status is CompilationStatus.ParsingFailed or > CompilationStatus.ResolutionStarted).FirstAsync().ToTask();
+    return States.Where(s => s.Status is CompilationStatus.ParsingFailed or > CompilationStatus.ResolutionStarted).FirstAsync().ToTask();
   }
 
   /// <summary>
diff --git a/Source/DafnyLanguageServer/Workspace/ScheduledVerification.cs b/Source/DafnyLanguageServer/Workspace/ScheduledVerification.cs
index 2889d66da0f..1aee4c28867 100644
--- a/Source/DafnyLanguageServer/Workspace/ScheduledVerification.cs
+++ b/Source/DafnyLanguageServer/Workspace/ScheduledVerification.cs
@@ -1,5 +1,6 @@
 using System.Collections.Immutable;
 using System.Linq;
+using System.Threading.Tasks;
 using Microsoft.Dafny.LanguageServer.Language;
 using Microsoft.Extensions.Logging;
 
@@ -7,7 +8,8 @@ namespace Microsoft.Dafny.LanguageServer.Workspace;
 
 record ScheduledVerification(ICanVerify CanVerify) : ICompilationEvent {
 
-  public IdeState UpdateState(DafnyOptions options, ILogger logger, IdeState previousState) {
+  public Task<IdeState> UpdateState(DafnyOptions options, ILogger logger, IProjectDatabase projectDatabase,
+    IdeState previousState) {
     var uri = CanVerify.Tok.Uri;
     var range = CanVerify.NameToken.GetLspRange();
     var previousVerificationResult = previousState.VerificationResults[uri][range];
@@ -19,8 +21,8 @@ public IdeState UpdateState(DafnyOptions options, ILogger logger, IdeState previ
         Status = PublishedVerificationStatus.Stale,
         Diagnostics = IdeState.MarkDiagnosticsAsOutdated(kv.Value.Diagnostics).ToList()
       }));
-    return previousState with {
+    return Task.FromResult(previousState with {
       VerificationResults = previousState.VerificationResults.SetItem(uri, previousState.VerificationResults[uri].SetItem(range, verificationResult))
-    };
+    });
   }
 }
\ No newline at end of file
diff --git a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs
index c19fcaaef15..a5e6ed94d99 100644
--- a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs
+++ b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs
@@ -48,32 +48,14 @@ ILogger<ITextDocumentLoader> logger
       return new TextDocumentLoader(logger, parser, symbolResolver, symbolTableFactory, ghostStateDiagnosticCollector);
     }
 
-    public async Task<Program> ParseAsync(ErrorReporter errorReporter, CompilationInput compilation, CancellationToken cancellationToken) {
+    public async Task<Program> ParseAsync(Compilation compilation, CancellationToken cancellationToken) {
 #pragma warning disable CS1998
       return await await DafnyMain.LargeStackFactory.StartNew(
-        async () => ParseInternal(errorReporter, compilation, cancellationToken), cancellationToken
+        async () => parser.Parse(compilation, cancellationToken), cancellationToken
 #pragma warning restore CS1998
       );
     }
 
-    private Program ParseInternal(ErrorReporter errorReporter, CompilationInput compilation,
-      CancellationToken cancellationToken) {
-      var program = parser.Parse(compilation, errorReporter, cancellationToken);
-      compilation.Project.Errors.CopyDiagnostics(program.Reporter);
-      var projectPath = compilation.Project.Uri.LocalPath;
-      if (projectPath.EndsWith(DafnyProject.FileName)) {
-        var projectDirectory = Path.GetDirectoryName(projectPath)!;
-        var filesMessage = string.Join("\n", compilation.RootUris.Select(uri => Path.GetRelativePath(projectDirectory, uri.LocalPath)));
-        if (filesMessage.Any()) {
-          program.Reporter.Info(MessageSource.Parser, compilation.Project.StartingToken, "Files referenced by project are:" + Environment.NewLine + filesMessage);
-        } else {
-          program.Reporter.Warning(MessageSource.Parser, CompilerErrors.ErrorId.None, compilation.Project.StartingToken, "Project references no files");
-        }
-      }
-
-      return program;
-    }
-
     public async Task<ResolutionResult> ResolveAsync(CompilationInput input,
       Program program,
       CancellationToken cancellationToken) {
diff --git a/Source/DafnyServer/DafnyHelper.cs b/Source/DafnyServer/DafnyHelper.cs
index 6bbcf7acdec..f85c2946af0 100644
--- a/Source/DafnyServer/DafnyHelper.cs
+++ b/Source/DafnyServer/DafnyHelper.cs
@@ -3,6 +3,7 @@
 
 using System;
 using System.Collections.Generic;
+using System.Collections.Immutable;
 using System.IO;
 using System.Linq;
 using System.Runtime.Serialization.Json;
@@ -44,7 +45,9 @@ public bool Verify() {
     private bool Parse() {
       var uri = new Uri("transcript:///" + fname);
       reporter = new ConsoleErrorReporter(options);
-      var program = new ProgramParser().ParseFiles(fname, new DafnyFile[] { new(reporter.Options, uri, null, () => new StringReader(source)) },
+      var fs = new InMemoryFileSystem(ImmutableDictionary<Uri, string>.Empty.Add(uri, source));
+      var file = DafnyFile.CreateAndValidate(reporter, fs, reporter.Options, uri, Token.NoToken);
+      var program = new ProgramParser().ParseFiles(fname, file == null ? Array.Empty<DafnyFile>() : new[] { file },
         reporter, CancellationToken.None);
 
       var success = reporter.ErrorCount == 0;
diff --git a/Source/DafnyTestGeneration/Utils.cs b/Source/DafnyTestGeneration/Utils.cs
index e82d6513fb8..2ca67043306 100644
--- a/Source/DafnyTestGeneration/Utils.cs
+++ b/Source/DafnyTestGeneration/Utils.cs
@@ -4,6 +4,7 @@
 #nullable disable
 using System;
 using System.Collections.Generic;
+using System.Collections.Immutable;
 using System.IO;
 using System.Linq;
 using System.Text.RegularExpressions;
@@ -84,10 +85,11 @@ public static Type CopyWithReplacements(Type type, List<string> from, List<Type>
     /// Parse a string read (from a certain file) to a Dafny Program
     /// </summary>
     public static Program/*?*/ Parse(ErrorReporter reporter, string source, bool resolve = true, Uri uri = null) {
-      uri ??= new Uri(Path.Combine(Path.GetTempPath(), Path.GetRandomFileName()));
+      uri ??= new Uri(Path.Combine(Path.GetTempPath(), "parseUtils.dfy"));
 
-      var program = new ProgramParser().ParseFiles(uri.LocalPath, new DafnyFile[] { new(reporter.Options, uri, null, () => new StringReader(source)) },
-        reporter, CancellationToken.None);
+      var fs = new InMemoryFileSystem(ImmutableDictionary<Uri, string>.Empty.Add(uri, source));
+      var program = new ProgramParser().ParseFiles(uri.LocalPath,
+        new[] { DafnyFile.CreateAndValidate(reporter, fs, reporter.Options, uri, Token.NoToken) }, reporter, CancellationToken.None);
 
       if (!resolve) {
         return program;
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/formatting2.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/formatting2.dfy.expect
index 76063704466..b9a5ee9e1b5 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/formatting2.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/formatting2.dfy.expect
@@ -1 +1 @@
-*** Error: file unexisting.dfy not found
+CLI: Error: file unexisting.dfy not found
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/doofiles/Test1.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/doofiles/Test1.dfy.expect
index 8526d344cb7..13f5dca4b9a 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/doofiles/Test1.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/doofiles/Test1.dfy.expect
@@ -1 +1 @@
-*** Error: file NoSuch.doo not found
+CLI: Error: file NoSuch.doo not found
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4048.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4048.dfy.expect
index ee31aaebd62..046851e0872 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4048.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4048.dfy.expect
@@ -1 +1 @@
-*** Error: file x.doo not found
+CLI: Error: file x.doo not found
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/separate-verification/app.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/separate-verification/app.dfy.expect
index 94150d81bf5..6db0240a124 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/separate-verification/app.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/separate-verification/app.dfy.expect
@@ -9,5 +9,5 @@ Dafny program verifier finished with 1 verified, 0 errors
 Dafny program verifier finished with 2 verified, 0 errors
 
 Dafny program verifier finished with 2 verified, 0 errors
-*** Error: Cannot load wrappers.doo: --unicode-char is set locally to False, but the library was built with True
-*** Error: Cannot load wrappers.doo: --boogie is set locally to [], but the library was built with [/vcsLoad:2]
+CLI: Error: cannot load wrappers.doo: --unicode-char is set locally to False, but the library was built with True
+CLI: Error: cannot load wrappers.doo: --boogie is set locally to [], but the library was built with [/vcsLoad:2]
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_Errors.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_Errors.dfy.expect
index b605c419f6d..c3e9db2cdb5 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_Errors.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_Errors.dfy.expect
@@ -4,7 +4,9 @@ Dafny program verifier finished with 1 verified, 0 errors
 Dafny program verifier finished with 1 verified, 0 errors
 StandardLibraries_Errors.dfy(20,29): Error: module DafnyStdLibs does not exist (position 0 in path DafnyStdLibs.Wrappers)
 1 resolution/type errors detected in StandardLibraries_Errors.dfy
-*** Error: Cannot load DafnyStandardLibraries-notarget.doo: --unicode-char is set locally to False, but the library was built with True
+CLI: Error: cannot load DafnyStandardLibraries-notarget.doo: --unicode-char is set locally to False, but the library was built with True
+CLI: Error: cannot load DafnyStandardLibraries.doo: --unicode-char is set locally to False, but the library was built with True
+CLI: Error: cannot load DafnyStandardLibraries-arithmetic.doo: --unicode-char is set locally to False, but the library was built with True
 Please use the '--check' and/or '--print' option as doo files cannot be formatted in place.
 Please use the '--check' and/or '--print' option as doo files cannot be formatted in place.
 Please use the '--check' and/or '--print' option as doo files cannot be formatted in place.