Automatically generated documentation for configuration options confuses users into using curly braces

[MartinSpiessl]

This came up here:

https://gitlab.com/sosy-lab/software/cpachecker/-/issues/578#note_412755260

Currently e.g. configuration options with ImmutableList.of() as default value are printed as myoption={} in the compiled documentation of configuration options. If the default value for a option is a non-empty collection, it will look like this:

slicing.conditionFiles = {
          Paths.get("output/AssumptionAutomaton.txt"),
          Classes.getCodeLocation(ReducerExtractor.class)
              .resolveSibling("config/specification/AssumptionGuidingAutomaton.spc")}

This leads to users expecting to be able to input curly braces when they specify a specific value for such an option.
In this case there also appears java code, which leads user's to think that they might also provide this.

Ideally the type information is conveyed in the documentation in a less confusing manner.

Let's take for example:

cpa.smg.deallocationFunctions = {"free"}

Here if we omit the {} it looks fine, that command could also be written like that in a configuration. But then of course the user loses the type information (the fact that the option is fine with more than one string, separated by commas).

For other kinds of option we already provide information about the argument type, e.g.:

cpa.slicing.weakeningStrategy = CEX
  enum:     [SYNTACTIC, DESTRUCTIVE, CEX]

One proposal how to solve this would be to specify a option that is backed by a collection with a trailing comma:

#proposal 1
cpa.smg.deallocationFunctions = free,

But I find that rather ugly. Another proposal would be to provide the type information in an extra line (much like with enums):

#proposal 2
cpa.smg.deallocationFunctions = free
  accepts a list of arguments (separated by ",")

Yet another way to do it completely different would be to use explicitly state the grammar/structure/type that is expected as value:

#proposal 3
cpa.smg.deallocationFunctions = <string>,...
  default:                    = free

or the other way around:

#proposal 4
cpa.smg.deallocationFunctions = free
  type: <string>,...

Maybe we can also provide more semantic type information, e.g. for slicing.conditionFiles something like:

#proposal 5
  type: List<Path>

[PhilippWendler]

The reason for using { and [ in the past was indeed to convey the information to the user that the respective option accepts a set or a list of values.

I do not like proposal 1 because it is easy to miss, does not nicely handle the case of an empty list, and I am actually not sure whether a trailing comma is allowed.

Proposals 3 to 5 would make sense if the information is correctly present for all kinds of values that we currently support, and if it turns out to not be irrelevant in most cases. Otherwise I would suggest proposal 2.

Note that the code already supports printing a verbose version of the option list, which currently looks like this:

# Deallocation functions
cpa.smg.deallocationFunctions
  field:    deallocationFunctions
  class:    org.sosy_lab.cpachecker.cpa.smg.SMGOptions
  type:     ImmutableSet
  default value: {"free"}

[MartinSpiessl]

Note that the code already supports printing a verbose version of the option list, which currently looks like this:

Cool feature, any chance you can tell my how I can output this? (I could search myself, but it looks like you already know how to do this).

The question is why the default value is still printed as {"free"} here when free would be more readable and closer to what is actually allowed as input

[kfriedberger]

For CPAchecker, you can un-comment the line <arg value="-v"/> in build/build-documentation-local.xml to get the verbose output.

[PhilippWendler]

If you use CPAchecker, you can just add -v when running scripts/cpa.sh -printOptions. For other projects you need to check how they expose this functionality.