Command-line setters for options

[SkySkimmer]

Draft until documented

TODO coqproject handling (for now it can be done through -arg I guess)

Closes #9295.

[ejgallego]

I am bit wary of stuff like this because I do believe that the whole option system should rewritten instead of keep adding some more kludges such as this one that may end up being technical debt in the end. For example doing #8666 is not possible with the current system.

But if people want that I am OK with this patch. You need however:

• to add documentation,
• to check that the command handling stuff work correctly w.r.t. workers (see asynctaskqueue)

[ejgallego]

So indeed maybe @SkySkimmer if you think this shouldn't go in 8.10 then I'd suggest we chat a bit about the Options API then we go ahead to merge this.

[SkySkimmer]

For example doing #8666 is not possible with the current system.

I don't understand.

to check that the command handling stuff work correctly w.r.t. workers (see asynctaskqueue)

How do I do that?

[ejgallego]

I don't understand.

The current API doesn't allow atomic setup of several options and that is a big problem for use cases such as the one in the PR [printing all has to become a bad hack]

How do I do that?

Good question, there is some filtering there, so I guess you should check that the options are correclty passed to the worker processes with ps ax or such.

[SkySkimmer]

Good question, there is some filtering there, so I guess you should check that the options are correclty passed to the worker processes with |ps ax| or such. no need to ps, just launching coqide with a -set caused it to die ;) fixed now Gaëtan Gilbert

…

On 01/04/2019 14:34, Emilio Jesús Gallego Arias wrote: I don't understand. The current API doesn't allow atomic setup of several options and that is a big problem for use cases such as the one in the PR [printing all has to become a bad hack] How do I do that? Good question, there is some filtering there, so I guess you should check that the options are correclty passed to the worker processes with |ps ax| or such. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#9876 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ACWQ7HFjuI_pNz6hg0Ccz-kASR6XWzI4ks5vcfy4gaJpZM4cVkc0>.

[Zimmi48]

Redesigning the whole option system would be definitely welcome (if someone has ideas, please start a CEP). However, in the meantime there are lots of low-hanging fruits (and TBH the option system works better than one could expect given the heavy use that we make of it).

In particular, this PR is very welcome, as are all incremental improvements until someone has a better proposal.

[ejgallego]

Preliminary review: this is looking good, I don't have any comment; I assigned to myself.

I will do in-depth review when the PR goes out of draft status.

[SkySkimmer]

Added doc.
The doc for -set-to is quite verbose due to the complex behaviour, maybe it would be better to have separate -set-int and -set-string so that we don't have to implement any quoting behaviour.

[ejgallego]

The doc for -set-to is quite verbose due to the complex behaviour, maybe it would be better to have separate -set-int and -set-string so that we don't have to implement any quoting behaviour.

Can't you delay the decision on the type after parsing the option and querying for its type?

I'd rather have a more uniform syntax by the way, what do you think of just:

• -set "Foo Bar=true"
• -set "Foo Bar=false"
• -set "Foo Ba=2" ,etc...

[ejgallego]

We need a choice on the milestone tho; this is the kind of change I'd even backport, but pinging @vbgl @Zimmi48 to see what they think.

[Zimmi48]

I agree with you: having -set-int and -set-string would avoid any confusion and would make the feature easier to use for this very special case when you want to pass "1" as the value of your option.

[SkySkimmer]

Why's appveyor complaining? And where's azure?
EDIT I'm touching the commit to reboot CI.

[Zimmi48]

I hadn't seen @ejgallego's comment above.

Can't you delay the decision on the type after parsing the option and querying for its type?

That sounds like a good solution too if it's not too heavy to implement.

I don't have any clear opinion on proposing integration in 8.10.

[ejgallego]

That sounds like a good solution too if it's not too heavy to implement.

Indeed it is more convenient for tools interacting with coqtop to expose single interface key=value so they don't have to be aware of types.

[ejgallego]

Indeed it is more convenient for tools interacting with coqtop to expose single interface key=value so they don't have to be aware of types.

Like imagine for example a project configuration in yaml, etc... this way you could write:

coq_options:
  printing all: true
  unification keys: active

etc...

[SkySkimmer]

In any case I'm not looking to change the semantics of v files for this PR.

[ejgallego]

In any case I'm not looking to change the semantics of v files for this PR.

@SkySkimmer I am waiting for an answer to #9876 (comment)

[SkySkimmer]

IMHO we should at least accept -set "Foo=" as unset;

Done for bool/int options

the type of Coqargs.option_command seems indeed too general [None should mean unset IMO].

It looks fine to me.

I'm keeping -unset

[ejgallego]

@SkySkimmer in:

type option_command = OptionSet of string option | OptionUnset

OptionSet None is just a special case for OptionSet (Some "true") IMO, you could remove the option type and just have parsing return true.

[ejgallego]

The change is pretty trivial, I've just done it.

[Zimmi48]

-set "Foo=" for unset sounds more reasonable for options than for flags IMHO. I think this is related to the current confusion around the Unset command that has a different meaning for options and flags (set to default vs set to false). Overall, I'm wondering if we are not rushing things by wanting this in 8.10. If we were to delay this to 8.11, and still merge early, it would leave time for everyone to check if they are satisfied with the chosen solution.

[SkySkimmer]

But then -set foo when foo is a string option means -set foo=true which is surprising to me, I prefer it being a type error.

[ejgallego]

LGTM, this is ready for merge an IMHO has a benefit/risk ratio high enough as to warrant inclusion in 8.10.

Semantics of UnSet and some other nuances with options predate this PR, it is a bit unfortunate we have to expose -unset in the command line as it will likely lead users towards -unset Foo instead of -set Foo=false which is IMO by far the preferred form.

This means this PR does introduce some technical debt at the cmdline level which is one of the worst parts of the system in terms of impact. I would still prefer if we could at least discourage the use of -unset in the documentation or restrict it somehow.

The note about improving the type of option_command does still apply indeed; I see no reason we should not tweak it before merge.

[ejgallego]

But then -set foo when foo is a string option means -set foo=true which is surprising to me, I prefer it being a type error.

Good point, no change then if you prefer. But for me this is indeed a warning that the shortcut -set Foo brings more ambiguity than benefits; I'm not sure allowing to omit the = sign is worth it.

Leaving a few hours more before merging so discussion can close.

[ejgallego]

Overall, I'm wondering if we are not rushing things by wanting this in 8.10. If we were to delay this to 8.11, and still merge early, it would leave time for everyone to check if they are satisfied with the chosen solution.

No problem in delaying this Theo if you think we should discuss more.

I think the first problem is that we don't agree on the distinction between "options" and "flags", I don't see why they are different; maybe I am influenced by my current choice of cmline handling in other projects. I dunno.

[ejgallego]

it would leave time for everyone to check if they are satisfied with the chosen solution.

I am personally OK with the current solution; I'd have chosen myself a more "regular" solution likely, but at some point stuff like this comes down to taste, and when you write the code, you have a fair amount of power XD so I guess at least myself I'm not willing to delay this more [otherwise at some point we will just halt all development]

[Zimmi48]

Not that I am not arguing to delay the merge. I'm perfectly OK with merging now. I'm just arguing to not squeeze this feature into 8.10, which seems like the normal thing to do when discussion has revealed that things are not that simple.

[Zimmi48]

I think the first problem is that we don't agree on the distinction between "options" and "flags", I don't see why they are different

Maybe, they should not be different. But they currently are (see documentation: https://coq.github.io/doc/master/refman/proof-engine/vernacular-commands.html#flags-options-and-tables).

[ejgallego]

I'm just arguing to not squeeze this feature into 8.10, which seems like the normal thing to do when discussion has revealed that things are not that simple.

Well, modulo a few nits, the current implementation seems reasonable to me; in the sense that semantics of the command line flags should match the ones of the vernaculars, is the current -set Foo= behavior a concern for you? My reasoning was to map to to the key/value system when Foo: appears.

If so we could revert.

[ejgallego]

I have been thinking about the milestone of this PR, and indeed it seems a bit complicated on the basis of what @Zimmi48 says:

• indeed, putting in to 8.10 seems a bit precipitate as we'd like maybe to think a bit more about what we do. On the other hand we seem to have reached a kind of fixpoint in the iterations, I'm not sure what more we'd like to change.
• on the other hand, putting this PR in 8.10 would greatly help us to get feedback from users, and thus help towards a more comprehensive re-design of the option / flag system.

So I dunno; I guess for me the best compromise in this case is to ship in 8.10, but declare the feature "experimental" , that is to say, 8.10 adopters should treat it like in beta / unstable, and thus only use it if they feel comfortable with having to tweak scripts in 8.11; on the other hand that'd allow us to get welcome feedback and testing.

[Zimmi48]

Sounds good to me.

[ejgallego]

Sounds good to me.

So is there some action to do on the docs then?

@SkySkimmer a last nit seems whether the non-uniformity of -set Foo vs -set Foo=true is worth the gain. That is of course a non-blocker for the PR but maybe we'd like to think twice.

IMVHO I'd at least add a note to the docs stating that -set Foo=true is preferred [and more future-proof]

[Zimmi48]

So is there some action to do on the docs then?

Well, at least the mention of the experimental status, no? Maybe also the link from the vernac section on options to the command-line flags section.

@SkySkimmer a last nit seems whether the non-uniformity of -set Foo vs -set Foo=true is worth the gain. That is of course a non-blocker for the PR but maybe we'd like to think twice.

IMVHO I'd at least add a note to the docs stating that -set Foo=true is preferred [and more future-proof]

I disagree... The doc could say that -set Foo is more human-oriented and -set Foo=true is more machine-oriented.

[ejgallego]

I disagree... The doc could say that -set Foo is more human-oriented and -set Foo=true is more machine-oriented.

That's another choice; but it not so much about "human vs machine" IMHO, more about how data formats these days work, for example JSON or YAML.

[ejgallego]

Leaving the question of the milestone and status of the PR open, IMHO no more benefit from delaying the actual merge; these issues could be addressed in additional PRs.