Stream: Coq users

Topic: Ltac

view this post on Zulip k32 (Jun 02 2020 at 22:31):

Is there a way to disable backtracking in Ltac match? I trying to debug a tactic where one of the branches fails. So instead of a meaningful error I get "no matching clauses for match". 

Ltac foo :=
  match goal with
  | [..... |- _] =>
      step1; step2; step3; step4
 end.

One of the steps fails, but backtracking eats the error message. I wonder if there is a way to debug this.

view this post on Zulip Kenji Maillard (Jun 02 2020 at 22:37):

I think that what you are looking for is called lazymatch. It is described succintly as a variant of match.

view this post on Zulip Michael Soegtrop (Jun 03 2020 at 13:44):

I have a question on cbn and simpl. I try to replace some uses on simpl in VST with cbn cause I have cases where simpl runs forever while cbn returns immediately. One issue is that VST has tactics which take simplification tactics as arguments. Passing simpl or idtac works fine, but passing cbn gives "undefined". Also Print cbn says it is undefined. Init has:

Ltac2 Notation "cbn" s(strategy) cl(opt(clause)) :=
Std.cbn s (default_on_concl cl).
Ltac2 Notation cbn := cbn.

@Théo Zimmermann already explained me that I have to Add Ltac cbn := cbn but it would be nice to understand what these 4 levels of definitions are good for (the core cbn in OCaml, the 2 notations in Init and the Ltac definition needed to pass it as Ltac). Also I wonder if this could be more consistent or if there are some principal restrictions.

view this post on Zulip Michael Soegtrop (Jun 03 2020 at 16:11):

Sorry, this was silly - I didn't see that this are Ltac2 Notations. So is there a difference between simpl and cbn visible in the standard library?

view this post on Zulip Théo Zimmermann (Jun 03 2020 at 16:13):

Yes, even if you don't load Ltac2, simpl is an Ltac reference while cbn is only a Tactic Notation.

view this post on Zulip Michael Soegtrop (Jun 03 2020 at 16:26):

Could you point me to these definitions? I am unable to find them. When I do in a plain session "Locate simpl" it says "Ltac Coq.Init.Notations.simpl"m but the word "simpl" doesn't seem to appear in Init.Notations.

view this post on Zulip Théo Zimmermann (Jun 03 2020 at 16:29):

They are defined in the Ltac (ML) plugin. That's why the Print Ltac command can only show Ltac simpl := simpl

Last updated: Apr 17 2024 at 23:01 UTC