Ali Caglayan (Jul 20 2021 at 15:06): 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
Ali Caglayan (Jul 20 2021 at 15:07):However it doesn't work and I would like to learn why :-)
Pierre-Marie Pédrot (Jul 20 2021 at 15:08):define "does not work"
Ali Caglayan (Jul 20 2021 at 15:09):I added a test case in the PR
Pierre-Marie Pédrot (Jul 20 2021 at 15:09):Yes, but what's the error?
Ali Caglayan (Jul 20 2021 at 15:09):It doesn't recognize support for attributes
Ali Caglayan (Jul 20 2021 at 15:10):This command does not support this attribute: export.
[unsupported-attributes,parsing]
you're probably using the wrong attribute specification
Pierre-Marie Pédrot (Jul 20 2021 at 15:10):let me look at what we do for other hint commands
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
Pierre-Marie Pédrot (Jul 20 2021 at 15:10):it should indeed parse export
Pierre-Marie Pédrot (Jul 20 2021 at 15:14):your example works for me ©
Ali Caglayan (Jul 20 2021 at 15:14):OK, then am I doing something stupid to test it
Ali Caglayan (Jul 20 2021 at 15:15):I run dune exec -- coqide
Pierre-Marie Pédrot (Jul 20 2021 at 15:17):don't ask me, this is dark magic to me
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
Pierre-Marie Pédrot (Jul 20 2021 at 15:18):in theory you must call a shim
Pierre-Marie Pédrot (Jul 20 2021 at 15:18):dune exec -- dev/shim/coqide-prelude or so
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.
Pierre-Marie Pédrot (Jul 20 2021 at 15:19):Yes, hence the shim above.
Pierre-Marie Pédrot (Jul 20 2021 at 15:19):But it has a net tendency to not work on a clean repo.
Pierre-Marie Pédrot (Jul 20 2021 at 15:19):I usually have to build bits of world to make it work.
Ali Caglayan (Jul 20 2021 at 15:20):Excellent it worked!
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
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.
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?
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
Pierre-Marie Pédrot (Jul 20 2021 at 15:24):I invoke the historical-miranda-reason rights
Ali Caglayan (Jul 20 2021 at 15:26):Where does Hint Opaque give warnings?
Pierre-Marie Pédrot (Jul 20 2021 at 15:27):Look for Hints.check_hint_locality.
Pierre-Marie Pédrot (Jul 20 2021 at 15:28):You can probably add the call to the classes.ml command
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?
Pierre-Marie Pédrot (Jul 20 2021 at 15:43):I don't think we test anything.
Pierre-Marie Pédrot (Jul 20 2021 at 15:43):You'll get errors if it interferes with output tests.
Ali Caglayan (Jul 20 2021 at 15:44):Doesn't look like we have any Typeclasses Opaque or Transparent in the test-suite however
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?
Ali Caglayan (Jul 20 2021 at 15:46):It's not bugs right?
Ali Caglayan (Jul 20 2021 at 15:47):Perhaps test-suite/typeclasses?
Pierre-Marie Pédrot (Jul 20 2021 at 15:50):looks ok indeed
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 ;_;
Ali Caglayan (Jul 20 2021 at 15:54):OK, then whats the better place?
Gaëtan Gilbert (Jul 20 2021 at 15:54):success/
Pierre-Marie Pédrot (Jul 20 2021 at 15:54):It's still time to deprecate these commands though...
Ali Caglayan (Jul 20 2021 at 15:57):You mean deprecate Typeclasses Opaque?
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
Ali Caglayan (Jul 20 2021 at 15:58):You can use typeclasses and have no clue about hints
Pierre-Marie Pédrot (Jul 20 2021 at 15:58):These commands are explicitly documented as aliases.
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...
Ali Caglayan (Jul 20 2021 at 15:59):We do it all the time in the HoTT library 0:-)
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
Pierre-Marie Pédrot (Jul 20 2021 at 16:00):Fair enough...
Ali Caglayan (Jul 20 2021 at 18:43):So I have run into a bit of a problem
Ali Caglayan (Jul 20 2021 at 18:44):The behavior of Typeclasses Opaque in sections was essentially always #[globa].
Ali Caglayan (Jul 20 2021 at 18:44):So I changed the default behaviour of Typeclasses Opaque to #[global]
Ali Caglayan (Jul 20 2021 at 18:44):but Hint doesn't allow this in a section
Ali Caglayan (Jul 20 2021 at 18:45):I guess I will have to create overlays?
Ali Caglayan (Jul 20 2021 at 18:45):But this is kind of impossible, especially when Typeclasses Opaque doesn't accept attributes yet
Ali Caglayan (Jul 20 2021 at 18:47):Or maybe I can get away with re-declaring Typeclasses Opaque outside of each section?
Gaëtan Gilbert (Jul 20 2021 at 18:49):Ali Caglayan said:
The behavior of
Typeclasses Opaquein sections was essentially always#[globa].
are you sure? that sounds wrong
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
Ali Caglayan (Jul 20 2021 at 19:00):Sorry I meant this one
Ali Caglayan (Jul 20 2021 at 19:00):https://github.com/coq/coq/runs/3116931816
Ali Caglayan (Jul 20 2021 at 19:05):Or maybe you are correct
Ali Caglayan (Jul 20 2021 at 19:06):Hmm I'll have to think about this more
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.
Ali Caglayan (Jul 20 2021 at 19:38):Thanks!
Ali Caglayan (Jul 20 2021 at 19:39):So make_section_locality returns a bool, is there a version that returns option_locality?
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?
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
Pierre-Marie Pédrot (Jul 21 2021 at 15:50):(this is due to the ability to add arbitrary terms as hints btw)
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
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
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.
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.
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.
Pierre-Marie Pédrot (Jul 21 2021 at 16:35):it's not very hard to implement
Pierre-Marie Pédrot (Jul 21 2021 at 16:36):barring idiosyncrasies of the hint code, that is
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
Ali Caglayan (Jul 21 2021 at 16:40):@Pierre-Marie Pédrot Whats a good example of an alias to have a look at.
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
Pierre-Marie Pédrot (Jul 21 2021 at 16:42):hmm, I don't think there is a trivial way to do that
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
Ali Caglayan (Jul 21 2021 at 16:45):also where do the locality attributes get passed to the hint commands?
Pierre-Marie Pédrot (Jul 21 2021 at 16:45):magic!
Pierre-Marie Pédrot (Jul 21 2021 at 16:45):in vernacentries because these are hardwired commands
Ali Caglayan (Jul 21 2021 at 16:46):I'm looking at comHints.ml and I don't see anything about locality
Ali Caglayan (Jul 21 2021 at 16:46):ah
Pierre-Marie Pédrot (Jul 21 2021 at 16:47):look at Vernacentries.vernac_hints
Ali Caglayan (Jul 21 2021 at 16:50):Maybe time for a vernac notation? ;-)
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?
Pierre-Marie Pédrot (Jul 21 2021 at 16:56):yes, it's getting merged fast indeed
Pierre-Marie Pédrot (Jul 21 2021 at 16:56):there is https://github.com/coq/coq/pull/14615 which you already commented on
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.
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: Sep 09 2024 at 06:02 UTC