Remove section paths from kernel names #8555

maximedenes · 2018-09-25T13:22:55Z

Let's see what CI says.

API documentation needs to be updated, and dev/doc/changes.md to mention a few renamings.

ppedrot · 2018-09-25T14:36:51Z

Looks broken...

gares · 2018-09-25T15:29:00Z

you need to fix dev/*ml stuff to :-/

herbelin · 2018-09-26T09:03:41Z

Can you explain your goals? Is it intended to be a purely internal cleaning or with a change of semantics in mind? For instance, does this have an impact in what About reports for constants in sections?

maximedenes · 2018-09-26T09:12:59Z

Can you explain your goals? Is it intended to be a purely internal cleaning or with a change of semantics in mind? For instance, does this have an impact in what About reports for constants in sections?

It is not fully internal, because it prevents for example:

Ltac f := idtac.
Section foo. Ltac f := idtac. End foo.

which was previously allowed. I didn't find an occurrence, except one in the test suite. But overall, it does not change much the semantics of names at the user level.

After this patch, About still reports the same thing, and you can still qualify constants using a section path, since this relies on the full_path / Nametab thing, not the kernel names that this patch cleans.

However, I was very surprised to discover one can qualify using section paths (and not just module paths), I'm not sure how aware users are of this feature. We may want to discuss it separately.

maximedenes · 2018-09-26T09:16:15Z

Can you explain your goals?

So the answer is I'm trying to clean (parts of) the section-related code, and save some memory.

ppedrot

I am supporting this change. It makes the kernel cleaner and reduces many places where we can break invariants while not removing any user-facing feature.

ppedrot · 2018-09-26T11:15:50Z

kernel/names.mli

  (** Projections *)

  val user : t -> KerName.t
  val canonical : t -> KerName.t

-  val repr3 : t -> ModPath.t * DirPath.t * Label.t
+  val repr2 : t -> ModPath.t * Label.t


Should probably be called repr.

I doubt it, because repr should return the two names...

ppedrot · 2018-09-26T11:17:17Z

kernel/term_typing.ml

-  let (_, dir, _) = Constant.repr3 kn in
-  let hcons = DirPath.is_empty dir in
+(*  let (_, dir, _) = Constant.repr3 kn in *)
+  let hcons = false (* XXX DirPath.is_empty dir *) in


Isn't that preventing section definitions from being hashconsed when they exit it?

In fact now that we don't have to change the names I think we could just hashcons when the cooking_info is empty.

Isn't that preventing section definitions from being hashconsed when they exit it?

Yeah, I completely forgot to come back to this part of the code, sorry.

Isn't that preventing section definitions from being hashconsed when they exit it?

In fact, I don't think so because the only call to translate_recipe already hash conses everything (body, type, universes)...

Can you confirm?

SkySkimmer · 2018-09-26T11:52:12Z

library/keys.ml

@@ -92,8 +92,7 @@ let subst_keys (subst,(k,k')) =
  (subst_key subst k, subst_key subst k')

 let discharge_key = function
-  | KGlob g when Lib.is_in_section g ->
-    if isVarRef g then None else Some (KGlob (pop_global_reference g))
+  | KGlob (VarRef _ as g) when Lib.is_in_section g -> None


Is there still a need for the when?

I don't know, the logic is pretty mysterious to me, so I kept the behavior of the original code.

herbelin · 2018-09-26T12:44:57Z

After this patch, About still reports the same thing, and you can still qualify constants using a section path, since this relies on the full_path / Nametab thing, not the kernel names that this patch cleans.

OK, I think I now understand.

One reason I'm worrying is that I feel that there is a general confusion about where to go with discharge and with overwriting the name of section variables in goal, a sea snake which blocks us to make progresses (e.g. with Proof using, with treating the copy of section variables in goal as goal variables, etc.). I'd like to hear a vision on this latter point, knowing that in the absence of a vision, I shall propose to have the discharge in the kernel and the section variables locally-global objects.

maximedenes · 2018-09-26T12:52:58Z

One reason I'm worrying is that I feel that there is a general confusion about where to go with discharge and with overwriting the name of section variables in goal, a sea snake which blocks us to make progresses (e.g. with Proof using, with treating the copy of section variables in goal as goal variables, etc.). I'd like to hear a vision on this latter point, knowing that in the absence of a vision, I shall propose to have the discharge in the kernel and the section variables locally-global objects.

I'm pretty sure discussion on these points is needed indeed, and you can open an issue about it. But as far as I can tell, this patch is completely orthogonal to these questions.

maximedenes · 2018-10-01T14:29:52Z

This is blocking on a fiat-crypto-legacy failure, but building it on my machine takes ~2h before I see the first coqc invocations...

maximedenes · 2018-10-03T13:58:11Z

Good, state what "essentially" means, like "they were used only in this case"

Ok, you're asking me to describe the previous design but I failed to understand it, so I'll let you amend the commit message in the way you like. I anyway exhausted the time I was planning to spend on this patch, and as mentioned above, I don't need it at all.

ejgallego · 2018-10-03T14:04:15Z

Ok, you're asking me to describe the previous design but I failed to understand it

Does that mean that you don't understand what this patch does?

I'll let you amend the commit message in the way you like.

I am very puzzled with this statement, which does seem wrong at several levels.

If you, the author of the patch, and maintainer of the subsystem in question, has deep trouble writing a short paragraph that documents the change for those doing git diving in the future, how am I supposed to come up with a description, precisely that I have no idea of what the patch does, nor what it does imply nor how does the kernel work.

maximedenes · 2018-10-03T14:05:45Z

Does that mean that you don't understand what this patch does?

Exactly.

ppedrot · 2018-10-03T14:11:44Z

Well, it's pretty clear: there is legacy code in the kernel that is essentially dead in a non-trivial way. So it doesn't hurt removing it, it makes the kernel more robust and reduces its attack surface.

gares · 2018-10-03T14:17:51Z

I dunno what others things

I'm fine with this patch.

ppedrot · 2018-10-04T09:08:40Z

@ejgallego are you reassured and OK for the PR?

ejgallego · 2018-10-04T09:10:18Z

Sure, I have nothing against the PR, which seems very welcome, I just said that the commit message could be a bit better than empty IMO. Give me a few minutes and I'll prepare a commit message then, given that I am supposed to do it, it seems.

ejgallego · 2018-10-04T16:27:52Z

Sorry for the delay, here it goes:

[kernel] Remove section paths from `KerName.t`

We remove sections paths from kernel names. This is a cleanup as most of the times this information was unused. This implies a change in the Kernel API and small user visible changes with regards to tactic qualification. In particular, the removal of "global discharge" implies a large cleanup of code.

Additionally, the change implies that some machinery in `library` and `safe_typing` must now take an `~in_section` parameter, as to provide the information whether a section is open or not.

We remove sections paths from kernel names. This is a cleanup as most of the times this information was unused. This implies a change in the Kernel API and small user visible changes with regards to tactic qualification. In particular, the removal of "global discharge" implies a large cleanup of code. Additionally, the change implies that some machinery in `library` and `safe_typing` must now take an `~in_section` parameter, as to provide the information whether a section is open or not.

maximedenes · 2018-10-05T06:58:21Z

Sorry for the delay, here it goes:

Thanks, commit updated.

ppedrot · 2018-10-05T09:34:19Z

CI failures are spurious, right? Iris is broken in master already...

ejgallego · 2018-10-05T14:17:04Z

CI failures are spurious, right? Iris is broken in master already...

Yup, CI here is good. However, this got bitten by the CHANGES disease so a new rebase seems to be needed :(

maximedenes · 2018-10-05T15:00:43Z

lol

gares · 2018-10-05T18:00:46Z

No rebase, the guy that merges should take care of the conflict.

ejgallego · 2018-10-06T15:00:34Z

I am confused or was this PR merged without the overlays having been properly submitted as PR @ppedrot ?

Anyways, CI in master is broken so please @maximedenes submit the corresponding PRs and @mattam82 @ppedrot merge, thanks.

ejgallego · 2018-10-06T15:01:23Z

Also not sure about the deprecation policy followed here.

ppedrot · 2018-10-06T15:08:03Z

I am confused or was this PR merged without the overlays having been properly submitted

Strange, the merge script didn't warn me that there were overlays, and I forgot to check that there were there indeed. I can merge the Ltac2 one quickly, and submit one in equations.

Also not sure about the deprecation policy followed here.

API changed in a non-backward compatible way, I don't think we can easily provide a deprecated interface.

ppedrot · 2018-10-06T15:12:36Z

PR submitted on equations and already merged in Ltac2.

maximedenes · 2018-10-06T15:19:30Z

Also not sure about the deprecation policy followed here.

API changed in a non-backward compatible way, I don't think we can easily provide a deprecated interface.

Yep, I did provide one deprecation warning for the construct for which I could see a transition path.

ejgallego · 2018-10-06T15:25:11Z

Cool, thanks @ppedrot

maximedenes requested review from amahboubi, forestjulien, gares, herbelin, mattam82, ppedrot and silene as code owners September 25, 2018 13:22

maximedenes added the needs: documentation Documentation was not added or updated. label Sep 25, 2018

maximedenes force-pushed the rm-section-path branch 4 times, most recently from 329d7d1 to b7b61f3 Compare September 26, 2018 07:36

maximedenes added the kind: cleanup Code removal, deprecation, refactorings, etc. label Sep 26, 2018

ppedrot approved these changes Sep 26, 2018

View reviewed changes

SkySkimmer reviewed Sep 26, 2018

View reviewed changes

maximedenes force-pushed the rm-section-path branch 5 times, most recently from 756d69a to 05ebff8 Compare October 1, 2018 08:47

maximedenes removed the needs: documentation Documentation was not added or updated. label Oct 1, 2018

gares approved these changes Oct 2, 2018

View reviewed changes

ppedrot added this to the 8.10+beta1 milestone Oct 3, 2018

This comment has been minimized.

Sign in to view

maximedenes force-pushed the rm-section-path branch from e75dfba to 650c65a Compare October 5, 2018 06:58

ejgallego added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Oct 5, 2018

ppedrot merged commit 650c65a into coq:master Oct 6, 2018

ppedrot added a commit that referenced this pull request Oct 6, 2018

Merge PR #8555: Remove section paths from kernel names

371566f

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

herbelin mentioned this pull request Oct 8, 2018

Clarifying that the "print" functions in Names are mainly for debugging #7817

Closed

1 task

jashug mentioned this pull request Oct 26, 2018

Proposal: Treat Section names only as documentation #8831

Open

maximedenes deleted the rm-section-path branch August 26, 2023 16:33

Remove section paths from kernel names #8555

Remove section paths from kernel names #8555

Conversation

maximedenes commented Sep 25, 2018

ppedrot commented Sep 25, 2018

gares commented Sep 25, 2018

herbelin commented Sep 26, 2018

maximedenes commented Sep 26, 2018

maximedenes commented Sep 26, 2018

ppedrot left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

herbelin commented Sep 26, 2018

maximedenes commented Sep 26, 2018

maximedenes commented Oct 1, 2018

maximedenes commented Oct 3, 2018

ejgallego commented Oct 3, 2018

maximedenes commented Oct 3, 2018

ppedrot commented Oct 3, 2018

gares commented Oct 3, 2018

ppedrot commented Oct 4, 2018

ejgallego commented Oct 4, 2018 • edited Loading

This comment has been minimized.

ejgallego commented Oct 4, 2018

maximedenes commented Oct 5, 2018

ppedrot commented Oct 5, 2018

ejgallego commented Oct 5, 2018 • edited Loading

maximedenes commented Oct 5, 2018

gares commented Oct 5, 2018

ejgallego commented Oct 6, 2018

ejgallego commented Oct 6, 2018

ppedrot commented Oct 6, 2018

ppedrot commented Oct 6, 2018

maximedenes commented Oct 6, 2018

ejgallego commented Oct 6, 2018

ejgallego commented Oct 4, 2018 •

edited

Loading

ejgallego commented Oct 5, 2018 •

edited

Loading