Stream: Coq users

Topic: Noisy printing with name mangling light

view this post on Zulip Robbert Krebbers (May 09 2023 at 15:43):

We recently started using the new name mangling light feature of Coq in std++ and Iris, see https://github.com/coq/coq/pull/14695

Export Set Mangle Names.
Export Set Mangle Names Light.
(** Make these names stand out more, in case one does end up in the proof script. *)
Export Set Mangle Names Prefix "__".

Instead of just prefixing names that are introduced into the context, it affects all pretty printing. For example:

Search big_sepL2.

...

big_sepL2_sep:
  ∀ {__PROP : bi} {__A __B : Type} (__Φ __Ψ : nat → __A → __B → __PROP) (__l1 : list __A) (__l2 : list __B),
    ([∗ list] __k↦__y1;__y2 ∈ __l1;__l2, __Φ __k __y1 __y2 ∗ __Ψ __k __y1 __y2)
    ⊣⊢ ([∗ list] __k↦__y1;__y2 ∈ __l1;__l2, __Φ __k __y1 __y2) ∗ ([∗ list] __k↦__y1;__y2 ∈ __l1;__l2, __Ψ __k __y1 __y2)
big_sepL2_app:
  ∀ {__PROP : bi} {__A __B : Type} (__Φ : nat → __A → __B → __PROP) (__l1 __l2 : list __A) (__l1' __l2' : list __B),
    ([∗ list] __k↦__y1;__y2 ∈ __l1;__l1', __Φ __k __y1 __y2)
    ⊢ ([∗ list] __k↦__y1;__y2 ∈ __l2;__l2', __Φ (length __l1 + __k) __y1 __y2) -∗
      [∗ list] __k↦__y1;__y2 ∈ (__l1 ++ __l2);(__l1' ++ __l2'), __Φ __k __y1 __y2
big_sepL2_sep_sepL_l:
  ∀ {__PROP : bi} {__A __B : Type} (__Φ : nat → __A → __PROP) (__Ψ : nat → __A → __B → __PROP) (__l1 : list __A) (__l2 : list __B),
    ([∗ list] __k↦__y1;__y2 ∈ __l1;__l2, __Φ __k __y1 ∗ __Ψ __k __y1 __y2) ⊣⊢ ([∗ list] __k↦__y1 ∈ __l1, __Φ __k __y1) ∗
    ([∗ list] __k↦__y1;__y2 ∈ __l1;__l2, __Ψ __k __y1 __y2)
big_sepL2_sep_sepL_r:
  ∀ {__PROP : bi} {__A __B : Type} (__Φ : nat → __A → __B → __PROP) (__Ψ : nat → __B → __PROP) (__l1 : list __A) (__l2 : list __B),
    ([∗ list] __k↦__y1;__y2 ∈ __l1;__l2, __Φ __k __y1 __y2 ∗ __Ψ __k __y2) ⊣⊢ ([∗ list] __k↦__y1;__y2 ∈ __l1;__l2, __Φ __k __y1 __y2) ∗
    ([∗ list] __k↦__y2 ∈ __l2, __Ψ __k __y2)

This not readable.

Is this a feature or a bug of name mangling light? Is there a way to disable it mangling names during pretty printing?

view this post on Zulip Pierre Roux (May 09 2023 at 15:46):

I would call it a feature. In Prosa we are only using -mangle-names in a dedicated CI job. I don't think it is meant to be used in everyday development.

view this post on Zulip Ralf Jung (May 09 2023 at 15:47):

Pierre Roux said:

I would call it a feature. In Prosa we are only using -mangle-names in a dedicated CI job. I don't think it is meant to be used in everyday development.

-mangle-names is not but the motivation behind "name mangling light" was exactly that

view this post on Zulip Ralf Jung (May 09 2023 at 15:47):

only having it on CI regularly leads to contributor confusion since when they locally go to where CI failed, everything works

view this post on Zulip Ralf Jung (May 09 2023 at 15:48):

so we'd like a mechanism that is more like ssreflect's, which is suited for local development (except I actually dont like that ssreflect rejects apply _H_ since that can make debugging very annoying)

view this post on Zulip Pierre Roux (May 09 2023 at 15:53):

Make sense. I guess the ssreflect rationale for forbidding the use of _H_ is that ? is meant to be used only very locally (the rule in mathcomp is "allowed only if the introduced variable is gone at the end of the line").

view this post on Zulip Ali Caglayan (May 09 2023 at 16:30):

I don't think it will be possible to print the mangled names differently since the mangling is happening at quite a low level.

view this post on Zulip Ali Caglayan (May 09 2023 at 16:31):

One workaround is to unset mangle names light before printing.

view this post on Zulip Ali Caglayan (May 09 2023 at 16:35):

We could make it so that certain cases of printing disable name mangling locally. But this seems like quite an ad-hoc behaviour.

view this post on Zulip Ali Caglayan (May 09 2023 at 16:36):

That way an error message from coqc would contain mangled names. But a user query like Search would disable name mangling.

view this post on Zulip Paolo Giarrusso (May 09 2023 at 17:24):

@Ralf Jung so you prefer Unset SsrIdents. during debugging? I've tried adding it ~/.coqrc like other "debugging" settings (Set Nested Proofs Allowed), but of course there are rough edges

view this post on Zulip Paolo Giarrusso (May 09 2023 at 17:25):

(that setting requires loading ssreflect in .coqrc, which is okayish in iris but for instance breaks stdpp)

view this post on Zulip Robbert Krebbers (May 09 2023 at 17:44):

I don't think it will be possible to print the mangled names differently since the mangling is happening at quite a low level.

Could you explain why ssreflect does not suffer from this problem? Ssreflect can mangle names when introducing them into the context, but printing is not affected.

view this post on Zulip Karl Palmskog (May 09 2023 at 17:46):

is everyone using Std++ going to get names mangled by the export (e.g., by importing the prelude)? I hope not, this would probably affect legacy code that is costly to update...

view this post on Zulip Robbert Krebbers (May 09 2023 at 17:51):

Karl Palmskog said:

is everyone using Std++ going to get names mangled by the export (e.g., by importing the prelude)? I hope not, this would probably affect legacy code that is costly to update...

No, only if you import the options file.

view this post on Zulip Karl Palmskog (May 09 2023 at 17:52):

OK, that's good to know. I don't think we do that in our projects.

view this post on Zulip Ralf Jung (May 09 2023 at 18:19):

Paolo Giarrusso said:

Ralf Jung so you prefer Unset SsrIdents. during debugging? I've tried adding it ~/.coqrc like other "debugging" settings (Set Nested Proofs Allowed), but of course there are rough edges

I just didnt know Unset SsrIdents is a thing. :joy:

view this post on Zulip Ralf Jung (May 09 2023 at 18:20):

Ali Caglayan said:

I don't think it will be possible to print the mangled names differently since the mangling is happening at quite a low level.

I mean ssreflect achieves what we need so it's clearly possible... we just want it on intros ? (and everywhere else coq accepts into patterns), where ssreflect only kicks in on move=>?.

view this post on Zulip Ralf Jung (May 09 2023 at 18:21):

Karl Palmskog said:

OK, that's good to know. I don't think we do that in our projects.

indeed that's why we have the options file, to share options across ssreflect/iris without forcing it on downstream users. maybe we should have more clear warnings about this somewhere against importing the options file.

view this post on Zulip Ali Caglayan (May 09 2023 at 18:27):

Ralf Jung said:

Ali Caglayan said:

I don't think it will be possible to print the mangled names differently since the mangling is happening at quite a low level.

I mean ssreflect achieves what we need so it's clearly possible... we just want it on intros ? (and everywhere else coq accepts into patterns), where ssreflect only kicks in on move=>?.

I'm not sure how ssreflect does name mangling. But the way it is currently implmemented is quite general. Everytime coq needs a fresh name it calls a naming function. Usually this increments a prefix index on the variable. With name mangling there is a prefix added instead or just an integer. These fresh names get used everywhere.

view this post on Zulip Ali Caglayan (May 09 2023 at 18:28):

It might be possible to do something satisfactory if ssreflect manages to do it like you have said. In which case it would be beneficial to open an issue tracking this feature request.

view this post on Zulip Ralf Jung (Jun 01 2023 at 15:03):

opened an issue: https://github.com/coq/coq/issues/17673

Last updated: Oct 13 2024 at 01:02 UTC