Switch tlapm to cmdliner #177

glondu · 2024-11-21T09:10:28Z

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.

lemmy · 2024-11-21T14:14:42Z

Unfortunately, there are no resources to change/fix the Toolbox.

ahelwer · 2024-11-21T14:39:28Z

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?

glondu · 2024-11-22T07:30:46Z

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.

glondu · 2024-11-22T13:10:17Z

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?

glondu · 2024-11-22T15:10:02Z

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 tlaplus/tlaplus#1085

ahelwer · 2024-11-22T15:17:54Z

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?

glondu · 2024-11-25T08:17:54Z

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.

ahelwer · 2024-11-26T15:39:41Z

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.

muenchnerkindl · 2024-11-26T15:59:01Z

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.

kape1395 · 2024-11-26T17:22:48Z

Maybe for backwards compatibility we can:

support --toolbox A:B or a variant of that with some delimiters. ":" seems natural to specify a range.
If --toolbox A B is provided, consider --toolbox A as 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?

ahelwer · 2024-11-26T17:50:12Z

@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.

kape1395 · 2024-11-26T17:59:40Z

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?

ahelwer · 2024-11-26T18:21:20Z

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).

damiendoligez · 2024-12-03T12:39:08Z

In glondu#1 I propose a small change to patch up the command line before calling Cmdliner.

glondu · 2024-12-03T15:26:17Z

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?

lemmy · 2024-12-03T15:28:48Z

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?

ahelwer · 2024-12-03T15:29:29Z

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.

glondu · 2024-12-03T15:39:26Z

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...

ahelwer · 2024-12-03T20:07:03Z

So some old versions of the toolbox still send the deprecated options, which newer versions of TLAPM ignore?

glondu · 2024-12-04T08:33:43Z

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 tlaplus/tlaplus#1085 will still fail with the new TLAPM.

glondu · 2024-12-04T13:18:14Z

I've just pushed a version that ignores deprecated options. As such, tlaplus/tlaplus#1085 is no longer required to use the new tlapm.

ahelwer · 2024-12-04T20:07:39Z

Excellent! I'll take a look. Do you think tlaplus/tlaplus#1085 could be adapted to remove the unused deprecated CLI parameters?

ahelwer

Overall looks good.

One larger change is I would like to see some in-file tests for all the CLI options. This would require a bit of git history rewriting; the CLI tests should go in their own commit, before changing to cmdliner, so we can see that they pass for the original CLI. Then the next commit is your changes to switch to using cmdliner, with the tests unchanged (or only changed by adding more tests), to see that their correctness is maintained and the cmdliner changes do not break the public API.

test/fast/fingerprint/load_v8_test.tla.disabled

src/tlapm_args.ml

ahelwer · 2024-12-04T21:14:45Z

src/tlapm_args.ml

+  Arg.(value & opt int 3 & info ["wait"] ~docv:"TIME" ~doc)
+
+let stdin_t =
+  let doc = "Read the tla file from stdin instead of file system. \


The help output spacing is weird here:

Read the tla file from stdin instead of file system. Only applies if single tla file is provided as input.

Maybe this is due to Cmdliner justifying the text when displaying help in a terminal? "Weird" spacing disappears when using --help=plain.

src/tlapm_args.ml

ahelwer · 2024-12-04T21:20:59Z

src/tlapm_args.ml

-             is specified, the default value is \".tlacache\".";
-  ]
+             is specified, the default value is \".tlacache\"." in
+  Arg.(value & opt (some dir) None & info ["cache-dir"] ~docv:"DIR" ~doc)


Could make .tlacache the default value of this parameter instead of spelling it out in the docs?

I don't think this would be correct, since the command-line option overrides the environment variable TLAPM_CACHE_DIR, and .tlacache is used only when neither is given.

src/tlapm_args.ml

Signed-off-by: Stephane Glondu <[email protected]>

A preprocessing step strips out deprecated options (`-d`, `--paranoid`, `--isaprove`, `--fpdir`) and merges arguments of options that take two arguments (`--toolbox`, `--nofpl` and `--erasefp`). Thanks to Damien Doligez for the preprocessing idea to keep backward-compatibility. Signed-off-by: Stephane Glondu <[email protected]>

glondu · 2024-12-11T09:05:33Z

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 · 2024-12-11T14:17:46Z

src/tlapm_args.ml

+
+(* Preprocess command line before feeding it to Cmdliner, to preserve
+   backward compatibility. In particular, Cmdliner does not support
+   options with direct multiple arguments. *)


Could you add an example of the specific types of text that are being rewritten?

ahelwer · 2024-12-11T14:18:08Z

Thanks! Did you see the comment about testing?

glondu force-pushed the cmdliner-tlapm branch from b0d1606 to a496fa5 Compare November 21, 2024 09:11

lemmy added the enhancement A new feature, an improvement, or other addition. label Nov 21, 2024

glondu force-pushed the cmdliner-tlapm branch from 6fa9ff1 to fc037ec Compare November 22, 2024 15:10

lemmy mentioned this pull request Nov 22, 2024

Add support for new tlapm command-line syntax tlaplus/tlaplus#1085

Open

damiendoligez mentioned this pull request Dec 3, 2024

add backward-compatibility hack for command-line parsing glondu/tlapm#1

Open

glondu force-pushed the cmdliner-tlapm branch from fc037ec to 319d2a1 Compare December 3, 2024 15:23

glondu force-pushed the cmdliner-tlapm branch from 319d2a1 to d7b988e Compare December 4, 2024 13:17

ahelwer requested changes Dec 4, 2024

View reviewed changes

Stephane Glondu added 2 commits December 11, 2024 09:49

Remove references to deprecated --isaprove option

f63ccf5

Signed-off-by: Stephane Glondu <[email protected]>

glondu force-pushed the cmdliner-tlapm branch from d7b988e to 178acd7 Compare December 11, 2024 08:50

ahelwer reviewed Dec 11, 2024

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Switch tlapm to cmdliner #177

Switch tlapm to cmdliner #177

glondu commented Nov 21, 2024

lemmy commented Nov 21, 2024

ahelwer commented Nov 21, 2024

glondu commented Nov 22, 2024

glondu commented Nov 22, 2024

glondu commented Nov 22, 2024

ahelwer commented Nov 22, 2024

glondu commented Nov 25, 2024

ahelwer commented Nov 26, 2024

muenchnerkindl commented Nov 26, 2024

kape1395 commented Nov 26, 2024

ahelwer commented Nov 26, 2024

kape1395 commented Nov 26, 2024

ahelwer commented Nov 26, 2024 •

edited

Loading

damiendoligez commented Dec 3, 2024

glondu commented Dec 3, 2024

lemmy commented Dec 3, 2024

ahelwer commented Dec 3, 2024

glondu commented Dec 3, 2024

ahelwer commented Dec 3, 2024

glondu commented Dec 4, 2024

glondu commented Dec 4, 2024

ahelwer commented Dec 4, 2024

ahelwer left a comment •

edited

Loading

ahelwer Dec 4, 2024

glondu Dec 11, 2024

ahelwer Dec 4, 2024

glondu Dec 11, 2024

glondu commented Dec 11, 2024

ahelwer Dec 11, 2024

ahelwer commented Dec 11, 2024

Switch tlapm to cmdliner #177

Are you sure you want to change the base?

Switch tlapm to cmdliner #177

Conversation

glondu commented Nov 21, 2024

lemmy commented Nov 21, 2024

ahelwer commented Nov 21, 2024

glondu commented Nov 22, 2024

glondu commented Nov 22, 2024

glondu commented Nov 22, 2024

ahelwer commented Nov 22, 2024

glondu commented Nov 25, 2024

ahelwer commented Nov 26, 2024

muenchnerkindl commented Nov 26, 2024

kape1395 commented Nov 26, 2024

ahelwer commented Nov 26, 2024

kape1395 commented Nov 26, 2024

ahelwer commented Nov 26, 2024 • edited Loading

damiendoligez commented Dec 3, 2024

glondu commented Dec 3, 2024

lemmy commented Dec 3, 2024

ahelwer commented Dec 3, 2024

glondu commented Dec 3, 2024

ahelwer commented Dec 3, 2024

glondu commented Dec 4, 2024

glondu commented Dec 4, 2024

ahelwer commented Dec 4, 2024

ahelwer left a comment • edited Loading

Choose a reason for hiding this comment

ahelwer Dec 4, 2024

Choose a reason for hiding this comment

glondu Dec 11, 2024

Choose a reason for hiding this comment

ahelwer Dec 4, 2024

Choose a reason for hiding this comment

glondu Dec 11, 2024

Choose a reason for hiding this comment

glondu commented Dec 11, 2024

ahelwer Dec 11, 2024

Choose a reason for hiding this comment

ahelwer commented Dec 11, 2024

ahelwer commented Nov 26, 2024 •

edited

Loading

ahelwer left a comment •

edited

Loading