Change the --extractTarget option into a command (#5799)

Touchup PR for #5621

### Description
- Change the --extractTarget option into a hidden command
- Make `--help` work when used on hidden commandds

### How has this been tested?
- Ran `make extract` in DafnyCore

<small>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).</small>

Source/DafnyCore/DafnyOptions.cs

@@ -320,7 +320,6 @@ public enum ContractTestingMode {
  public PrintModes PrintMode = PrintModes.Everything; // Default to printing everything
  public bool DafnyVerify = true;
  public string DafnyPrintResolvedFile = null;
- public string BoogieExtractionTargetFile = null;
  public List<string> DafnyPrintExportedViews = new List<string>();
  public bool Compile = true;
  public List<string> MainArgs = new List<string>();

Source/DafnyCore/Prelude/Makefile

@@ -15,6 +15,6 @@ DafnyPrelude.bpl: PreludeCore.bpl Sequences.bpl
  sed -e "s|PRIME|'|g" -i "" PreludeCore.bpl Sequences.bpl DafnyPrelude.bpl
 
 Sequences.bpl: Lists.dfy Boxes.dfy Sequences.dfy
- $(DAFNY) verify Lists.dfy Boxes.dfy Sequences.dfy --extract:Sequences.bpl
+ $(DAFNY) extract Sequences.bpl Lists.dfy Boxes.dfy Sequences.dfy
  # Remove trailing spaces that the Boogie pretty printer emits
  sed -e "s| *$$||" -i "" Sequences.bpl

Source/DafnyDriver/Commands/ExtractCommand.cs

@@ -0,0 +1,59 @@
+#nullable enable
+using System.Collections.Generic;
+using System.CommandLine;
+using System.IO;
+using System.Threading.Tasks;
+using DafnyDriver.Commands;
+using Microsoft.Boogie;
+using Microsoft.Dafny.Compilers;
+
+namespace Microsoft.Dafny;
+
+public static class ExtractCommand {
+ public static Command Create() {
+
+ var result = new Command("extract", "Can be used to generate DafnyPrelude.bpl. Uses the ':extract_boogie_name' attribute to rename symbols. Turns lemmas into universally quantified axioms, as opposed to verify which turns them into Boogie procedures. When translating Dafny expressions to Boogie ones, no well-formedness checks are created.");
+
+ result.IsHidden = true;
+ result.AddArgument(Target);
+ result.AddArgument(DafnyCommands.FilesArgument);
+ foreach (var option in ExtractOptions) {
+ result.AddOption(option);
+ }
+ DafnyNewCli.SetHandlerUsingDafnyOptionsContinuation(result, (options, _) => HandleExtraction(options));
+ return result;
+ }
+
+ private static readonly Argument<FileInfo> Target = new("The path of the extracted file.");
+
+ private static IReadOnlyList<Option> ExtractOptions =>
+ new Option[] { }.
+ Concat(DafnyCommands.ConsoleOutputOptions).
+ Concat(DafnyCommands.ResolverOptions);
+
+ public static async Task<int> HandleExtraction(DafnyOptions options) {
+ if (options.Get(CommonOptionBag.VerificationCoverageReport) != null) {
+ options.TrackVerificationCoverage = true;
+ }
+
+ var compilation = CliCompilation.Create(options);
+ compilation.Start();
+
+ var resolution = await compilation.Resolution;
+ if (resolution is not { HasErrors: false }) {
+ return await compilation.GetAndReportExitCode();
+ }
+
+ var outputPath = options.Get(Target).FullName;
+ using var engine = ExecutionEngine.CreateWithoutSharedCache(options);
+ try {
+ var extractedProgram = BoogieExtractor.Extract(resolution.ResolvedProgram);
+ engine.PrintBplFile(outputPath, extractedProgram, true, pretty: true);
+ } catch (ExtractorError extractorError) {
+ await options.OutputWriter.WriteLineAsync($"Boogie axiom extraction error: {extractorError.Message}");
+ return 1;
+ }
+
+ return await compilation.GetAndReportExitCode();
+ }
+}

Source/DafnyDriver/Commands/VerifyCommand.cs

@@ -22,13 +22,6 @@ static VerifyCommand() {
  OptionRegistry.RegisterOption(FilterSymbol, OptionScope.Cli);
  OptionRegistry.RegisterOption(FilterPosition, OptionScope.Cli);
  OptionRegistry.RegisterOption(PerformanceStatisticsOption, OptionScope.Cli);
- OptionRegistry.RegisterOption(ExtractTarget, OptionScope.Cli);
-
- DafnyOptions.RegisterLegacyBinding(ExtractTarget, (options, f) => {
- options.BoogieExtractionTargetFile = f;
- options.ExpandFilename(options.BoogieExtractionTargetFile, x => options.BoogieExtractionTargetFile = x, options.LogPrefix,
- options.FileTimestamp);
- });
  }
 
  public static readonly Option<int> PerformanceStatisticsOption = new("--performance-stats",
@@ -42,13 +35,6 @@ static VerifyCommand() {
  public static readonly Option<string> FilterPosition = new("--filter-position",
  @"Filter what gets verified based on a source location. The location is specified as a file path suffix, optionally followed by a colon and a line number. For example, `dafny verify dfyconfig.toml --filter-position=source1.dfy:5` will only verify things that range over line 5 in the file `source1.dfy`. In combination with `--isolate-assertions`, individual assertions can be verified by filtering on the line that contains them. When processing a single file, the filename can be skipped, for example: `dafny verify MyFile.dfy --filter-position=:23`");
 
- public static readonly Option<string> ExtractTarget = new("--extract", @"
-Extract Dafny types, functions, and lemmas to Boogie.
-(use - as <file> to output to console.)".TrimStart()) {
- IsHidden = true,
- ArgumentHelpName = "file",
- };
-
  public static Command Create() {
  var result = new Command("verify", "Verify the program.");
  result.AddArgument(DafnyCommands.FilesArgument);
@@ -64,7 +50,6 @@ public static Command Create() {
  PerformanceStatisticsOption,
  FilterSymbol,
  FilterPosition,
- ExtractTarget,
  DafnyFile.DoNotVerifyDependencies
  }.Concat(DafnyCommands.VerificationOptions).
  Concat(DafnyCommands.ConsoleOutputOptions).
@@ -91,21 +76,11 @@ public static async Task<int> HandleVerification(DafnyOptions options) {
  await verificationSummarized;
  await verificationResultsLogged;
  await proofDependenciesReported;
-
- if (!resolution.HasErrors && options.BoogieExtractionTargetFile != null) {
- using var engine = ExecutionEngine.CreateWithoutSharedCache(options);
- try {
- var extractedProgram = BoogieExtractor.Extract(resolution.ResolvedProgram);
- engine.PrintBplFile(options.BoogieExtractionTargetFile, extractedProgram, true, pretty: true);
- } catch (ExtractorError extractorError) {
- await options.OutputWriter.WriteLineAsync($"Boogie axiom extraction error: {extractorError.Message}");
- return 1;
- }
- }
  }
 
  return await compilation.GetAndReportExitCode();
  }
+
  public static async Task ReportVerificationSummary(
  CliCompilation cliCompilation,
  IObservable<CanVerifyResult> verificationResults) {

Source/DafnyDriver/DafnyNewCli.cs

@@ -2,7 +2,6 @@
 using System;
 using System.Collections;
 using System.Collections.Generic;
-using System.Collections.Immutable;
 using System.CommandLine;
 using System.CommandLine.Builder;
 using System.CommandLine.Invocation;
@@ -11,16 +10,12 @@
 using System.IO;
 using System.Linq;
 using System.Reflection;
-using System.Security.AccessControl;
-using System.Text.RegularExpressions;
 using System.Threading.Tasks;
 using DafnyCore;
-using DafnyCore.Options;
 using DafnyDriver.Commands;
 using Microsoft.Boogie;
 using Microsoft.Dafny.Compilers;
 using Microsoft.Dafny.LanguageServer;
-using Microsoft.Dafny.LanguageServer.Workspace;
 
 namespace Microsoft.Dafny;
 
@@ -50,6 +45,7 @@ static DafnyNewCli() {
  AddCommand(AuditCommand.Create());
  AddCommand(CoverageReportCommand.Create());
  AddCommand(DocumentationCommand.Create());
+ AddCommand(ExtractCommand.Create());
 
  OptionRegistry.CheckOptionsAreKnown(AllOptions);
 
@@ -176,12 +172,7 @@ private static void ProcessOption(InvocationContext context, Option option, Dafn
  }
 
  public static Task<int> Execute(IConsole console, IReadOnlyList<string> arguments) {
- bool allowHidden = arguments.All(a => a != ToolchainDebuggingHelpName);
  foreach (var symbol in AllSymbols) {
- if (!allowHidden) {
- symbol.IsHidden = false;
- }
-
  if (symbol is Option option) {
  if (!option.Arity.Equals(ArgumentArity.ZeroOrMore) && !option.Arity.Equals(ArgumentArity.OneOrMore)) {
  option.AllowMultipleArgumentsPerToken = true;
@@ -261,8 +252,16 @@ private static CommandLineBuilder AddDeveloperHelp(RootCommand rootCommand, Comm
  var languageDeveloperHelp = new Option<bool>(ToolchainDebuggingHelpName,
  "Show help and usage information, including options designed for developing the Dafny language and toolchain.");
  rootCommand.AddGlobalOption(languageDeveloperHelp);
+ bool helpShown = false;
+ builder = builder.UseHelp(_ => helpShown = true);
+
  builder = builder.AddMiddleware(async (context, next) => {
- if (context.ParseResult.FindResultFor(languageDeveloperHelp) is { }) {
+ if ((context.ParseResult.CommandResult.Command.IsHidden && helpShown) || context.ParseResult.FindResultFor(languageDeveloperHelp) is { }) {
+
+ foreach (var symbol in AllSymbols) {
+ symbol.IsHidden = false;
+ }
+
  context.InvocationResult = new HelpResult();
  } else {
  await next(context);