Michael Soegtrop (Oct 20 2023 at 08:41): Michael Soegtrop (Oct 20 2023 at 08:41):It might be of more help if you post the proof. I had such issues before and I always found ways around them. The link Jason initially posted is currently the best resource of hints on this I am aware of.
Usually what made Qed slow for me was doing a change in a hypothesis - using replace instead can result in astronomic speed up factors in Qed time. If a few rules are observed, Qed should not take longer than the construction of the proof term.
Huỳnh Trần Khanh (Oct 20 2023 at 09:07):time to move to #Coq users? it's p clear that this isn't a bug in Coq
Huỳnh Trần Khanh (Oct 20 2023 at 09:09):yeah I second Michael's suggestion. post code and we'll debug
Notification Bot (Oct 20 2023 at 09:14):This topic was moved here from #Coq devs & plugin devs > Coq hangs on Qed by Karl Palmskog.
Vadim Zaliva (Oct 20 2023 at 16:14):Michael Soegtrop said:
It might be of more help if you post the proof. I had such issues before and I always found ways around them. The link Jason initially posted is currently the best resource of hints on this I am aware of.
do you mean proof object or proof script?
Huỳnh Trần Khanh (Oct 20 2023 at 16:17):script
Vadim Zaliva (Oct 20 2023 at 17:02):These are 2 lemmas where it happens: https://github.com/rems-project/cerberus/blob/80344228c91967743539abc41c030d1c93a365e4/coq/Proofs/Revocation.v#L950 and https://github.com/rems-project/cerberus/blob/80344228c91967743539abc41c030d1c93a365e4/coq/Proofs/Revocation.v#L1020
Vadim Zaliva (Oct 20 2023 at 17:03):the project builds cleanly but requires some dependencies per READEM-cheri.md in top level directory. May take awhile to install :(
Vadim Zaliva (Oct 20 2023 at 23:15):@Jason Gross I've followed your debugging technique to find the place and the tactic slowing down Qed. I've narrowed it down to a single destruct. Not sure where to go from here...
Vadim Zaliva (Oct 20 2023 at 23:27):this is the exact line: https://github.com/rems-project/cerberus/blob/80344228c91967743539abc41c030d1c93a365e4/coq/Proofs/Revocation.v#L912C29-L912C45 (break_let even without repeat is the problem). I can show the proof state before and after if that helps.
Vadim Zaliva (Oct 20 2023 at 23:29): Jason Gross (Oct 21 2023 at 03:03):What's the definition of break_let?
Jason Gross (Oct 21 2023 at 03:09):Assuming it really is a single destruct causing the issue: can you remember term as var in * before destruct var and still have the slowness show up on destruct but not remember? If so, what is the type of the variable being destructed? If I recall correctly, destruct uses hnf which uses simpl to determine the inductive type of the object being destructed, so it may be the case that you are hitting slowness of simpl. If so, I would encourage you to write something like let T := type of var in let T' := eval hnf in T in replace T with T' in var by reflexivity before doing destruct, or something like that. Or otherwise try to hand code the destruct as a refine match and see if you can avoid / diagnose the slowness that way
Vadim Zaliva (Oct 21 2023 at 04:14):Ltac break_let :=
match goal with
| [ H : context [ (let (_,_) := ?X in _) ] |- _ ] => destruct X eqn:?
| [ |- context [ (let (_,_) := ?X in _) ] ] => destruct X eqn:?
end.
removing the break_let may remove the slowness but that doesn't mean it's the root cause
AFAIK doing destruct X when X appears in hypothesis H will do something like revert H; destruct X; intros H (ie create a term match X with bla => fun H => ... end H)
if the type of H was modified (IIRC your script calls eg cbn on some hypotheses) this introduces a "use" of H which means the kernel will check H : original type |- H : changed_type (simpl in H; clear H or otherwise not using H is the same as just clear H)
you can test this hypothesis by inserting "uses" of hypotheses with pose proof H as _, if Qed is slow with those and without break_let then you can find which specific hypothesis (or plural hypotheses) is the problem
Vadim Zaliva (Oct 24 2023 at 00:14):I've followed @Jason Gross suggestions. remember did not cause slowness. Furthermore I've modified my break_let tactics as follows:
Ltac break_let_hyp :=
match goal with
| [ H : context [ (let (_,_) := ?X in _) ] |- _ ] =>
let var := fresh "blet" in
remember X as var in *;
let T := type of var in
idtac T;
let T' := eval hnf in T in
replace T with T' in var by reflexivity
; destruct var eqn:?
end.
But it is still slow. The type of var is (CheriMemoryWithoutPNVI.mem_state * (memMError + CheriMemoryWithoutPNVI.storage_instance_id * AddressValue.t))%type
Vadim Zaliva (Oct 24 2023 at 00:21):I have more luck with @Gaëtan Gilbert hint. Adding pose proof Heqp0 as _. even without destruct causes a slowdown. The hypothesis has the following (abridged) shape:
Heqp0 : (let (s', s0) := .. in
match s0 with
| inl v => (s', inl v)
| inr x => ...
end) = (m0, inl m2)
It is however still unclear to me how to fix that.
Vadim Zaliva (Oct 24 2023 at 22:44):I've narrowed down the problem to a single cbn. The following is slow:
Axiom admit : forall {T}, T.
Lemma foo:
forall a b c d m s,
CheriMemoryWithoutPNVI.allocate_region a b c d m = (m, s) -> False.
Proof.
intros a b c d m s H.
cbn in H.
pose proof H as _.
exact admit.
Qed.
If there is a way to do a "safe" cbn here?
Vadim Zaliva (Oct 25 2023 at 00:32):As workaround, I managed to replace this cbn with a combination of unfold and simpl but I would love to have a more generic solution.
Michael Soegtrop (Oct 25 2023 at 14:22):I should have been clearer: doing any kind of change like tactics on hypothesis - that is tactics which replace hypothesis with convertible variants - is dangerous (not just change). You can replace this with a combination of eval and replace or assert an equality and rewrite with it. rewrite and replace in H are safe in my experience.
Michael Soegtrop (Oct 25 2023 at 14:26):As far as I can tell, unrestricted cbv and lazy are the only "change like" tactics, which are safe on hypothesis. Everything else (change, simpl, cbn, restricted cbv and lazy, hnf, ...) should be avoided on hypothesis (in larger proofs).
Vadim Zaliva (Oct 25 2023 at 16:10):I tried something like let T := type of var in let T' := eval cbv in T in replace T with T' in var by reflexivity but it did not work.
Michael Soegtrop (Oct 25 2023 at 16:22):It should work. E.g. this works:
Example Ex1: 1+1=2 -> True.
intros H.
let T:= type of H in
let T':= eval simpl in T in
replace T with T' in H by reflexivity.
What did not work? Did you get an error or didn't Qed become faster?
Notification Bot (Oct 25 2023 at 16:22):Michael Soegtrop has marked this topic as unresolved.
Vadim Zaliva (Oct 25 2023 at 17:00):in my case it works for simpl but for cbv it hangs right there in eval cbv.
Paolo Giarrusso (Oct 25 2023 at 17:41):That's not surprising, cbv will diverge on tons of stuff
Paolo Giarrusso (Oct 25 2023 at 17:42):As I read it, the point is that if you need cbv/lazy on hypotheses you're fine, if you need sth else you need such workarounds.
Vadim Zaliva (Oct 25 2023 at 17:44):well, suprisingly if I just do cbv in H instead of this, it works instantly but Qed will be slow later
Paolo Giarrusso (Oct 25 2023 at 17:45):What's the resulting H?
Paolo Giarrusso (Oct 25 2023 at 17:48):either the function is (almost) a normal form, or the result will be so huge to be a benchmark for the editor or for pretty-printing
Paolo Giarrusso (Oct 25 2023 at 17:51):We lack enough data but I'd already consider sealing CheryMemoryWithoutPNVI.allocate_region, since reduction for it can (effectively) diverge
Vadim Zaliva (Oct 25 2023 at 18:03):the result of cbn is unfolded and normalized function just 65 lines long.
Vadim Zaliva (Oct 25 2023 at 18:03):I need to unfold and normalize allocate_region for further proofs
Vadim Zaliva (Oct 25 2023 at 18:04):FYI, the workaround is instead of cbn in Heqp. to use unfold CheriMemoryWithPNVI.allocate_region, WithPNVISwitches.get_switches, bind, ret in Heqp; simpl in Heqp which gives me about the same result (minus some non-essential unfolding)
Vadim Zaliva (Oct 25 2023 at 18:06):the problem with this approach is that it is not generic and each time I need to look at the definition and see what I want to manually unforld and normalize. cbn usually does it for me.
Michael Soegtrop (Oct 26 2023 at 06:42):@Vadim Zaliva : can it be that you are mixing up cbv and cbn? They are very different tactics. cbv does a full reduction, while cbn is a newer variant of simpl, which does only very limited reduction.
As far as I understand what is going on under the hood is this:
Vadim Zaliva (Oct 26 2023 at 17:38):I just double-checked and let T := type of Heqp in let T' := eval cbn in T in replace T with T' in Heqp by reflexivity hangs but cbn in Heqp works.
Paolo Giarrusso (Oct 26 2023 at 17:41):And if you replace reflexivity by cbn; reflexivity?
Paolo Giarrusso (Oct 26 2023 at 17:45):the conjecture is that reflexivity calls unification, and there's no reason why unifying cbn's input with its output should be fast. Especially if cbn's output is 65 lines.
Vadim Zaliva (Oct 26 2023 at 17:57):the following passed: let T := type of Heqp in let T' := eval cbn in T in replace T with T' in Heqp by (cbn;reflexivity).
Vadim Zaliva (Oct 26 2023 at 17:58):need to check how it will affect Qed.
Vadim Zaliva (Oct 26 2023 at 17:59):Qed is fast!
Vadim Zaliva (Oct 26 2023 at 18:00):I guess I can define small tactics like this:
Ltac cbn_hyp H :=
let T := type of H in let T' := eval cbn in T in replace T with T' in H by (cbn;reflexivity).
and use it instead of cbn in H everywhere? If that works, maybe worth suggesting in FAQ?
Vadim Zaliva (Oct 26 2023 at 18:06):thanks!
Michael Soegtrop (Oct 27 2023 at 07:20):I must also say that I don't quite understand the reason why reduction tactics applied in hypothesis don't leave a cast as they do when applied to the goal. @Gaëtan Gilbert : do you know why this is as it is?
Gaëtan Gilbert (Oct 27 2023 at 07:26):you can't just do refine (_ : oldt) when it's the hypothesis
you could try refine (let H := H : newt in _) but then the conversion is in the wrong direction (rtl vs ltr)
to keep the conversion in the right direction I think you would have to do something like refine ((fun H : newt => _) H) (not sure that even works)
tldr leaving a cast in the hypothesis isn't as trivial as leaving a cast in the goal
Michael Soegtrop (Oct 27 2023 at 07:33):@Gaëtan Gilbert : my question was more: why do Coq users don't have to bother when using cbn on the goal but do have to bother when using cbn in a hypothesis? Is there some deeper reason for this?
In case it has to be like this, it would indeed help if someone with deeper insight into the kernel reduction machinery would suggest an efficient work around. One issue with the workaround suggested above is that cbn is called twice on the original term and once on the already simplified term, which might not be that fast.
Michael Soegtrop (Oct 27 2023 at 07:35):Sorry, I just understood on third read of your post that you explained what the problem is - I thought you are discussing more efficient workarounds.
Michael Soegtrop (Oct 27 2023 at 07:38):Obviously the 3x cbv solution discussed by Paolo and Vadim does solve the problem. The question is: can one come up with a solution which calls cbn only once. And if so, why can't this be the default when doing cbn in a hypothesis.
Michael Soegtrop (Oct 27 2023 at 07:54):The main issue with this is that it likely works > 99.99% to use cbn in a hypothesis and usually fails only in large deep automation cases, where it is a nightmare to debug this - especially because the problem happens at Qed time. I think I spent several weeks debugging such cases in Princeton VST - down to running coqtop in the OCaml debugger and printing terms in the kernel reduction engine and going through GBs of logs. IMHO everybody using Coq in the large stumbles over this one day, so that this a largish road blocker for using Coq in the large.
Paolo Giarrusso (Oct 27 2023 at 22:25):If you use Coq in the large you must seal definitions, indeed.
Paolo Giarrusso (Oct 27 2023 at 22:28):and indeed, the performance problems only show up too late when rewriting code is painful, and figuring out what to seal is hard (don't take my word, take Jason's or look at math-comp https://stackoverflow.com/a/46138499/53974 )
Paolo Giarrusso (Oct 27 2023 at 22:31):I agree we'd want a smarter reduction on hyps, but that won't fix divergence on simpl/apply/... which also arise in such cases. At least for apply for this is only common for failing invocations
Michael Soegtrop (Oct 30 2023 at 08:35):@Paolo Giarrusso : I tend to use a different approach, reduction with tailored, usually computed delta reduction symbol lists. It is not that feasible to introduce sealing in e.g. VST after the facts, and with this method I got very good and reliable speed ups. I could do dynamic sealing - actually Andrew does this to a certain extend - but this is too slow for my purposes. But this does not help for reductions in hypothesis - I would really appreciate a solution for this - or at least a Coq kernel expert approved work around.
Jason Gross (Nov 02 2023 at 19:31):@Gaëtan Gilbert @Michael Soegtrop I believe there's a recipe in the wiki / FAQ for reversing the direction of conversion.
Michael Soegtrop (Nov 03 2023 at 08:38):@Jason Gross : do you have a link?
Karl Palmskog (Nov 03 2023 at 08:40):is there a bottom line for regular Coq users on how to keep their Qed time short? Are heuristics like "don't run simpl in a hypothesis if you can avoid it" meaningful?
Michael Soegtrop (Nov 03 2023 at 08:49):I personally never had any Qed time issues (that Qed was substantially slower than creating the proof script) other than doing simplification, reduction or change tactics on a hypothesis. But Jason suggested that there are other cases around simpl on the goal. I might have escaped these because I hardly every use simpl in automation. I am not sure if for cbv and lazy with explicit delta lists the casts are sufficiently expressive or if I have just been lucky so far.
Jason Gross (Nov 06 2023 at 05:01):@Michael Soegtrop
Link: the code block right above https://github.com/coq/coq/wiki/Troubleshooting#an-explosion-of-universes and the paragraph above that
As far as explicit delta links: you've mostly been lucky, but not unreasonably so. You should expect to hit a Qed issue if you have two separate calls to CBV/lazy with different lists such that if you replaced either list with the other the call to CBV/lazy would take a very long time. In general any call to CBV/lazy can be made fast by issuing a Strategy command that tells the kernel to unfold constants in the same order. However, each Qed processes the entire proof term with a single set of constant strategy levels, so if you need different subterms to be checked with different strategy level assignments, you'll be sad. There might be some relevant examples in the test-suite for with_strategy
Jason Gross (Nov 06 2023 at 05:04):@Karl Palmskog indeed the bottom line is roughly "don't use simpl, don't use reduction tactics in hypotheses unless you revert and reintroduce them after, don't use change ... with ... only change"
Guillaume Melquiond (Nov 06 2023 at 05:48):Also, don't use change on a goal with existential variables.
Vadim Zaliva (Nov 09 2023 at 22:03):perhaps coq should issue warnings (which could be disabled by user) in such known problematic cases?
Michael Soegtrop (Nov 10 2023 at 08:52):Even better would be to by default use one of the discussed work arounds by default and provide a separate variant of the tactic which works as today.
Last updated: Oct 13 2024 at 01:02 UTC