From f4b7ccda8ce95412615c42412bfd3bf3bf40ad41 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= Date: Mon, 10 Jul 2023 04:07:07 -0500 Subject: [PATCH] Feat: Support for `--bprint` in language server. (#4206) I add this as a way to simplify boogie debugging, especially in cases when VSCode is not consistent with the command-line like in #4205 I did not add any test for that as it's meant for Dafny development only, but I tested it manually. I borrowed the code from the driver. Should I still list it as a feature? By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt). --- Source/DafnyDriver/DafnyDriver.cs | 6 +++--- .../Language/DafnyProgramVerifier.cs | 11 +++++++++-- Source/DafnyLanguageServer/ServerCommand.cs | 1 + docs/dev/news/bprint-option-in language-server.feat | 1 + 4 files changed, 14 insertions(+), 5 deletions(-) create mode 100644 docs/dev/news/bprint-option-in language-server.feat diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index 659d391bad2..293394f8e22 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -607,16 +607,16 @@ public enum CommandLineArgumentsResult { } public static IEnumerable> Translate(ExecutionEngineOptions options, Program dafnyProgram) { - var nmodules = Translator.VerifiableModules(dafnyProgram).Count(); + var modulesCount = Translator.VerifiableModules(dafnyProgram).Count(); foreach (var prog in Translator.Translate(dafnyProgram, dafnyProgram.Reporter)) { if (options.PrintFile != null) { - var nm = nmodules > 1 ? Dafny.DafnyMain.BoogieProgramSuffix(options.PrintFile, prog.Item1) : options.PrintFile; + var fileName = modulesCount > 1 ? Dafny.DafnyMain.BoogieProgramSuffix(options.PrintFile, prog.Item1) : options.PrintFile; - ExecutionEngine.PrintBplFile(options, nm, prog.Item2, false, false, options.PrettyPrint); + ExecutionEngine.PrintBplFile(options, fileName, prog.Item2, false, false, options.PrettyPrint); } yield return prog; diff --git a/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs b/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs index b168d2518c7..9d7355e1651 100644 --- a/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs +++ b/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs @@ -52,10 +52,17 @@ DafnyOptions options cancellationToken.ThrowIfCancellationRequested(); + if (engine.Options.PrintFile != null) { + var moduleCount = Translator.VerifiableModules(program).Count(); + foreach (var (suffix, boogieProgram) in translated) { + var fileName = moduleCount > 1 ? DafnyMain.BoogieProgramSuffix(engine.Options.PrintFile, suffix) : engine.Options.PrintFile; + ExecutionEngine.PrintBplFile(engine.Options, fileName, boogieProgram, false, false, engine.Options.PrettyPrint); + } + } + return translated.SelectMany(t => { var (_, boogieProgram) = t; - var results = engine.GetImplementationTasks(boogieProgram); - return results; + return engine.GetImplementationTasks(boogieProgram); }).ToList(); } diff --git a/Source/DafnyLanguageServer/ServerCommand.cs b/Source/DafnyLanguageServer/ServerCommand.cs index 1b4b320bbb5..24e1223d8ca 100644 --- a/Source/DafnyLanguageServer/ServerCommand.cs +++ b/Source/DafnyLanguageServer/ServerCommand.cs @@ -59,6 +59,7 @@ related locations GhostIndicators, LineVerificationStatus, VerifySnapshots, + DeveloperOptionBag.BoogiePrint, CommonOptionBag.EnforceDeterminism, CommonOptionBag.UseJavadocLikeDocstringRewriterOption }.Concat(ICommandSpec.VerificationOptions). diff --git a/docs/dev/news/bprint-option-in language-server.feat b/docs/dev/news/bprint-option-in language-server.feat new file mode 100644 index 00000000000..31918005d9c --- /dev/null +++ b/docs/dev/news/bprint-option-in language-server.feat @@ -0,0 +1 @@ +Support for the `--bprint` option for language server arguments \ No newline at end of file