`/print` option shows command line arguments but not the actual configured options

[keyboardDrummer]

When Boogie is run through another tool, the /print option outputs Boogie file that at the top of the file show the command line options passed to that other tool, but not all the non-default Boogie options that Boogie was run with.

It would be great if Boogie would print the command that allows executing Boogie in the same way as in which it is currently executing.

[shazqadeer]

I did not understand this issue, perhaps because I did not try the experiment of running Boogie through another tool. When I run Boogie on the command line with /print option, I see the options I supplied on the command-line being printed in a comment at the top of the output file. This seemed good to me. Are you saying the problem happens only when Boogie is run via Dafny, for example?

[keyboardDrummer]

I did not understand this issue, perhaps because I did not try the experiment of running Boogie through another tool. When I run Boogie on the command line with /print option, I see the options I supplied on the command-line being printed in a comment at the top of the output file. This seemed good to me. Are you saying the problem happens only when Boogie is run via Dafny, for example?

Yes, this issue only occurs when Boogie is running programmatically. It will print the command line arguments from the originally invoked program, say Dafny, but not how you should invoke Boogie to get the same effect.

[RustanLeino]

Currently, a typical Boogie client (like Dafny) sets the Boogie options by assigning to fields in a Boogie.CommandLineOptions object. For example,

BCLO.TimeLimit = 10;
BCLO.VerifySnapshots = 3;

Any such assignment is unknown to the machinery that responds to /print.

Here are five possibilities:

0. Let /print output the value of every possible option, whether or not the client has set the option.

1. Let /print output the value of every option that, at the time of /print-ing, has a value that is different from Boogie's default for that option.

2. Change each Boogie.CommandLineOptions property setter to not just set a backing field but also store away, for the later benefit of /print, any option/value that was set.

3. Add a method

   void SetBoogieOption(string optionName, string optionValue)

   that parses the given optionName and optionValue, sets the corresponding Boogie.CommandLineOptions field, and also remembers these settings so that /print can reproduce them. A client would then use this method rather than setting the Boogie.CommandLineOptions fields directly.

4. Add a field ``` c# string OtherThingsIWantPrintToSay; ``` in `Boogie.CommandLineOptions`. Then, a client can set this field to whatever and `/print` can just output this string along with the other options.

Any thoughts on these?

[keyboardDrummer]

I suggest defining Boogie options using an abstraction that allows both parsing and printing the option, and that groups all code related to defining the option in one definition. Also, to define the UI for options more concisely and to enable autocompletion on the CLI, we should use System.CommandLine.

Below is a sketch for what it could look like.

interface IOption {
  System.CommandLine.Option CommandLineEquivalent { get; }
  object Get(CommandLineOptions options);
  void Set(CommandLineOptions options, value);
}

public CommandLineParser {
   private IReadOnlyList<IOption> options;

   public CommandLineParser(IReadOnlyList<IOption> options) {
     this.options = options;
   }

   public (int exitCode, CommandLineOptions result) Parse(string[] arguments) {
      // define a System.Command.RootCommand which will do the heavy lifting of the parsing.
      // Uses IOption.Set to fill CommandLineOptions
   }

  string PrintAllNonDefaultValues(CommandLineOptions options) {
    var result = new StringBuilder();
    foreach(var option in options) {
      var value = option.Get(options);
      var cliOption = option.CommandLineEquivalent;
      var default = cliOption.GetDefaultValue();
      if (!Equals(default, value)) {
        result.Write($"{cliOption.Name} = {value}");
      }
    }
    return result.ToString();
  }
}

class SpecificIntOption : Option<int> {
  public static readonly SpecificOption Instance = new SpecificIntOption();

  public int Get(CommandLineOptions options) => options.SpecificOption;
  public void Set(CommandLineOptions options, int value) => options.SpecificOption = value;

  System.CommandLine.Option CommandLineEquivalent {
    get {
      var result  = new Option<int>("--my-name", "my description");
      result.SetDefaultValue(3);
      return result;
    }
  }
}

In a later stage we could also replace CommandLineOptions with an untyped record Options(IDictionary<IOption, object> OptionValues);, and replace option uses of the form CommandLineOptions.OptionName with OptionName.Instance.Get(Options options)