tlaplus
Switch tlapm to cmdliner
This pull request switches tlapm to cmdliner for command-line parsing. Note that it slightly changes the syntax and reverse dependencies (TLA Toolbox? VSCode?) will have to be fixed.
Note that it slightly changes the syntax and reverse dependencies (TLA Toolbox? VSCode?) will have to be fixed.
Can you expand what is meant by this?
Note that it slightly changes the syntax and reverse dependencies (TLA Toolbox? VSCode?) will have to be fixed.
Can you expand what is meant by this?
It means some adaptation is needed by users of tlapm. They are described in the first commit.
Unfortunately, there are no resources to change/fix the Toolbox.
I will try to fix it myself. What is the proper venue for support? Is there a mailing-list or forum?
Unfortunately, there are no resources to change/fix the Toolbox.
I will try to fix it myself. What is the proper venue for support? Is there a mailing-list or forum?
I've added an item to tlapm --config output and adapted the Toolbox in https://github.com/tlaplus/tlaplus/pull/1085
I don't think it is a good idea to break the public API of the command unless there's a very good reason; what do you see as the benefits of this change?
I don't think it is a good idea to break the public API of the command unless there's a very good reason
I generally agree with this statement.
what do you see as the benefits of this change?
Cmdliner is a library with a nicer API than Arg that has traction in the OCaml community. It imposes POSIX and GNU conventions on command-line syntaxes and automatically generates manpages.
It turns out that Cmdliner does not (and won't) support options with several arguments (as in --toolbox A B) because it doesn't fit said conventions. I chose to support --toolbox A,B which is Cmdliner's default for this kind of option. Note that --toolbox=A,B is also automatically supported. I could have chosen --toolbox "A B" as well (but it doesn't solve the compatibility issue).
Note that this pull request doesn't take much advantage Cmdliner's nicer API; in my opinion, more refactoring would be needed. I tried to have the changes localized in a single file for this pull request.
Maybe @muenchnerkindl (the one who asked me to do this) or @damiendoligez have other reasons.
If Stephan is interested in doing this then I am fine with it, versioning an API isn't the worst thing in the world - especially because this tool hasn't seen a point release in a while.
Before I get too much credit for the idea, the change was suggested by @kape1395 with the objective to ultimately reduce the number of global variables. As @glondu says, the current PR is only a first step towards achieving this goal. Unfortunately, it turned out (much to our surprise) that Cmdliner doesn't support command-line options that take more than one parameter, unless separated by a symbol other than a space.
Maybe for backwards compatibility we can:
- support
--toolbox A:Bor a variant of that with some delimiters. ":" seems natural to specify a range. - If
--toolbox A Bis provided, consider--toolbox Aas a "named option" and "B" as a separate "positional" argument. I guess currently, all the positional options are considered files. But if --toolbox only gets one number and there is a positional argument that looks like a number, consider it an end of the range.
That's not very clean from the implementation perspective, but maybe would help to resolve the problem?
@glondu already implemented API versioning (see toolbox PR) so I don't think having a separate toolbox command would be necessary. Also not a fan of hacking around the behavior of cmdliner, which seems to go against the original reason for adopting it.
The original reason was to reduce the number of global refs. Interpreting the cmdliner arguments doesn't sound like hacking it or objecting to the initial goal.
I thought you were in favor of not changing the CLI API:
I don't think it is a good idea to break the public API of the command unless there's a very good reason; what do you see as the benefits of this change?
I think breaking CLI API without good reason is bad but greatly simplifying the CLI parsing code (or reducing the number of global refs, although I am not sure what that means) could be a good reason.
I don't think exposing the old CLI API through an extra --toolbox flag is a good design; it's easy to update the toolbox to use the new API, the hard part is dealing with people using the old toolbox before those fixes and new version of TLAPM. (edit: I misunderstood, the --toolbox flag is the actual CLI arg that is broken not a new arg we are adding for compatibility).
In https://github.com/glondu/tlapm/pull/1 I propose a small change to patch up the command line before calling Cmdliner.
I've updated my branch with the tip from Damien which restores the compatibility of two-argument options.
What about deprecated options? Do we want to continue to accept (and ignore) them?
I've updated my branch with the tip from Damien which restores the compatibility of two-argument options.
Does this make https://github.com/tlaplus/tlaplus/pull/1085 obsolete?
Oh wonderful!!! It would be nice to accept & ignore deprecated options if that does not induce any difficulty, although since the next release of TLAPM will probably be at least 1.6.0 (a minor version bump), that does indicate to users that API compatibility breaks are possible so I would accept dropping long-deprecated options.
I've updated my branch with the tip from Damien which restores the compatibility of two-argument options.
Does this make tlaplus/tlaplus#1085 obsolete?
The part about --toolbox, yes, but not the part about stopping using deprecated options...
So some old versions of the toolbox still send the deprecated options, which newer versions of TLAPM ignore?
So some old versions of the toolbox still send the deprecated options, which newer versions of TLAPM ignore?
In the current state of main branches, the Toolbox sends deprecated options that TLAPM ignores.
With the current state of this PR, deprecated options are removed, and TLAPM fails if they are used. So the Toolbox without https://github.com/tlaplus/tlaplus/pull/1085 will still fail with the new TLAPM.
I've just pushed a version that ignores deprecated options. As such, https://github.com/tlaplus/tlaplus/pull/1085 is no longer required to use the new tlapm.
Excellent! I'll take a look. Do you think https://github.com/tlaplus/tlaplus/pull/1085 could be adapted to remove the unused deprecated CLI parameters?
Excellent! I'll take a look. Do you think tlaplus/tlaplus#1085 could be adapted to remove the unused deprecated CLI parameters?
Already done!
@ahelwer: it seems a bit strange to use in-file tests to check CLI parsing, but why not. Where would you put these tests? Would they simply call Cmd.eval_value' with a bunch of different arrays?
I haven't scoped out the best place to put the tests but perhaps they'd best be placed somewhere else. I realize it is a fairly large ask of the contributor so I am happy to write the tests myself in the coming month. But basically yeah the tests should just isolate the command-line parsing logic as it is, ensuring that when the logic is swapped out here nothing changes.
In fact, since you want to use the same tests for both the old-style and the Cmdliner command-line parsers, we'll have no choice but to test from the shell itself, because they don't share a common function.
But then, we'll need to have a way to print out the result of parsing the command-line without launching the proof-checking.
Do you think it's possible to do some preliminary refactoring to isolate the command line parsing code before writing the tests? This is a common issue I've run into in a lot of projects, which tend to put the command line parsing logic right in the main method which makes it very hard to test. Of course that then would interfere with these changes.