Slightly tweak the heuristic to pose dependent metas in case_pf. #17564
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
ppedrot
added
kind: cleanup
coqbot-app
bot
removed
the
request: full CI
|
The job library:ci-fiat_crypto_legacy has failed in allow failure mode |
ppedrot
added a commit
to ppedrot/cross-crypto
that referenced
this pull request
May 3, 2023
ppedrot
added a commit
to ppedrot/bignums
that referenced
this pull request
May 3, 2023
|
🔴 CI failures at commit 59b2ccd without any failure in the test-suite ✔️ Corresponding jobs for the base commit 65720db succeeded ❔ Ask me to try to extract minimal test cases that can be added to the test-suite 🏃
|
|
Most of the failures are faulty calls to intropatterns that silently introduce shelved evars. The new PR fails on these ones so that the calling tactic (destruct / intros) must be turned into its e-variant. |
ppedrot
added a commit
to ppedrot/QuickChick
that referenced
this pull request
May 3, 2023
|
Is there a way to have a warning instead of an error for backwards compat? |
ppedrot
added a commit
to ppedrot/verdi
that referenced
this pull request
May 3, 2023
ppedrot
added a commit
to coq-community/bignums
that referenced
this pull request
May 3, 2023
palmskog
added a commit
to uwplse/verdi
that referenced
this pull request
May 3, 2023
andres-erbsen
pushed a commit
to mit-plv/cross-crypto
that referenced
this pull request
May 3, 2023
|
Depends for which behaviour change (intopattern stricter vs. slight unification differences). Given the nature of the code it's probably going to be either hard or costly to implement, though. |
|
@coqbot ci minimize |
ppedrot
added a commit
to ppedrot/perennial
that referenced
this pull request
May 3, 2023
|
Minimized File /github/workspace/builds/coq/coq-failing/_build_ci/quickchick/src/Instances.v (from ci-quickchick) (full log on GitHub Actions) We are collecting data on the user experience of the Coq Bug Minimizer. Minimized Coq File (consider adding this file to the test-suite)(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/quickchick/src" "QuickChick" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/ExtLib" "ExtLib" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/SimpleIO" "SimpleIO" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/mathcomp" "mathcomp" "-I" "/github/workspace/builds/coq/coq-failing/_build_ci/quickchick/plugin" "-top" "QuickChick.Instances") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 764 lines to 26 lines, then from 39 lines to 570 lines, then from 567 lines to 26 lines, then from 31 lines to 27 lines *)
(* coqc version 8.18+alpha compiled with OCaml 4.14.1
coqtop version runner-ktkhz2yw-project-6138686-concurrent-0:/builds/coq/coq/_build/default,(HEAD detached at 69a2874) (69a2874a4bfab2dd4f363143378d7a21d9413771)
Expected coqc runtime on this file: 0.533 sec *)
Require QuickChick.Classes.
Import QuickChick.Classes.
Import QuickChick.Sets.
Import QuickChick.Producer.
#[global] Instance enumPairSized {A B : Type} `{EnumSized A} `{EnumSized B}
: EnumSized (A*B).
Admitted.
#[global] Instance enumPairSized_CorrectSized
A {_ : EnumSized A} { _ : forall s, SizeMonotonic (@enumSized A _ s)}
{ _ : SizedMonotonic (@enumSized A _)} { _ : CorrectSized (@enumSized A _)}
B {_ : EnumSized B} { _ : forall s, SizeMonotonic (@enumSized B _ s)}
{ _ : SizedMonotonic (@enumSized B _)} { _ : CorrectSized (@enumSized B _)}:
CorrectSized (@enumSized (A * B) enumPairSized).
Proof.
constructor.
split.
{
intros.
reflexivity.
}
destruct a.
intros _.
destruct H1 as [[_ Hca]].Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 4.3MiB file on GitHub Actions Artifacts under
|
zeldovich
added a commit
to mit-pdos/perennial
that referenced
this pull request
May 3, 2023
|
Minimized File /github/workspace/builds/coq/coq-failing/_build_ci/vst/msl/knot_prop.v (from ci-vst) (full log on GitHub Actions) We are collecting data on the user experience of the Coq Bug Minimizer. Minimized Coq File (consider adding this file to the test-suite)(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "-deprecated-native-compiler-option,-native-compiler-disabled" "-native-compiler" "ondemand" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/vst/msl" "VST.msl" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/vst/sepcomp" "VST.sepcomp" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/vst/veric" "VST.veric" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/vst/zlist" "VST.zlist" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/vst/floyd" "VST.floyd" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/vst/progs" "VST.progs" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/vst/concurrency" "VST.concurrency" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/vst/atomics" "VST.atomics" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/vst/wand_demo" "wand_demo" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/vst/sha" "sha" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/vst/hmacfcf" "hmacfcf" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/vst/tweetnacl20140427" "tweetnacl20140427" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/vst/hmacdrbg" "hmacdrbg" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/vst/aes" "aes" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/vst/mailbox" "mailbox" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/vst/compcert/lib" "compcert.lib" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/vst/compcert/common" "compcert.common" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/vst/compcert/x86_32" "compcert.x86_32" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/vst/compcert/x86" "compcert.x86" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/vst/compcert/cfrontend" "compcert.cfrontend" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/vst/compcert/export" "compcert.export" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Flocq" "Flocq" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "VST.msl.knot_prop") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 274 lines to 63 lines, then from 76 lines to 805 lines, then from 809 lines to 80 lines, then from 93 lines to 607 lines, then from 610 lines to 142 lines, then from 155 lines to 736 lines, then from 740 lines to 159 lines, then from 172 lines to 1133 lines, then from 1137 lines to 206 lines, then from 219 lines to 463 lines, then from 468 lines to 214 lines, then from 227 lines to 391 lines, then from 396 lines to 216 lines, then from 229 lines to 292 lines, then from 295 lines to 220 lines, then from 225 lines to 220 lines *)
(* coqc version 8.18+alpha compiled with OCaml 4.14.1
coqtop version runner-ktkhz2yw-project-6138686-concurrent-0:/builds/coq/coq/_build/default,(HEAD detached at 69a2874) (69a2874a4bfab2dd4f363143378d7a21d9413771)
Expected coqc runtime on this file: 0.476 sec *)
Require Coq.Logic.ClassicalFacts.
Require Coq.Logic.FunctionalExtensionality.
Require Coq.micromega.Lia.
Export Coq.Logic.FunctionalExtensionality.
Axiom prop_ext: ClassicalFacts.prop_extensionality.
Tactic Notation "extensionality" ident(x0) ident(x1) ident(x2) :=
extensionality x0; extensionality x1; extensionality x2.
Export Coq.micromega.Lia.
Definition compose (A B C:Type) (g:B -> C) (f:A -> B) := fun x => g (f x).
Arguments compose [A B C] _ _ _.
Infix "oo" := compose (at level 54, right associativity).
Definition id (A:Type) := fun x:A => x.
Record ageable_facts (A:Type) (level: A -> nat) (age1:A -> option A) :=
{ af_unage : forall x':A, exists x, age1 x = Some x'
; af_level1 : forall x, age1 x = None <-> level x = 0
; af_level2 : forall x y, age1 x = Some y -> level x = S (level y)
}.
Class ageable (A:Type) := mkAgeable
{ level : A -> nat
; age1 : A -> option A
; age_facts : ageable_facts A level age1
}.
Section level'.
End level'.
Section RtRft.
End RtRft.
Section NAT_AGEABLE.
End NAT_AGEABLE.
Section BIJECTION.
End BIJECTION.
Section PROD.
Variable A B : Type.
Variable agA: ageable A.
Let levelAB (x:prod A B) := level (fst x).
Let age1AB (x:prod A B) :=
match age1 (fst x) with
| None => None
| Some a' => Some (a',snd x)
end.
Lemma ag_prod_facts : ageable_facts (prod A B) levelAB age1AB.
Admitted.
Definition ag_prod :=
mkAgeable (prod A B) levelAB age1AB ag_prod_facts.
End PROD.
Section PROD'.
End PROD'.
Set Implicit Arguments.
Module Export CovariantFunctor.
Record functorFacts (PS : Type -> Type)
(fmap : forall A B (f : A -> B), PS A -> PS B) : Type :=
FunctorFacts {
ff_id : forall A, fmap _ _ (id A) = id (PS A);
ff_comp : forall A B C (f : B -> C) (g : A -> B),
fmap _ _ f oo fmap _ _ g = fmap _ _ (f oo g)
}.
Record functor : Type := Functor {
_functor: Type -> Type;
fmap : forall A B (f : A -> B), _functor A -> _functor B;
functor_facts : functorFacts _functor fmap
}.
Coercion CovariantFunctor._functor:
CovariantFunctor.functor >-> Funclass.
Module Type TY_FUNCTOR.
Parameter F : functor.
Parameter T : Type.
Parameter T_bot : T.
Parameter other : Type.
End TY_FUNCTOR.
Module Type KNOT.
Declare Module TF:TY_FUNCTOR.
Import TF.
Parameter knot : Type.
Parameter ag_knot : ageable knot.
#[global] Existing Instance ag_knot.
#[global] Existing Instance ag_prod.
Definition predicate := (knot * other) -> T.
Parameter squash : (nat * F predicate) -> knot.
Parameter unsquash : knot -> (nat * F predicate).
Definition approx (n:nat) (p:predicate) : predicate.
exact (fun w => if Compare_dec.le_gt_dec n (level w) then T_bot else p w).
Defined.
Axiom unsquash_squash : forall n x', unsquash (squash (n,x')) = (n,fmap F (approx n) x').
End KNOT.
Module Knot (TF':TY_FUNCTOR) : KNOT with Module TF:=TF'.
Module TF := TF'.
Import TF.
Fixpoint sinv (n: nat) : Type.
Admitted.
Definition knot := { n:nat & F (sinv n) }.
Definition predicate := knot * other -> T.
Definition squash (x:nat * F predicate) : knot.
Admitted.
Definition unsquash (x:knot) : (nat * F predicate).
Admitted.
Definition def_knot_level (k:knot) := fst (unsquash k).
Definition def_knot_age1 (k:knot) : option knot.
Admitted.
Definition approx (n:nat) (p:predicate) : predicate.
exact (fun w => if Compare_dec.le_gt_dec n (def_knot_level (fst w)) then T_bot else p w).
Defined.
Lemma unsquash_squash : forall n x', unsquash (squash (n,x')) = (n,fmap F (approx n) x').
Admitted.
Lemma ag_knot_facts : ageable_facts knot def_knot_level def_knot_age1.
Admitted.
Definition ag_knot : ageable knot.
exact (mkAgeable knot def_knot_level def_knot_age1 ag_knot_facts).
Defined.
End Knot.
Module Type TY_FUNCTOR_PROP.
Parameter F : functor.
Parameter other : Type.
End TY_FUNCTOR_PROP.
Module Type KNOT_HERED.
Declare Module TF:TY_FUNCTOR_PROP.
End KNOT_HERED.
Module KnotHered (TF':TY_FUNCTOR_PROP) : KNOT_HERED with Module TF:=TF'.
Module Export TF:=TF'.
Section stratifies.
End stratifies.
End KnotHered.
Module Type KNOT_PROP.
Declare Module TF:TY_FUNCTOR_PROP.
End KNOT_PROP.
Module TyFunctorProp2TyFunctor (TF : TY_FUNCTOR_PROP) <: TY_FUNCTOR.
Definition F := TF.F.
Definition T: Type.
exact (Prop).
Defined.
Definition T_bot : T.
exact (False).
Defined.
Definition other := TF.other.
End TyFunctorProp2TyFunctor.
Module KnotProp (TF':TY_FUNCTOR_PROP) : KNOT_PROP with Module TF:=TF'.
Module TF := TF'.
Module TF_G := TyFunctorProp2TyFunctor(TF).
Module Knot_G := Knot(TF_G).
Import TF.
Definition knot : Type.
exact (Knot_G.knot).
Defined.
Definition predicate := (knot * other) -> Prop.
Definition squash : (nat * F predicate) -> knot.
exact (Knot_G.squash).
Defined.
Definition unsquash : knot -> (nat * F predicate).
exact (Knot_G.unsquash).
Defined.
Definition ag_knot := Knot_G.ag_knot.
#[global] Existing Instance ag_knot.
Definition approx (n:nat) (p:predicate) : predicate.
exact (fun w => level w < n /\ p w).
Defined.
Lemma unsquash_squash : forall n x', unsquash (squash (n,x')) = (n,fmap F (approx n) x').
Proof.
replace approx with Knot_G.approx.
apply Knot_G.unsquash_squash.
extensionality n p w.
unfold approx, Knot_G.approx, TF_G.T_bot.
case (Compare_dec.le_gt_dec n (level w)); intro; apply prop_ext; firstorder.
unfold knot, TF_G.other, ag_knot in *.
lia.Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 3.7MiB file on GitHub Actions Artifacts under
|
liyishuai
pushed a commit
to QuickChick/QuickChick
that referenced
this pull request
May 3, 2023
|
Minimized File /github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto_legacy/src/Util/Loops.v (from ci-fiat_crypto_legacy) (full log on GitHub Actions) We are collecting data on the user experience of the Coq Bug Minimizer. Minimized Coq File (consider adding this file to the test-suite)(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "-deprecated-hint-rewrite-without-locality,+deprecated-hint-without-locality,+deprecated-instance-without-locality,unsupported-attributes" "-w" "-notation-overridden" "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto_legacy/src" "Crypto" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto_legacy/bbv/src/bbv" "bbv" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto_legacy/coqprime/src/Coqprime" "Coqprime" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-I" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto_legacy/coqprime/src" "-top" "Crypto.Util.Loops") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 478 lines to 90 lines, then from 95 lines to 91 lines *)
(* coqc version 8.18+alpha compiled with OCaml 4.14.1
coqtop version runner-ktkhz2yw-project-6138686-concurrent-0:/builds/coq/coq/_build/default,(HEAD detached at 69a2874) (69a2874a4bfab2dd4f363143378d7a21d9413771)
Expected coqc runtime on this file: 0.480 sec *)
Require Coq.micromega.Lia.
Import Coq.micromega.Lia.
Section Loops.
Context {A B : Type} (body : A -> A + B).
Fixpoint loop (fuel : nat) (s : A) {struct fuel} : A + B.
Admitted.
Context (body_cps : A -> forall T, (A + B -> T) -> T).
Context (body_cps_ok : forall s {R} f, body_cps s R f = f (body s)).
Context (body_cps2 : A -> forall R, (A -> R) -> (B -> R) -> R).
Context (body_cps2_ok : forall s {R} continue break,
body_cps2 s R continue break =
match body s with
| inl a => continue a
| inr b => break b
end).
Local Lemma loop_fuel_0 s : loop 0 s = body s.
Admitted.
Lemma loop_fuel_irrelevant n m s bn bm
(Hn : loop n s = inr bn)
(Hm : loop m s = inr bm)
: bn = bm.
Admitted.
Definition iterations_required fuel s : option nat :=
nat_rect _ None
(fun n r =>
match r with
| Some _ => r
| None =>
match loop n s with
| inl a => None
| inr b => Some n
end
end
) fuel.
Lemma iterations_required_correct fuel s :
(forall m, iterations_required fuel s = Some m ->
m < fuel /\
exists b, forall n, (n < m -> exists a, loop n s = inl a) /\ (m <= n -> loop n s = inr b))
/\
(iterations_required fuel s = None -> forall n, n < fuel -> exists a, loop n s = inl a).
Admitted.
Lemma iterations_required_step fuel s s' n
(Hs : iterations_required fuel s = Some (S n))
(Hstep : body s = inl s')
: iterations_required fuel s' = Some n.
Admitted.
Local Lemma invariant_complete (P:_->Prop) f s0 b (H:loop f s0 = inr b) (HP:P b)
: exists inv measure,
(inv s0 /\ measure s0 <= f)
/\ forall s, inv s -> match body s with
| inl s' => inv s' /\ measure s' < measure s
| inr s' => P s'
end.
Proof.
set (measure s := match iterations_required (S f) s with None => 0 | Some n => n end).
exists (fun s => match loop (measure s) s with
| inl a => False
| inr r => r = b end).
exists (measure); split; [ |repeat match goal with |- _ /\ _ => split end..].
{
cbv [measure].
destruct (iterations_required (S f) s0) eqn:Hs0;
eapply iterations_required_correct in Hs0;
[ .. | exact (ltac:(lia):f <S f)]; [|destruct Hs0; congruence].
destruct Hs0 as [? [? Hs0]]; split; [|lia].
pose proof (proj2 (Hs0 n) ltac:(lia)) as HH; rewrite HH.
exact (loop_fuel_irrelevant _ _ _ _ _ HH H).
}
{
intros s Hinv; destruct (body s) as [s'|c] eqn:Hstep.
{
destruct (loop (measure s) s) eqn:Hs; [contradiction|subst].
cbv [measure] in *.
destruct (iterations_required (S f) s) eqn:Hs' in *; try destruct n;
try (rewrite loop_fuel_0 in Hs; congruence); [].
pose proof (iterations_required_step _ _ s' _ Hs' Hstep) as HA.
rewrite HA.
destruct (proj1 (iterations_required_correct _ _) _ HA) as [? [? [? HE']]].Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 11MiB file on GitHub Actions Artifacts under
|
|
🔴 CI failures at commit 59b2ccd without any failure in the test-suite ✔️ Corresponding jobs for the base commit 65720db succeeded ❔ Ask me to try to extract minimal test cases that can be added to the test-suite 🏃
|
|
Minimized File /github/workspace/builds/coq/coq-failing/_build_ci/perennial/src/base_logic/lib/wsat.v (from ci-perennial) (interrupted by timeout, being automatically continued) (full log on GitHub Actions) Minimized Coq File (truncated to 32KiB; full 48KiB file on GitHub Actions Artifacts under
|
|
Minimized File /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/pcuic/theories/PCUICProgress.v (from ci-metacoq) (interrupted by timeout, being automatically continued) (full log on GitHub Actions) Minimized Coq File (truncated to 32KiB; full 42KiB file on GitHub Actions Artifacts under
|
|
Minimized File /github/workspace/builds/coq/coq-failing/_build_ci/perennial/src/base_logic/lib/wsat.v (from ci-perennial) (interrupted by timeout, being automatically continued) (full log on GitHub Actions) Minimized Coq File (truncated to 32KiB; full 93KiB file on GitHub Actions Artifacts under
|
|
Minimized File /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/pcuic/theories/PCUICProgress.v (from ci-metacoq) (interrupted by timeout, being automatically continued) (full log on GitHub Actions) Minimized Coq File (truncated to 32KiB; full 45KiB file on GitHub Actions Artifacts under
|
|
🔴 CI failures at commit 59b2ccd without any failure in the test-suite ✔️ Corresponding jobs for the base commit 65720db succeeded ❔ Ask me to try to extract minimal test cases that can be added to the test-suite 🏃
|
|
Minimized File /github/workspace/builds/coq/coq-failing/_build_ci/perennial/src/base_logic/lib/wsat.v (from ci-perennial) (interrupted by timeout, being automatically continued) (full log on GitHub Actions) Minimized Coq File (truncated to 32KiB; full 168KiB file on GitHub Actions Artifacts under
|
|
Minimized File (from ci-perennial) (full log on GitHub Actions) We are collecting data on the user experience of the Coq Bug Minimizer. Minimized Coq File (truncated to 32KiB; full 168KiB file on GitHub Actions Artifacts under
|
|
Minimized File (from ci-metacoq) (full log on GitHub Actions) We are collecting data on the user experience of the Coq Bug Minimizer. Minimized Coq File (truncated to 32KiB; full 75KiB file on GitHub Actions Artifacts under
|
|
🔴 CI failure at commit edca56e without any failure in the test-suite ✔️ Corresponding job for the base commit a85232c succeeded ❔ Ask me to try to extract a minimal test case that can be added to the test-suite 🏃
|
andrew-appel
added a commit
to PrincetonUniversity/VST
that referenced
this pull request
May 9, 2023
We only use ecase to interpret split intropatterns for eintros and instead use case when used with intros.
We preemptively pose all dependent metas as evars and instead rely on tclWITHHOLES to check that they were resolved by unification. This might change the return clause a bit since legacy unification does not handle metas exactly like evars.
We pose them as proper goals before calling case_pf.
ppedrot
added
the
request: full CI
ppedrot
force-pushed
the
case-pf-pose-dependent-metas
branch
from
edca56e
to
8583ab4
Compare
coqbot-app
bot
removed
the
request: full CI
|
just in case @coqbot bench |
|
🏁 Bench results: 🐢 Top 25 slow downs┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 4.4170 16.6260 12.2090 276.41% 84 coq-vst/veric/binop_lemmas2.v.html │ │ 43.0770 44.5950 1.5180 3.52% 236 coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html │ │ 19.3480 20.5320 1.1840 6.12% 2061 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │ │ 3.5730 4.4430 0.8700 24.35% 937 coq-vst/veric/binop_lemmas2.v.html │ │ 7.1660 7.7900 0.6240 8.71% 881 coq-vst/veric/binop_lemmas4.v.html │ │ 6.5000 7.1180 0.6180 9.51% 477 coq-vst/veric/expr_lemmas3.v.html │ │ 5.7970 6.3230 0.5260 9.07% 5 coq-fiat-crypto-with-bedrock/src/Assembly/Parse/Examples/fiat_p256_mul_optimised_seed12.v.html │ │ 1.4340 1.8780 0.4440 30.96% 60 coq-vst/veric/binop_lemmas2.v.html │ │ 0.6370 1.0220 0.3850 60.44% 1763 coq-perennial/src/program_proof/simplepb/apps/eesm_proof.v.html │ │ 6.4700 6.8100 0.3400 5.26% 629 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/LAN9250.v.html │ │ 4.2400 4.5700 0.3300 7.78% 237 coq-fiat-parsers/src/Parsers/ParserFromParserADT.v.html │ │ 10.6870 11.0060 0.3190 2.98% 55 coq-category-theory/Construction/Comma/Natural/Transformation.v.html │ │ 29.4070 29.7070 0.3000 1.02% 12 coq-fourcolor/theories/job399to438.v.html │ │ 0.7580 1.0430 0.2850 37.60% 16 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/New/WordByWordMontgomery.v.html │ │ 0.0030 0.2760 0.2730 9100.00% 371 coq-fiat-crypto-with-bedrock/src/CLI.v.html │ │ 23.3450 23.6110 0.2660 1.14% 12 coq-fourcolor/theories/job511to516.v.html │ │ 0.7600 1.0250 0.2650 34.87% 9 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/Field25519.v.html │ │ 0.0000 0.2640 0.2640 inf% 164 coq-metacoq-erasure/erasure/theories/Typed/ErasureCorrectness.v.html │ │ 1.6360 1.8960 0.2600 15.89% 716 coq-vst/veric/expr_lemmas.v.html │ │ 0.0010 0.2590 0.2580 25800.00% 473 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/New/Signature.v.html │ │ 3.0160 3.2730 0.2570 8.52% 492 coq-perennial/src/program_proof/examples/async_mem_alloc_inode_proof.v.html │ │ 0.0450 0.3010 0.2560 568.89% 144 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.v.html │ │ 0.3890 0.6370 0.2480 63.75% 238 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Translation/Proofs/Cmd.v.html │ │ 9.6870 9.9340 0.2470 2.55% 446 coq-mathcomp-odd-order/theories/PFsection12.v.html │ │ 0.0020 0.2460 0.2440 12200.00% 327 coq-metacoq-pcuic/pcuic/theories/PCUICFirstorder.v.html │ └──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 43.4110 41.6410 -1.7700 -4.08% 236 coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html │ │ 42.2740 40.5060 -1.7680 -4.18% 224 coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html │ │ 158.6580 157.1250 -1.5330 -0.97% 233 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │ │ 126.0000 124.7160 -1.2840 -1.02% 22 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html │ │ 18.4410 17.1770 -1.2640 -6.85% 376 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvMetric.v.html │ │ 40.9120 39.7270 -1.1850 -2.90% 827 coq-vst/veric/binop_lemmas4.v.html │ │ 142.7180 141.5910 -1.1270 -0.79% 1190 coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html │ │ 128.7230 127.7680 -0.9550 -0.74% 999 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 128.8330 127.8930 -0.9400 -0.73% 968 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 59.9890 59.0790 -0.9100 -1.52% 27 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html │ │ 25.1210 24.2370 -0.8840 -3.52% 25 coq-fiat-crypto-with-bedrock/src/Spec/Test/X25519.v.html │ │ 25.1450 24.2710 -0.8740 -3.48% 20 coq-fiat-crypto-with-bedrock/src/Spec/Test/X25519.v.html │ │ 20.0320 19.1820 -0.8500 -4.24% 420 coq-perennial/src/program_proof/simplepb/pb_setstate_proof.v.html │ │ 53.0680 52.3060 -0.7620 -1.44% 50 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 34.3760 33.6230 -0.7530 -2.19% 548 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html │ │ 32.0870 31.3670 -0.7200 -2.24% 1333 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │ │ 65.2180 64.5140 -0.7040 -1.08% 103 coq-fiat-crypto-with-bedrock/src/Arithmetic/BarrettReduction.v.html │ │ 30.4150 29.7130 -0.7020 -2.31% 515 coq-metacoq-erasure/erasure/theories/ErasureFunction.v.html │ │ 212.6850 212.0160 -0.6690 -0.31% 141 coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html │ │ 4.7210 4.0540 -0.6670 -14.13% 22 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html │ │ 19.7000 19.0440 -0.6560 -3.33% 28 coq-fiat-crypto-with-bedrock/src/Spec/Test/X25519.v.html │ │ 12.0020 11.3850 -0.6170 -5.14% 126 coq-vst/veric/binop_lemmas6.v.html │ │ 28.6810 28.1010 -0.5800 -2.02% 1387 coq-fourcolor/theories/cfmap.v.html │ │ 27.6940 27.1320 -0.5620 -2.03% 79 coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.v.html │ │ 79.9330 79.3970 -0.5360 -0.67% 618 coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
|
The VST slowdowns in the binop files are real, but funnily enough it's somewhat an indirect bug. They happen with well-known degenerate examples of nested destruct calls that generate a gazillion subgoals. Since we're now checking that intropatterns are not introducing unshelved evars, we observe the bad algorithmic behaviour of I don't think it's really worth being concerned about. First, I've had these destruct lines on my radar for a while and I was already aware of the evar check issue. The total time added to VST is neglectible, the problem is really in a handful of extremely localized calls to destruct. Second, forgetting about the algorithmic issue with the check for a second, this PR cannot be tweaked insofar as we must indeed check for these evars whatsoever. So, from my point of view, this PR is ready. |
ppedrot
added a commit
to ppedrot/coq
that referenced
this pull request
May 10, 2023
We only care about the difference between undefined evars, so whenever the new evarmap has physically the same undefined evars as the original one, we return immediately. This seriously alleviates the slowdowns introduced in coq#17564.
|
See #17590 for a workaround. On my machine, that PR seems to be enough to eliminate the slowdown. |
SkySkimmer
approved these changes
May 10, 2023
|
@coqbot merge now |
Merged
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
We refine the case scrutinee before calling the case_pf function proper, and rely on tclWITHHOLES instead of the legacy refiner to check that holes are correctly solved rather than turned into shelved evars.
As a side-effect, this fixes a bug with intropatterns that silently introduced shelved evars even though the toplevel tactic should have forbidden them. A trivial fix is to turn the offending tactic into its e-variant.