Draft
Conversation
coqbot-app
bot
added
the
needs: full CI
Contributor
Author
|
@coqbot run full ci |
coqbot-app
bot
removed
the
needs: full CI
thomas-lamiaux
force-pushed
the
filePrelude
branch
from
94801ea to
deb5e51
Compare
coqbot-app
bot
added
the
needs: full CI
thomas-lamiaux
force-pushed
the
filePrelude
branch
2 times, most recently
from
7c4d7a9 to
1b90beb
Compare
Contributor
Author
|
@coqbot run full ci |
coqbot-app
bot
removed
the
needs: full CI
Contributor
Author
|
@coqbot ci minimize ci-iris |
Contributor
|
I am now running minimization at commit 1b90beb on requested target ci-iris. I'll come back to you with the results once it's done. |
Contributor
|
Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/builds/coq/coq-failing/_build_ci/iris/iris/program_logic/adequacy.v in 2h 57m 11s (from ci-iris) (full log on GitHub Actions - verbose log) 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" "-notation-overridden" "-w" "-redundant-canonical-projection" "-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" "-coqlib" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq//" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/iris/iris" "iris" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/iris/iris_heap_lang" "iris.heap_lang" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/iris/iris_unstable" "iris.unstable" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/iris/iris_deprecated" "iris.deprecated" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Autosubst" "Autosubst" "-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/Stdlib" "Stdlib" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/stdpp" "stdpp" "-top" "iris.program_logic.adequacy") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 396 lines to 14 lines, then from 28 lines to 918 lines, then from 925 lines to 14 lines, then from 28 lines to 631 lines, then from 638 lines to 73 lines, then from 87 lines to 604 lines, then from 611 lines to 76 lines, then from 90 lines to 2716 lines, then from 2723 lines to 89 lines, then from 103 lines to 353 lines, then from 360 lines to 101 lines, then from 115 lines to 369 lines, then from 376 lines to 107 lines, then from 121 lines to 375 lines, then from 382 lines to 116 lines, then from 130 lines to 939 lines, then from 946 lines to 147 lines, then from 161 lines to 1838 lines, then from 1840 lines to 149 lines, then from 163 lines to 432 lines, then from 439 lines to 162 lines, then from 176 lines to 1257 lines, then from 1262 lines to 171 lines, then from 185 lines to 552 lines, then from 559 lines to 183 lines, then from 197 lines to 336 lines, then from 343 lines to 192 lines, then from 206 lines to 1948 lines, then from 1951 lines to 232 lines, then from 246 lines to 4379 lines, then from 4359 lines to 247 lines, then from 261 lines to 298 lines, then from 305 lines to 257 lines, then from 271 lines to 316 lines, then from 321 lines to 274 lines, then from 288 lines to 302 lines, then from 309 lines to 286 lines, then from 300 lines to 314 lines, then from 321 lines to 299 lines, then from 314 lines to 301 lines, then from 316 lines to 99 lines, then from 114 lines to 99 lines *)
(* coqc version 9.2+alpha compiled with OCaml 4.14.2
coqtop version 9.2+alpha
Expected coqc runtime on this file: 0.137 sec
Expected coqc peak memory usage on this file: 607784.0 kb *)
Require Corelib.Setoids.Setoid.
Require Corelib.Lists.ListDef.
Export Corelib.Lists.ListDef.
Export Corelib.Setoids.Setoid.
Notation "∃ x .. y , P" := (exists x, .. (exists y, P) ..)
(at level 10, x binder, y binder, P at level 200,
format "'[ ' '[ ' ∃ x .. y ']' , '/' P ']'") : type_scope.
Notation "x ∨ y" := (x \/ y) (at level 85, right associativity) : type_scope.
Notation "x → y" := (x -> y)
(at level 99, y at level 200, right associativity): type_scope.
Notation "[ x ]" := (cons x nil) : list_scope.
Global Generalizable All Variables.
Declare Scope stdpp_scope.
Global Open Scope stdpp_scope.
Definition is_Some {A} (mx : option A) := ∃ x, mx = Some x.
Class ElemOf A B := elem_of: A → B → Prop.
Infix "∈" := elem_of (at level 70) : stdpp_scope.
Inductive list_elem_of {A} : ElemOf A (list A) :=
| list_elem_of_here (x : A) l : x ∈ x :: l
| list_elem_of_further (x y : A) l : x ∈ l → x ∈ y :: l.
Global Existing Instance list_elem_of.
Section definitions.
Context `(R : relation A).
Inductive rtc : relation A :=
| rtc_refl x : rtc x x
| rtc_l x y z : R x y → rtc y z → rtc x z.
End definitions.
Inductive stuckness := NotStuck | MaybeStuck.
Section language_mixin.
Context {expr val state observation : Type}.
Context (of_val : val → expr).
Context (to_val : expr → option val).
Context (prim_step : expr → state → list observation → expr → state → list expr → Prop).
Record LanguageMixin := {
mixin_to_of_val v : to_val (of_val v) = Some v;
mixin_of_to_val e v : to_val e = Some v → of_val v = e;
mixin_val_stuck e σ κ e' σ' efs : prim_step e σ κ e' σ' efs → to_val e = None
}.
End language_mixin.
Structure language := Language {
expr : Type;
val : Type;
state : Type;
observation : Type;
of_val : val → expr;
to_val : expr → option val;
prim_step : expr → state → list observation → expr → state → list expr → Prop;
language_mixin : LanguageMixin of_val to_val prim_step
}.
Global Arguments of_val {_} _.
Global Arguments to_val {_} _.
Global Arguments prim_step {_} _ _ _ _ _ _.
Definition cfg (Λ : language) := (list (expr Λ) * state Λ)%type.
Section language.
Context {Λ : language}.
Definition reducible (e : expr Λ) (σ : state Λ) :=
∃ κ e' σ' efs, prim_step e σ κ e' σ' efs.
Definition not_stuck (e : expr Λ) (σ : state Λ) :=
is_Some (to_val e) ∨ reducible e σ.
Inductive step (ρ1 : cfg Λ) (κ : list (observation Λ)) (ρ2 : cfg Λ) : Prop :=
| step_atomic e1 σ1 e2 σ2 efs t1 t2 :
ρ1 = (t1 ++ e1 :: t2, σ1) →
ρ2 = (t1 ++ e2 :: t2 ++ efs, σ2) →
prim_step e1 σ1 κ e2 σ2 efs →
step ρ1 κ ρ2.
Definition erased_step (ρ1 ρ2 : cfg Λ) := ∃ κ, step ρ1 κ ρ2.
End language.
Record adequate {Λ} (s : stuckness) (e1 : expr Λ) (σ1 : state Λ)
(φ : val Λ → state Λ → Prop) := {
adequate_result t2 σ2 v2 :
rtc erased_step ([e1], σ1) (of_val v2 :: t2, σ2) → φ v2 σ2;
adequate_not_stuck t2 σ2 e2 :
s = NotStuck →
rtc erased_step ([e1], σ1) (t2, σ2) →
e2 ∈ t2 → not_stuck e2 σ2
}.🛠️ Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)🛠️ 📜 Intermediate Coq File log (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 6.9MiB file on GitHub Actions Artifacts under
|
Contributor
Author
|
Fixed in #21429 |
thomas-lamiaux
force-pushed
the
filePrelude
branch
from
1b90beb to
949c5e3
Compare
coqbot-app
bot
added
the
needs: full CI
Contributor
Author
|
@coqbot run full ci |
coqbot-app
bot
removed
the
needs: full CI
Contributor
Author
|
MWE math-classes |
thomas-lamiaux
force-pushed
the
filePrelude
branch
from
949c5e3 to
c95a22f
Compare
coqbot-app
bot
added
the
needs: full CI
Contributor
Author
|
@coqbot run full ci |
coqbot-app
bot
added
needs: full CI
thomas-lamiaux
force-pushed
the
filePrelude
branch
from
31b017a to
164357e
Compare
Contributor
Author
|
@coqbot run full ci |
coqbot-app
bot
removed
the
needs: full CI
thomas-lamiaux
force-pushed
the
filePrelude
branch
from
164357e to
eab27bc
Compare
coqbot-app
bot
added
the
needs: full CI
4 tasks
github-actions
bot
added
the
needs: rebase
thomas-lamiaux
force-pushed
the
filePrelude
branch
from
eab27bc to
53f8bb4
Compare
coqbot-app
bot
removed
the
needs: rebase
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
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.
Fixes / closes #????
make doc_gram_rsts.