[K-Bug] Missing file argument in kompile's flag

[Robertorosmaninho]

What component is the issue in?

Front-End

Which command

• kompile
• kast
• krun
• kprove
• kprovex
• ksearch

What K Version?

v6.0.83-0-gc2ad66e022

Operating System

MacOS (Apple Silicon/AMD)

Steps to Reproduce

When I tried to use --profile-rule-parsing as it's defined on our hidden-help flag

$ kompile -hh
...
 --profile-rule-parsing
      Generate time in milliseconds to parse each rule in the semantics.

I got the following confusing error message:

$ kompile -v --profile-rule-parsing test.k --main-module TEST

Parse command line options                                   =  0,014s
[Error] Critical: You have to provide exactly one main file in order to do
outer parsing.

After talking with @radumereuta at #3611 (comment) I saw the this flag actually expects a new file to write the time taken to parse each rule.

Expected Results

I would expect 3 things here:

• Check if any other flag expects a file or other type of input that isn’t currently described on -hh or -h.
• Modify the help message to be --profile-rule-parsing <file> and probably contain a more helpful description like Store in this file time taken in ms to parse each rule in the semantics as suggested by @radumereuta.
• If possible, modify the error message to be different when a flag doesn’t receive input.

The last is optional, but it’s something to consider. Currently kompile works as Usage: kompile [options] <file>, in this case, the --profile-rule-parsing consumed the K file instead of kompile. This could be avoided if we swap the order to kompile <file> [options], and then it will be easier to identify when we don’t pass input to kompile and when we don’t pass input for a kompile’s flag. Although, I admit that’s counterintuitive considering other compiler’s CLI design.

PS.: Also from @radumereuta:
"The output for the help command is handled automatically by thejcommnader library here: https://github.com/runtimeverification/k/blob/master/kernel/src/main/java/org/kframework/kompile/KompileUsageFormatter.java"

[radumereuta]

Find where the message is constructed in this file: https://github.com/runtimeverification/k/blob/master/kernel/src/main/java/org/kframework/kompile/KompileUsageFormatter.java

[Robertorosmaninho]

I've edited the table from #3417 (thanks for it @radumereuta).

kompile -h	parameter	kompile -hh	parameter
--backend	<backend>	--allow-anywhere-haskell	❌
--concrete-rules	<rules>	--bison-file	<path> or <file>
--coverage	❌	--bison-lists	❌
--debug	❌	--bison-parser-library	❌
--debug-warnings	❌	--bison-stack-max-depth	<size>
--emit-json	❌	--cache-file	<path> or <file>
--enable-llvm-debug	❌	--debug-type-inference	<path> or <file>
--enable-search	❌	--directory, -d	<path> or <dir>
--gen-bison-parser	❌	--enable-kore-antileft	❌
--gen-glr-bison-parser	❌	--floats-as-po	❌
--help, -h	❌	--haskell-backend-command	<command>
--help-hidden, -hh	❌	--heuristic	<heuristics>
--md-selector	<selectors>	--hook-namespaces	<string> or <namespaces>
--no-haskell-binary	❌	--ignore-missing-smtlib-warning	❌
--output-definition, -o	<path>	--iterated	❌
--syntax-module	<module>	--iterated-threshold	<value>
--temp-dir	<path>
--top-cell	❓	--llvm-kompile-output	<path> or <binary>
--verbose, -v	❌	--llvm-kompile-type	<type>
--version	❌	--maps-as-int-array	❌
--warnings, -w	<level>	--no-exc-wrap	❌
--warnings-to-errors, -w2e	❌	--no-llvm-kompile	❌
-E	❌	--no-prelude	❌
-I	<path> or <dir>	--post-process	<command>
-O1	❌	--profile-rule-parsing	<file>
-O2	❌	--read-only-kompiled-directory	❌
-O3	❌	--shutdown-wait-time	<time>
-W	<warning>	--smt	<solver>
-Wno	<warning>	--smt-prelude, --smt_prelude	<path>
		--timeout	<time>
		--z3-jni	❌
		--z3-tactic	<path> or <solver>
		-ccopt	<options>

I have some doubts about the name of the parameter (choosing between one or another) and what should be passed as a parameter (the items with ❓). Any help defining them is very welcome!

[radumereuta]

If you can't find a way to annotate the parameters with the value description, then you can simply modify the existing description with some message: Expected value: <file>

Now about your suggestions:
--backend = llvm|haskell|kore
--concrete-rules=labels
--md-selector=expression
--haskell-backend-command=command or executable
--post-process=command or executable
--smt=command or executable? (not sure)
--timeout=duration (seconds if it accepts only one format)
--z3-cnstr-timeout=duration^

[Robertorosmaninho]

@radumereuta, for kast, we have these:
I omitted the ones that don't need or that I've already implemented for kompile, and we get in kast for free.

parameter	argument
--color	<mode>
--expression, -e	<expression>
--input, -i	<mode>
--module, -m	<module>
--output, -o	<mode>
--output-file	<file>
--output-flatten	<KLabels>
--output-omit	<KLabels>
--output-tokast	<KLabels>
--output-tokenize	<KLabels>
--sort, -s	<sort>
--steps	<steps>
--definition	<path>

I'm unsure about --output-flatten, --output-omit, --output-tokast, and --output-tokenize as I never used them nor could find an example...
sort and steps looks silly, but it is the best one-word description that we have.

[Robertorosmaninho]

Here is the same table for kprove:

parameter	argument
--branching-allowed	<value>
--claims	<claims>
--color	<mode>
--debug-script	<file>
--default-claim-type	<type>
--definition	<path>
--depth	<value>
--emit-json-spec	<file>
--exclude	<claims>
--output, -o	<mode>
--output-file	<file>
--output-flatten	<KLabels>
--output-omit	<KLabels>
--output-tokast	<KLabels>
--output-tokenize	<KLabels>
--spec-module, -sm	<module>
--trusted	<claims>
--haskell-backend-command	<command>
--haskell-backend-home	<directory>
--smt-timeout	<milliseconds>