Skip to content
Snippets Groups Projects

decrease priority for rtc_reflexive instance

Merged Ralf Jung requested to merge ralf/rtc into master

We give this instance a lower-than-usual priority because when it is applied to Reflexive ?, it leads to a new evar being created for R. Unfortunately, we cannot set Hint Mode for Reflexive in a way that just rules out Reflexive ? [1], but we can at least stop TC search from using this instance. This helps performance because it gives TC search less freedom in the remainder of the search. It doesn't seem like backtracking is happening here.

Also see the discussion below https://gitlab.mpi-sws.org/FP/iris-coq/commit/8e8c722870b36c23032d9bc10019e40e6eb6be62. I think this is useful even if we decide to roll back the IntoVal change as there may be other places where rtc_reflexive inadvertently gets chosen.

[1] That would break https://gitlab.mpi-sws.org/FP/iris-coq/blob/38ba379fae88865ed3a06ba44bf22938b6524610/theories/algebra/list.v#L213

Edited by Ralf Jung

Merge request reports

Loading
Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
Please register or sign in to reply
Loading