Stream: Coq devs & plugin devs

Topic: rewrite opacity

Jason Gross (Sep 14 2023 at 23:22):

Is there no way to tell rewrite in Keyed Unification mode to not unfold some constants? Set Debug "tactic-unification,Cbv". Set Printing All. hangs for a couple seconds on

Debug:
[tactic-unification]
  Starting unification:
  @Model.logit_delta float Truncating.coer_Z_float float_has_sub
    (@has_default_max_leb float float_has_leb) (@has_default_min_leb float float_has_leb) true
    (@all_tokens false)
  ~=
  @Model.logit_delta

despite

  Hint Opaque Model.logit_delta Truncating.coer_Z_float float_has_sub has_default_max_leb float_has_leb has_default_min_leb float_has_leb all_tokens : rewrite.
  Opaque Model.logit_delta Truncating.coer_Z_float float_has_sub has_default_max_leb float_has_leb has_default_min_leb float_has_leb all_tokens.

Jason Gross (Sep 14 2023 at 23:31):

I guess I've been asking for this since 2016 :-/ https://github.com/coq/coq/issues/5117

Paolo Giarrusso (Sep 15 2023 at 01:46):

you can mlock that constant using coq-elpi

Paolo Giarrusso (Sep 15 2023 at 01:46):

that's as opaque as Axiom, thanks to module sealing

Paolo Giarrusso (Sep 15 2023 at 01:47):

(the _only_ thing that can break both is Include module if module is concrete — OTOH, Include on Module Types is safe).

Last updated: Nov 29 2023 at 21:01 UTC