-
Notifications
You must be signed in to change notification settings - Fork 28
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Gobra CLI Input Documentation #610
Conversation
Maybe I am biased because I already know what the flags do but the description seems sufficient |
s""" Usage: ${GoVerifier.name} -i <input-files> [OPTIONS] OR | ||
| ${GoVerifier.name} -p <directory> [OPTIONS] | ||
s""" ${GoVerifier.name} supports three modes for specifying input files that should be verified: | ||
| ${GoVerifier.name} -i <input-files> [OPTIONS] OR |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
to my understanding the project root is relevant to resolve Go's package imports. Why is there no optional project root for -i
. Also, if the project root works the same for any input kind, then maybe the project root can be explained as a separate entity.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is what I tried to clarify on line 383:
You have the option --include
in mind, which is indeed applicable to all 3 modes.
However, --projectRoot
specifies a root directory based on which a unique identifier for each package should be derived (this is imho the only use case). This unique identifier is then used for caching purposes and the idea was that the same project on different computers (and thus different absolute paths) come up with the same unique package identifier (since the paths relative to the project root should be the same if configured correctly), such that cache files can be shared between machines
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Getting back to your original question, I honestly don't recall why we explicitly excluded the project root option from -i
. It might be related to the fact that the provided files might not fully represent a package (e.g. the files are located in different folders but all have the same package clause or only a subset of files of a package has been provided)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
In the explanation, I believe it is still a good idea to give a separate explanation for --projectRoot
if its semantics can be explained independent of the mode. Currently, it is also not clear to me what kind of criteria the argument to --projectRoot
has to satisfy.
| | ||
| Note that --include <directories> is unrelated to the modes above and controls how ${GoVerifier.name} resolves | ||
| package imports. | ||
| |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It seems to me that mode 2 and 3 are a bit confusing. Mode 2 could take a list of packages and then verify them. Mode 3 could take a list of dictonaries and verify all packages found therein (where one can still blacklist packages). The project root is a separate entity that just influences how package names are resolved. Then we would have an option to verify single files, single packages, and entire projects. Mode 2 could maybe even also use -i.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Isn't that what we have?
I think of these modes as follows:
- mode 1: take these files and verify them, don't care about where they are located in the filesystem
- mode 2: take these packages (specified via the directory in which they are located) and verify them
- mode 3: take this module / repo / ... and verify the packages in there (or only a subset as specified via includePackages and excludePackages)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think the confusion comes from the concrete flags and mode 3. For mode 3, the repo is given in a roundabout way through --projectRoot
which otherwise has a different purpose. The --includePackages
is counterintuitive to me because it specifies additional packages in a command that is supposed to verify all packages in folders; "Verify all packages in my project, ... and also these ones". If mode 3 takes a list of dictonaries, then the --includePackages
becomes redundant (and maybe mode 2 also becomes redundant). Regarding the flags, I think --dictonaries
for packages and --recursive
for something that currently does not have a provided target (like -d /wireguard -r
) is a bit counterintuitive.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I agree that the current separation between mode 2 and mode 3 is confusing, but at least the current description describes accurately what these modes do. From my perspective, --recursive
should be an option for mode two, instead of a separate option (this way, we might be able to deprecate --projectRoot
). Given this, we might want to change the flags already in this PR and change the corresponding description, or we might merge the description as is at the moment and later change it when we change the modes in a different PR
@jcp19 Felix suggested to merge the 2nd and 3rd input mode: 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:
If we were to delete a mode, I would delete the recursive mode but keep the option |
Interesting! For me,
|
Why do you prefer |
I'd say that's the reason. More specifically, if I don't add |
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 |
Co-authored-by: João Pereira <[email protected]>
a1bcfa9
to
529b823
Compare
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.