Gobra CLI Input Documentation

[ArquintL]

Extends banner to explain the 3 different modes for providing inputs to Gobra.

@reviewers: Please let me know whether this is (1) understandable and (2) sufficient.

[Dspil]

Maybe I am biased because I already know what the flags do but the description seems sufficient

[ArquintL]

@jcp19 Felix suggested to merge the 2nd and 3rd input mode: -d <list of dirs> --projectRoot <optional project root> takes the provided list of directories and searches (recursively!) for packages in them. --includePackage and --excludePackage would control which packages end up being verified. We were also thinking about good default values and I'd suggest the following: --projectRoot defaults to the current working directory (as of now). -d has to list at least one directory. (We could also default to the current directory or the project root but I don't see such a huge benefit justifying the added complexity of explaining what the default is)

Would this suggestion work for you / verified SCION? Or do you need something specifically from today's 2nd mode that would no longer be possible?

[jcp19]

@jcp19 Felix suggested to merge the 2nd and 3rd input mode: -d <list of dirs> --projectRoot <optional project root> takes the provided list of directories and searches (recursively!) for packages in them. --includePackage and --excludePackage would control which packages end up being verified. We were also thinking about good default values and I'd suggest the following: --projectRoot defaults to the current working directory (as of now). -d has to list at least one directory. (We could also default to the current directory or the project root but I don't see such a huge benefit justifying the added complexity of explaining what the default is)

Would this suggestion work for you / verified SCION? Or do you need something specifically from today's 2nd mode that would no longer be possible?

I would strongly oppose having the recursive mode take over the place of the directory mode for the following reasons:

• to me, it is a lot more common to verify a single package (i.e., the package I am verifying at the moment) instead of its entire list of dependencies.
• To have the behavior that I want, I would need to pass even more flags (by means of the include and exclude packages), which makes the usual case for me quite laborious. ~~In particular, if the packages passed to includePackages are themselves verified recursively, I would need to pass a single package and exclude all its dependencies. For reference, the router package of scion depends directly on, at least, 35 packages.~~
• From a usability standpoint, having the recursive mode by default sounds odd and may surprise users - for example, most command line tools I know allow you to apply a command recursively (usually, with -r or -R), but I don't recall seeing one command that does it by default.

If we were to delete a mode, I would delete the recursive mode but keep the option --recursive (to the directory mode, that is) and I would drop the includePackages option, which to me always felt redundant. Instead, we could verify recursively the list of packages passed to the directory mode, with the exception of those listed in excludePackages.

[ArquintL]

Interesting! For me, includePackages is very handy: I configure the Gobra command once more a particular module (consisting of various packages in its subfolders) by specifying the project root (i.e. the current directory) and the include paths (i.e. some directory to which I've downloaded (external) dependencies). I then either verify all packages in the module or individual ones by using includePackages.

includePackages is by no means recursive and (as soon as it's provided) acts as an allow list such that only the listed packages are verified (independently of the directories (whether recursive or not) provided as input to Gobra)

[jcp19]

includePackages is by no means recursive and (as soon as it's provided) acts as an allow list such that only the listed packages are verified (independently of the directories (whether recursive or not) provided as input to Gobra)

Why do you prefer includePackages over passing a list of directories to the directory mode? Is it because that way you can only pass the package name instead of the full path? I wonder if we could combine the two in the directory mode

[ArquintL]

I'd say that's the reason. More specifically, if I don't add --includePackages it will verify all and if I provide it (usually with only a single package name) verification is restricted. This seems more elegant to me that either specifying 8 or 9 paths to different packages (when I want to verify them all) or use 2 completely different set of commands to invoke Gobra

[jcp19]

The problem is that you may have different packages with the same name, in which case this approach is no longer expressive enough

[ArquintL]

The problem is that you may have different packages with the same name, in which case this approach is no longer expressive enough

That's correct. I think in that case one must resort to the directory mode