Is there any situation where it is expected that tactic.
fails but Fail tactic.
also fails?
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".
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.)
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.)
it doesnt look like an anomaly to me :shrug:
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.^^
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
.
@Ralf Jung proof general has bugs in failure recognition (it's text matching), so can you confirm that Fail actually failed? Link coming.
Or at least, PG has one bug there https://github.com/ProofGeneral/PG/issues/597#issuecomment-916830083
"stepping to a later command works differently" is also in common between the two bugs.
@Paolo Giarrusso yes I think that's it; there is "in nested ltac call" in the output. Thanks!
Last updated: Oct 13 2024 at 01:02 UTC