About the command line options

[herbelin]

Collecting miscellaneous directions in passing about the handling the command-line arguments (sorry in advance if redundance with proposals I did not see):

• adding a unified way to declare a Set option on the command line (see @zimmi48's proposal) [Done by @SkySkimmer in #9876]
• adding a way to register new command-line flags dynamically, locally to a component which needs it (in the same spirit as Goptions.declare_bool_option).
• making a distinction between the different effects of a command line option:
  • configuration (e.g. -diffs on, or -debug)
  • initialization action (e.g. -l foo.v, or -q)
  • main action (e.g. batch query mode à la -where, or, implicitly, interactive)
  • post action (e.g. --memory , which should actually be -memory, or -output-context)
• incidentally fixing bugs such as -where/-config/-list-tags silently discarding other options
• collecting the configuration state into a record which can be passed around functionally

See also #9236, #9148, #6877.

Note: This is initially motivated by the discussion at #8669 but it goes beyond the scope of #8669, so I put it as an issue.

[Zimmi48]

Also related:

• having a generic way to declare an attribute associated to an option.

[ejgallego]

cc #9876

[herbelin]

The clarification of the differences and similarities between coqc and coqtop in the code is very useful. I now have other questions about the coqc command-line. If I understand correctly, there are two models used in parallel:

• the (default) .vo mode, the -vio2vo mode and the -quick mode take all remaining (non-option) arguments as names of targets to compile
• the -schedule-vio-check, -schedule-vio2vo and -check-vio-tasks takes all following names as targets to compile or check, until another -foo option is found

An advantage of the second model is that different kinds of compilation can be done in the same invocation of coqc. Moving the default, -vio2vo and -quick to the second model would however introduce a risk of incompatibility.

It would be simpler to implement, and simpler to remember the syntax, if all forms of compilation would follow the same syntax. Any opinions on what model to prefer?

Cc @ejgallego, @gares

Added note: What to do with the option -o? It can give only one name. So, in the second model, it could be given in the form -schedule-vio2vo k file1 -o fileout1 file2 -fileout2? In the first model, it would be forbiddent with more than one file.

[ejgallego]

Good question @herbelin , IMVHO it certainly deserves some more thinking.

A preliminary thought that comes to me is that usually, leaving processing of different targets to the build system [and thus having many invocations] tends to allow for better parallelism, but indeed one needs to think what the constraints are here.

[herbelin]

By the way, what should be the semantics of command line when there are interdepencies between components?

For instance, in

coqtop -w none -require Foo -w all -color no -require Bar

when, e.g., Foo and Bar print and warn? Should it be an error? Should it respect the order of options as if they were vernacular commands?

[ejgallego]

That's a very interesting example for a few reasons; I am not sure what the answer should be.

The first thought that came to my head is that -require is indeed a bit of a problematic option, as for example IDEs would have a hard time processing it due to the hidden dependencies it introduces.

What is the main rationale for supporting -require as opposed to Require Foo Bar.?

[herbelin]

What is the main rationale for supporting -require as opposed to Require Foo Bar.?

We could acccept only one -require. But there is also -load-vernac-object (the poorly-named equivalent to Require without Import) and we could ask the same for coqtop -w none -require Foo -w all -color no -load-vernac-object Bar.

Actually, the question is the same also for coqc -w none foo.v -color no -w all bar.v (or even coqide -w none foo.v -color no -w all bar.v). Is it "obvious" from the command line in which order will all its components be executed (or even discarded)?

Somehow, the sequential order would then be the most natural order (and even the simplest to implement if we consider what it would cost to provide appropriate error messages for every cases where an option will be silently discarded because it is incompatible with another one).

[herbelin]

As a matter of comparison, here are a few examples of gcc command line behaviors:

Query --help silently discards everything else in sight (relatively to what I tested)

  gcc -print-prog-name=foo --help
  gcc --help -print-prog-name=foo
  gcc titi.c --help toto.c

are all reinterpreted as:

  gcc --help

The other query, -print-prog-name=foo, silently discards other options (but --help)

gcc toto.c -print-prog-name=foo titi.c

is reinterpreted as

gcc -print-prog-name=foo

Repeating an option such as -o silently discards all instances except the last one

gcc toto.c -save-temps titi.c -o foo -o bar

is reinterpreted as

gcc -save-temps toto.c titi.c -o bar

as witnessed by the production of only a bar executable file.

A configuration option such as -save-temps is interpreted before actually compiling

gcc toto.c -save-temps titi.c

is reinterpreted as

gcc -save-temps toto.c titi.c

as witnessed by the presence of a .bc file also for toto.

Some tests of consistency between options are however sometimes done

gcc toto.c titi.c -o foo -c 

fails with "cannot specify -o when generating multiple output files".