Stream: Coq devs & plugin devs

Topic: Adding locality to Typeclasses Opaque


view this post on Zulip Ali Caglayan (Jul 20 2021 at 15:06):

I am trying to add attribute support for Typeclasses Opaque and Transparent and I have made a draft PR: https://github.com/coq/coq/pull/14685

view this post on Zulip Ali Caglayan (Jul 20 2021 at 15:07):

However it doesn't work and I would like to learn why :-)

view this post on Zulip Pierre-Marie Pédrot (Jul 20 2021 at 15:08):

define "does not work"

view this post on Zulip Ali Caglayan (Jul 20 2021 at 15:09):

I added a test case in the PR

view this post on Zulip Pierre-Marie Pédrot (Jul 20 2021 at 15:09):

Yes, but what's the error?

view this post on Zulip Ali Caglayan (Jul 20 2021 at 15:09):

It doesn't recognize support for attributes

view this post on Zulip Ali Caglayan (Jul 20 2021 at 15:10):

This command does not support this attribute: export.
[unsupported-attributes,parsing]

view this post on Zulip Pierre-Marie Pédrot (Jul 20 2021 at 15:10):

you're probably using the wrong attribute specification

view this post on Zulip Pierre-Marie Pédrot (Jul 20 2021 at 15:10):

let me look at what we do for other hint commands

view this post on Zulip Ali Caglayan (Jul 20 2021 at 15:10):

But I thought this would be enough:

VERNAC COMMAND EXTEND Typeclasses_Rigid_Settings CLASSIFIED AS SIDEFF
| [ "Typeclasses" "Opaque" ne_reference_list(cl) ] -> {
    set_transparency cl false }
| #[ locality = Attributes.option_locality; ] [ "Typeclasses" "Opaque" ne_reference_list(cl) ] -> {
    set_transparency locality cl false }
END

sorry this is a poorly copied diff

view this post on Zulip Pierre-Marie Pédrot (Jul 20 2021 at 15:10):

it should indeed parse export

view this post on Zulip Pierre-Marie Pédrot (Jul 20 2021 at 15:14):

your example works for me ©

view this post on Zulip Ali Caglayan (Jul 20 2021 at 15:14):

OK, then am I doing something stupid to test it

view this post on Zulip Ali Caglayan (Jul 20 2021 at 15:15):

I run dune exec -- coqide

view this post on Zulip Pierre-Marie Pédrot (Jul 20 2021 at 15:17):

don't ask me, this is dark magic to me

view this post on Zulip Pierre-Marie Pédrot (Jul 20 2021 at 15:18):

I don't know of a way to make coqide really work out of the box

view this post on Zulip Pierre-Marie Pédrot (Jul 20 2021 at 15:18):

in theory you must call a shim

view this post on Zulip Pierre-Marie Pédrot (Jul 20 2021 at 15:18):

dune exec -- dev/shim/coqide-prelude or so

view this post on Zulip Guillaume Melquiond (Jul 20 2021 at 15:18):

Coqide and Coqtop (or rather Coqidetop) are two separate programs. If you just recompile Coqide, your changes are not taken into account.

view this post on Zulip Pierre-Marie Pédrot (Jul 20 2021 at 15:19):

Yes, hence the shim above.

view this post on Zulip Pierre-Marie Pédrot (Jul 20 2021 at 15:19):

But it has a net tendency to not work on a clean repo.

view this post on Zulip Pierre-Marie Pédrot (Jul 20 2021 at 15:19):

I usually have to build bits of world to make it work.

view this post on Zulip Ali Caglayan (Jul 20 2021 at 15:20):

Excellent it worked!

view this post on Zulip Pierre-Marie Pédrot (Jul 20 2021 at 15:21):

@Ali Caglayan you should also call the same warning as for Hint Opaque without an explicit locality

view this post on Zulip Pierre-Marie Pédrot (Jul 20 2021 at 15:21):

I am starting to get slightly bored of the whack-a-mole game of flagging superglobal commands as we have random aliases all over the place.

view this post on Zulip Ali Caglayan (Jul 20 2021 at 15:23):

Is it normal for Typeclasses Opaque to be part of the ltac plugin even though it has very little to do with ltac?

view this post on Zulip Ali Caglayan (Jul 20 2021 at 15:23):

I feel like it got left behind when some of the hint stuff was moved away from ltac

view this post on Zulip Pierre-Marie Pédrot (Jul 20 2021 at 15:24):

I invoke the historical-miranda-reason rights

view this post on Zulip Ali Caglayan (Jul 20 2021 at 15:26):

Where does Hint Opaque give warnings?

view this post on Zulip Pierre-Marie Pédrot (Jul 20 2021 at 15:27):

Look for Hints.check_hint_locality.

view this post on Zulip Pierre-Marie Pédrot (Jul 20 2021 at 15:28):

You can probably add the call to the classes.ml command

view this post on Zulip Ali Caglayan (Jul 20 2021 at 15:42):

@Pierre-Marie Pédrot Are you testing the deprecation message for hints? If so how? Using test-suite/sucess?

view this post on Zulip Pierre-Marie Pédrot (Jul 20 2021 at 15:43):

I don't think we test anything.

view this post on Zulip Pierre-Marie Pédrot (Jul 20 2021 at 15:43):

You'll get errors if it interferes with output tests.

view this post on Zulip Ali Caglayan (Jul 20 2021 at 15:44):

Doesn't look like we have any Typeclasses Opaque or Transparent in the test-suite however

view this post on Zulip Ali Caglayan (Jul 20 2021 at 15:46):

If I want to add tests showing the desired behavior in the issue is now possible where do I put them?

view this post on Zulip Ali Caglayan (Jul 20 2021 at 15:46):

It's not bugs right?

view this post on Zulip Ali Caglayan (Jul 20 2021 at 15:47):

Perhaps test-suite/typeclasses?

view this post on Zulip Pierre-Marie Pédrot (Jul 20 2021 at 15:50):

looks ok indeed

view this post on Zulip Gaëtan Gilbert (Jul 20 2021 at 15:53):

Ali Caglayan said:

Perhaps test-suite/typeclasses?

no, those are fake tests, they never get run
this is not a joke ;_;

view this post on Zulip Ali Caglayan (Jul 20 2021 at 15:54):

OK, then whats the better place?

view this post on Zulip Gaëtan Gilbert (Jul 20 2021 at 15:54):

success/

view this post on Zulip Pierre-Marie Pédrot (Jul 20 2021 at 15:54):

It's still time to deprecate these commands though...

view this post on Zulip Ali Caglayan (Jul 20 2021 at 15:57):

You mean deprecate Typeclasses Opaque?

view this post on Zulip Ali Caglayan (Jul 20 2021 at 15:58):

I am a bit weary of this since users might not know what is going on under the hood

view this post on Zulip Ali Caglayan (Jul 20 2021 at 15:58):

You can use typeclasses and have no clue about hints

view this post on Zulip Pierre-Marie Pédrot (Jul 20 2021 at 15:58):

These commands are explicitly documented as aliases.

view this post on Zulip Pierre-Marie Pédrot (Jul 20 2021 at 15:59):

If you use typeclasses without any clue about hint, you're probably a bit reckless...

view this post on Zulip Ali Caglayan (Jul 20 2021 at 15:59):

We do it all the time in the HoTT library 0:-)

view this post on Zulip Ali Caglayan (Jul 20 2021 at 15:59):

In fact, before looking into this issue today I was in the "no clue (about the implementation at least)" camp

view this post on Zulip Pierre-Marie Pédrot (Jul 20 2021 at 16:00):

Fair enough...

view this post on Zulip Ali Caglayan (Jul 20 2021 at 18:43):

So I have run into a bit of a problem

view this post on Zulip Ali Caglayan (Jul 20 2021 at 18:44):

The behavior of Typeclasses Opaque in sections was essentially always #[globa].

view this post on Zulip Ali Caglayan (Jul 20 2021 at 18:44):

So I changed the default behaviour of Typeclasses Opaque to #[global]

view this post on Zulip Ali Caglayan (Jul 20 2021 at 18:44):

but Hint doesn't allow this in a section

view this post on Zulip Ali Caglayan (Jul 20 2021 at 18:45):

I guess I will have to create overlays?

view this post on Zulip Ali Caglayan (Jul 20 2021 at 18:45):

But this is kind of impossible, especially when Typeclasses Opaque doesn't accept attributes yet

view this post on Zulip Ali Caglayan (Jul 20 2021 at 18:47):

Or maybe I can get away with re-declaring Typeclasses Opaque outside of each section?

view this post on Zulip Gaëtan Gilbert (Jul 20 2021 at 18:49):

Ali Caglayan said:

The behavior of Typeclasses Opaque in sections was essentially always #[globa].

are you sure? that sounds wrong

view this post on Zulip Ali Caglayan (Jul 20 2021 at 19:00):

I don't know how else the errors here would happen however: https://github.com/coq/coq/pull/14685

view this post on Zulip Ali Caglayan (Jul 20 2021 at 19:00):

Sorry I meant this one

view this post on Zulip Ali Caglayan (Jul 20 2021 at 19:00):

https://github.com/coq/coq/runs/3116931816

view this post on Zulip Ali Caglayan (Jul 20 2021 at 19:05):

Or maybe you are correct

view this post on Zulip Ali Caglayan (Jul 20 2021 at 19:06):

Hmm I'll have to think about this more

view this post on Zulip Guillaume Melquiond (Jul 20 2021 at 19:14):

The old code was calling make_section_locality, which returns Local in sections and Global outside. You should not blindly pass the Default locality to Hints.add_hints, as it would cause it to be interpreted as Global instead of Local.

view this post on Zulip Ali Caglayan (Jul 20 2021 at 19:38):

Thanks!

view this post on Zulip Ali Caglayan (Jul 20 2021 at 19:39):

So make_section_locality returns a bool, is there a version that returns option_locality?

view this post on Zulip Ali Caglayan (Jul 21 2021 at 15:47):

OK I have just realised that we don't allow #[export] Hint Opaque inside sections. @Pierre-Marie Pédrot Why?

view this post on Zulip Pierre-Marie Pédrot (Jul 21 2021 at 15:49):

no reason for this one, but some other Hint commands are hard to handle inside sections so they don't accept locality qualfiers

view this post on Zulip Pierre-Marie Pédrot (Jul 21 2021 at 15:50):

(this is due to the ability to add arbitrary terms as hints btw)

view this post on Zulip Ali Caglayan (Jul 21 2021 at 15:55):

So people want exportable opaqueness in https://github.com/coq/coq/issues/14513 but this would basically require the underlying hint opaque command to do the same

view this post on Zulip Ali Caglayan (Jul 21 2021 at 15:55):

From reading the Hint blah code it looks very tied together so I don't really know how to go about doing this

view this post on Zulip Pierre-Marie Pédrot (Jul 21 2021 at 16:20):

The issue report is ambiguous. On the one hand, it asks for the same qualifiers as Hint Unfold (which doesn't accept them in a section) but the intended use case is precisely outside of this fragment.

view this post on Zulip Pierre-Marie Pédrot (Jul 21 2021 at 16:20):

For the time being I'd simply defer the decision to the underlying command and handle Typeclass Opaque really as a trivial alias.

view this post on Zulip Janno (Jul 21 2021 at 16:30):

I would love to have #[export] Hint Opaque. All our definitions live in sections and almost all of them need to be Hint Opaque for performance reasons. Right now we usually have to have two Hint Opaque blocks, one in the section, and one with #[export] after the section. It is very easy to only add a new definition to one of these two blocks (usually the one in the section) and thus lose out on performance. Sometimes people forget entirely about the block with #[export] or just copy the previous block without adding #[export]. It's quite a mess.

view this post on Zulip Pierre-Marie Pédrot (Jul 21 2021 at 16:35):

it's not very hard to implement

view this post on Zulip Pierre-Marie Pédrot (Jul 21 2021 at 16:36):

barring idiosyncrasies of the hint code, that is

view this post on Zulip Pierre-Marie Pédrot (Jul 21 2021 at 16:36):

if you get my last round of cleanup PRs to get merged quickly I'll have a look at it

view this post on Zulip Ali Caglayan (Jul 21 2021 at 16:40):

@Pierre-Marie Pédrot Whats a good example of an alias to have a look at.

view this post on Zulip Ali Caglayan (Jul 21 2021 at 16:41):

I want to essentially write Hint Opaque in the grammar for Typeclasses Opaque but I have no idea what to call

view this post on Zulip Pierre-Marie Pédrot (Jul 21 2021 at 16:42):

hmm, I don't think there is a trivial way to do that

view this post on Zulip Pierre-Marie Pédrot (Jul 21 2021 at 16:44):

AFAICT there is no way in VERNAC EXTEND to parse arbitrary attributes and pass them to the underlying command

view this post on Zulip Ali Caglayan (Jul 21 2021 at 16:45):

also where do the locality attributes get passed to the hint commands?

view this post on Zulip Pierre-Marie Pédrot (Jul 21 2021 at 16:45):

magic!

view this post on Zulip Pierre-Marie Pédrot (Jul 21 2021 at 16:45):

in vernacentries because these are hardwired commands

view this post on Zulip Ali Caglayan (Jul 21 2021 at 16:46):

I'm looking at comHints.ml and I don't see anything about locality

view this post on Zulip Ali Caglayan (Jul 21 2021 at 16:46):

ah

view this post on Zulip Pierre-Marie Pédrot (Jul 21 2021 at 16:47):

look at Vernacentries.vernac_hints

view this post on Zulip Ali Caglayan (Jul 21 2021 at 16:50):

Maybe time for a vernac notation? ;-)

view this post on Zulip Janno (Jul 21 2021 at 16:51):

Pierre-Marie Pédrot said:

if you get my last round of cleanup PRs to get merged quickly I'll have a look at it

I was looking at coq/coq#14675 but it was sneakily merged before I could make sense of the changes. What other cleanup PRs need feedback?

view this post on Zulip Pierre-Marie Pédrot (Jul 21 2021 at 16:56):

yes, it's getting merged fast indeed

view this post on Zulip Pierre-Marie Pédrot (Jul 21 2021 at 16:56):

there is https://github.com/coq/coq/pull/14615 which you already commented on

view this post on Zulip Paolo Giarrusso (Jul 22 2021 at 14:44):

Just FTR on what people want, even if we can't have it, we probably want all qualifiers on all commands. Just today we had to workaround the lack of global on canonical instances, because not like all modules are meant for imports.

view this post on Zulip Paolo Giarrusso (Jul 22 2021 at 14:46):

“you think it takes a PhD to write Haskell? What about a language where a PhD is not enough?” :-P

(me ranting on that discussion). Anyway, </rant>.


Last updated: Oct 16 2021 at 07:02 UTC