Stream: Coq users

Topic: "Fail failing_tactic" fails to fail


view this post on Zulip Ralf Jung (Sep 27 2021 at 14:57):

Is there any situation where it is expected that tactic. fails but Fail tactic. also fails?

view this post on Zulip Ralf Jung (Sep 27 2021 at 14:58):

I am getting the following from Fail f_contractive. (which is a custom Iris tactic, and I am using it somewhere deep in Perennial)

In nested Ltac calls to "f_contractive" and
"simple apply (_ : Proper (_ ==> dist_later _ ==> _) f)", last call failed.
In environment
Λ : language
Σ : gFunctors
irisGS0 : irisGS Λ Σ
generationGS0 : generationGS Λ Σ
s : stuckness
mj : fracR
n : nat
wp, wp' : coPset -d> expr Λ -d> (val Λ -d> iPropO Σ) -d> iPropO Σ -d> iPropO Σ
Hwp : dist_later n wp wp'
E1 : coPset
e1 : expr Λ
Φ : val Λ -d> iPropO Σ
Φc : iPropO Σ
Unable to unify "Proper (?R ==> dist_later ?n ==> ?R') bi_and" with
 "(match to_val e1 with
   | Some v =>
       ∀ (q : fracR) (g1 : global_state Λ) (ns : nat) (D : coPset) (κs : list (observation Λ)),
         global_state_interp g1 ns mj D κs -∗
         NC q -∗ ||={E1|⊤ ∖ D}=> Φ v ∗ global_state_interp g1 ns mj D κs ∗ NC q
   | None =>
       ∀ (q : fracR) (σ1 : state Λ) (g1 : global_state Λ) (ns : nat) (D : coPset)
         (κ κs : list (observation Λ)) (nt : nat),
         state_interp σ1 nt -∗
         global_state_interp g1 ns mj D (κ ++ κs) -∗
         NC q -∗
         ||={E1|⊤ ∖ D,∅|∅}=>
           ||▷=>^(S (num_laters_per_step ns)) ⌜match s with
                                               | NotStuck => reducible e1 σ1 g1
                                               | MaybeStuck => True
                                               end⌝ ∗
           (∀ (e2 : expr Λ) (σ2 : state Λ) (g2 : global_state Λ) (efs : list (expr Λ)),
              ⌜prim_step e1 σ1 g1 κ e2 σ2 g2 efs⌝ -∗
              ||={∅|∅,E1|⊤ ∖ D}=> state_interp σ2 (length efs + nt) ∗
                global_state_interp g2 (step_count_next ns) mj D κs ∗
                wp match to_val e2 with
                   | Some _ => E1
                   | None => ⊤
                   end e2 Φ Φc ∗ ([∗ list] ef ∈ efs, wp ⊤ ef fork_post True) ∗
                NC q)
   end
   ∧ (∀ (g1 : global_state Λ) (ns : nat) (D : coPset) (κs : list (observation Λ)),
        global_state_interp g1 ns mj D κs -∗
        C -∗
        ||={E1|⊤ ∖ D,∅|∅}=>
          ||▷=>^(num_laters_per_step ns) ||={∅|∅,E1|⊤ ∖ D}=> global_state_interp g1 ns mj D κs ∗ Φc))%I ≡{n}≡ (match
                                                                       to_val e1
                                                                       with
                                                                       | Some v =>
                                                                       ∀ (q : fracR)
                                                                       (g1 :
                                                                       global_state Λ)
                                                                       (ns : nat)
                                                                       (D : coPset)
                                                                       (κs :
                                                                       list (observation Λ)),
                                                                       global_state_interp g1 ns mj
                                                                       D κs -∗
                                                                       NC q -∗
                                                                       ||={E1|
                                                                       ⊤ ∖ D}=>
                                                                       Φ v ∗
                                                                       global_state_interp g1 ns mj
                                                                       D κs ∗
                                                                       NC q
                                                                       | None =>
                                                                       ∀ (q : fracR)
                                                                       (σ1 : state Λ)
                                                                       (g1 :
                                                                       global_state Λ)
                                                                       (ns : nat)
                                                                       (D : coPset)
                                                                       (κ κs :
                                                                       list (observation Λ))
                                                                       (nt : nat),
                                                                       state_interp σ1 nt -∗
                                                                       global_state_interp g1 ns mj
                                                                       D (κ ++ κs) -∗
                                                                       NC q -∗
                                                                       ||={E1|
                                                                       ⊤ ∖ D,∅|∅}=>
                                                                       ||▷=>^
                                                                       (S (num_laters_per_step ns)) ⌜
                                                                       match s with
                                                                       | NotStuck =>
                                                                       reducible e1 σ1 g1
                                                                       | MaybeStuck => True
                                                                       end⌝ ∗
                                                                       (∀ (e2 : expr Λ)
                                                                       (σ2 :
                                                                       state Λ)
                                                                       (g2 :
                                                                       global_state Λ)
                                                                       (efs :
                                                                       list (expr Λ)),

                                                                       prim_step e1 σ1 g1 κ e2 σ2 g2
                                                                       efs⌝ -∗
                                                                       ||={∅|∅,E1|
                                                                       ⊤ ∖ D}=>
                                                                       state_interp σ2
                                                                       (length efs + nt) ∗
                                                                       global_state_interp g2
                                                                       (step_count_next ns) mj D κs ∗
                                                                       wp'
                                                                       match to_val e2 with
                                                                       | Some _ => E1
                                                                       | None => ⊤
                                                                       end e2 Φ Φc ∗
                                                                       ([∗ list] ef ∈ efs,
                                                                       wp' ⊤ ef fork_post True) ∗
                                                                       NC q)
                                                                       end
                                                                       ∧ (∀ (g1 : global_state Λ)
                                                                       (ns : nat)
                                                                       (D : coPset)
                                                                       (κs :
                                                                       list (observation Λ)),
                                                                       global_state_interp g1 ns mj
                                                                       D κs -∗
                                                                       C -∗
                                                                       ||={E1|
                                                                       ⊤ ∖ D,∅|∅}=>
                                                                       ||▷=>^
                                                                       (num_laters_per_step ns)
                                                                       ||={∅|∅,E1|
                                                                       ⊤ ∖ D}=>
                                                                       global_state_interp g1 ns mj
                                                                       D κs ∗ Φc))%I".

view this post on Zulip Ralf Jung (Sep 27 2021 at 14:59):

This is quite problematic because I was trying to see which kinds of TC search that tactic is doing, and Set Typelasses Debug output is only visible in Proof Generation when the command succeeds (so Fail foo. is required to see the output for tactics that fail.)

view this post on Zulip Guillaume Melquiond (Sep 27 2021 at 15:03):

Fail will fail in case of anomalies, so that they are not silently ignored. (This is unrelated to your case though, unless the exception was somehow camouflaged as an anomaly.)

view this post on Zulip Ralf Jung (Sep 27 2021 at 18:14):

it doesnt look like an anomaly to me :shrug:

view this post on Zulip Ralf Jung (Sep 27 2021 at 18:19):

sadly it happens in the middle of perennial... to reproduce, go to this line (commit ID is embedded in URL):
https://github.com/mit-pdos/perennial/blob/3ebb6f05456e2378e687e7eb99c30001930ff396/src/program_logic/crash_weakestpre.v#L104
after that line insert

Set Ltac Profiling.
Fail f_contractive.

the Set is required, somehow. Then single-step over these two commands in ProofGeneral.
When stepping immediately to a later command, for some reason it works again... none of this makes any sense to me.^^

view this post on Zulip Guillaume Melquiond (Sep 27 2021 at 18:28):

What I meant is that, if the code that classifies anomalies (so as to let them through) misclassifies the error raised by your tactic, then it will escape the Fail.

view this post on Zulip Paolo Giarrusso (Sep 27 2021 at 20:47):

@Ralf Jung proof general has bugs in failure recognition (it's text matching), so can you confirm that Fail actually failed? Link coming.

view this post on Zulip Paolo Giarrusso (Sep 27 2021 at 20:48):

Or at least, PG has one bug there https://github.com/ProofGeneral/PG/issues/597#issuecomment-916830083

view this post on Zulip Paolo Giarrusso (Sep 27 2021 at 20:48):

"stepping to a later command works differently" is also in common between the two bugs.

view this post on Zulip Ralf Jung (Sep 27 2021 at 21:45):

@Paolo Giarrusso yes I think that's it; there is "in nested ltac call" in the output. Thanks!


Last updated: Jan 29 2023 at 01:02 UTC