Tactic simpl causes Anomaly "Uncaught exception Not_found."

[fpottier]

Description of the problem

The attached project ends with a use of the tactic simpl that causes Anomaly "Uncaught exception Not_found.". Use make to compile. The project depends on coq-stdpp. bug2.tar.gz

Coq Version

8.16.1

[SkySkimmer]

@coqbot: minimize

#!/usr/bin/env bash
opam install -y coq-stdpp
eval $(opam env)
wget 'https://github.com/coq/coq/files/11050326/bug2.tar.gz'
tar -xf bug2.tar.gz
cd bug2
make

[coqbot-app[bot]]

Hey @SkySkimmer, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.

[coqbot-app[bot]]

@SkySkimmer, Minimized File /github/workspace/bug2/theories/examples.v (full log on GitHub Actions)

Minimized Coq File (consider adding this file to the test-suite)

```coq (* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "-deprecated-native-compiler-option" "-R" "/github/workspace/bug2" "AmpleStep" "-Q" "/github/workspace/cwd" "Top" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Bignums" "Bignums" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Ltac2" "Ltac2" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/stdpp" "stdpp" "-top" "AmpleStep.theories.examples" "-native-compiler" "no") -*- *) (* File reduced by coq-bug-minimizer from original input, then from 283 lines to 42 lines, then from 55 lines to 180 lines, then from 185 lines to 91 lines, then from 104 lines to 164 lines, then from 169 lines to 93 lines, then from 106 lines to 1017 lines, then from 1022 lines to 164 lines, then from 177 lines to 646 lines, then from 651 lines to 223 lines, then from 236 lines to 519 lines, then from 524 lines to 336 lines, then from 349 lines to 695 lines, then from 700 lines to 408 lines, then from 421 lines to 642 lines, then from 647 lines to 490 lines, then from 503 lines to 556 lines, then from 561 lines to 490 lines, then from 503 lines to 667 lines, then from 672 lines to 493 lines, then from 506 lines to 5801 lines, then from 5806 lines to 494 lines, then from 507 lines to 2008 lines, then from 2012 lines to 495 lines, then from 508 lines to 2062 lines, then from 2063 lines to 510 lines, then from 515 lines to 511 lines *) (* coqc version 8.16.1 compiled with OCaml 4.13.1 coqtop version 8.16.1 Expected coqc runtime on this file: 0.361 sec *) Require Coq.NArith.NArith. Require Coq.Program.Syntax. Require Coq.Unicode.Utf8. Export Coq.Unicode.Utf8. Export Coq.Program.Syntax. Declare Scope stdpp_scope. Global Open Scope stdpp_scope. Class MBind (M : Type → Type) := mbind : ∀ {A B}, (A → M B) → M A → M B. Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : stdpp_scope. Notation "x ← y ; z" := (y ≫= (λ x : _, z)) (at level 20, y at level 100, z at level 200, only parsing) : stdpp_scope. Notation "' x ← y ; z" := (y ≫= (λ x : _, z)) (at level 20, x pattern, y at level 100, z at level 200, only parsing) : stdpp_scope. Export Coq.Strings.String. Global Open Scope string_scope. Definition var := string. Definition data := string. Inductive pat := | PAny | PVar (x : var) | PTuple (ps : pats) | PData (c : data) (p : pat) with pats := | PNil | PCons (p : pat) (ps : pats). Inductive expr := | EVar (x : var) | ERec (f x : var) (e : expr) | EApp (e1 e2 : expr) | ETuple (es : exprs) | EData (c : data) (e : expr) | EMatch (e : expr) (bs : branches) | EAssertFalse | EAssert (e : expr) with exprs := | ENil | ECons (e : expr) (es : exprs) with branch := | Branch (pat : pat) (e : expr) with branches := | BNil | BCons (b : branch) (bs : branches). Inductive val := | VRec (η : env) (f x : var) (e : expr) | VTuple (vs : vals) | VData (c : data) (v : val) with vals := | VNil | VCons (v : val) (vs : vals) with env := | EnvNil | EnvCons (x : var) (v : val) (η : env). Notation EUnit := (ETuple ENil). Notation VUnit := (VTuple VNil). Notation EConstant c := (EData c EUnit). Notation VConstant c := (VData c VUnit). Notation EPair e1 e2 := (ETuple (ECons e1 (ECons e2 ENil))). Notation VPair v1 v2 := (VTuple (VCons v1 (VCons v2 VNil))). Inductive free A := | Ret (a : A) | Fail | Next | Stop (η : env) (e : expr) (k : val → free A) | Flip (k : bool → free A) | Par {A1 A2} (m1 : free A1) (m2 : free A2) (k : A1 * A2 → free A) (ko : unit → free A) . Arguments Ret {A}. Arguments Fail {A}. Arguments Next {A}. Arguments Stop {A} η e k. Arguments Flip {A} k. Arguments Par {A A1 A2} m1 m2 k ko. Notation ret := (Ret). Notation fail := (Fail). Notation next := (λ tt, Next). Definition choose {A} (m1 m2 : free A) : free A. Admitted. Definition par {A1 A2} (m1 : free A1) (m2 : free A2) : free (A1 * A2). exact (Par m1 m2 ret next). Defined. Fixpoint bind {A B} (m : free A) (f : A → free B) : free B := match m with | Ret a => f a | Fail => Fail | Next => Next | Stop η e k => Stop η e (λ v, bind (k v) f) | Flip k => Flip (λ v, bind (k v) f) | Par m1 m2 k ko => Par m1 m2 (λ v, bind (k v) f) (λ tt, bind (ko()) f) end. Fixpoint try {A B} (m : free A) (f : A → free B) (g : unit → free B) : free B := match m with | Ret a => f a | Fail => Fail | Next => g() | Stop η e k => Stop η e (λ v, try (k v) f g) | Flip k => Flip (λ v, try (k v) f g) | Par m1 m2 k ko => Par m1 m2 (λ v, try (k v) f g) (λ tt, try (ko()) f g) end. Global Instance free_mbind : MBind free := { mbind := λ {A B} (f : A → free B) (m : free A), bind m f }. Module Export eval. Implicit Type f x : var. Implicit Type v : val. Implicit Type η : env. Notation ok := (ret VUnit). Fixpoint lookup η x : free val. exact (match η with | EnvCons x' v η => if x =? x' then ret v else lookup η x | EnvNil => fail end). Defined. Fixpoint extend η p v : free env := match p, v with | PAny, _ => ret η | PVar x, _ => ret (EnvCons x v η) | PTuple ps, VTuple vs => extends η ps vs | PData c p, VData c' v => if c =? c' then extend η p v else next() | PTuple _, _ | PData _ _, _ => fail end with extends η ps vs : free env := match ps, vs with | PNil, VNil => ret η | PCons p ps, VCons v vs => η ← extend η p v ; η ← extends η ps vs ; ret η | _, _ => fail end. Definition call v1 v2 : free val. Admitted. Definition as_bool (m : free val) : free bool. Admitted. Fixpoint eval η e : free val := match e with | EVar x => lookup η x | ERec f x e => ret (VRec η f x e) | EApp e1 e2 => '(v1, v2) ← par (eval η e1) (eval η e2) ; call v1 v2 | ETuple es => vs ← evals η es ; ret (VTuple vs) | EData c e => v ← eval η e ; ret (VData c v) | EMatch e bs => v ← eval η e ; eval_match η v bs | EAssertFalse => fail | EAssert e => let test : free val := b ← as_bool (eval η e) ; if (b : bool) then ok else fail in choose ok test end with evals η es : free vals := match es with | ENil => ret VNil | ECons e es => '(v, vs) ← par (eval η e) (evals η es) ; ret (VCons v vs) end with eval_match η v bs := match bs with | BNil => fail | BCons (Branch p e) bs => try (extend η p v) (λ η, eval η e) (λ tt, eval_match η v bs) end. End eval. Inductive step {A} : free A → free A → Prop := | StepStop : ∀ η e k, step (Stop η e k) (bind (eval η e) k) | StepFlip : ∀ b k, step (Flip k) (k b) | StepParRetRet : ∀ {A1 A2} (v1 : A1) (v2 : A2) k ko, step (Par (Ret v1) (Ret v2) k ko) (k (v1, v2)) | StepParFailLeft : ∀ {A1 A2} (m2 : free A2) k ko, step (Par (@Fail A1) m2 k ko) Fail | StepParFailRight : ∀ {A1 A2} (m1 : free A1) k ko, step (Par m1 (@Fail A2) k ko) Fail | StepParNextLeft : ∀ {A1 A2} (m2 : free A2) k ko, step (Par (@Next A1) m2 k ko) (ko()) | StepParNextRight : ∀ {A1 A2} (m1 : free A1) k ko, step (Par m1 (@Next A2) k ko) (ko()) | StepParLeft : ∀ {A1 A2} (m1 m'1 : free A1) (m2 : free A2) k ko, step m1 m'1 → step (Par m1 m2 k ko) (Par m'1 m2 k ko) | StepParRight : ∀ {A1 A2} (m1 : free A1) {m2 m'2 : free A2} k ko, step m2 m'2 → step (Par m1 m2 k ko) (Par m1 m'2 k ko) . Definition can_step {A} (m : free A) := ∃ m', step m m'. Fixpoint initially_safe {A} (n : nat) (m : free A) (φ : A → Prop) : Prop := match n with | 0 => True | S n => (∃ v, m = Ret v ∧ φ v) ∨ ( can_step m ∧ (∀ m', step m m' → initially_safe n m' φ) ) end. Definition safe {A} (m : free A) (φ : A → Prop) := ∀ n, initially_safe n m φ. Lemma safe_covariant {A} (m : free A) (φ φ' : A → Prop) : safe m φ → (∀ a, φ a → φ' a) → safe m φ'. Admitted. Lemma prove_safe_ret {A} (a : A) (φ : A → Prop) : φ a → safe (ret a) φ. Admitted. Lemma prove_safe_bind {A B} (m1 : free A) (m2 : A → free B) (φ : B → Prop) : safe m1 (λ a, safe (m2 a) φ) → safe (bind m1 m2) φ. Admitted. Lemma prove_safe_stop {A} η e (k : val → free A) φ : safe (eval η e) (λ v, safe (k v) φ) → safe (Stop η e k) φ. Admitted. Lemma prove_safe_flip {A} (k : bool → free A) φ : (∀ b, safe (k b) φ) → safe (Flip k) φ. Admitted. Lemma prove_safe_par_ret_ret {A1 A2 A} a1 a2 (k : A1 * A2 → free A) ko φ : safe (k (a1, a2)) φ → safe (Par (Ret a1) (Ret a2) k ko) φ. Admitted. Lemma prove_safe_par {A1 A2 A} m1 m2 (k : A1 * A2 → free A) ko φ : ∀ φ1 φ2, safe m1 φ1 → safe m2 φ2 → (∀ v1 v2, φ1 v1 → φ2 v2 → safe (k (v1, v2)) φ) → safe (Par m1 m2 k ko) φ. Admitted. Lemma prove_safe_Par_ret_left {A1 A2 A} a1 m2 (k : A1 * A2 → free A) (φ : A → Prop) : safe m2 (λ v2, safe (k (a1, v2)) φ) → safe (Par (Ret a1) m2 k next) φ. Admitted. Lemma prove_safe_Par_ret_right {A1 A2 A} m1 a2 (k : A1 * A2 → free A) (φ : A → Prop) : safe m1 (λ v1, safe (k (v1, a2)) φ) → safe (Par m1 (Ret a2) k next) φ. Admitted. Definition wp η e φ := safe (eval η e) φ. Ltac wp_simplify := cbn. Ltac wp_intros := repeat match goal with | |- ∀ v, _ => intro | |- ?v = _ → _ => intro; try subst v end. Ltac wp_use H := first [ eapply H | eapply safe_covariant; [ eapply H |] ]; simpl; wp_intros. Ltac wp_scoped_case_analysis := match goal with |- safe (if ?b then Ret VUnit else _) _ => eapply safe_covariant with (φ := λ v, v = VUnit); [ destruct b; [ wp_step; apply eq_refl | idtac ] | wp_intros ] end with wp_step := first [ apply prove_safe_ret; wp_simplify | apply prove_safe_bind; wp_simplify | apply prove_safe_stop; wp_simplify | apply prove_safe_flip; intro; wp_simplify | apply prove_safe_par_ret_ret; wp_simplify | apply prove_safe_Par_ret_left; wp_simplify | apply prove_safe_Par_ret_right; wp_simplify | wp_scoped_case_analysis ]. Ltac wp_par := eapply prove_safe_par. Ltac wp := unfold wp; wp_simplify; repeat wp_step. Definition example3 := let idA := EApp (EVar "id") (EConstant "A") in EPair idA idA. Ltac wp_set_postcondition := match goal with |- ?φ ?v => is_evar φ; instantiate (1 := λ v', v' = v); reflexivity end. Lemma spec_example3: ∀ (id : val), (∀ v, safe (call id v) (λ v', v' = v)) → let env := EnvCons "id" id EnvNil in wp env example3 (λ v, v = VPair (VConstant "A") (VConstant "A")). Proof. intros id Hid. wp. wp_par. { wp. wp_use Hid. } { wp. wp_use Hid. wp. wp_set_postcondition. } simpl. ```

Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)

```coq ```

Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 15KiB file on GitHub Actions Artifacts under build.log)

``` 0.82.113.4|:443... connected. HTTP request sent, awaiting response... 302 Found Location: https://objects.githubusercontent.com/github-production-repository-file-5c1aeb/1377159/11050326?X-Amz-Algorithm=AWS4-HMAC-SHA256&X-Amz-Credential=AKIAIWNJYAX4CSVEH53A%2F20230323%2Fus-east-1%2Fs3%2Faws4_request&X-Amz-Date=20230323T132708Z&X-Amz-Expires=300&X-Amz-Signature=3c4636994a3f1127643ac47d82c8f5dd8d854323468e63c399968d587fd56bb1&X-Amz-SignedHeaders=host&actor_id=0&key_id=0&repo_id=1377159&response-content-disposition=attachment%3Bfilename%3Dbug2.tar.gz&response-content-type=application%2Fx-gzip [following] --2023-03-23 13:27:08-- https://objects.githubusercontent.com/github-production-repository-file-5c1aeb/1377159/11050326?X-Amz-Algorithm=AWS4-HMAC-SHA256&X-Amz-Credential=AKIAIWNJYAX4CSVEH53A%2F20230323%2Fus-east-1%2Fs3%2Faws4_request&X-Amz-Date=20230323T132708Z&X-Amz-Expires=300&X-Amz-Signature=3c4636994a3f1127643ac47d82c8f5dd8d854323468e63c399968d587fd56bb1&X-Amz-SignedHeaders=host&actor_id=0&key_id=0&repo_id=1377159&response-content-disposition=attachment%3Bfilename%3Dbug2.tar.gz&response-content-type=application%2Fx-gzip Resolving objects.githubusercontent.com (objects.githubusercontent.com)... 185.199.111.133, 185.199.109.133, 185.199.110.133, ... Connecting to objects.githubusercontent.com (objects.githubusercontent.com)|185.199.111.133|:443... connected. HTTP request sent, awaiting response... 200 OK Length: 17395 (17K) [application/x-gzip] Saving to: 'bug2.tar.gz' 0K .......... ...... 100% 27.8M=0.001s 2023-03-23 13:27:08 (27.8 MB/s) - 'bug2.tar.gz' saved [17395/17395] ++ (/github/workspace/run-script.sh @ line 5) $ tar -xf bug2.tar.gz ++ (/github/workspace/run-script.sh @ line 6) $ cd bug2 ++ (/github/workspace/run-script.sh @ line 7) $ make coq_makefile -f _CoqProject -o Makefile.coq MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/bug2 MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig --print-version MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.1HxdYn5rhC MINIMIZER_DEBUG: files: COQDEP VFILES MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/bug2 MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig --print-version MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.WkmZznITV2 MINIMIZER_DEBUG: files: MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/bug2 MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig --print-version MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.NS5hcVQS3g MINIMIZER_DEBUG: files: MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/bug2 MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig --print-version MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.cb2KeT7oaj MINIMIZER_DEBUG: files: COQC theories/base.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/bug2 MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig -q -w -deprecated-native-compiler-option -native-compiler no -R /github/workspace/bug2 AmpleStep theories/base.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.2noBK5LvMg MINIMIZER_DEBUG: files: theories/base.v COQC theories/lang.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/bug2 MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig -q -w -deprecated-native-compiler-option -native-compiler no -R /github/workspace/bug2 AmpleStep theories/lang.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.yqC5xwM9fv MINIMIZER_DEBUG: files: theories/lang.v COQC theories/free.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/bug2 MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig -q -w -deprecated-native-compiler-option -native-compiler no -R /github/workspace/bug2 AmpleStep theories/free.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.FcAFXVyMvs MINIMIZER_DEBUG: files: theories/free.v COQC theories/eval.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/bug2 MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig -q -w -deprecated-native-compiler-option -native-compiler no -R /github/workspace/bug2 AmpleStep theories/eval.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.iPizICrjMN MINIMIZER_DEBUG: files: theories/eval.v COQC theories/step.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/bug2 MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig -q -w -deprecated-native-compiler-option -native-compiler no -R /github/workspace/bug2 AmpleStep theories/step.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.L2OJrH132U MINIMIZER_DEBUG: files: theories/step.v COQC theories/steps.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/bug2 MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig -q -w -deprecated-native-compiler-option -native-compiler no -R /github/workspace/bug2 AmpleStep theories/steps.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.8AynsP2A71 MINIMIZER_DEBUG: files: theories/steps.v COQC theories/safe.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/bug2 MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig -q -w -deprecated-native-compiler-option -native-compiler no -R /github/workspace/bug2 AmpleStep theories/safe.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.1ROF7s5qs6 MINIMIZER_DEBUG: files: theories/safe.v COQC theories/wp.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/bug2 MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig -q -w -deprecated-native-compiler-option -native-compiler no -R /github/workspace/bug2 AmpleStep theories/wp.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.GQAmtXlL2E MINIMIZER_DEBUG: files: theories/wp.v COQC theories/wp_tactics.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/bug2 MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig -q -w -deprecated-native-compiler-option -native-compiler no -R /github/workspace/bug2 AmpleStep theories/wp_tactics.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.OtVhz8R3Be MINIMIZER_DEBUG: files: theories/wp_tactics.v COQC theories/examples.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/bug2 MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig -q -w -deprecated-native-compiler-option -native-compiler no -R /github/workspace/bug2 AmpleStep theories/examples.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.PxAJALAxOy MINIMIZER_DEBUG: files: theories/examples.v File "./theories/examples.v", line 71, characters 2-7: Error: Anomaly "Uncaught exception Not_found." Please report at http://coq.inria.fr/bugs/. make[1]: *** [Makefile.coq:793: theories/examples.vo] Error 1 make: *** [Makefile.coq:409: all] Error 2 ```

Minimization Log (truncated to last 8.0KiB; full 438KiB file on GitHub Actions Artifacts under bug.log)

``` : File "/tmp/tmpwzroryp2/AmpleStep/theories/examples.v", line 451, characters 9-16: Error: The reference wp_step was not found in the current environment. Intermediate code not saved. I will now attempt to remove unused definitions Non-fatal error: Failed to remove definitions and preserve the error. The new error was: File "/tmp/tmpoygsxfga/AmpleStep/theories/examples.v", line 29, characters 3-9: Error: The reference ETuple was not found in the current environment. Intermediate code not saved. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-fatal error: Failed to remove non-instance definitions and preserve the error. The new error was: File "/tmp/tmpfjzvsspy/AmpleStep/theories/examples.v", line 29, characters 3-9: Error: The reference ETuple was not found in the current environment. Intermediate code not saved. I will now attempt to remove unused variables  Variable removal successful. I will now attempt to remove unused contexts  Context removal successful. I will now attempt to replace Qed Obligation with Admit Obligations  Admitting Qed Obligations successful. Failed to do everything at once; trying one at a time. Admitting Qed Obligations unsuccessful. No successful changes. I will now attempt to replace Qeds with Admitteds  Admitting Qeds successful. Failed to do everything at once; trying one at a time. Admitting Qeds unsuccessful. No successful changes. I will now attempt to replace Qeds with admit. Defined.  Admitting Qeds successful. Failed to do everything at once; trying one at a time. Admitting Qeds unsuccessful. No successful changes. I will now attempt to remove goals ending in [Abort.]  Aborted removal successful. I will now attempt to remove unused Ltacs Non-fatal error: Failed to remove Ltac and preserve the error. The new error was: File "/tmp/tmpwzroryp2/AmpleStep/theories/examples.v", line 451, characters 9-16: Error: The reference wp_step was not found in the current environment. Intermediate code not saved. I will now attempt to remove unused definitions Non-fatal error: Failed to remove definitions and preserve the error. The new error was: File "/tmp/tmpoygsxfga/AmpleStep/theories/examples.v", line 29, characters 3-9: Error: The reference ETuple was not found in the current environment. Intermediate code not saved. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-fatal error: Failed to remove non-instance definitions and preserve the error. The new error was: File "/tmp/tmpfjzvsspy/AmpleStep/theories/examples.v", line 29, characters 3-9: Error: The reference ETuple was not found in the current environment. Intermediate code not saved. I will now attempt to remove unused variables  Variable removal successful. I will now attempt to remove unused contexts  Context removal successful. I will now attempt to admit [abstract ...]s  Admitting [abstract ...] successful.  Admitting [abstract ...] successful. Admitting [abstract ...] unsuccessful. Admitting [abstract ...] unsuccessful. I will now attempt to remove goals ending in [Abort.]  Aborted removal successful. I will now attempt to remove unused Ltacs Non-fatal error: Failed to remove Ltac and preserve the error. The new error was: File "/tmp/tmpwzroryp2/AmpleStep/theories/examples.v", line 451, characters 9-16: Error: The reference wp_step was not found in the current environment. Intermediate code not saved. I will now attempt to remove unused definitions Non-fatal error: Failed to remove definitions and preserve the error. The new error was: File "/tmp/tmpoygsxfga/AmpleStep/theories/examples.v", line 29, characters 3-9: Error: The reference ETuple was not found in the current environment. Intermediate code not saved. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-fatal error: Failed to remove non-instance definitions and preserve the error. The new error was: File "/tmp/tmpfjzvsspy/AmpleStep/theories/examples.v", line 29, characters 3-9: Error: The reference ETuple was not found in the current environment. Intermediate code not saved. I will now attempt to remove unused variables  Variable removal successful. I will now attempt to remove unused contexts  Context removal successful. I will now attempt to replace Obligation with Admit Obligations  Admitting Obligations successful. Failed to do everything at once; trying one at a time. Admitting Obligations unsuccessful. No successful changes. I will now attempt to admit lemmas with Admitted Non-fatal error: Failed to admit lemmas and preserve the error. The new error was: Intermediate code not saved. Failed to do everything at once; trying one at a time. Admitting lemmas unsuccessful. No successful changes. I will now attempt to admit definitions with Admitted Non-fatal error: Failed to admit definitions and preserve the error. The new error was: Intermediate code not saved. Failed to do everything at once; trying one at a time. Admitting definitions unsuccessful. No successful changes. I will now attempt to admit lemmas with admit. Defined Non-fatal error: Failed to admit lemmas and preserve the error. The new error was: File "/tmp/tmpw5ofrlyc/AmpleStep/theories/examples.v", line 495, characters 0-8: Error: (in proof spec_example3): Attempt to save a proof with given up goals. If this is really what you want to do, use Admitted in place of Qed. Intermediate code not saved. Failed to do everything at once; trying one at a time. Admitting lemmas unsuccessful. No successful changes. I will now attempt to admit definitions with admit. Defined Non-fatal error: Failed to admit definitions and preserve the error. The new error was: File "/tmp/tmp2b4ffb1d/AmpleStep/theories/examples.v", line 138, characters 0-8: Error: (in proof par): Attempt to save a proof with given up goals. If this is really what you want to do, use Admitted in place of Qed. Intermediate code not saved. Failed to do everything at once; trying one at a time. Admitting definitions unsuccessful. No successful changes. I will now attempt to export modules Module exportation unsuccessful. I will now attempt to split imports and exports Import/Export splitting unsuccessful. I will now attempt to split := definitions One-line definition splitting unsuccessful. I will now attempt to remove all lines, one at a time Line removal unsuccessful. I will now attempt to remove goals ending in [Abort.]  Aborted removal successful. I will now attempt to remove unused Ltacs Non-fatal error: Failed to remove Ltac and preserve the error. The new error was: File "/tmp/tmpwzroryp2/AmpleStep/theories/examples.v", line 451, characters 9-16: Error: The reference wp_step was not found in the current environment. Intermediate code not saved. I will now attempt to remove unused definitions Non-fatal error: Failed to remove definitions and preserve the error. The new error was: File "/tmp/tmpoygsxfga/AmpleStep/theories/examples.v", line 29, characters 3-9: Error: The reference ETuple was not found in the current environment. Intermediate code not saved. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-fatal error: Failed to remove non-instance definitions and preserve the error. The new error was: File "/tmp/tmpfjzvsspy/AmpleStep/theories/examples.v", line 29, characters 3-9: Error: The reference ETuple was not found in the current environment. Intermediate code not saved. I will now attempt to remove unused variables  Variable removal successful. I will now attempt to remove unused contexts  Context removal successful. I will now attempt to remove empty sections No empty sections to remove. Now, I will attempt to strip repeated newlines and trailing spaces from this file... No strippable newlines or spaces. ```

If you have any comments on your experience of the minimizer, please share them in a reply (possibly tagging @JasonGross). If you believe there's a bug in the bug minimizer, please report it on the bug minimizer issue tracker.

[SkySkimmer]

The instantiate in

Ltac wp_set_postcondition :=
  match goal with |- ?φ ?v =>
    is_evar φ;
    instantiate (1 := λ v', v' = v);
    reflexivity
  end.

is combining with https://github.com/coq/coq/issues?q=label%3A%22wellknown%3A+ltac+variable+bypasses+typechecking%22