Structure and share command line arguments among components and tools

[gares]

Rendered https://github.com/gares/ceps/blob/argument-parsing/text/000-argument-parsing-oo.md

[gares]

Some excerpts.

How an option is declared:

type diffs_t = On | Off | Removed
class         diffs = fun r -> object
  val mutable diffs = Off
       method diffs = diffs
  initializer r#register
    "-diffs" "highlight differences between proof steps"
    (Enum(["on",On;"off",Off;"removed",Removed], (fun x -> diffs <- x)))
end

How options are put into a set:

class coqtop_options r = object
    inherit option_set r

    inherit stm_options r (* we take all options of the stm component *)
    inherit diffs r (* plus this one *)
    inherit coqdep_options r (* plus the ones supported by coqdep *)
 end

How a componet/tool can use these sets:

module Stm : sig

  val init : #stm_options -> unit

end

module Coqtop : sig

  val main : coqtop_options -> unit

end = struct
 
  let main o =
     (* the Stm.init type accepts any large enough set of options, so we can directly pass o *)
     Stm.init o;
     Format.printf "diffs are: %s@\n"
        (match o#diffs with Removed -> "rm" | On -> "ok" | Off -> "off");;

end

[gares]

Output of the toplevel sentences in the code of the CEP:

coqdep usage:
option           description
-print-version   prints the version of Coq
-file-name       <string> sets the file name of whatever


Coqdep receives options: true foo

Coqdep receives options: true foo

coqtop usage:
option           description
-file-name       <string> sets the file name of whatever
-diffs           (on|off|removed) highlight differences between proof steps
-async-proofs    <yes/no> enables/disables super powers and this is a
                 terribly long line that wraps around to test the
                 documentation layout
-print-version   prints the version of Coq


diffs are: rm

[gares]

This CEP is to address some of the issue identified in coq/coq#8818 and it is also pretty close to the way the state of Matita is implemented. So this CEP may also give ideas on how to organize the system state on a per component basis.

[ejgallego]

I think this looks fine tho the issues in Coq seem largely orthogonal to the current argument parsing mechanism , see https://github.com/coq/coq/pull/8690

This CEP is to address some of the issue identified in coq/coq#8818

I am not sure I do understand this part, I hope that parsing of configuration files doesn't need to know about the syntax of arguments themselves. That'd seem pretty heavyweight. If coqProject is missing structure we should add it I think, not try to infer it using internals of the tools.

[aspiwack]

You should probably explain in your CEP while you want to roll your own library rather than using an established one like cmdliner.

[gares]

Thanks for pointing out that library, it is really nice. The only missing bit is the oo part. Maybe could just reuse that library for parsing and printing and just craft an adaptor.

If I'm not mistaken (I gave only a quick read) the library lets you pass the values of the flags as function arguments to some code (lifted with const for example). More precisely, what I don't see is a way to:

• declare set of options and make a union of them
• organize the parsed values as objects collecting them rather than separate values

But given that things seem to be first class in that library, I guess one could wrap them in objects and obtain the same functionality without re-implementing parsing and printing!

My question now is why I did not find this library when I googled for it...

[ejgallego]

We have discussed cmdliner a few times, including https://github.com/coq/coq/issues/8818 , so I dunno.

Unfortunately it won't work for Coq unless we want to drop compatibility with the current set of arguments, as it implements getopt style arguments and there are some nits where the two are not compatible.

Also, it is not the best library to manage sets of arguments.

[gares]

If coqProject is missing structure we should add it I think, not try to infer it using internals of the tools.

Sure, but this is not the only problem I raise there.

coqc, coqtop, coqdep, coq_makefile... they all share some coq specific command line options. This CEP is about sharing their declaration, parsing and printing. And be able to have components (eg the STM) declare the subset it understands and be able to pass to the STM the options without rewriting them in a specific format or subset (this is what oo subtyping gives you).

You could say coq_makefile should not be in the list and parse a specific file format and have a completely disjoint set of command line options. I could buy that. Still it could benefit from a library for parsing and printing them.

[ejgallego]

This CEP is about sharing their declaration, parsing and printing.

Well, this is where I am lost, AFAICS, having implemented already sharing of arguments between coqtop and coqc, I see that issue is fully orthogonal to what is proposed here.

And be able to have components (eg the STM) declare the subset it understands and be able to pass to the STM the options without rewriting them in a specific format or subset (this is what oo subtyping gives you).

Well, it would be nice to have subtyping but so far the main problem you have here is that the STM is passing arguments not in the record format but mangling the actual command line, which is a serious problem and neither technique helps.

You could say coq_makefile should not be in the list and parse a specific file format and have a completely disjoint set of command line options. I could buy that. Still it could benefit from a library for parsing and printing them.

Oh, coq_makefile may share options, why not? I think that at least coqdep should share with coqc / coqtop and it will as soon as the other PRs get merged. However in order to do that we don't need any kind of subtyping or fancy stuff, thus the thing is orthogonal IMO.

Regarding _CoqProject the thing is that the file format has no structure, so no wonder you got problems there.

[ejgallego]

For the record this is the compat problem you would have with cmdliner:

      {- [names] defines the names under which an optional argument
         can be referred to. Strings of length [1] (["c"]) define
         short option names (["-c"]), longer strings (["count"])
         define long option names (["--count"]). [names] must be empty
         for positional arguments.}

I use cmdliner in all my projects, and I like it, however it is not compatible with Coq's format :(

[aspiwack]

Just to be clear: I don't want to say that cmdliner should be the solution. I'm saying that, if you are not using it, the CEP document should explain why not in reasonably compelling argument. Otherwise the question will keep popping up.

Related question: why does the OO bit matter, compared to the applicative-functor style of cmdliner? (again this would benefit from being explained in the document).

[gares]

About orthogonality and OO, the thing is the same.

You have components A and B in your system. You tools T and S.

T and S have to parse some arguments and represent their value, I call it o. Then You have to pass o, or better parts of it, to A and B. Some parts of o are A specific, some B specific, some are common.

1. If o is a record, you can't express that easily. You need o_unionAB, and o_A and o_B plus the various projections.

2. If o is a bunch of arguments (cmdliner style) then you don't have an easy way to pass it, you have to pass n arguments to A, m to B.

3. If o is an object, the type of A and B tell you which subset they use and you can pass o to both directly.

To me 1 is a pain to use, 2 is bearable, 3 is better. 1 is close to what we have today.

Having the list of arguments and their doc as a first class value is applicable in all cases. But writing the generic code that given a list generates the parser and printer and gives you o is only possible in 2 and 3.