Skip to content

Support Coq 8.20 #258

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
4ever2 merged 10 commits into from
Jan 21, 2025
Merged

Support Coq 8.20 #258

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
13313e9
Update opam dependencies
4ever2 Jan 20, 2025
e3555b6
Update coq-nix-toolbox
4ever2 Jan 20, 2025
d82c2b5
Add Coq 8.20 Nix bundle
4ever2 Jan 20, 2025
092f197
Compatible with Coq 8.20
4ever2 Jan 20, 2025
2d118de
Add concurrency grups to nix workflows
4ever2 Jan 20, 2025
a1a9105
Don't run nix workflow for non Nix/Coq related changes
4ever2 Jan 20, 2025
bbb75f1
no message
4ever2 Jan 20, 2025
fd940f4
Fix warnings
4ever2 Jan 20, 2025
4ac01e6
Fix Nix workflows
4ever2 Jan 21, 2025
f47d004
Remove 8.19 Nix bundle
4ever2 Jan 21, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
37 changes: 19 additions & 18 deletions .github/coq-concert.opam.locked
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,28 +10,29 @@ homepage: "https://github.com/AU-COBRA/ConCert"
doc: "https://au-cobra.github.io/ConCert/toc.html"
bug-reports: "https://github.com/AU-COBRA/ConCert/issues"
depends: [
"coq" {= "8.19.0"}
"coq-bignums" {= "9.0.0+coq8.19"}
"coq-metacoq-common" {= "1.3.2+8.19"}
"coq-metacoq-erasure" {= "1.3.2+8.19"}
"coq-metacoq-pcuic" {= "1.3.2+8.19"}
"coq-metacoq-safechecker" {= "1.3.2+8.19"}
"coq-metacoq-template" {= "1.3.2+8.19"}
"coq-metacoq-template-pcuic" {= "1.3.2+8.19"}
"coq-metacoq-utils" {= "1.3.2+8.19"}
"coq-rust-extraction" {= "0.1.0"}
"coq" {= "8.20.0"}
"coq-bignums" {= "9.0.0+coq8.20"}
"coq-metacoq-common" {= "1.3.2+8.20"}
"coq-metacoq-erasure" {= "1.3.2+8.20"}
"coq-metacoq-pcuic" {= "1.3.2+8.20"}
"coq-metacoq-safechecker" {= "1.3.2+8.20"}
"coq-metacoq-template" {= "1.3.2+8.20"}
"coq-metacoq-template-pcuic" {= "1.3.2+8.20"}
"coq-metacoq-utils" {= "1.3.2+8.20"}
"coq-rust-extraction" {= "dev"}
"coq-elm-extraction" {= "0.1.0"}
"coq-quickchick" {= "2.0.4"}
"coq-stdpp" {= "1.10.0"}
"coq-stdpp" {= "1.11.0"}
]
pin-depends: [
["coq-metacoq-utils.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
["coq-metacoq-common.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
["coq-metacoq-template.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
["coq-metacoq-template-pcuic.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
["coq-metacoq-pcuic.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
["coq-metacoq-safechecker.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
["coq-metacoq-erasure.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
["coq-metacoq-utils.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
["coq-metacoq-common.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
["coq-metacoq-template.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
["coq-metacoq-template-pcuic.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
["coq-metacoq-pcuic.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
["coq-metacoq-safechecker.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
["coq-metacoq-erasure.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
["coq-rust-extraction.dev" "git+https://github.com/AU-COBRA/coq-rust-extraction.git#c5d9cbae417213fe25b42f08678f28507cc6b99e"]
]
build: [
[make "core"]
Expand Down
188 changes: 120 additions & 68 deletions .github/workflows/nix-action-8.19.yml → .github/workflows/nix-action-8.20.yml
View file
Open in desktop

Large diffs are not rendered by default.

12 changes: 6 additions & 6 deletions .nix/config.nix
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,14 +6,14 @@

attribute = "ConCert";

default-bundle = "8.19";
default-bundle = "8.20";

bundles."8.19" = {
coqPackages.coq.override.version = "8.19";
coqPackages.metacoq.override.version = "coq-8.19";
coqPackages.stdpp.override.version = "1.10.0";
bundles."8.20" = {
coqPackages.coq.override.version = "8.20";
coqPackages.metacoq.override.version = "coq-8.20";
coqPackages.stdpp.override.version = "1.11.0";
coqPackages.QuickChick.override.version = "2.0.4";
coqPackages.RustExtraction.override.version = "0.1.0";
coqPackages.RustExtraction.override.version = "coq-8.20";
coqPackages.ElmExtraction.override.version = "0.1.0";
};

Expand Down
2 changes: 1 addition & 1 deletion .nix/coq-nix-toolbox.nix
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
"a24e6f4fb01d4ca0811dc8d16246cfe36b37ac52"
"78d95509824be9e3339c1c0ee19f9c085f32b23e"
2 changes: 1 addition & 1 deletion Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
all: utils execution embedding extraction examples
all: core examples
.PHONY: all

core: utils execution embedding extraction
Expand Down
21 changes: 11 additions & 10 deletions coq-concert.opam
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ bug-reports: "https://github.com/AU-COBRA/ConCert/issues"
doc: "https://au-cobra.github.io/ConCert/toc.html"

depends: [
"coq" {>= "8.19" & < "8.20~"}
"coq" {>= "8.20" & < "8.21~"}
"coq-bignums" {>= "8"}
"coq-quickchick" {>= "2.0.4"}
"coq-metacoq-utils" {>= "1.3.1" & < "1.4~"}
Expand All @@ -24,19 +24,20 @@ depends: [
"coq-metacoq-pcuic" {>= "1.3.1" & < "1.4~"}
"coq-metacoq-safechecker" {>= "1.3.1" & < "1.4~"}
"coq-metacoq-erasure" {>= "1.3.1" & < "1.4~"}
"coq-rust-extraction" {= "0.1.0"}
"coq-rust-extraction" {= "dev"}
"coq-elm-extraction" {= "0.1.0"}
"coq-stdpp" {>= "1.9.0" & < "1.11~"}
"coq-stdpp" {>= "1.10.0" & < "1.12~"}
]

pin-depends: [
["coq-metacoq-utils.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
["coq-metacoq-common.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
["coq-metacoq-template.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
["coq-metacoq-template-pcuic.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
["coq-metacoq-pcuic.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
["coq-metacoq-safechecker.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
["coq-metacoq-erasure.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
["coq-metacoq-utils.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
["coq-metacoq-common.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
["coq-metacoq-template.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
["coq-metacoq-template-pcuic.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
["coq-metacoq-pcuic.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
["coq-metacoq-safechecker.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
["coq-metacoq-erasure.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
["coq-rust-extraction.dev" "git+https://github.com/AU-COBRA/coq-rust-extraction.git#c5d9cbae417213fe25b42f08678f28507cc6b99e"]
]

build: [
Expand Down
1 change: 1 addition & 0 deletions embedding/theories/EvalE.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ From ConCert.Utils Require Import Env.
but (as actually comment in the [monad_utils] says, we
should use a real monad library) *)
(* We need some definitions like [All] from utils *)
#[warnings="-notation-incompatible-prefix"]
From MetaCoq.Utils Require Import utils.

From Coq Require Import String.
Expand Down
2 changes: 1 addition & 1 deletion embedding/theories/Misc.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -94,7 +94,7 @@ Section CombineProp.
+ simpl. intros l1 Heq. destruct l1; eauto.
simpl; destruct (rev l1 ++ [a]); reflexivity.
+ simpl. intros l1 Heq. destruct l1 using rev_ind; auto.
repeat rewrite app_length in Heq; simpl in *.
repeat rewrite length_app in Heq; simpl in *.
assert (#|l1| = #|l2|) by lia.
repeat rewrite rev_unit. simpl.
rewrite IHl2 by auto.
Expand Down
1 change: 1 addition & 0 deletions embedding/theories/TranslationUtils.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ From ConCert.Embedding Require Utils.
From ConCert.Embedding Require Import PCUICTranslate.
From ConCert.Embedding Require Import PCUICtoTemplate.
From ConCert.Utils Require Import Env.
#[warnings="-notation-incompatible-prefix"]
From MetaCoq.Template Require Import All.

From Coq Require Import String.
Expand Down
67 changes: 35 additions & 32 deletions embedding/theories/pcuic/PCUICCorrectness.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,9 @@ Hint Resolve assumption_context_subst
assumption_context_map_vass
PCUICSigmaCalculus.context_assumptions_context : hints.

#[local]
Arguments monad_utils.bind /.

(** Soundness (In the paper: Theorem 1) *)
Theorem expr_to_term_sound (n : nat) (ρ : env val) Σ1 Σ2
(e1 e2 : expr) (v : val) :
Expand Down Expand Up @@ -92,7 +95,7 @@ Proof.
assert (ty_expr_env_ok (exprs ρ # [e ~> of_val_i v0]) 0 e1_2).
{ change (exprs ρ # [e ~> of_val_i v0]) with (exprs (ρ # [e ~> v0])).
eapply eval_ty_expr_env_ok; eauto with hints. simpl.
replace #|ρ| with (#|exprs ρ|) by apply map_length.
replace #|ρ| with (#|exprs ρ|) by apply length_map.
eapply subst_env_iclosed_n_inv with (n := 1); eauto with hints. }

assert (val_ok Σ1 v0) by (eapply eval_val_ok; eauto with hints).
Expand Down Expand Up @@ -132,7 +135,7 @@ Proof.
now rewrite Hres. }
rewrite Hc.
eapply IHn; eauto with hints.
repeat rewrite map_length. unfold PcbvCurr.cstr_arity. propify. lia.
repeat rewrite length_map. unfold PcbvCurr.cstr_arity. propify. lia.
* destruct c.
** (* the closure corresponds to lambda *)
simpl in *. rename e0 into n0.
Expand Down Expand Up @@ -297,7 +300,7 @@ Proof.
destruct (resolve_inductive _ _) eqn:HresI; tryfalse.
destruct (lookup_with_ind _ _) eqn:Hfind_i; tryfalse.
destruct p as [nparams cs]. destruct p0 as [i ci]. simpl in *.
rewrite map_length.
rewrite length_map.
destruct_match eqn:Hnparams; tryfalse.
assert (HresC: resolve_constr Σ1 i0 e = Some (nparams,i, ci)).
{ unfold resolve_constr. rewrite HresI. rewrite Hfind_i. reflexivity. }
Expand Down Expand Up @@ -327,7 +330,7 @@ Proof.
destruct H2 as [Hdctor?].
eapply PcbvCurr.eval_iota; eauto.
* now eapply map_nth_error.
* cbn. rewrite map_length. unfold PcbvCurr.cstr_arity. propify. lia.
* cbn. rewrite length_map. unfold PcbvCurr.cstr_arity. propify. lia.
* cbn.
unfold etrans_branch.
unfold fun_prod,id; cbn.
Expand All @@ -340,8 +343,8 @@ Proof.
rewrite Heq; cbn.
assert (Hvass : forall xs, context_assumptions (map (fun '(nm, ty) => vass (aRelevant (nNamed (TCString.of_string nm))) ty) xs) = #|xs|).
{ intros; rewrite PCUICSigmaCalculus.context_assumptions_context by auto with hints.
now rewrite map_length. }
rewrite Hvass. rewrite combine_length, map_length.
now rewrite length_map. }
rewrite Hvass. rewrite length_combine, length_map.
lia.
* unfold iota_red in *. simpl in *.
unfold expand_lets,expand_lets_k,inst_case_branch_context,inst_case_context; cbn.
Expand All @@ -355,7 +358,7 @@ Proof.
inversion Hnth_eq; subst; clear Hnth_eq.
assert (Heq : (#|pVars v2.1| =? #|remove_proj c|)%nat) by (propify; lia).
rewrite Heq; cbn.
repeat rewrite map_length. rewrite combine_length,map_length.
repeat rewrite length_map. rewrite length_combine,length_map.
replace (min #|pVars v2.1| #|remove_proj c|) with (#|pVars v2.1|) by lia.
rewrite <- map_skipn.
rewrite <- map_rev.
Expand Down Expand Up @@ -398,12 +401,12 @@ Proof.
specialize (find_forallb_map _ Hfnd HH) as Hclosed_t2; cbn in Hclosed_t2.

erewrite PCUICInstConv.subst_id with (s := rev (_)); eauto.
2: { rewrite rev_length. rewrite to_extended_list_k_length. rewrite Hvass_eq.
subst g. repeat rewrite map_length. rewrite combine_length.
2: { rewrite length_rev. rewrite to_extended_list_k_length. rewrite Hvass_eq.
subst g. repeat rewrite length_map. rewrite length_combine.
replace (min #|pVars v2.1| #|remove_proj c|) with (#|pVars v2.1|) by lia.
rewrite PCUICSigmaCalculus.context_assumptions_context.
* rewrite subst_context_length.
repeat rewrite map_length. rewrite combine_length,map_length.
repeat rewrite length_map. rewrite length_combine,length_map.
replace (min #|pVars v2.1| #|remove_proj c|) with (#|pVars v2.1|) by lia.
replace (#|pVars v2.1| + 0) with #|pVars v2.1| in * by lia.
rewrite <- Hf.
Expand All @@ -416,11 +419,11 @@ Proof.
(subst_context (rev (map (fun x : type => T⟦ subst_env_i_ty 0 (exprs ρ) x ⟧) l0)) 0 g)) = #|pVars v2.1|).
{ rewrite PCUICSigmaCalculus.context_assumptions_context by auto with hints.
rewrite subst_context_length. subst g.
repeat rewrite map_length. rewrite combine_length.
repeat rewrite length_map. rewrite length_combine.
replace #|remove_proj c| with #|pVars v2.1| by (propify; lia).
now replace (min #|pVars v2.1| #|pVars v2.1|) with #|pVars v2.1| by lia.
}
assert (#|pVars v2.1| = #|skipn (ind_npars mib) l2|) by (rewrite skipn_length; lia).
assert (#|pVars v2.1| = #|skipn (ind_npars mib) l2|) by (rewrite length_skipn; lia).

rewrite Hvass_eq1.

Expand All @@ -442,7 +445,7 @@ Proof.
rewrite <- map_map with (g := (expr_to_term Σ1) ∘ of_val_i)
(f := snd).
rewrite map_combine_snd. now subst.
now repeat rewrite rev_length. }
now repeat rewrite length_rev. }
rewrite Hmap. subst h te3.
replace (#|pVars v2.1| + 0) with #|pVars v2.1| in * by lia.
apply Nat.eqb_eq in Hnparams.
Expand All @@ -455,9 +458,9 @@ Proof.
rewrite map_app.
remember (rev (combine (pVars v2.1) (skipn (ind_npars mib) l2))) as l_rev.
assert (Hlrev : #|pVars v2.1| = #|exprs l_rev|).
{ subst. rewrite map_length.
rewrite rev_length. rewrite combine_length.
rewrite skipn_length; lia. }
{ subst. rewrite length_map.
rewrite length_rev. rewrite length_combine.
rewrite length_skipn; lia. }
rewrite Hlrev.
symmetry. eapply subst_env_swap_app with (n := 0);
eauto with hints.
Expand All @@ -471,55 +474,55 @@ Proof.
eapply subst_env_iclosed_0; eauto with hints.
remember ((combine (rev (pVars v2.1)) (map of_val_i (rev (skipn _ l2))))) as l_comb.
assert (Hlen : #|l_comb| = #|pVars v2.1|).
{ subst. rewrite combine_length. rewrite map_length.
repeat rewrite rev_length. rewrite skipn_length; lia. }
{ subst. rewrite length_combine. rewrite length_map.
repeat rewrite length_rev. rewrite length_skipn; lia. }
rewrite <- Hlen.
eapply ty_expr_env_ok_subst_env with (k := 0).
assert (Hcomb : exprs (rev (combine (pVars v2.1) (skipn (ind_npars mib) l2))) = l_comb).
{ subst. repeat rewrite map_rev. rewrite combine_rev.
apply f_equal. now rewrite map_combine_snd_funprod.
rewrite map_length. rewrite skipn_length; lia. }
rewrite length_map. rewrite length_skipn; lia. }
rewrite <- Hcomb. rewrite <- map_app.
eapply eval_ty_expr_env_ok; eauto with hints.
rewrite app_length.
rewrite length_app.
replace (#|rev (combine (pVars v2.1) (skipn (ind_npars mib) l2))|) with #|pVars v2.1| by
(rewrite rev_length, combine_length, skipn_length; lia).
replace #|ρ| with #|exprs ρ| by apply map_length. eauto with hints.
(rewrite length_rev, length_combine, length_skipn; lia).
replace #|ρ| with #|exprs ρ| by apply length_map. eauto with hints.

eapply closed_exprs; eauto.

eapply All_snd_combine with (p := iclosed_n 0); eauto with hints.
apply All_map. apply All_rev.
eapply All_expr_iclosed_of_val; eauto using All_skipn.

rewrite combine_length. rewrite map_length.
repeat rewrite rev_length. rewrite skipn_length by lia.
rewrite length_combine. rewrite length_map.
repeat rewrite length_rev. rewrite length_skipn by lia.
replace (min #|pVars v2.1| (#|l2| - ind_npars mib)) with #|pVars v2.1| by lia.
eauto with hints.

** rewrite <- combine_rev by auto.
rewrite map_combine_snd_funprod.
remember ((combine (rev (pVars v2.1)) (map of_val_i (rev (skipn _ l2))))) as l_comb.
assert (Hlen : #|l_comb| = #|pVars v2.1|).
{ subst. rewrite combine_length. rewrite map_length.
repeat rewrite rev_length. rewrite skipn_length; lia. }
{ subst. rewrite length_combine. rewrite length_map.
repeat rewrite length_rev. rewrite length_skipn; lia. }
rewrite <- Hlen.
eapply ty_expr_env_ok_subst_env with (k := 0).
remember (ind_npars mib) as nparams.
assert (Hcomb : exprs (rev (combine (pVars v2.1) (skipn nparams l2))) = l_comb).
{ subst. repeat rewrite map_rev. rewrite combine_rev.
apply f_equal. now rewrite map_combine_snd_funprod.
rewrite map_length. rewrite skipn_length; lia. }
rewrite length_map. rewrite length_skipn; lia. }
rewrite <- Hcomb. rewrite <- map_app.
subst nparams. eapply eval_ty_expr_env_ok; eauto with hints.
rewrite app_length.
rewrite length_app.
replace (#|rev (combine (pVars v2.1) (skipn _ l2))|) with #|pVars v2.1| by
(rewrite rev_length, combine_length, skipn_length; lia).
replace #|ρ| with #|exprs ρ| by apply map_length. eauto with hints.
(rewrite length_rev, length_combine, length_skipn; lia).
replace #|ρ| with #|exprs ρ| by apply length_map. eauto with hints.
eapply closed_exprs; eauto.
** rewrite map_length.
** rewrite length_map.
replace (#|rev (combine (pVars v2.1) (skipn _ l2))|) with #|pVars v2.1| by
(rewrite rev_length, combine_length, skipn_length; lia).
(rewrite length_rev, length_combine, length_skipn; lia).
eauto with hints.
** apply All_map. subst.
apply All_rev. unfold compose. simpl.
Expand Down
Loading
Loading