From 838d4b52c0fc8bc13c22ea396d582f3d6cef0a73 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lennard=20G=C3=A4her?= <l.gaeher@posteo.de>
Date: Thu, 1 Jul 2021 09:47:34 +0200
Subject: [PATCH] fix
---
theories/simulang/na_inv/examples/data_races.v | 2 +-
theories/simulang/tactics.v | 8 ++++++--
2 files changed, 7 insertions(+), 3 deletions(-)
diff --git a/theories/simulang/na_inv/examples/data_races.v b/theories/simulang/na_inv/examples/data_races.v
index c6e4aa07..21672c1e 100644
--- a/theories/simulang/na_inv/examples/data_races.v
+++ b/theories/simulang/na_inv/examples/data_races.v
@@ -152,7 +152,7 @@ Section data_race.
rewrite bool_decide_eq_true_2; last done.
sim_pures. iApply sim_expr_base. iLeft. iApply lift_post_val.
- sim_pures. source_load. target_load. to_sim. sim_pures.
+ sim_pures. source_load. target_load. sim_pures.
(* cleanup *)
source_free. source_free. target_free. target_free. sim_pures.
iApply (sim_bij_release (NaRead q) with "Hbij Hc Hl_t Hl_s [//]").
diff --git a/theories/simulang/tactics.v b/theories/simulang/tactics.v
index bdf8b975..0e21457a 100644
--- a/theories/simulang/tactics.v
+++ b/theories/simulang/tactics.v
@@ -384,10 +384,14 @@ Ltac simpl_subst :=
let e' := W.of_expr e in
simple refine (W.tac_to_expr_subst _ _ _ _ e' _ _ _ _); [ shelve
| simpl; rewrite ?list_to_map_to_list; reflexivity
- | simpl; compute_done
+ |
+ (* FIXME: really hacky hack to speed up goals on which [compute_done] takes forever due to evars,
+ but where [simpl] would suffice...*)
+ first [timeout 1 compute_done | simpl; reflexivity]
|];
simple refine (W.tac_to_expr_combine_subst_map _ _ _ _ _); [ shelve |
- simpl; compute_done | ];
+ (* FIXME *)
+ first [timeout 1 compute_done | simpl; reflexivity] | ];
simpl
end.
Arguments subst : simpl never.
--
GitLab