Export options by ppedrot · Pull Request #6923 · rocq-prover/rocq

ppedrot · 2018-03-06T13:03:22Z

This PR implements the Export Set/Unset feature as discussed in the last WG.

This feature has been asked many times by different people, and allows to have options in a module that are performed when this module is imported.

This supersedes the well-numbered cursed PR #313.

I did not document it in the refman yet, as I don't know what's the protocol regarding the sphinx port of the documentation. What is recommended?

ejgallego · 2018-03-06T13:07:50Z

I think this looks good @ppedrot , however I wonder what level of "promise" should be made on this extension. IMVHO it is still not clear what the story with scoping may be, so we may want to label this option as "Use at your own risk".

Maybe the "Coq 9" project would be a good moment to unify the handling of scoped semantics.

maximedenes · 2018-03-06T13:09:17Z

I did not document it in the refman yet, as I don't know what's the protocol regarding the sphinx port of the documentation. What is recommended?

My plan is to integrate the infrastructure PR ASAP. Then, chapters will be merged one by one and removed from the manual. So it is probably best to wait. What chapter would this doc go in?

ppedrot · 2018-03-06T13:10:30Z

@ejgallego I don't know if this should be flagged as experimental. I definitely dislike the syntax inflation that is used to work around the scoping mess, but I'm fundamentally convinced this is the correct semantics for module-bound options. If anything, the syntax should be marked experimental, not what it does.

ppedrot · 2018-03-06T13:12:00Z

@maximedenes I guess in the description of variants of Set and Unset, in Chapter 6: Vernacular commands.

ejgallego · 2018-03-06T13:12:19Z

Yup I suggest we add a small warning so at least users are aware syntax [and maybe semantics even if I agree with you] may be still in flux, so those wanting to write "super-stable" Coq can avoid this.

maximedenes · 2018-03-06T13:13:20Z

so those wanting to write "super-stable" Coq can avoid this.

What should the warning recommend them to use instead, if they want to be stable?

ejgallego · 2018-03-06T13:14:37Z

What should the warning recommend them to use instead, if they want to be stable?

You just don't use it. I mean a sentence in the documentation by the way, not an actual warning in the code.

maximedenes · 2018-03-06T13:16:48Z

You just don't use it.

If you mean use Set without the Export modifier, isn't it going to make them write code that is going to break semantically (more painful) when we do the cleanup? I'm not convinced it would be a good recommendation.

ejgallego · 2018-03-06T13:21:07Z

If you mean use Set without the Export modifier, isn't it going to make them write code that is going to break semantically (more painful) when we do the cleanup? I'm not convinced it would be a good recommendation.

I'm afraid I cannot follow. When we do the cleanup many things will break almost for sure, but if you keep the status-quo nothing should become worse.

maximedenes · 2018-03-06T13:22:58Z

I'm afraid I cannot follow. When we do the cleanup many things will break almost for sure, but if you keep the status-quo nothing should become worse.

What I'm trying to say is that using the Export modifier is probably going to make things better in terms of stability for most users. Indeed, after the cleanup, we may want to remove that specific syntax at some point, but at least the semantics should stay in some form. So I'm afraid that telling users who want stable code not to use this feature is counter productive for them.

ejgallego · 2018-03-06T13:31:56Z

Hard to say, we will see. It will be quite confusing as for example Export is not supported on many other things such as Coercions etc... in fact, as of today it is a quite rushed hack.

So I'm fine with rushed hacks as long as they are documented as such.

Zimmi48 · 2018-03-06T13:33:11Z

If we are pretty confident that the semantics is the right one, then we can use this new syntax to unify the rest around this. And thus, keep the new syntax (and probably completely deprecate Global).

maximedenes · 2018-03-07T10:21:46Z

@ppedrot can you assign a reviewer?

ppedrot · 2018-03-07T12:36:16Z

I'm not quite sure about the proper person to review that patch. Any volunteers?

vbgl · 2018-03-07T12:47:11Z

@@ -150,11 +152,11 @@ val get_ref_table :

 (** The first argument is a locality flag.
    [Some true] = "Local", [Some false]="Global". *)


This comment is outdated and should be fixed.

vbgl · 2018-03-07T13:03:13Z

-  | VernacSetAppendOption (key,v) -> vernac_set_append_option ~atts key v
-  | VernacUnsetOption key -> vernac_unset_option ~atts key
+  | VernacSetOption (export, key,v) -> vernac_set_option ~atts export key v
+  | VernacSetAppendOption (key,v) -> vernac_set_append_option ~atts false key v


This is dead code. The constructor VernacSetAppendOption should be removed from the vernac_expr data type.

SkySkimmer · 2018-03-07T13:33:08Z

-val set_string_option_value_gen : bool option -> option_name -> string -> unit
-val set_string_option_append_value_gen : bool option -> option_name -> string -> unit
-val unset_option_value_gen : bool option -> option_name -> unit
+val set_int_option_value_gen    : ?locality:option_locality -> option_name -> int option -> unit


Why not keep it as a required argument?

Well, there is a default value in the type, so it's just a matter of taste.

maximedenes · 2018-03-08T10:25:12Z

@ppedrot ping

ppedrot · 2018-03-08T11:49:51Z

@maximedenes Changes addressed.

maximedenes · 2018-03-09T08:35:02Z

@vbgl do you approve now?

vbgl

I did not test, but the diff looks good.

maximedenes · 2018-03-09T09:07:54Z

@ppedrot Doesn't this break equations and ltac2?

maximedenes · 2018-03-09T12:41:58Z

@RalfJung @ppedrot this is going to miss 8.8 just because it doesn't have overlays. If you don't want that to happen, please push them ASAP (I'm wrapping up all integrations this afternoon, and CI takes a long time to run).

RalfJung · 2018-03-09T12:47:09Z

What's an overlay...?

maximedenes · 2018-03-09T12:50:05Z

What's an overlay...?

This PR breaks ltac2 and equations, and no fixes where pushed there AFAICT. An overlay is what makes CI picks up those fixes when testing external devs.

ppedrot · 2018-03-09T13:13:50Z

I'm on it.

This prevents relying on an underspecified bool option argument.

This feature has been asked many times by different people, and allows to have options in a module that are performed when this module is imported. This supersedes the well-numbered cursed PR rocq-prover#313.

Zimmi48 · 2018-03-09T13:21:12Z

@RalfJung FYI you should read https://github.com/coq/coq/blob/master/dev/ci/README.md#information-for-developers (even if partially outdated) and check this https://github.com/coq/coq/tree/master/dev/ci/user-overlays (linked from the previous file. BTW the first file was linked from the contributing guide but I suppose you have already read this one.

maximedenes · 2018-03-09T16:11:45Z

Success here: https://travis-ci.org/ppedrot/coq/builds/351302366

maximedenes · 2018-03-09T16:13:21Z

@ppedrot you forgot to open PRs...

maximedenes · 2018-03-09T16:15:56Z

I did it for you...

Zimmi48 · 2018-03-09T16:30:21Z

An issue should be open not to forget to document this before 8.8.0.

RalfJung · 2018-03-10T14:43:18Z

@Zimmi48 done (#6963). I don't know which labels to use though, and whom to assign. I hope I got the milestone right :D

ppedrot added needs: review kind: feature New user-facing feature request or implementation. labels Mar 6, 2018

ppedrot added this to the 8.8+beta1 milestone Mar 6, 2018

ppedrot mentioned this pull request Mar 6, 2018

Scoped options #313

Closed

vbgl self-requested a review March 7, 2018 12:39

vbgl reviewed Mar 7, 2018

View reviewed changes

SkySkimmer reviewed Mar 7, 2018

View reviewed changes

ppedrot force-pushed the export-options branch from fc6b09a to 4d7b754 Compare March 8, 2018 11:49

vbgl approved these changes Mar 9, 2018

View reviewed changes

vbgl added needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. and removed needs: review labels Mar 9, 2018

maximedenes removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Mar 9, 2018

ppedrot added 3 commits March 9, 2018 10:17

Export the various option localities in the API.

38a671f

This prevents relying on an underspecified bool option argument.

Implement the Export Set/Unset feature.

25b07a6

This feature has been asked many times by different people, and allows to have options in a module that are performed when this module is imported. This supersedes the well-numbered cursed PR rocq-prover#313.

Documenting the Export modifier for options in CHANGES.

eca4848

Add an overlay for Equations and Ltac2.

a8297dd

ppedrot force-pushed the export-options branch from 4d7b754 to a8297dd Compare March 9, 2018 13:30

maximedenes merged commit a8297dd into rocq-prover:master Mar 9, 2018

maximedenes added a commit that referenced this pull request Mar 9, 2018

Merge PR #6923: Export options

3b4bae6

RalfJung mentioned this pull request Mar 10, 2018

Document Export Set/Unset #6963

Closed

ppedrot deleted the export-options branch March 27, 2018 13:32

		@@ -150,11 +152,11 @@ val get_ref_table :

		(** The first argument is a locality flag.
		[Some true] = "Local", [Some false]="Global". *)

Conversation

ppedrot commented Mar 6, 2018

Uh oh!

ejgallego commented Mar 6, 2018

Uh oh!

maximedenes commented Mar 6, 2018

Uh oh!

ppedrot commented Mar 6, 2018

Uh oh!

ppedrot commented Mar 6, 2018

Uh oh!

ejgallego commented Mar 6, 2018

Uh oh!

maximedenes commented Mar 6, 2018

Uh oh!

ejgallego commented Mar 6, 2018

Uh oh!

maximedenes commented Mar 6, 2018

Uh oh!

ejgallego commented Mar 6, 2018

Uh oh!

maximedenes commented Mar 6, 2018

Uh oh!

ejgallego commented Mar 6, 2018

Uh oh!

Zimmi48 commented Mar 6, 2018

Uh oh!

maximedenes commented Mar 7, 2018

Uh oh!

ppedrot commented Mar 7, 2018

Uh oh!

vbgl Mar 7, 2018

Choose a reason for hiding this comment

Uh oh!

vbgl Mar 7, 2018

Choose a reason for hiding this comment

Uh oh!

SkySkimmer Mar 7, 2018

Choose a reason for hiding this comment

Uh oh!

ppedrot Mar 8, 2018

Choose a reason for hiding this comment

Uh oh!

maximedenes commented Mar 8, 2018

Uh oh!

ppedrot commented Mar 8, 2018

Uh oh!

maximedenes commented Mar 9, 2018

Uh oh!

vbgl left a comment

Choose a reason for hiding this comment

Uh oh!

maximedenes commented Mar 9, 2018

Uh oh!

maximedenes commented Mar 9, 2018

Uh oh!

RalfJung commented Mar 9, 2018

Uh oh!

maximedenes commented Mar 9, 2018

Uh oh!

ppedrot commented Mar 9, 2018

Uh oh!

Zimmi48 commented Mar 9, 2018

Uh oh!

maximedenes commented Mar 9, 2018

Uh oh!

maximedenes commented Mar 9, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

maximedenes commented Mar 9, 2018

Uh oh!

Zimmi48 commented Mar 9, 2018

Uh oh!

RalfJung commented Mar 10, 2018

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

maximedenes commented Mar 9, 2018 •

edited

Loading