Certain invalid flags to idris2 return a successful exit code

[alexhumphreys]

Steps to Reproduce

$ idris2 --check --build lsp.ipkg
Not all command line options can be used to override package options.

Overridable options are:
    --quiet
    --verbose
    --timing
    --log <log level>
    --dumpcases <file>
    --dumplifted <file>
    --dumpvmcode <file>
    --debug-elab-check
    --codegen <cg>
    --directive <directive>
    --build-dir <dir>
    --output-dir <dir>

$ echo $?
0

Expected Behavior

The above looks like an error to me, as I'm using the flags incorrectly. I'd expect the command to return a non-zero exit code.

Observed Behavior

The exit code is 0.

Notes

Idris2 produces non-zero error codes for other failures, eg.

$ idris2 --build not-found.ipkg
Uncaught error: File error (not-found.ipkg): File Not Found
$ echo $?
1

I tried briefly to dig into the code to see where these error codes are set, but wasn't able to work it out.

[gallais]

We are pretty sloppy when it comes to validating options. That is true for Idris itself and for the cli arguments handled by the test lib too.

In Idris itself we have (at least):

• processPackageOpts that only care about packages
• preOptions that only cares about options wrt loading the code
• postOptions that cares about what is to be done once the code is loaded

So if we never load the code (e.g. because processPackageOpts identified we just wanted to do something package-related) then a bunch of cli arguments are never actually looked at and checked.

Additionally, these functions tend to blindly overwrite an existing value if the valid format assumes that you may supply an argument only at most once e.g. idris2 --cg node --cg chez is equivalent to idris2 --cg chez.

[buzden]

e.g. idris2 --cg node --cg chez is equivalent to idris2 --cg chez

Sometimes for some CLI commands it is intentional and convenient when you use such command in scripts and when you form the arguments automatically. So if you want your setting strictly, you put it in the end, if not, you put it in the beginning.

[kenaryn]

Maybe something like exitWith (ExitFailure 64) could be added somewhere in a preOptions definition in src/Idris/SetOptions.idr or altering the processOptions definition in src/Idris/Package.idr in order to deal with a Enumerated type or something and therefore return 64 instead of 0. But I do not know how to do that in Idris2.

With regard to your Notes-related snippet outputing exit code 1, it shall be (from my point of view): exitWith (ExitFailure 65) because it represents a invalid data input injected by the user. Here is a link regarding to what could be closer to a "convention" exit coding style: https://www.freebsd.org/cgi/man.cgi?query=sysexits&apropos=0&sektion=0&manpath=FreeBSD+4.3-RELEASE&format=html

It is often useful to convey more information into the exit code to avoid looking at the source code while still having an approximate understanding of the failure.