Let with Qed: produce really-Qed side definition #17576
Merged
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
coqbot-app
bot
added
the
needs: full CI
|
@coqbot run full ci |
coqbot-app
bot
removed
the
needs: full CI
|
@coqbot bench |
|
NB: when univ monomorphic we could support async / vos for these proofs AFAICT (the current code forces the body but at least in principle we could stop doing that) |
|
🏁 Bench results: INFO: failed to install coq-iris-examples 🐢 Top 25 slow downs🐇 Top 25 speed ups |
|
@coqbot ci minimize ci-iris |
|
I am now running minimization at commit d185ff1 on requested target ci-iris. I'll come back to you with the results once it's done. |
|
Minimized File /github/workspace/builds/coq/coq-failing/_build_ci/iris/iris/algebra/ofe.v (from ci-iris) (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" "-notation-overridden" "-w" "-redundant-canonical-projection" "-w" "-future-coercion-class-field" "-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/iris/iris/prelude" "iris.prelude" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/iris/iris/algebra" "iris.algebra" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/iris/iris/si_logic" "iris.si_logic" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/iris/iris/bi" "iris.bi" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/iris/iris/proofmode" "iris.proofmode" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/iris/iris/base_logic" "iris.base_logic" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/iris/iris/program_logic" "iris.program_logic" "-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/stdpp" "stdpp" "-top" "iris.algebra.ofe") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 1931 lines to 33 lines, then from 46 lines to 107 lines, then from 112 lines to 34 lines, then from 47 lines to 112 lines, then from 117 lines to 34 lines, then from 47 lines to 111 lines, then from 116 lines to 34 lines, then from 47 lines to 1625 lines, then from 1626 lines to 47 lines, then from 60 lines to 93 lines, then from 98 lines to 46 lines, then from 51 lines to 46 lines *)
(* coqc version 8.18+alpha compiled with OCaml 4.14.1
coqtop version runner-zseo-lx5-project-6138686-concurrent-0:/builds/coq/coq/_build/default,(HEAD detached at a3534d472d) (a3534d472d952ca4b560c3e82043b36c11fa47bf)
Expected coqc runtime on this file: 0.203 sec *)
Require Coq.Lists.List.
Require Coq.Unicode.Utf8.
Export Set Default Proof Using "Type".
Export Coq.Classes.Morphisms.
Export Coq.Setoids.Setoid.
Export Coq.Unicode.Utf8.
Global Generalizable All Variables.
Declare Scope stdpp_scope.
Global Open Scope stdpp_scope.
Class Equiv A := equiv: relation A.
Infix "≡" := equiv (at level 70, no associativity) : stdpp_scope.
Class Dist A := dist : nat → relation A.
Notation "x ≡{ n }≡ y" := (dist n x y)
(at level 70, n at next level, format "x ≡{ n }≡ y").
Notation NonExpansive f := (∀ n, Proper (dist n ==> dist n) f).
Record OfeMixin A `{Equiv A, Dist A} := {
mixin_equiv_dist (x y : A) : x ≡ y ↔ ∀ n, x ≡{n}≡ y;
mixin_dist_equivalence n : Equivalence (@dist A _ n);
mixin_dist_lt n m (x y : A) : x ≡{n}≡ y → m < n → x ≡{m}≡ y;
}.
Structure ofe := Ofe {
ofe_car :> Type;
ofe_equiv : Equiv ofe_car;
ofe_dist : Dist ofe_car;
ofe_mixin : OfeMixin ofe_car
}.
Global Hint Extern 0 (Dist _) => refine (ofe_dist _); shelve : typeclass_instances.
Section iso_cofe_subtype.
Context {A B : ofe} `{Cofe A} (P : A → Prop) (f : ∀ x, P x → B) (g : B → A).
Context (g_dist : ∀ n y1 y2, y1 ≡{n}≡ y2 ↔ g y1 ≡{n}≡ g y2).
Let Hgne : NonExpansive g.
Proof.
intros n y1 y2.
apply g_dist.
Qed.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.8MiB file on GitHub Actions Artifacts under
|
|
I'm wondering if in the end the best solution would be to have an attribute that controls when something is added to the named environment? |
|
I don't understand what you mean. |
I mean that the operation of defining a constant vs adding it to the section environment (main use of So instead of: Let foo : T. Proof. ... Qed.we could have Lemma foo : T. Proof. ... Qed.
Add Named Variable foo. |
|
Is that different from Section S.
Definition foo := 0. (* or any other definition / tactic proof *)
Let foo := foo.which can be done in master? |
SkySkimmer
added
the
request: full CI
coqbot-app
bot
removed
the
request: full CI
|
The 10% speedup on odd-order is impressive. |
SkySkimmer
added
the
request: full CI
coqbot-app
bot
removed
the
request: full CI
|
@coqbot bench |
|
🏁 Bench results: INFO: failed to install coq-coquelicot 🐢 Top 25 slow downs🐇 Top 25 speed ups |
|
@ejgallego you didn't answer #17576 (comment) |
Yes I didn't have time to look at what is going there in detail, it is in my todo list tho. |
github-actions
bot
added
the
needs: rebase
|
The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed. |
|
This PR was not rebased after 30 days despite the warning, it is now closed. |
coqbot-app
bot
removed
the
request: full CI
|
@coqbot merge now |
|
@proux01: Please take care of the following overlays:
|
ppedrot
added a commit
to MetaCoq/metacoq
that referenced
this pull request
Nov 4, 2023
Adapt to coq/coq#17576 (declare_variable takes typing flags argument)
|
FYI @proux01, given this merge makes coq.dev incompatible with previous releases of math-comp (2.1.0 and 1.8.0), |
erikmd
added a commit
to math-comp/docker-mathcomp
that referenced
this pull request
Nov 4, 2023
|
Indeed, thanks @erikmd I forgot that point |
|
@proux01 seems like you forgot fiat crypto legacy |
|
I'm not sure in which state it is since it was already broken. |
SkySkimmer
added a commit
to SkySkimmer/fiat-crypto
that referenced
this pull request
Nov 6, 2023
|
Thanks |
JasonGross
pushed a commit
to SkySkimmer/fiat-crypto
that referenced
this pull request
Nov 6, 2023
JasonGross
pushed a commit
to mit-plv/fiat-crypto
that referenced
this pull request
Nov 6, 2023
proux01
added a commit
to coq-community/graph-theory
that referenced
this pull request
Nov 7, 2023
palmskog
added a commit
to coq-community/graph-theory
that referenced
this pull request
Nov 7, 2023
proux01
added a commit
to proux01/coq
that referenced
this pull request
Jan 30, 2024
proux01
added a commit
to proux01/coq
that referenced
this pull request
Feb 8, 2024
coqbot-app bot
added a commit
that referenced
this pull request
Feb 9, 2024
Reviewed-by: jfehrle Ack-by: SkySkimmer Co-authored-by: jfehrle <jfehrle@users.noreply.github.com>
6 tasks
louiseddp
pushed a commit
to louiseddp/coq
that referenced
this pull request
Feb 27, 2024
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.
cf discussion in #17544
This does have a tradeoff as the side definition still exists after the section is closed unlike usual.
Overlays:
To be merged before the PR
To be merged in sync