diff --git a/Source/DafnyCore/DafnyFile.cs b/Source/DafnyCore/DafnyFile.cs index bd5ac78048..54118edfcc 100644 --- a/Source/DafnyCore/DafnyFile.cs +++ b/Source/DafnyCore/DafnyFile.cs @@ -29,7 +29,7 @@ public class DafnyFile { private static readonly Dictionary ExternallyVisibleEmbeddedFiles = new(); static DafnyFile() { - DooFile.RegisterLibraryCheck(UnsafeDependencies, OptionCompatibility.OptionLibraryImpliesLocalError); + DooFile.RegisterLibraryCheck(DoNotVerifyDependencies, OptionCompatibility.OptionLibraryImpliesLocalError); } public static Uri ExposeInternalUri(string externalName, Uri internalUri) { @@ -108,7 +108,7 @@ public static async IAsyncEnumerable CreateAndValidate(IFileSystem fi } } - public static readonly Option UnsafeDependencies = new("--dont-verify-dependencies", + public static readonly Option DoNotVerifyDependencies = new("--dont-verify-dependencies", "Allows Dafny to accept dependencies that may not have been previously verified, which can be useful during development."); public static DafnyFile? HandleDafnyFile(IFileSystem fileSystem, @@ -141,7 +141,7 @@ public static async IAsyncEnumerable CreateAndValidate(IFileSystem fi return null; } - if (!options.Get(UnsafeDependencies) && asLibrary && warnLibrary) { + if (!options.Get(DoNotVerifyDependencies) && asLibrary && warnLibrary) { reporter.Warning(MessageSource.Project, "", origin, $"The file '{options.GetPrintPath(filePath)}' was passed to --library. " + $"Verification for that file might have used options incompatible with the current ones, or might have been skipped entirely. " + diff --git a/Source/DafnyCore/Options/DafnyCommands.cs b/Source/DafnyCore/Options/DafnyCommands.cs index 1cdb93ff7b..67b3f734b0 100644 --- a/Source/DafnyCore/Options/DafnyCommands.cs +++ b/Source/DafnyCore/Options/DafnyCommands.cs @@ -107,6 +107,7 @@ static DafnyCommands() { CommonOptionBag.WarnMissingConstructorParenthesis, PrintStmt.TrackPrintEffectsOption, CommonOptionBag.AllowAxioms, - MethodOrFunction.AllowExternalContracts + MethodOrFunction.AllowExternalContracts, + DafnyProject.FindProjectOption }).Concat(ParserOptions).ToList(); } \ No newline at end of file diff --git a/Source/DafnyCore/Options/DafnyProject.cs b/Source/DafnyCore/Options/DafnyProject.cs index d8de8ac29d..d3c2f783f2 100644 --- a/Source/DafnyCore/Options/DafnyProject.cs +++ b/Source/DafnyCore/Options/DafnyProject.cs @@ -8,6 +8,7 @@ using System.Linq; using System.Text.RegularExpressions; using System.Threading.Tasks; +using DafnyCore; using DafnyCore.Options; using Microsoft.Extensions.FileSystemGlobbing; using Tomlyn; @@ -16,6 +17,13 @@ namespace Microsoft.Dafny; public class DafnyProject : IEquatable { + public static Option FindProjectOption = new("--find-project", + "Given a filesystem path, search for a project file by traversing up the file tree."); + + static DafnyProject() { + DooFile.RegisterNoChecksNeeded(FindProjectOption, false); + } + public const string Extension = ".toml"; public const string FileName = "dfyconfig" + Extension; @@ -48,7 +56,7 @@ public DafnyProject(Uri uri, Uri? @base, ISet includes, ISet? ex Options = options ?? new Dictionary(); } - public static async Task Open(IFileSystem fileSystem, DafnyOptions dafnyOptions, Uri uri, IToken uriOrigin, + public static async Task Open(IFileSystem fileSystem, Uri uri, IToken uriOrigin, bool defaultIncludes = true, bool serverNameCheck = true) { var emptyProject = new DafnyProject(uri, null, new HashSet(), new HashSet(), @@ -67,7 +75,7 @@ public static async Task Open(IFileSystem fileSystem, DafnyOptions model.Options ?? new Dictionary()); if (result.Base != null) { - var baseProject = await Open(fileSystem, dafnyOptions, result.Base, new Token { + var baseProject = await Open(fileSystem, result.Base, new Token { Uri = uri, line = 1, col = 1 diff --git a/Source/DafnyCore/Options/ProjectFileOpener.cs b/Source/DafnyCore/Options/ProjectFileOpener.cs new file mode 100644 index 0000000000..50e17b57d7 --- /dev/null +++ b/Source/DafnyCore/Options/ProjectFileOpener.cs @@ -0,0 +1,48 @@ +#nullable enable +using System; +using System.IO; +using System.Threading.Tasks; +using Microsoft.Dafny; + +public class ProjectFileOpener { + private readonly IFileSystem fileSystem; + private readonly IToken origin; + + public ProjectFileOpener(IFileSystem fileSystem, IToken origin) { + this.fileSystem = fileSystem; + this.origin = origin; + } + + public async Task TryFindProject(Uri uri) { + return uri.LocalPath.EndsWith(DafnyProject.FileName) + ? await DafnyProject.Open(fileSystem, uri, origin) + : await FindProjectFile(uri); + } + + private async Task FindProjectFile(Uri sourceUri) { + DafnyProject? projectFile = null; + + var folder = Path.GetDirectoryName(sourceUri.LocalPath); + while (!string.IsNullOrEmpty(folder) && projectFile == null) { + projectFile = await OpenProjectInFolder(folder); + + if (projectFile != null && projectFile.Uri != sourceUri && + !(projectFile.Errors.HasErrors || projectFile.ContainsSourceFile(sourceUri))) { + projectFile = null; + } + + folder = Path.GetDirectoryName(folder); + } + + return projectFile; + } + + protected virtual Task OpenProjectInFolder(string folderPath) { + var configFileUri = new Uri(Path.Combine(folderPath, DafnyProject.FileName)); + if (!fileSystem.Exists(configFileUri)) { + return Task.FromResult(null); + } + + return DafnyProject.Open(fileSystem, configFileUri, origin)!; + } +} \ No newline at end of file diff --git a/Source/DafnyDriver/Commands/ResolveCommand.cs b/Source/DafnyDriver/Commands/ResolveCommand.cs index a244b349e0..a6775138f7 100644 --- a/Source/DafnyDriver/Commands/ResolveCommand.cs +++ b/Source/DafnyDriver/Commands/ResolveCommand.cs @@ -13,7 +13,7 @@ public static Command Create() { result.AddOption(option); } DafnyNewCli.SetHandlerUsingDafnyOptionsContinuation(result, async (options, _) => { - options.Set(DafnyFile.UnsafeDependencies, true); + options.Set(DafnyFile.DoNotVerifyDependencies, true); var compilation = CliCompilation.Create(options); compilation.Start(); await compilation.Resolution; diff --git a/Source/DafnyDriver/Commands/ServerCommand.cs b/Source/DafnyDriver/Commands/ServerCommand.cs index d4f10de8ee..c7f9526719 100644 --- a/Source/DafnyDriver/Commands/ServerCommand.cs +++ b/Source/DafnyDriver/Commands/ServerCommand.cs @@ -32,7 +32,7 @@ private static Command Create() { result.Add(option); } DafnyNewCli.SetHandlerUsingDafnyOptionsContinuation(result, async (options, context) => { - options.Set(DafnyFile.UnsafeDependencies, true); + options.Set(DafnyFile.DoNotVerifyDependencies, true); LanguageServer.ConfigureDafnyOptionsForServer(options); await LanguageServer.Start(options); return 0; diff --git a/Source/DafnyDriver/Commands/VerifyCommand.cs b/Source/DafnyDriver/Commands/VerifyCommand.cs index 26aab2dc4e..293951b034 100644 --- a/Source/DafnyDriver/Commands/VerifyCommand.cs +++ b/Source/DafnyDriver/Commands/VerifyCommand.cs @@ -42,7 +42,7 @@ public static Command Create() { new Option[] { FilterSymbol, FilterPosition, - DafnyFile.UnsafeDependencies + DafnyFile.DoNotVerifyDependencies }.Concat(DafnyCommands.VerificationOptions). Concat(DafnyCommands.ConsoleOutputOptions). Concat(DafnyCommands.ResolverOptions); diff --git a/Source/DafnyDriver/DafnyNewCli.cs b/Source/DafnyDriver/DafnyNewCli.cs index 879d50ec0b..ed9dd010e3 100644 --- a/Source/DafnyDriver/DafnyNewCli.cs +++ b/Source/DafnyDriver/DafnyNewCli.cs @@ -20,6 +20,7 @@ using Microsoft.Boogie; using Microsoft.Dafny.Compilers; using Microsoft.Dafny.LanguageServer; +using Microsoft.Dafny.LanguageServer.Workspace; namespace Microsoft.Dafny; @@ -108,12 +109,23 @@ async Task Handle(InvocationContext context) { } } } + + ProcessOption(context, DafnyProject.FindProjectOption, dafnyOptions); + var findProjectPath = dafnyOptions.Get(DafnyProject.FindProjectOption); + if (dafnyOptions.DafnyProject == null && findProjectPath != null) { + var opener = new ProjectFileOpener(OnDiskFileSystem.Instance, Token.Cli); + var project = await opener.TryFindProject(new Uri(findProjectPath.FullName)); + project?.Validate(dafnyOptions.OutputWriter, AllOptions); + dafnyOptions.DafnyProject = project; + } + foreach (var option in command.Options) { - if (option == CommonOptionBag.UseBaseFileName) { + if (option == CommonOptionBag.UseBaseFileName || option == DafnyProject.FindProjectOption) { continue; } ProcessOption(context, option, dafnyOptions); } + foreach (var option in command.Options) { try { dafnyOptions.ApplyBinding(option); @@ -219,7 +231,7 @@ private static async Task ProcessProjectFile(DafnyOptions dafnyOptions, Ur await dafnyOptions.ErrorWriter.WriteLineAsync($"Error: file {dafnyOptions.GetPrintPath(file.LocalPath)} not found"); return false; } - var projectFile = await DafnyProject.Open(OnDiskFileSystem.Instance, dafnyOptions, file, Token.Cli); + var projectFile = await DafnyProject.Open(OnDiskFileSystem.Instance, file, Token.Cli); projectFile.Validate(dafnyOptions.OutputWriter, AllOptions); dafnyOptions.DafnyProject = projectFile; @@ -271,14 +283,14 @@ private static async IAsyncEnumerable HandleDafnyProject(IFileSystem yield break; } - var dependencyProject = await DafnyProject.Open(fileSystem, options, uri, uriOrigin); + var dependencyProject = await DafnyProject.Open(fileSystem, uri, uriOrigin); var dependencyOptions = DooFile.CheckAndGetLibraryOptions(reporter, uri, options, uriOrigin, dependencyProject.Options); if (dependencyOptions == null) { yield break; } - if (options.Get(DafnyFile.UnsafeDependencies) || !options.Verify) { + if (options.Get(DafnyFile.DoNotVerifyDependencies) || !options.Verify) { foreach (var libraryRootSetFile in dependencyProject.GetRootSourceUris(fileSystem)) { var file = DafnyFile.HandleDafnyFile(fileSystem, reporter, dependencyOptions, libraryRootSetFile, dependencyProject.StartingToken, true, false); @@ -301,7 +313,7 @@ private static async IAsyncEnumerable HandleDafnyProject(IFileSystem dependencyOptions.Compile = true; dependencyOptions.RunAfterCompile = false; var exitCode = await SynchronousCliCompilation.Run(dependencyOptions); - if (exitCode == 0) { + if (exitCode == 0 && libraryBackend.DooPath != null) { var dooUri = new Uri(libraryBackend.DooPath); await foreach (var dooResult in DafnyFile.HandleDooFile(fileSystem, reporter, options, dooUri, uriOrigin, true)) { yield return dooResult; diff --git a/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs b/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs index 11c46ddd1d..de256011f1 100644 --- a/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs +++ b/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs @@ -105,7 +105,7 @@ public AnonymousDisposable(Action action) { private Action GetServerOptionsAction(Action modifyOptions) { var dafnyOptions = DafnyOptions.CreateUsingOldParser(output); dafnyOptions.Set(ProjectManager.UpdateThrottling, 0); - dafnyOptions.Set(ProjectManagerDatabase.ProjectFileCacheExpiry, 0); + dafnyOptions.Set(CachingProjectFileOpener.ProjectFileCacheExpiry, 0); modifyOptions?.Invoke(dafnyOptions); dafnyOptions.UsingNewCli = true; LanguageServer.ConfigureDafnyOptionsForServer(dafnyOptions); diff --git a/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs b/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs index b860b86417..51b3d09a08 100644 --- a/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs +++ b/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs @@ -92,7 +92,7 @@ public async Task ProjectFileChangesArePickedUpAfterCacheExpiration() { const int cacheExpiry = 1000; await SetUp(options => { options.WarnShadowing = false; - options.Set(ProjectManagerDatabase.ProjectFileCacheExpiry, cacheExpiry); + options.Set(CachingProjectFileOpener.ProjectFileCacheExpiry, cacheExpiry); }); var tempDirectory = GetFreshTempPath(); Directory.CreateDirectory(tempDirectory); diff --git a/Source/DafnyLanguageServer/LanguageServer.cs b/Source/DafnyLanguageServer/LanguageServer.cs index d80f22afac..a3fe662552 100644 --- a/Source/DafnyLanguageServer/LanguageServer.cs +++ b/Source/DafnyLanguageServer/LanguageServer.cs @@ -27,7 +27,7 @@ public class LanguageServer { VerifySnapshots, DafnyLangSymbolResolver.UseCaching, ProjectManager.UpdateThrottling, - ProjectManagerDatabase.ProjectFileCacheExpiry, + CachingProjectFileOpener.ProjectFileCacheExpiry, DeveloperOptionBag.BoogiePrint, CommonOptionBag.EnforceDeterminism, InternalDocstringRewritersPluginConfiguration.UseJavadocLikeDocstringRewriterOption, diff --git a/Source/DafnyLanguageServer/Workspace/CachingProjectFileOpener.cs b/Source/DafnyLanguageServer/Workspace/CachingProjectFileOpener.cs new file mode 100644 index 0000000000..6abb2031bc --- /dev/null +++ b/Source/DafnyLanguageServer/Workspace/CachingProjectFileOpener.cs @@ -0,0 +1,45 @@ +using System; +using System.CommandLine; +using System.Runtime.Caching; +using System.Threading.Tasks; +using DafnyCore; +using Microsoft.Dafny; + +public class CachingProjectFileOpener : ProjectFileOpener { + public const int DefaultProjectFileCacheExpiryTime = 100; + private readonly object nullRepresentative = new(); // Needed because you can't store null in the MemoryCache, but that's a value we want to cache. + private readonly DafnyOptions serverOptions; + private readonly MemoryCache projectFilePerFolderCache = new("projectFiles"); + + + static CachingProjectFileOpener() { + DooFile.RegisterNoChecksNeeded(ProjectFileCacheExpiry, false); + } + + public CachingProjectFileOpener(IFileSystem fileSystem, DafnyOptions serverOptions, IToken origin) : base(fileSystem, origin) { + this.serverOptions = serverOptions; + } + + public static readonly Option ProjectFileCacheExpiry = new("--project-file-cache-expiry", () => DefaultProjectFileCacheExpiryTime, + @"How many milliseconds the server will cache project file contents".TrimStart()) { + IsHidden = true + }; + + protected override async Task OpenProjectInFolder(string folderPath) { + var cacheExpiry = serverOptions.Get(ProjectFileCacheExpiry); + if (cacheExpiry == 0) { + return await base.OpenProjectInFolder(folderPath); + } + + var cachedResult = projectFilePerFolderCache.Get(folderPath); + if (cachedResult != null) { + return cachedResult == nullRepresentative ? null : ((DafnyProject?)cachedResult)?.Clone(); + } + + var result = await base.OpenProjectInFolder(folderPath); + projectFilePerFolderCache.Set(new CacheItem(folderPath, (object?)result ?? nullRepresentative), new CacheItemPolicy { + AbsoluteExpiration = new DateTimeOffset(DateTime.Now.Add(TimeSpan.FromMilliseconds(cacheExpiry))) + }); + return result?.Clone(); + } +} \ No newline at end of file diff --git a/Source/DafnyLanguageServer/Workspace/ProjectManagerDatabase.cs b/Source/DafnyLanguageServer/Workspace/ProjectManagerDatabase.cs index 5709e4166d..5900c44617 100644 --- a/Source/DafnyLanguageServer/Workspace/ProjectManagerDatabase.cs +++ b/Source/DafnyLanguageServer/Workspace/ProjectManagerDatabase.cs @@ -1,7 +1,6 @@ using OmniSharp.Extensions.LanguageServer.Protocol.Models; using System; using System.Collections.Generic; -using System.CommandLine; using System.IO; using System.Linq; using System.Runtime.Caching; @@ -10,23 +9,15 @@ using Microsoft.Boogie; using Microsoft.Extensions.Logging; using OmniSharp.Extensions.LanguageServer.Protocol; +using Token = Microsoft.Boogie.Token; namespace Microsoft.Dafny.LanguageServer.Workspace { /// /// Contains a collection of ProjectManagers /// public class ProjectManagerDatabase : IProjectDatabase { - public static readonly Option ProjectFileCacheExpiry = new("--project-file-cache-expiry", () => DefaultProjectFileCacheExpiryTime, - @"How many milliseconds the server will cache project file contents".TrimStart()) { - IsHidden = true - }; - - static ProjectManagerDatabase() { - DooFile.RegisterNoChecksNeeded(ProjectFileCacheExpiry, false); - } private readonly object myLock = new(); - public const int DefaultProjectFileCacheExpiryTime = 100; private readonly CreateProjectManager createProjectManager; private readonly ILogger logger; @@ -36,9 +27,8 @@ static ProjectManagerDatabase() { private readonly LanguageServerFilesystem fileSystem; private readonly VerificationResultCache verificationCache = new(); private readonly TaskScheduler scheduler; - private readonly MemoryCache projectFilePerFolderCache = new("projectFiles"); - private readonly object nullRepresentative = new(); // Needed because you can't store null in the MemoryCache, but that's a value we want to cache. private readonly DafnyOptions serverOptions; + private CachingProjectFileOpener projectFileOpener; private const int stackSize = 10 * 1024 * 1024; @@ -52,6 +42,7 @@ public ProjectManagerDatabase( this.fileSystem = fileSystem; this.serverOptions = serverOptions; this.scheduler = CustomStackSizePoolTaskScheduler.Create(stackSize, serverOptions.VcsCores); + projectFileOpener = new CachingProjectFileOpener(fileSystem, serverOptions, Token.Ide); } public async Task OpenDocument(TextDocumentItem document) { @@ -204,9 +195,7 @@ public void CloseDocument(TextDocumentIdentifier documentId) { } public async Task GetProject(Uri uri) { - return uri.LocalPath.EndsWith(DafnyProject.FileName) - ? await DafnyProject.Open(fileSystem, serverOptions, uri, Token.Ide) - : (await FindProjectFile(uri) ?? ImplicitProject(uri)); + return await projectFileOpener.TryFindProject(uri) ?? ImplicitProject(uri); } public static DafnyProject ImplicitProject(Uri uri) { @@ -218,51 +207,6 @@ public static DafnyProject ImplicitProject(Uri uri) { return implicitProject; } - private async Task FindProjectFile(Uri sourceUri) { - DafnyProject? projectFile = null; - - var folder = Path.GetDirectoryName(sourceUri.LocalPath); - while (!string.IsNullOrEmpty(folder) && projectFile == null) { - projectFile = await OpenProjectInFolder(folder); - - if (projectFile != null && projectFile.Uri != sourceUri && - !(projectFile.Errors.HasErrors || projectFile.ContainsSourceFile(sourceUri))) { - projectFile = null; - } - - folder = Path.GetDirectoryName(folder); - } - - return projectFile; - } - - private async Task OpenProjectInFolder(string folderPath) { - var cacheExpiry = serverOptions.Get(ProjectFileCacheExpiry); - if (cacheExpiry == 0) { - return await OpenProjectInFolderUncached(folderPath); - } - - var cachedResult = projectFilePerFolderCache.Get(folderPath); - if (cachedResult != null) { - return cachedResult == nullRepresentative ? null : ((DafnyProject?)cachedResult)?.Clone(); - } - - var result = await OpenProjectInFolderUncached(folderPath); - projectFilePerFolderCache.Set(new CacheItem(folderPath, (object?)result ?? nullRepresentative), new CacheItemPolicy { - AbsoluteExpiration = new DateTimeOffset(DateTime.Now.Add(TimeSpan.FromMilliseconds(cacheExpiry))) - }); - return result?.Clone(); - } - - private Task OpenProjectInFolderUncached(string folderPath) { - var configFileUri = new Uri(Path.Combine(folderPath, DafnyProject.FileName)); - if (!fileSystem.Exists(configFileUri)) { - return Task.FromResult(null); - } - - return DafnyProject.Open(fileSystem, serverOptions, configFileUri, Token.Ide)!; - } - public IEnumerable Managers => managersByProject.Values; public void Dispose() { foreach (var manager in Managers) { @@ -270,4 +214,4 @@ public void Dispose() { } } } -} +} \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/projectFile.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/projectFile.dfy index 187680cf63..3a5553d8d5 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/projectFile.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/projectFile.dfy @@ -37,4 +37,7 @@ // Files excluded by the project file and included on the CLI, are included // RUN: ! %resolve "%S/dfyconfig.toml" "%S/src/excluded.dfy" &>> "%t" +// A project file can be found from an input file +// RUN: ! %resolve --find-project %S/src/input.dfy &>> "%t" + // RUN: %diff "%s.expect" "%t" diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/projectFile.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/projectFile.dfy.expect index c956bfcd9c..49490f4282 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/projectFile.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/projectFile.dfy.expect @@ -23,3 +23,5 @@ excluded.dfy(3,7): Error: Duplicate member name: Foo input.dfy(6,8): Warning: Shadowed local-variable name: x excluded.dfy(6,8): Warning: Shadowed local-variable name: z 1 resolution/type errors detected in dfyconfig.toml +input.dfy(6,8): Warning: Shadowed local-variable name: x +Compilation failed because warnings were found and --allow-warnings is false