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
Structure and share command line arguments among components and tools #39
base: master
Are you sure you want to change the base?
Conversation
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 |
Output of the toplevel sentences in the code of the CEP:
|
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. |
I think this looks fine tho the issues in Coq seem largely orthogonal to the current argument parsing mechanism , see coq/coq#8690
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. |
You should probably explain in your CEP while you want to roll your own library rather than using an established one like cmdliner. |
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
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... |
We have discussed cmdliner a few times, including coq/coq#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 Also, it is not the best library to manage sets of arguments. |
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. |
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.
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.
Oh, Regarding _CoqProject the thing is that the file format has no structure, so no wonder you got problems there. |
For the record this is the compat problem you would have with
I use cmdliner in all my projects, and I like it, however it is not compatible with Coq's format :( |
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). |
About orthogonality and OO, the thing is the same. You have components A and B in your system. 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.
To me 1 is a pain to use, 2 is bearable, 3 is better. Having the list of arguments and their doc as a first class value is applicable in all cases. |
Rendered https://github.com/gares/ceps/blob/argument-parsing/text/000-argument-parsing-oo.md