Remove obsolete locality #1049

maximedenes · 2017-09-13T13:12:25Z

We remove deprecated syntax "Coercion Local" and such, and seize the
opportunity to refactor some code around vernac_expr.

This is a preliminary step for the work on attributes.

We also fix a related classification issue in the STM.

silene · 2017-09-13T13:24:58Z

The existence of both Discharge:discharge and Discharge:locality confuses me to no end. I am even surprised you never had to disambiguate between the two, for example in vernac/lemmas.ml.

maximedenes · 2017-09-13T13:26:40Z

Well, they really mean the same thing. So is that so much of a problem? And of course, the point is to make the discharge type disappear at some point.

SkySkimmer · 2017-09-13T13:27:13Z

Ocaml is pretty smart about disambiguating constructors. Enable warnings 41 and 42 in the configure.ml to see how much it happens in the coq code.

maximedenes · 2017-09-13T13:27:49Z

I'm fine with changing it btw, if you suggest a name :)

maximedenes · 2017-09-13T13:29:49Z

In fact maybe I have a candidate. We could rename Discharge:locality into SectionLocal because it will then reflect the three values I plan to allow for this attribute.

silene · 2017-09-13T13:31:47Z

We could rename Discharge:locality into SectionLocal

What would Local:locality mean then? ModuleLocal? (Is that a thing?)

maximedenes · 2017-09-13T13:32:17Z

What would Local:locality mean then? ModuleLocal? (Is that a thing?)

Yes. (I guess)

maximedenes · 2017-09-13T13:32:33Z

Note that it is already what it means. AFAIK

silene · 2017-09-13T13:35:22Z

Note that it is already what it means.

It is not always clear to me when Local means module or file locality. Anyway, yes, please change locality to reflect these subtle details; that would be quite an improvement over the current code.

maximedenes · 2017-09-13T13:37:28Z

Oh my god! I realize only now a huge flaw of this PR. The syntax:

Coercion Local zar := fun n : nat => n.

is still valid (but with a different meaning), since Local is not a keyword.

maximedenes · 2017-09-13T13:44:35Z

It is not always clear to me when Local means module or file locality. Anyway, yes, please change locality to reflect these subtle details; that would be quite an improvement over the current code.

The Local keyword (which is not a keyword) can mean module-local or section-local, but IIUC, Local:locality means module-local. You're right, I'll update the code to better reflect it.

Any objection to making Local and Global true keywords? Otherwise I don't see how to guarantee that this removal will not do crazy things.

SkySkimmer · 2017-09-13T13:46:02Z

Otherwise I don't see how to guarantee that this removal will not do crazy things.

Leave the grammar entry in but parse to an error?

silene · 2017-09-13T13:51:12Z

Any objection to making Local and Global true keywords?

No objection on my side, and Coercion too.

But it seems that there has never been any warning Deprecated syntax: use "Local" as a prefix regarding Coercion Local. This is a serious flaw, which should be dealt with, as soon as in 8.7.

maximedenes · 2017-09-13T13:57:42Z

Leave the grammar entry in but parse to an error?

Yeah, but it's many grammar entries, and the point of this PR was to remove them :)

maximedenes · 2017-09-13T13:58:09Z

But it seems that there has never been any warning Deprecated syntax: use "Local" as a prefix regarding Coercion Local. This is a serious flaw, which should be dealt with, as soon as in 8.7.

Oh! I didn't know. I'll fix it, and hopefully try to make the beautifier do this translation for 8.7.

herbelin

This looks very good.

The solution adopted for Let does not look bad: like Coercion, Class, etc., it adds a flavor to Definition, namely here the Discharge flavor.

About Coercion Local, maybe an error for some while. Otherwise Definition Local := 0 is accepted, so why not Coercion Local?

About clarifying when Local/Global refers to a section or module scope, something remains to be done, certainly. Maybe elaborating about the names Private, Extern, ... @aspiwack and @ppedrot also had ideas about that.

(edited for typos)

herbelin · 2017-09-13T13:27:03Z

parsing/g_vernac.ml4

@@ -1145,33 +1132,33 @@ GEXTEND Gram
     | IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with";
       refl = LIST1 class_rawexpr -> VernacBindScope (sc,refl)

-     | IDENT "Infix"; local = obsolete_locality;
+     | IDENT "Infix";


To satisfy at the nitpicking tradition, I would delete the newline here.

Sure, will fix, thanks!

herbelin · 2017-09-13T13:30:42Z

plugins/ssr/ssrvernac.ml4

@@ -546,7 +546,7 @@ GEXTEND Gram
          d = G_vernac.def_body ->
          let s = coerce_reference_to_id qid in
 	  Vernacexpr.VernacDefinition
-	    ((Some Decl_kinds.Global,Decl_kinds.CanonicalStructure),
+	    ((NoDischarge,Decl_kinds.CanonicalStructure),


Isn't this a change of semantics of Local Canonical? (By the way - heavily insisting 😄 -, what are the motivations and mid-term plans of SSReflect developers w.r.t. this redundancy?)

Good question, I wasn't too sure about this one. Do you mean that the current default locality for definitions depend on their kind? I'll double check.

herbelin · 2017-09-13T13:35:18Z

stm/vernac_classifier.ml

+         match discharge with
+         | Decl_kinds.NoDischarge -> GuaranteesOpacity
+         | Decl_kinds.Discharge -> Doesn'tGuaranteeOpacity
+       in


This is a fix compared to previous version?

Yes, see commit message.

herbelin · 2017-09-13T13:36:01Z

vernac/locality.ml

+  | None, NoDischarge -> Global
+  | None, Discharge -> Discharge
+  | Some true, Discharge -> CErrors.user_err Pp.(str "Local not allowed in this case")
+  | Some false, Discharge -> CErrors.user_err Pp.(str "Global not allowed in this case")


herbelin · 2017-09-13T14:03:53Z

@silene:

> Coercion Local S:nat>->nat.
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^
Warning: Deprecated syntax: use "Local" as a prefix.
[deprecated-local-syntax,deprecated]

maximedenes · 2017-09-13T14:04:27Z

Is it also triggered when the body is provided?

herbelin · 2017-09-13T14:08:08Z

Is it also triggered when the body is provided?

Ah, ok, now I connect to the gitter quiproquo.

maximedenes · 2017-09-18T14:25:31Z

It is not always clear to me when Local means module or file locality.

Oh, I had read your question incorrectly. I have no idea about the distinction of module locality vs file locality. @ppedrot?

gares

I've only looked at the classifier fix

maximedenes · 2017-10-09T13:07:20Z

Oh, I had read your question incorrectly. I have no idea about the distinction of module locality vs file locality. @ppedrot?

@ppedrot?

ppedrot · 2017-10-09T18:53:51Z

@maximedenes What? The question is not even well-defined, there is not even such thing as a module or section locality, locality is a property of libobjects and they have idiosyncratic implementations that cannot be unified.

ejgallego · 2017-10-09T19:31:10Z

idiosyncratic implementations that cannot be unified.

Not even in part? What could/would be some good candidates to move to a unified direct-control implementation?

This is preparing the landing of coq/coq#1049. For now, I'm duplicating this patch which was already done upstream in CoqPrime, but please consider removing this ad-hoc copy (see discussion on PR mit-plv#269).

This is preparing the landing of coq/coq#1049. For now, I'm duplicating this patch which was already done upstream in CoqPrime, but please consider removing this ad-hoc copy (see discussion on PR #269).

maximedenes · 2017-11-22T10:32:42Z

Green light here:
https://travis-ci.org/maximedenes/coq/builds/305513414

Zimmi48 · 2017-11-22T16:06:51Z

So have you chosen a solution to avoid the issue with Coercion Local and such. Have you made Local into a keyword?

maximedenes · 2017-11-22T16:10:54Z

So have you chosen a solution to avoid the issue with Coercion Local and such. Have you made Local into a keyword?

No, I did not. Since this syntax was deprecated really a long time ago, I think it is ok. I should add an entry in CHANGES, to help porting, though.

maximedenes · 2017-11-28T14:21:29Z

Green light here: https://travis-ci.org/maximedenes/coq/builds/308320677

We remove deprecated syntax "Coercion Local" and such, and seize the opportunity to refactor some code around vernac_expr. We also do a small fix on the STM classification, which didn't know about Let Fixpoint and Let CoFixpoint. This is a preliminary step for the work on attributes.

maximedenes · 2017-11-30T15:21:23Z

green light again: https://travis-ci.org/maximedenes/coq/builds/309020975

maximedenes requested review from herbelin and gares September 13, 2017 13:14

herbelin reviewed Sep 13, 2017

View reviewed changes

gares approved these changes Sep 19, 2017

View reviewed changes

maximedenes added the needs: feedback Feeback from users and testers would be welcome. label Oct 9, 2017

maximedenes force-pushed the remove-obsolete-locality branch from 795066c to fca135d Compare October 11, 2017 08:00

maximedenes removed the needs: feedback Feeback from users and testers would be welcome. label Oct 11, 2017

Zimmi48 added the kind: cleanup Code removal, deprecation, refactorings, etc. label Oct 11, 2017

maximedenes added the needs: progress Work in progress: awaiting action from the author. label Oct 19, 2017

This was referenced Oct 30, 2017

Fix warnings math-comp/math-comp#90

Open

Fix obsolete vernacular syntax for locality. math-comp/math-comp#153

Merged

maximedenes force-pushed the remove-obsolete-locality branch from fca135d to 8daec9b Compare October 30, 2017 14:18

maximedenes added this to the 8.8 milestone Oct 30, 2017

maximedenes mentioned this pull request Nov 17, 2017

Remove ad-hoc copy of CoqPrime. mit-plv/fiat-crypto#269

Closed

maximedenes mentioned this pull request Nov 20, 2017

Remove obsolete syntax for locality. mit-plv/fiat-crypto#270

Merged

maximedenes force-pushed the remove-obsolete-locality branch 2 times, most recently from 60595d7 to 9bbb2f8 Compare November 21, 2017 22:16

maximedenes removed the needs: progress Work in progress: awaiting action from the author. label Nov 22, 2017

maximedenes force-pushed the remove-obsolete-locality branch from 9bbb2f8 to a18185a Compare November 22, 2017 13:20

maximedenes force-pushed the remove-obsolete-locality branch 2 times, most recently from 33a1b80 to dd65bb5 Compare November 23, 2017 16:34

maximedenes added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Nov 27, 2017

maximedenes force-pushed the remove-obsolete-locality branch from dd65bb5 to 90ea619 Compare November 28, 2017 08:48

maximedenes force-pushed the remove-obsolete-locality branch from 90ea619 to ae5944b Compare November 29, 2017 15:12

maximedenes merged commit ae5944b into coq:master Nov 30, 2017

maximedenes added a commit that referenced this pull request Nov 30, 2017

Merge PR #1049: Remove obsolete locality

e29993c

maximedenes deleted the remove-obsolete-locality branch November 30, 2017 15:23

Zimmi48 removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Nov 30, 2017

Remove obsolete locality #1049

Remove obsolete locality #1049

Conversation

maximedenes commented Sep 13, 2017

silene commented Sep 13, 2017

maximedenes commented Sep 13, 2017

SkySkimmer commented Sep 13, 2017

maximedenes commented Sep 13, 2017

maximedenes commented Sep 13, 2017

silene commented Sep 13, 2017

maximedenes commented Sep 13, 2017

maximedenes commented Sep 13, 2017 • edited

silene commented Sep 13, 2017

maximedenes commented Sep 13, 2017

maximedenes commented Sep 13, 2017

SkySkimmer commented Sep 13, 2017

silene commented Sep 13, 2017

maximedenes commented Sep 13, 2017

maximedenes commented Sep 13, 2017

herbelin left a comment • edited

Choose a reason for hiding this comment

herbelin Sep 13, 2017

Choose a reason for hiding this comment

maximedenes Sep 13, 2017

Choose a reason for hiding this comment

herbelin Sep 13, 2017

Choose a reason for hiding this comment

maximedenes Sep 13, 2017

Choose a reason for hiding this comment

herbelin Sep 13, 2017

Choose a reason for hiding this comment

maximedenes Sep 13, 2017

Choose a reason for hiding this comment

herbelin Sep 13, 2017

Choose a reason for hiding this comment

herbelin commented Sep 13, 2017

maximedenes commented Sep 13, 2017

herbelin commented Sep 13, 2017

maximedenes commented Sep 18, 2017

gares left a comment

Choose a reason for hiding this comment

maximedenes commented Oct 9, 2017

ppedrot commented Oct 9, 2017

ejgallego commented Oct 9, 2017

maximedenes commented Nov 22, 2017

Zimmi48 commented Nov 22, 2017

maximedenes commented Nov 22, 2017

maximedenes commented Nov 28, 2017

maximedenes commented Nov 30, 2017

maximedenes commented Sep 13, 2017 •

edited

herbelin left a comment •

edited