Skip to content
Snippets Groups Projects

Add annotations to avoid evars

Open Add annotations to avoid evars
Tragicus/examples:rocq19987 into master
2 unresolved threads
Open Quentin VERMANDE requested to merge Tragicus/examples:rocq19987 into master
2 unresolved threads

There are a few iApply in theories/logrel/F_mu_ref_conc/binary/fundamental.v that introduce evars, which causes the subsequent dones to be very slow (~10s each). This was also very fragile to https://github.com/coq/coq/pull/19987.

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
theories/logrel/F_mu_ref_conc/binary/fundamental.v
560 560 Theorem binary_fundamental Γ e τ :
561 561 Γ ⊢ₜ e : τ → ⊢ Γ ⊨ e ≤log≤ e : τ.
562 562 Proof.
563 induction 1.
564 - iApply bin_log_related_var; done.
563 elim=> {}Γ {e τ}.
  • Ralf Jung
    Ralf Jung @jung started a thread on the diff
    • theories/logrel/F_mu_ref_conc/binary/fundamental.v
    580 - move=> e1 e2 τ1 τ2 ? ? ? ?.
    581 iApply (bin_log_related_seq _ _ _ _ _ τ1); done.
    582 - move=> e1 e2 τ1 τ2 ? ? ? ?.
    583 iApply (bin_log_related_app _ _ _ _ _ τ1); done.
    584 - intros; iApply bin_log_related_tlam; done.
    585 - intros; iApply bin_log_related_tapp; done.
    586 - intros; iApply bin_log_related_pack; done.
    587 - intros; iApply bin_log_related_unpack; done.
    588 - intros; iApply bin_log_related_fold; done.
    589 - intros; iApply bin_log_related_unfold; done.
    590 - intros; iApply bin_log_related_fork; done.
    591 - intros; iApply bin_log_related_alloc; done.
    592 - intros; iApply bin_log_related_load; done.
    593 - move=> e1 e2 τ ? ? ? ?; iApply (bin_log_related_store _ _ _ _ _ τ); done.
    594 - intros; iApply bin_log_related_CAS; done.
    595 - intros; iApply bin_log_related_FAA; done.
    • Ralf Jung
      Ralf Jung @jung ·
      Owner

      Something is wrong if we need to write different scripts for the different cases here -- they should all be entirely uniform.

      Cc @amintimany @robbertkrebbers who wrote this code IIRC.

    • Quentin VERMANDE
      Quentin VERMANDE @Tragicus ·
      Author

      The behavior of Rocq on the different goals is not the same, since sometimes there are uninstantiated evars left in the goal by iApply, so I am not sure why the scripts should all be exactly the same. As it happens, Rocq spends a minute and a half half a minute here figuring out the correct values for these evars, and even more with the above mentioned PR.

      Edited by Quentin VERMANDE
    • Robbert Krebbers
      Robbert Krebbers @robbertkrebbers ·
      Owner

      The fact that Rocq takes 1 minute there seems like a bug (in Rocq or Iris).

      Are you able to produce a minimal example?

      Any idea if it's due to unification or TC resolution? Do you see an endless log if you enable Typeclasses eauto := debug.

      Edited by Robbert Krebbers
    • Ralf Jung
      Ralf Jung @jung ·
      Owner

      The behavior of Rocq on the different goals is not the same, since sometimes there are uninstantiated evars left in the goal by iApply, so I am not sure why the scripts should all be exactly the same.

      Each of these lemmas is specifically stated to match the case in this induction. So there shouldn't be large differences in what iApply has to do.

    • Robbert Krebbers
      Robbert Krebbers @robbertkrebbers ·
      Owner

      If Quentin reports some take 1.5 minute, there clearly is a difference, i.e., a bug...

    • Quentin VERMANDE
      Quentin VERMANDE @Tragicus ·
      Author

      Oh, um, sorry, half a minute, not a minute and a half. It is around 11s for three branches.

    • Robbert Krebbers
      Robbert Krebbers @robbertkrebbers ·
      Owner

      I'd say that's still a bug for something as simple as an iApply. That should succeed immediately.

    • Quentin VERMANDE
      Quentin VERMANDE @Tragicus ·
      Author

      To be very precise, it is the done after the iApply that takes a lot of time. This is still probably too much, but maybe less unexpected.

    • Quentin VERMANDE
      Quentin VERMANDE @Tragicus ·
      Author

      I have 200 lines of log with Typeclasses eauto := debug. on the first problematic iApply and 40 on the corresponding done, so the issue is probably not there.

    • Robbert Krebbers
      Robbert Krebbers @robbertkrebbers ·
      Owner

      Sounds like unification. I wonder if this is the "usual" bug (due to Rocq's unification being a random number generator) and we should seal more. E.g., seal the semantic typing judgment.

    • Quentin VERMANDE
      Quentin VERMANDE @Tragicus ·
      Author

      Each of these lemmas is specifically stated to match the case in this induction. So there shouldn't be large differences in what iApply has to do.

      The issue is that tau1 does not appear in the goal, so unless it is given explicitly, Rocq will not guess it until it reaches done and tries to apply the wrong hypothesis, which does indeed trigger an ages long unification.

    • Ralf Jung
      Ralf Jung @jung ·
      Owner

      (Btw you can edit your comments, no need to delete the old one and add a new one.)

    • Quentin VERMANDE
      Quentin VERMANDE @Tragicus ·
      Author

      Sounds like unification. I wonder if this is the "usual" bug (due to Rocq's unification being a random number generator) and we should seal more. E.g., seal the semantic typing judgment.

      That looks indeed to be the case, I killed Rocq at a million lines of log. That could be a solution. I have no idea how you seal things or what exactly would best be sealed, may I ask for help?

    • Quentin VERMANDE
      Quentin VERMANDE @Tragicus ·
      Author

      (Yes, sorry, I keep putting them outside of the conversation for some reason)

    • Please register or sign in to reply
    Please register or sign in to reply