A common execution path for universe restriction + universe declaration check - #19031
Merged
coqbot-app[bot] merged 3 commits intoSep 5, 2024
Conversation
herbelin
added
kind: cleanup
coqbot-app
Bot
added
the
needs: full CI
github-actions
Bot
added
the
needs: rebase
herbelin
added
the
request: full CI
herbelin
force-pushed
the
master+factorization-make-univs-declare.ml
branch
from
May 20, 2024 12:41
836d873 to
384653c
Compare
coqbot-app
Bot
removed
needs: rebase
herbelin
added
the
request: full CI
herbelin
force-pushed
the
master+factorization-make-univs-declare.ml
branch
from
May 21, 2024 19:49
384653c to
c975015
Compare
coqbot-app
Bot
removed
the
request: full CI
herbelin
marked this pull request as ready for review
May 21, 2024 19:49
github-actions
Bot
added
the
needs: rebase
herbelin
force-pushed
the
master+factorization-make-univs-declare.ml
branch
from
May 26, 2024 08:53
c975015 to
fbde001
Compare
coqbot-app
Bot
added
needs: full CI
github-actions
Bot
added
the
needs: rebase
proux01
removed
the
needs: merge of dependency
Contributor
|
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. |
herbelin
changed the title
herbelin
added
the
request: full CI
herbelin
force-pushed
the
master+factorization-make-univs-declare.ml
branch
from
June 29, 2024 15:22
fbde001 to
f626d99
Compare
coqbot-app
Bot
removed
the
needs: rebase
github-actions
Bot
added
the
needs: rebase
herbelin
added
the
request: full CI
herbelin
force-pushed
the
master+factorization-make-univs-declare.ml
branch
from
July 23, 2024 07:42
29dfdca to
ad41be4
Compare
coqbot-app
Bot
removed
needs: rebase
Contributor
|
🔴 CI failure at commit ad41be4 without any failure in the test-suite ✔️ Corresponding job for the base commit 43402d4 succeeded ❔ Ask me to try to extract a minimal test case that can be added to the test-suite 🏃
|
Contributor
|
@coqbot ci minimize |
Contributor
|
I have initiated minimization at commit ad41be4 for the suggested target ci-category_theory as requested. |
Contributor
|
Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/builds/coq/coq-failing/_build_ci/category_theory/Lib/MapDecide.v (from ci-category_theory) (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" "-deprecated-native-compiler-option" "-native-compiler" "no" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/category_theory" "Category" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Equations" "Equations" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "Category.Lib.MapDecide") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 623 lines to 153 lines, then from 166 lines to 1050 lines, then from 1055 lines to 178 lines, then from 191 lines to 221 lines, then from 226 lines to 187 lines, then from 200 lines to 540 lines, then from 545 lines to 187 lines, then from 200 lines to 338 lines, then from 343 lines to 186 lines, then from 199 lines to 295 lines, then from 300 lines to 186 lines, then from 199 lines to 273 lines, then from 278 lines to 184 lines, then from 189 lines to 186 lines *)
(* coqc version 8.21+alpha compiled with OCaml 4.09.0
coqtop version runner-t7b1znuaq-project-4504-concurrent-0:/builds/coq/coq/_build/default,(HEAD detached at 14d8c90519eb69) (14d8c90519eb6969fe87f3a9232e07b074dd7387)
Expected coqc runtime on this file: 0.468 sec *)
Require Coq.FSets.FMaps.
Require Coq.Program.Program.
Axiom proof_admitted : False.
Tactic Notation "admit" := abstract case proof_admitted.
Declare Scope category_theory_scope.
Open Scope category_theory_scope.
Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
(at level 200, x binder, y binder, right associativity) :
category_theory_scope.
Notation "x → y" := (x -> y)
(at level 99, y at level 200, right associativity): category_theory_scope.
Notation "x ≠ y" := (x <> y) (at level 70) : category_theory_scope.
Module Export Category_DOT_Lib_WRAPPED.
Module Export Lib.
#[export] Set Universe Polymorphism.
#[export] Set Uniform Inductive Parameters.
#[export] Unset Universe Minimization ToSet.
End Lib.
End Category_DOT_Lib_WRAPPED.
Module Export Category_DOT_Lib_DOT_FMapExt_WRAPPED.
Module Export FMapExt.
Import Coq.FSets.FMapFacts.
Module FMapExt (E : DecidableType) (M : WSfun E).
Module P := WProperties_fun E M.
Module F := P.F.
#[export] Hint Extern 5 =>
match goal with
[ H : M.MapsTo _ _ (M.empty _) |- _ ] =>
apply F.empty_mapsto_iff in H; contradiction
end : core.
End FMapExt.
End FMapExt.
End Category_DOT_Lib_DOT_FMapExt_WRAPPED.
Module Export Lib.
Module Export FMapExt.
Include Category_DOT_Lib_DOT_FMapExt_WRAPPED.FMapExt.
End FMapExt.
End Lib.
Import Coq.NArith.NArith.
Import Coq.FSets.FMaps.
Module PO := PairOrderedType N_as_OT N_as_OT.
Module M := FMapList.Make(PO).
Module Import FMapExt := FMapExt PO M.
Inductive partial (P : Prop) : Set :=
| Proved : P → partial
| Uncertain : partial.
Notation "[ P ]" := (partial P) : type_scope.
Notation "'Yes'" := (Proved _ _) : partial_scope.
Notation "'No'" := (Uncertain _) : partial_scope.
#[local] Open Scope partial_scope.
Notation "'Reduce' v" := (if v then Yes else No) (at level 100) : partial_scope.
Notation "x && y" := (if x then Reduce y else No) : partial_scope.
Record environment : Set := {
vars : positive → N
}.
Inductive term : Set :=
| Var : positive → term
| Value : N → term.
Program Definition term_eq_dec (x y : term) : {x = y} + {x ≠ y} :=
match x, y with
| Var x, Var y => if Pos.eq_dec x y then left _ else right _
| Value x, Value y => if N.eq_dec x y then left _ else right _
| _, _ => right _
end.
Definition subst_all {A} (f : A → term → term → A) :
A → list (term * term) → A.
exact (fold_right (fun '(v, v') rest => f rest v v')).
Defined.
Definition term_denote env (x : term) : N :=
match x with
| Var n => vars env n
| Value n => n
end.
Inductive map_expr : Set :=
| Empty : map_expr
| Add : term → term → term → map_expr → map_expr.
Fixpoint map_expr_denote env (m : map_expr) : M.t N :=
match m with
| Empty => M.empty N
| Add x y f m' => M.add (term_denote env x, term_denote env y)
(term_denote env f) (map_expr_denote env m')
end.
Inductive formula : Set :=
| Top : formula
| Bottom : formula
| Maps : term → term → term → map_expr → formula
| Impl : formula → formula → formula.
Fixpoint subst_formula (t : formula) (v v' : term) : formula.
Admitted.
Fixpoint formula_denote env (t : formula) : Prop :=
match t with
| Top => True
| Bottom => False
| Maps x y f m =>
M.MapsTo (term_denote env x, term_denote env y)
(term_denote env f) (map_expr_denote env m)
| Impl p q => formula_denote env p → formula_denote env q
end.
Fixpoint formula_size (t : formula) : nat.
Admitted.
Fixpoint substitutions (xs : list (term * term)) : list (term * term).
Admitted.
Fixpoint remove_conflicts (x y f : term) (m : map_expr) : map_expr.
Admitted.
Import ListNotations.
Program Definition formula_forward (t : formula) env (hyp : formula)
(cont : ∀ env' defs,
[formula_denote env' (subst_all subst_formula t defs)]) :
[formula_denote env hyp → formula_denote env t] :=
match hyp with
| Top => Reduce (cont env [])
| Bottom => Yes
| Maps x y f m =>
let fix go n : [formula_denote env (Maps x y f n)
→ formula_denote env t] :=
match n with
| Empty => Yes
| Add x' y' f' m' =>
cont env (substitutions [(x, x'); (y, y'); (f, f')]) && go m'
end in Reduce (go (remove_conflicts x y f m))
| Impl _ _ => Reduce (cont env [])
end.
Next Obligation.
Admitted.
Next Obligation.
admit.
Defined.
Admit Obligations.
Fixpoint map_contains env (x y : N) (m : map_expr) : option term :=
match m with
| Empty => None
| Add x' y' f' m' =>
if (N.eqb x (term_denote env x') &&
N.eqb y (term_denote env y'))%bool
then Some f'
else map_contains env x y m'
end.
Program Fixpoint formula_backward (t : formula) env {measure (formula_size t)} :
[formula_denote env t] :=
match t with
| Top => Yes
| Bottom => No
| Maps x y f m =>
match map_contains env (term_denote env x) (term_denote env y) m with
| Some f' => Reduce (term_eq_dec f' f)
| None => No
end
| Impl p q =>
formula_forward q env p
(fun env' defs' => formula_backward (subst_all subst_formula q defs') env')
end.
Admit Obligations.🛠️ 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 3.0MiB file on GitHub Actions Artifacts under
|
Member
Author
|
The category_theory failure is due to the hook receiving the unrestricted uctx instead of the restricted one (in |
github-actions
Bot
added
the
needs: rebase
herbelin
added
the
request: full CI
herbelin
force-pushed
the
master+factorization-make-univs-declare.ml
branch
from
July 26, 2024 12:26
ad41be4 to
db327ce
Compare
coqbot-app
Bot
removed
needs: rebase
…efinitions and fixpoints. Note: That would require a "sealed" attribute to be observed (as in CEP rocq-prover#42).
herbelin
added
the
request: full CI
herbelin
force-pushed
the
master+factorization-make-univs-declare.ml
branch
from
July 26, 2024 13:56
db327ce to
832aeb9
Compare
coqbot-app
Bot
removed
the
request: full CI
Member
Author
|
I fixed the ustate for the hook in |
Member
Author
|
This PR is a priori ready. Looking for a reviewer. |
Contributor
|
@coqbot merge now |
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
3 participants
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.
The PR redirects the calls to
UState.restricton definitions/theorems/fixpoints indeclare.mltowards a reusable encapsulationmake_univsof the three functions used to build monomorphic deferred, polymorphic private or regular universe restrictions (still to be done for obligations, Derive, Equations though).In addtion to the centralization, it ensures that
Set Private Universesis used when defining an opaque polymorphic non-interactive definition or fixpoint (so assuming that asealedattribute is available).Depends on:
Theorem withmore flexible + code cleanup #18743