From 80a36caea70e03866df15811a8e2408636044242 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 19 May 2022 15:12:37 +0200 Subject: [PATCH 1/3] Port to hierarchy builder --- .nix/config.nix | 26 ++--- coq-mathcomp-abel.opam | 6 +- theories/abel.v | 102 ++++++++++--------- theories/xmathcomp/algR.v | 85 ++++++---------- theories/xmathcomp/char0.v | 33 ++++--- theories/xmathcomp/classic_ext.v | 31 +++--- theories/xmathcomp/cyclotomic_ext.v | 4 +- theories/xmathcomp/map_gal.v | 40 ++++---- theories/xmathcomp/various.v | 147 +++++++++++++++------------- 9 files changed, 241 insertions(+), 233 deletions(-) diff --git a/.nix/config.nix b/.nix/config.nix index 0fc2100..42998fe 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -31,7 +31,7 @@ ## select an entry to build in the following `bundles` set ## defaults to "default" - default-bundle = "coq8.15+mc1.14"; + default-bundle = "coq8.16+mcmathcomp-2.0.0"; ## write one `bundles.name` attribute set per ## alternative configuration @@ -43,27 +43,19 @@ coq.override.version = coqv; mathcomp.override.version = mcv; mathcomp.job = false; - } // (if (mcv == "master") then { + } // (if (coqv == "master") then { + coq-elpi.override.version = "coq-master"; + hierarchy-builder.override.version = "proux01:coq-master"; + } else {}) // (if (mcv == "master") then { mathcomp-real-closed.override.version = "master"; mathcomp-bigenough.override.version = "1.0.1"; - } else {}) // (if (mcv == "mathcomp-1.15.0") then { - mathcomp-real-closed.override.version = "1.1.3"; + } else {}) // (if (mcv == "mathcomp-2.0.0") then { + mathcomp-real-closed.override.version = "master"; mathcomp-bigenough.override.version = "1.0.1"; } else {}); }; in - gen "8.12" "1.13" // - gen "8.13" "1.13" // - gen "8.14" "1.13" // - gen "8.13" "1.14" // - gen "8.14" "1.14" // - gen "8.15" "1.14" // - gen "8.13" "master" // - gen "8.14" "master" // - gen "8.15" "master" // - gen "8.13" "mathcomp-1.15.0" // - gen "8.14" "mathcomp-1.15.0" // - gen "8.15" "mathcomp-1.15.0" // - gen "8.16" "mathcomp-1.15.0" // + gen "8.16" "mathcomp-2.0.0" // + gen "8.17" "mathcomp-2.0.0" // gen "master" "master"; ## Cachix caches to use in CI diff --git a/coq-mathcomp-abel.opam b/coq-mathcomp-abel.opam index 31456e7..b21ec61 100644 --- a/coq-mathcomp-abel.opam +++ b/coq-mathcomp-abel.opam @@ -21,13 +21,13 @@ Mathematical Components library.""" build: [make "-j%{jobs}%"] install: [make "install"] depends: [ - "coq" { (>= "8.10" & < "8.17~") | = "dev" } - "coq-mathcomp-ssreflect" { (>= "1.13.0" & < "1.17~") | = "dev" } + "coq" { (>= "8.16" & < "8.19~") | = "dev" } + "coq-mathcomp-ssreflect" { (>= "2.0.0" & < "2.2~") | = "dev" } "coq-mathcomp-fingroup" "coq-mathcomp-algebra" "coq-mathcomp-solvable" "coq-mathcomp-field" - "coq-mathcomp-real-closed" { (>= "1.1.1") | = "dev" } + "coq-mathcomp-real-closed" { (>= "2.0.0") | = "dev" } ] tags: [ diff --git a/theories/abel.v b/theories/abel.v index b7525f7..b0ff1cf 100644 --- a/theories/abel.v +++ b/theories/abel.v @@ -1,3 +1,4 @@ +From HB Require Import structures. From mathcomp Require Import all_ssreflect all_fingroup all_algebra. From mathcomp Require Import all_solvable all_field polyrcf. From Abel Require Import various classic_ext map_gal algR. @@ -458,7 +459,7 @@ apply/eqP; rewrite /image_mem (map_comp (fun i => x * w ^+ i)) val_enum_ord. rewrite -[p]prednK//= mulr1 -[p.-1]prednK//= expr1 !adjoin_cons. have -> : <<<>; x * w>>%VS = <<<>; x>>%VS. apply/eqP; rewrite [X in _ == X]adjoinC eqEsubv/= !Fadjoin_sub//. - by rewrite -(@fpredMl _ _ _ _ x)// ?memv_adjoin//= adjoinC memv_adjoin. + by rewrite -(@fpredMl _ _ x)// ?memv_adjoin//= adjoinC memv_adjoin. by rewrite rpredM// ?memv_adjoin//= adjoinC memv_adjoin. rewrite (Fadjoin_seq_idP _)// all_map; apply/allP => i _/=. by rewrite rpredM ?rpredX//= ?memv_adjoin// adjoinC memv_adjoin. @@ -637,7 +638,7 @@ apply/(@AbelGalois _ _ w) => //. by rewrite normalClosure_id ?dimv1 ?divn1 ?sub1v//. have /= := solrs L' (map iota rs) _ w. rewrite -(aimg1 iota) -!aimg_adjoin_seq dim_aimg. -apply => //; have := pE; rewrite -(eqp_map [rmorphism of iota]). +apply => //; have := pE; rewrite -(eqp_map iota). by rewrite -map_poly_comp/= (eq_map_poly (rmorph_alg _)) map_prod_XsubC. Qed. @@ -659,16 +660,17 @@ apply: classic_bind (@classic_fieldExtFor _ _ (p : {poly F^o}) p_neq0). exists rs => //; suff <- : limg iota = 1%VS by []. apply/eqP; rewrite eqEsubv sub1v andbT; apply/subvP => v. by move=> /memv_imgP[u _ ->]; rewrite iotaF/= rpredZ// rpred1. - pose S := SplittingFieldType F L splitL. + pose sM := FieldExt_isSplittingField.Build F L splitL. + pose S : splittingFieldType F := HB.pack L sM. exists S, rs; split => //=; first by rewrite -(eq_map_poly iotaF). by apply: (sol_p S rs); rewrite -(eq_map_poly iotaF). move=> L rs prs; apply: sol_p => -[M [rs' [prs']]]. have charL : has_char0 L by move=> n; rewrite char_lalg charF. have charM : has_char0 M by move=> n; rewrite char_lalg charF. -pose K := [fieldExtType F of subvs_of <<1 & rs>>%VS]. +pose K : fieldExtType F := subvs_of <<1 & rs>>%VS. pose rsK := map (vsproj <<1 & rs>>%VS) rs. have pKrs : p ^^ in_alg K %= \prod_(x <- rsK) ('X - x%:P). - rewrite -(eqp_map [rmorphism of vsval])/= map_prod_XsubC/= -map_poly_comp/=. + rewrite -(eqp_map vsval)/= map_prod_XsubC/= -map_poly_comp/=. rewrite -map_comp (@eq_map_poly _ _ _ (in_alg L)); last first. by move=> v; rewrite /= algid1. have /eq_in_map-> : {in rs, cancel (vsproj <<1 & rs>>%VS) vsval}. @@ -684,7 +686,8 @@ have splitK : splittingFieldFor 1 (p ^^ in_alg K) fullv. by rewrite lfunE subvsP. have sfK : SplittingField.axiom K. by exists (p ^^ in_alg K) => //; apply/polyOver1P; exists p. -pose S := SplittingFieldType F K sfK. +pose sM := FieldExt_isSplittingField.Build F K sfK. +pose S : splittingFieldType F := HB.pack K sM. have splitS : splittingFieldFor 1 (p ^^ in_alg S) fullv by []. have splitM : splittingFieldFor 1 (p ^^ in_alg M) <<1 & rs'>> by exists rs'. have splitL : splittingFieldFor 1 (p ^^ in_alg L) <<1 & rs>> by exists rs. @@ -721,7 +724,8 @@ have splitL : SplittingField.axiom L. exists rs => //; suff <- : limg f = 1%VS by []. apply/eqP; rewrite eqEsubv sub1v andbT; apply/subvP => v. by move=> /memv_imgP[u _ ->]; rewrite fF/= rpredZ// rpred1. -pose S := SplittingFieldType F L splitL. +pose sM := FieldExt_isSplittingField.Build F L splitL. +pose S : splittingFieldType F := HB.pack L sM. pose d := \dim <<1 & (rs : seq S)>>. have /classic_cycloSplitting-/(_ S) : d%:R != 0 :> F. by have /charf0P-> := charF0; rewrite -lt0n adim_gt0. @@ -752,7 +756,9 @@ have prs : p ^^ in_alg L %= \prod_(z <- rs) ('X - z%:P). by rewrite (eq_map_poly (fmorph_eq_rat _)). have splitL : SplittingField.axiom L. by exists (p ^^ in_alg L); [by apply/polyOver1P; exists p | exists rs]. -pose S := SplittingFieldType rat L splitL. +pose Frat := [the fieldType of rat : Type]. +pose sM := FieldExt_isSplittingField.Build Frat L splitL. +pose S : splittingFieldType Frat := HB.pack L sM. pose d := \dim <<1 & (rs : seq S)>>. have d_gt0 : (d > 0)%N by rewrite adim_gt0. have [ralg ralg_prim] := C_prim_root_exists d_gt0. @@ -769,7 +775,8 @@ have splitL' : SplittingField.axiom L'. have [us cycloE usw] := splitting_Fadjoin_cyclotomic 1%AS w_prim. exists (us ++ rs'); last by rewrite adjoin_cat usw -adjoin_cons. by rewrite big_cat/= (eqp_trans (eqp_mulr _ cycloE))// eqp_mull//. -pose S' := SplittingFieldType rat L' splitL'. +pose sM' := FieldExt_isSplittingField.Build Frat L' splitL'. +pose S' : splittingFieldType Frat := HB.pack L' sM'. have splitS : splittingFieldFor 1 (p ^^ in_alg S) fullv by exists rs. have splitS' : splittingFieldFor 1 (p ^^ in_alg S') <<1 & rs'>> by exists rs'. have [f /= imgf] := splitting_ahom splitS splitS'. @@ -780,10 +787,9 @@ Qed. Lemma splitting_num_field (p : {poly rat}) : {L : splittingFieldType rat & { LtoC : {rmorphism L -> algC} | (p != 0 -> splittingFieldFor 1 (p ^^ in_alg L) {:L}) - /\ (p = 0 -> L = [splittingFieldType rat of rat^o]) }}. + /\ (p = 0 -> L = [the splittingFieldType rat of rat^o]) }}. Proof. -have [->|p_neq0] := eqVneq p 0. - by exists [splittingFieldType rat of rat^o], [rmorphism of ratr]; split. +have [->|p_neq0] := eqVneq p 0; first by exists rat^o, ratr; split. have [/= rsalg pE] := closed_field_poly_normal (p ^^ (ratr : _ -> algC)). have {}pE : p ^^ ratr %= \prod_(z <- rsalg) ('X - z%:P). by rewrite pE (eqp_trans (eqp_scale _ _)) ?eqpxx// lead_coef_eq0 map_poly_eq0. @@ -793,7 +799,10 @@ have splitL' : splittingFieldFor 1 (p ^^ in_alg L') {: L'}%AS. by rewrite -map_poly_comp map_prod_XsubC rs'E (eq_map_poly (fmorph_eq_rat _)). have splitaxL' : SplittingField.axiom L'. by exists (p ^^ in_alg L'); first by apply/polyOver1P; exists p. -exists (SplittingFieldType rat L' splitaxL'), L'toC; split => //. +pose Frat := [the fieldType of rat : Type]. +pose sM' := FieldExt_isSplittingField.Build Frat L' splitaxL'. +pose S' : splittingFieldType Frat := HB.pack L' sM'. +exists S', L'toC; split => //. by move=> p_eq0; rewrite p_eq0 eqxx in p_neq0. Qed. @@ -813,7 +822,7 @@ Qed. Definition numfield (p : {poly rat}) : splittingFieldType rat := projT1 (splitting_num_field p). -Lemma numfield0 : numfield 0 = [splittingFieldType rat of rat^o]. +Lemma numfield0 : numfield 0 = [the splittingFieldType rat of rat^o]. Proof. by rewrite /numfield; case: splitting_num_field => //= ? [? [_ ->]]. Qed. Definition numfield_inC (p : {poly rat}) : @@ -903,7 +912,7 @@ Qed. Let rp'_uniq : uniq rp'. Proof. rewrite -separable_prod_XsubC -(eqp_separable ratr_p'). -rewrite -char0_ratrE separable_map. +rewrite -char0_ratrE separable_map separable_poly.unlock. apply/coprimepP => d; have [sp_gt1 eqp] := p_irr => /eqp. rewrite size_poly_eq1; have [//|dN1 /(_ isT)] := boolP (d %= 1). move=> /eqp_dvdl-> /dvdp_leq; rewrite -size_poly_eq0 polyorder.size_deriv. @@ -944,7 +953,7 @@ Proof. by exists rp => //; rewrite ratr_p eqpxx. Qed. Let p_sep : separable_poly p. Proof. -rewrite -(separable_map [rmorphism of char0_ratr charL]). +rewrite -(separable_map (char0_ratr charL)). by rewrite (eqp_separable ratr_p) separable_prod_XsubC. Qed. @@ -1001,8 +1010,8 @@ rewrite -(eqp_rtrans ratr_p) big_map. apply: (@eqp_trans _ (map_poly (g \o ratr) p)); last first. apply/eqpW/eq_map_poly => x /=; rewrite (fixed_gal _ (gal1 g)) ?sub1v//. by rewrite -alg_num_field rpredZ ?mem1v. -rewrite map_poly_comp/=; have := ratr_p; rewrite -(eqp_map [rmorphism of g])/=. -move=> /eqp_rtrans/=->; apply/eqpW; rewrite rmorph_prod. +rewrite map_poly_comp/=; have := ratr_p; rewrite -(eqp_map g)/=. +move=> /eqp_rtrans/=->; apply/eqpW; rewrite rmorph_prod /=. by apply: eq_bigr => x; rewrite rmorphB/= map_polyX map_polyC/=. Qed. @@ -1033,7 +1042,9 @@ have : size (minPoly 1 x) != 1%N by rewrite size_minPoly. have /polyOver1P[q ->] := minPolyOver 1 x. have /eq_map_poly -> : in_alg L =1 ratr. by move=> r; rewrite in_algE alg_num_field. -by rewrite -char0_ratrE /eqp !dvdp_map -/(_ %= _) size_map_poly; apply: p_irr. +rewrite -char0_ratrE /eqp. +rewrite 2!(dvdp_map (char0_ratr charL)). +by rewrite -/(_ %= _) size_map_poly; apply: p_irr. Qed. Lemma injm_gal_perm : ('injm gal_perm)%g. @@ -1075,7 +1086,7 @@ Lemma gal_perm_cycle_order : #[(gal_perm gal_cycle)]%g = d. Proof. by rewrite order_injm ?gal_cycle_order ?injm_gal_perm ?gal1. Qed. Definition conjL : {lrmorphism L -> L} := - projT1 (restrict_aut_to_normal_num_field iota conjC). + projT1 (restrict_aut_to_normal_num_field iota Num.conj_op). Definition iotaJ : {morph iota : x / conjL x >-> x^*} := projT2 (restrict_aut_to_normal_num_field _ _). @@ -1211,6 +1222,7 @@ Qed. Lemma separable_example : separable_poly poly_example. Proof. +rewrite separable_poly.unlock. apply/coprimepP => q /(irredp_XsubCP irreducible_example) [//| eqq]. have size_deriv_example : size poly_example^`() = 5%N. rewrite !derivCE addr0 alg_polyC -scaler_nat addr0. @@ -1271,7 +1283,7 @@ apply: lt_sorted_eq; rewrite ?sorted_roots//. by rewrite /= andbT -subr_gt0 opprK ?addr_gt0 ?alpha_gt0. move=> x; rewrite mem_rootsR ?map_poly_eq0// !inE -topredE/= orbC. rewrite deriv_poly_example /root. -rewrite rmorphB linearZ/= map_polyC/= map_polyXn !pesimp. +rewrite rmorphB /= linearZ map_polyC/= map_polyXn !pesimp. rewrite -[5%:R]sqr_sqrtr ?ler0n// (exprM _ 2 2) -exprMn (natrX _ 2 2) subr_sqr. rewrite mulf_eq0 [_ + 2%:R == 0]gt_eqF ?orbF; last first. by rewrite ltr_spaddr ?ltr0n// mulr_ge0 ?sqrtr_ge0// exprn_even_ge0. @@ -1293,11 +1305,11 @@ rewrite -big_filter (perm_big (map algRval (rootsR pR))); last first. rewrite uniq_perm ?filter_uniq ?example_roots_uniq//. by rewrite (map_inj_uniq (fmorph_inj _)) uniq_roots. move=> x; rewrite mem_filter -root_prod_XsubC -ratr_example_poly. - rewrite -(eq_map_poly (fmorph_eq_rat [rmorphism of algRval \o ratr]))/=. + rewrite -(eq_map_poly (fmorph_eq_rat (algRval \o ratr)))/=. rewrite map_poly_comp/=. apply/andP/mapP => [[xR xroot]|[y + ->]]. exists (in_algR xR); rewrite // mem_rootsR// -topredE/=. - by rewrite -(mapf_root algRval_rmorphism)/=. + by rewrite -(mapf_root algRval)/=. rewrite mem_rootsR// -[y \in _]topredE/=. by split; [apply/algRvalP|rewrite mapf_root]. apply/eqP; rewrite sum1_size size_map eqn_leq. @@ -1356,12 +1368,7 @@ Definition decode_const (n : nat) : const := match n with 0 => Zero | 1 => One | n.+2 => URoot n end. Lemma code_constK : cancel encode_const decode_const. Proof. by case. Qed. -Definition const_eqMixin := CanEqMixin code_constK. -Canonical const_eqType := EqType const const_eqMixin. -Definition const_choiceMixin := CanChoiceMixin code_constK. -Canonical const_choiceType := ChoiceType const const_choiceMixin. -Definition const_countMixin := CanCountMixin code_constK. -Canonical const_countType := CountType const const_countMixin. +HB.instance Definition _ := Countable.copy const (can_type code_constK). Definition encode_binOp (c : binOp) : bool := match c with Add => false | Mul => true end. @@ -1369,12 +1376,7 @@ Definition decode_binOp (b : bool) : binOp := match b with false => Add | _ => Mul end. Lemma code_binOpK : cancel encode_binOp decode_binOp. Proof. by case. Qed. -Definition binOp_eqMixin := CanEqMixin code_binOpK. -Canonical binOp_eqType := EqType binOp binOp_eqMixin. -Definition binOp_choiceMixin := CanChoiceMixin code_binOpK. -Canonical binOp_choiceType := ChoiceType binOp binOp_choiceMixin. -Definition binOp_countMixin := CanCountMixin code_binOpK. -Canonical binOp_countType := CountType binOp binOp_countMixin. +HB.instance Definition _ := Countable.copy binOp (can_type code_binOpK). Definition encode_unOp (c : unOp) : nat + nat := match c with Opp => inl _ 0%N | Inv => inl _ 1%N @@ -1384,12 +1386,7 @@ Definition decode_unOp (n : nat + nat) : unOp := | inl n.+2 => Exp n | inr n => Root n end. Lemma code_unOpK : cancel encode_unOp decode_unOp. Proof. by case. Qed. -Definition unOp_eqMixin := CanEqMixin code_unOpK. -Canonical unOp_eqType := EqType unOp unOp_eqMixin. -Definition unOp_choiceMixin := CanChoiceMixin code_unOpK. -Canonical unOp_choiceType := ChoiceType unOp unOp_choiceMixin. -Definition unOp_countMixin := CanCountMixin code_unOpK. -Canonical unOp_countType := CountType unOp unOp_countMixin. +HB.instance Definition _ := Countable.copy unOp (can_type code_unOpK). Fixpoint encode_algT F (f : algterm F) : GenTree.tree (F + const) := let T_ isbin := if isbin then binOp else unOp in @@ -1416,14 +1413,12 @@ Lemma code_algTK F : cancel (@encode_algT F) (@decode_algT F). Proof. by elim => // [u f IHf|b f IHf f' IHf']/=; rewrite pickleK -lock ?IHf ?IHf'. Qed. -Definition algT_eqMixin (F : eqType) := CanEqMixin (@code_algTK F). -Canonical algT_eqType (F : eqType) := EqType (algterm F) (@algT_eqMixin F). -Definition algT_choiceMixin (F : choiceType) := CanChoiceMixin (@code_algTK F). -Canonical algT_choiceType (F : choiceType) := - ChoiceType (algterm F) (@algT_choiceMixin F). -Definition algT_countMixin (F : countType) := CanCountMixin (@code_algTK F). -Canonical algT_countType (F : countType) := - CountType (algterm F) (@algT_countMixin F). +HB.instance Definition _ (F : eqType) := Equality.copy (algterm F) + (can_type (@code_algTK F)). +HB.instance Definition _ (F : choiceType) := Choice.copy (algterm F) + (can_type (@code_algTK F)). +HB.instance Definition _ (F : countType) := Countable.copy (algterm F) + (can_type (@code_algTK F)). Declare Scope algT_scope. Delimit Scope algT_scope with algT. @@ -1484,7 +1479,7 @@ have Cchar := Cchar => p_neq0; split. algT_eval (iota \o vsval) f = iota r. elim: f => //= [[/= _/vlineP[s ->]]|cst|op|op]. - exists (Base s) => /=. - by rewrite [RHS](fmorph_eq_rat [rmorphism of iota \o in_alg L]). + by rewrite [RHS](fmorph_eq_rat (iota \o in_alg L)). - by exists (Const cst). - by move=> _ [f1 <-]; exists (UnOp op f1). - by move=> _ [f1 <-] _ [f2 <-]; exists (BinOp op f1 f2). @@ -1554,7 +1549,8 @@ have mprs : mp ^^ in_alg L %= \prod_(z <- rsmp) ('X - z%:P). by rewrite -char0_ratrE// (eq_map_poly (fmorph_eq_rat _)) eqpxx. have splitL : SplittingField.axiom L. by exists (mp ^^ in_alg L); [apply/polyOver1P; exists mp | exists rsmp]. -pose S := SplittingFieldType rat L splitL. +pose sM := FieldExt_isSplittingField.Build rat L splitL. +pose S : splittingFieldType rat := HB.pack L sM. have algsW: {subset rsalg <= algs}. move=> x; rewrite -fsE => /mapP[{x}f ffs ->]. apply/flattenP; exists (subeval ratr f); rewrite ?map_f//. @@ -1576,7 +1572,7 @@ rewrite {p p_neq0 mkalg pE prs rsmp iota_rs mprs rsf rs rsE mp suff: forall (L : splittingFieldType rat) (iota : {rmorphism L -> algC}) als, map iota als = algs -> radical.-ext 1%VS <<1 & als>>%VS. by move=> /(_ S iota als alsE). -move=> {}L {}iota {splitL S} {}als {}alsE; rewrite {}/algs in alsE. +move=> {sM}L {}iota {splitL S} {}als {}alsE; rewrite {}/algs in alsE. elim: fs => [|f fs IHfs]//= in rsalg fsE als alsE *. case: als => []// in alsE *. by rewrite Fadjoin_nil; apply: rext_refl. @@ -1596,7 +1592,7 @@ elim: f => //= [x|c|u f1 IHf1|b f1 IHf1 f2 IHf2] in k {r fr} als1 als1E *. rewrite adjoin_seq1 (Fadjoin_idP _); first exact: rext_refl. suff: y \in 1%VS by apply/subvP; rewrite sub1v. apply/vlineP; exists x; apply: (fmorph_inj iota); rewrite yx. - by rewrite [RHS](fmorph_eq_rat [rmorphism of iota \o in_alg _]). + by rewrite [RHS](fmorph_eq_rat (iota \o in_alg _)). - case: als1 als1E => [|y []]//= []/=; rewrite adjoin_seq1. case: c => [/eqP|/eqP|n yomega]. + rewrite fmorph_eq0 => /eqP->; rewrite (Fadjoin_idP _) ?rpred0//. diff --git a/theories/xmathcomp/algR.v b/theories/xmathcomp/algR.v index d16fcc2..cd98e39 100644 --- a/theories/xmathcomp/algR.v +++ b/theories/xmathcomp/algR.v @@ -1,3 +1,4 @@ +From HB Require Import structures. From mathcomp Require Import all_ssreflect all_fingroup all_algebra. From mathcomp Require Import all_solvable all_field. From Abel Require Import various. @@ -15,37 +16,22 @@ Local Notation "p ^^ f" := (map_poly f p) Record algR := in_algR {algRval : algC; algRvalP : algRval \is Num.real}. -Canonical algR_subType := [subType for algRval]. -Definition algR_eqMixin := [eqMixin of algR by <:]. -Canonical algR_eqType := EqType algR algR_eqMixin. -Definition algR_choiceMixin := [choiceMixin of algR by <:]. -Canonical algR_choiceType := ChoiceType algR algR_choiceMixin. -Definition algR_countMixin := [countMixin of algR by <:]. -Canonical algR_countType := CountType algR algR_countMixin. -Definition algR_zmodMixin := [zmodMixin of algR by <:]. -Canonical algR_zmodType := ZmodType algR algR_zmodMixin. -Definition algR_ringMixin := [ringMixin of algR by <:]. -Canonical algR_ringType := RingType algR algR_ringMixin. -Definition algR_comRingMixin := [comRingMixin of algR by <:]. -Canonical algR_comRingType := ComRingType algR algR_comRingMixin. -Definition algR_unitRingMixin := [unitRingMixin of algR by <:]. -Canonical algR_unitRingType := UnitRingType algR algR_unitRingMixin. -Canonical algR_comUnitRingType := [comUnitRingType of algR]. -Definition algR_idomainMixin := [idomainMixin of algR by <:]. -Canonical algR_idomainType := IdomainType algR algR_idomainMixin. -Definition algR_fieldMixin := [fieldMixin of algR by <:]. -Canonical algR_fieldType := FieldType algR algR_fieldMixin. -Definition algR_porderMixin := [porderMixin of algR by <:]. -Canonical algR_porderType := POrderType ring_display algR algR_porderMixin. -Lemma total_algR : totalPOrderMixin [porderType of algR]. +HB.instance Definition _ := [isSub for algRval]. +HB.instance Definition _ := [Countable of algR by <:]. +HB.instance Definition _ := [SubChoice_isSubIntegralDomain of algR by <:]. +HB.instance Definition _ := [SubIntegralDomain_isSubField of algR by <:]. +HB.instance Definition _ : Order.isPOrder ring_display algR := + Order.CancelPartial.Pcan _ valK. +Lemma total_algR : total (<=%O : rel (algR : porderType _)). Proof. by move=> x y; apply/real_leVge/valP/valP. Qed. -Canonical algR_latticeType := LatticeType algR total_algR. -Canonical algR_distrLatticeType := DistrLatticeType algR total_algR. -Canonical algR_orderType := OrderType algR total_algR. +HB.instance Definition _ := Order.POrder_isTotal.Build _ algR total_algR. -Lemma algRval_is_rmorphism : rmorphism algRval. Proof. by []. Qed. -Canonical algRval_additive := Additive algRval_is_rmorphism. -Canonical algRval_rmorphism := RMorphism algRval_is_rmorphism. +Lemma algRval_is_additive : additive algRval. Proof. by []. Qed. +Lemma algRval_is_multiplicative : multiplicative algRval. Proof. by []. Qed. +HB.instance Definition _ := GRing.isAdditive.Build algR algC algRval + algRval_is_additive. +HB.instance Definition _ := GRing.isMultiplicative.Build algR algC algRval + algRval_is_multiplicative. Definition algR_norm (x : algR) : algR := in_algR (normr_real (val x)). Lemma algR_ler_norm_add x y : algR_norm (x + y) <= (algR_norm x + algR_norm y). @@ -58,8 +44,6 @@ Lemma algR_normrN x : algR_norm (- x) = algR_norm x. Proof. by apply/val_inj; apply: normrN. Qed. Section Num. -Definition algR_normedMixin := - Num.NormedMixin algR_ler_norm_add algR_normr0_eq0 algR_normrMn algR_normrN. Section withz. Let z : algR := 0. @@ -73,21 +57,13 @@ Lemma algR_ler_def (x y : algR) : (x <= y) = (algR_norm (y - x) == y - x). Proof. by apply: ler_def. Qed. End withz. -Let algR_ring := (GRing.Ring.Pack (GRing.ComRing.base - (GRing.ComUnitRing.base (GRing.IntegralDomain.base - (GRing.IntegralDomain.class [idomainType of algR]))))). -Definition algR_numMixin : @Num.mixin_of algR_ring _ _ := - @Num.Mixin _ _ algR_normedMixin - algR_addr_gt0 algR_ger_leVge algR_normrM algR_ler_def. - -Canonical algR_numDomainType := NumDomainType algR algR_numMixin. -Canonical algR_normedZmodType := NormedZmodType algR algR algR_normedMixin. -Canonical algR_numFieldType := [numFieldType of algR]. -Canonical algR_realDomainType := [realDomainType of algR]. -Canonical algR_realFieldType := [realFieldType of algR]. +HB.instance Definition _ := Num.Zmodule_isNormed.Build _ algR + algR_ler_norm_add algR_normr0_eq0 algR_normrMn algR_normrN. +HB.instance Definition _ := Num.isNumRing.Build algR + algR_addr_gt0 algR_ger_leVge algR_normrM algR_ler_def. End Num. -Definition algR_archiFieldMixin : Num.archimedean_axiom [numDomainType of algR]. +Definition algR_archiFieldMixin : Num.archimedean_axiom algR. Proof. move=> /= x; have /andP[/= _] := floorC_itv (valP `|x|). set n := floorC _; have [n_lt0|n_ge0] := ltP n 0. @@ -96,7 +72,8 @@ set n := floorC _; have [n_lt0|n_ge0] := ltP n 0. move=> x_lt; exists (`|(n + 1)%R|%N); apply: lt_le_trans x_lt _. by rewrite /= rmorphMn/= pmulrn gez0_abs// addr_ge0. Qed. -Canonical algR_archiFieldType := ArchiFieldType algR algR_archiFieldMixin. +HB.instance Definition _ := Num.RealField_isArchimedean.Build algR + algR_archiFieldMixin. Definition algRpfactor (x : algC) : {poly algR} := if x \is Num.real =P true is ReflectT xR then 'X - (in_algR xR)%:P else @@ -123,8 +100,8 @@ Lemma algCpfactorCE (x : algC) : x \isn't Num.real -> algCpfactor x = ('X - x%:P) * ('X - x^*%:P). Proof. move=> xNR; rewrite algRpfactorCE//=. -rewrite rmorphD rmorphB/= !map_polyZ !map_polyXn/= map_polyX. -rewrite (map_polyC [rmorphism of algRval])/=. +rewrite rmorphD /= rmorphB/= !map_polyZ !map_polyXn/= map_polyX. +rewrite (map_polyC algRval)/=. rewrite mulrBl !mulrBr -!addrA; congr (_ + _). rewrite opprD addrA opprK -opprD -rmorphM/= -normCK; congr (- _ + _). rewrite mulrC !mul_polyC -scalerDl. @@ -205,7 +182,7 @@ elim: n r => // n IHn [|x r]/= in p pr *. rewrite ltnS => r_lt. have xJxr : x^* \in x :: r. rewrite -root_prod_XsubC -pr. - have /eq_map_poly-> : algRval =1 conjC \o algRval. + have /eq_map_poly-> : algRval =1 Num.conj_op \o algRval. by move=> a /=; rewrite (CrealP (algRvalP _)). by rewrite map_poly_comp mapf_root pr root_prod_XsubC mem_head. have xJr : (x \isn't Num.real) ==> (x^* \in r) by rewrite implyNb CrealE. @@ -223,7 +200,7 @@ case: (_ \is _) => /= in xJr *; first by rewrite divp1//. by rewrite (big_rem _ xJr)/= mulKp ?polyXsubC_eq0. Qed. -Definition algR_rcfMixin : Num.real_closed_axiom [numDomainType of algR]. +Definition algR_rcfMixin : Num.real_closed_axiom algR. Proof. move=> p a b le_ab /andP[pa_le0 pb_ge0]/=. case: ltgtP pa_le0 => //= pa0 _; last first. @@ -255,8 +232,10 @@ wlog : p pab0 {p_neq0 prs} / have := pab0; rewrite pqu !hornerM mulrACA [_ * _ * _ < 0]pmulr_llt0//. rewrite !horner_prod -big_split/= prodr_gt0// => x. have [xR|xNR] := boolP (x \is Num.real); last first. - by rewrite ?ltEsub/= -!horner_map/= mulr_gt0 ?algCpfactorCgt0 ?algRvalP. - apply: contraNT; rewrite -leNgt ?leEsub/= -!horner_map/=. + rewrite (_ : (0 < ?[a]) = (algRval 0 < algRval ?a))//=. + by rewrite -!horner_map/= mulr_gt0 ?algCpfactorCgt0 ?algRvalP. + apply: contraNT; rewrite -leNgt. + rewrite (_ : (?[a] <= 0) = (algRval ?a <= algRval 0))//= -!horner_map/=. by rewrite algRpfactorR_mul_gt0 ?algRvalP. rewrite -big_filter; have := filter_all ab rs. set rsab := filter _ _. @@ -268,6 +247,6 @@ case: rsab => [_ _|x rsab]/=; rewrite (big_nil, big_cons). by rewrite !hornerE ltr10. move=> /andP[xR rsabR] /andP[axb arsb] prsab. exists (in_algR xR) => //=. -by rewrite -(mapf_root [rmorphism of algRval])//= prsab rootM root_XsubC eqxx. +by rewrite -(mapf_root algRval)//= prsab rootM root_XsubC eqxx. Qed. -Canonical algR_rcfType := RcfType algR algR_rcfMixin. +HB.instance Definition _ := Num.RealField_isClosed.Build algR algR_rcfMixin. diff --git a/theories/xmathcomp/char0.v b/theories/xmathcomp/char0.v index 49ea16d..e6b5c1c 100644 --- a/theories/xmathcomp/char0.v +++ b/theories/xmathcomp/char0.v @@ -1,3 +1,4 @@ +From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra all_field. Set Implicit Arguments. @@ -45,26 +46,36 @@ Hypothesis charF0 : has_char0 F. Local Notation ratrF := (char0_ratr charF0). -Fact char0_ratr_is_rmorphism : rmorphism ratrF. +Fact char0_ratr_is_additive : additive ratrF. Proof. rewrite /char0_ratr. have injZtoQ: @injective rat int intr by apply: intr_inj. have nz_den x: (denq x)%:~R != 0 :> F by rewrite char0_intr_eq0 // denq_eq0. -do 2?split; rewrite /ratr ?divr1 // => x y; last first. - rewrite mulrC mulrAC; apply: canLR (mulKf (nz_den _)) _; rewrite !mulrA. - do 2!apply: canRL (mulfK (nz_den _)) _; rewrite -!rmorphM; congr _%:~R. - apply: injZtoQ; rewrite !rmorphM [x * y]lock /= !numqE -lock. - by rewrite -!mulrA mulrA mulrCA -!mulrA (mulrCA y). +rewrite /ratr ?divr1 // => x y. apply: (canLR (mulfK (nz_den _))); apply: (mulIf (nz_den x)). -rewrite mulrAC mulrBl divfK ?nz_den // mulrAC -!rmorphM. +rewrite mulrAC mulrBl divfK ?nz_den // mulrAC -!rmorphM /=. apply: (mulIf (nz_den y)); rewrite mulrAC mulrBl divfK ?nz_den //. rewrite -!(rmorphM, rmorphB); congr _%:~R; apply: injZtoQ. -rewrite !(rmorphM, rmorphB) [_ - _]lock /= -lock !numqE. -by rewrite (mulrAC y) -!mulrBl -mulrA mulrAC !mulrA. +rewrite !(rmorphM, rmorphB) [_ - _]lock /= -lock. +by rewrite !numqE (mulrAC y) -!mulrBl -mulrA mulrAC !mulrA. Qed. -Canonical char0_ratr_additive := Additive char0_ratr_is_rmorphism. -Canonical char0_ratr_rmorphism := RMorphism char0_ratr_is_rmorphism. +Fact char0_ratr_is_multiplicative : multiplicative ratrF. +Proof. +rewrite /char0_ratr. +have injZtoQ: @injective rat int intr by apply: intr_inj. +have nz_den x: (denq x)%:~R != 0 :> F by rewrite char0_intr_eq0 // denq_eq0. +split; rewrite /ratr ?divr1 // => x y. +rewrite mulrC mulrAC; apply: canLR (mulKf (nz_den _)) _; rewrite !mulrA. +do 2!apply: canRL (mulfK (nz_den _)) _; rewrite -!rmorphM; congr _%:~R. +apply: injZtoQ; rewrite !rmorphM [x * y]lock /= !numqE -lock. +by rewrite -!mulrA mulrA mulrCA -!mulrA (mulrCA y). +Qed. + +HB.instance Definition _ := GRing.isAdditive.Build rat F ratrF + char0_ratr_is_additive. +HB.instance Definition _ := GRing.isMultiplicative.Build rat F ratrF + char0_ratr_is_multiplicative. End Char0MorphismsField. diff --git a/theories/xmathcomp/classic_ext.v b/theories/xmathcomp/classic_ext.v index 21eb643..168431a 100644 --- a/theories/xmathcomp/classic_ext.v +++ b/theories/xmathcomp/classic_ext.v @@ -1,3 +1,4 @@ +From HB Require Import structures. From mathcomp Require Import all_ssreflect all_fingroup all_algebra. From mathcomp Require Import all_solvable all_field. From Abel Require Import various cyclotomic_ext. @@ -54,19 +55,23 @@ apply: classic_bind (@classic_EM (irreducible_poly p)) => -[]; last first. by rewrite adjoin_cat limg_comp -aimg_adjoin_seq rs1_full rs2_full. rewrite big_cat/= big_map (eq_map_poly (comp_lfunE _ _)) map_poly_comp pE. rewrite !rmorphM/= mulrC (eqp_trans (eqp_mull _ rE))// eqp_mulr//. - have := qE; rewrite -(eqp_map [rmorphism of iota2]) => /eqp_trans->//=. + have := qE; rewrite -(eqp_map iota2) => /eqp_trans->//=. rewrite (big_morph _ (rmorphM _) (rmorph1 _))/=. under eq_bigr do rewrite rmorphB/= -/iota map_polyX map_polyC/=. by rewrite eqpxx. move=> /irredp_FAdjoin[L1 df [r1 r1_root r1_full]]. -pose L01 := [fieldExtType F0 of baseFieldType L1]. +pose L01 : fieldExtType F0 := baseFieldType L1. pose r01 : L01 := r1. pose inL01 : L -> L01 := in_alg L1. -have iota_morph : lrmorphism inL01. -split; [split; [exact: rmorphB|split; [exact: rmorphM|]]|]. - by rewrite /inL01 rmorph1. +have iotam : multiplicative inL01. + by split; [exact: rmorphM|rewrite /inL01 rmorph1]. +have iotal : scalable inL01. by move=> k a; rewrite /inL01 -mulr_algl rmorphM/= mulr_algl. -pose iota1 : 'AHom(L, L01) := AHom (linfun_is_ahom (LRMorphism iota_morph)). +pose iotaaM := GRing.isAdditive.Build _ _ inL01 (rmorphB _). +pose iotamM := GRing.isMultiplicative.Build _ _ inL01 iotam. +pose iotalM := GRing.isScalable.Build _ _ _ _ inL01 iotal. +pose iotaLRM : {lrmorphism _ -> _} := HB.pack inL01 iotaaM iotamM iotalM. +pose iota1 : 'AHom(L, L01) := AHom (linfun_is_ahom iotaLRM). have inL01E : inL01 =1 iota1 by move=> x; rewrite lfunE. have r01_root : root (p ^^ iota1) r01 by rewrite -(eq_map_poly inL01E). have r01_full : <>%VS = fullv. @@ -103,7 +108,7 @@ case: n => [|[_|[two_neq0|n']]]//; first by rewrite eqxx. by rewrite lim1g (Fadjoin_idP _)// rpred1. - apply/classicW; exists L, (- 1), (id_ahom _) => /=. by rewrite lim1g (Fadjoin_idP _)// rpredN1. - by rewrite prim2_rootN1// -(rmorph_nat [rmorphism of in_alg L]) fmorph_eq0. + by rewrite prim2_rootN1// -(rmorph_nat (in_alg L)) fmorph_eq0. set n := n'.+3 => nF0neq0. have poly_XnsubC_neq0 : 'X^n - 1 != 0 :> {poly L}. by rewrite -size_poly_eq0 size_XnsubC. @@ -150,7 +155,7 @@ exists (map iota rsq ++ rs); last first. by rewrite adjoin_cat -(aimg1 iota) -aimg_adjoin_seq rsqf rsf. rewrite big_cat/= rmorphM/= big_map mulrC. rewrite (eqp_trans (eqp_mull _ pE))// eqp_mulr//. -have := qE; rewrite -(eqp_map [rmorphism of iota])/=. +have := qE; rewrite -(eqp_map iota)/=. rewrite (big_morph _ (rmorphM _) (rmorph1 _))/=. under eq_bigr do rewrite rmorphB/= map_polyX map_polyC/=. by rewrite -map_poly_comp (eq_map_poly (rmorph_alg _)). @@ -164,7 +169,9 @@ Proof. move=> /(@classic_cycloExt _ L). apply/classic_bind => -[M [w [iota wfull wprim]]]; apply/classicW. suff splitM : SplittingField.axiom M. - by exists (SplittingFieldType F0 M splitM), w, iota. + pose mM := FieldExt_isSplittingField.Build F0 M splitM. + pose mT : splittingFieldType F0 := HB.pack M mM. + by exists mT, w, iota. apply: (@SplittingFieldExt _ L ('Phi_n ^^ intr) _ iota). rewrite -map_poly_comp (eq_map_poly (rmorph_int _)) -wfull. by rewrite (Phi_cyclotomic wprim); apply: splitting_Fadjoin_cyclotomic. @@ -181,8 +188,10 @@ move=> nN0; suff: classically { L' : fieldExtType F & { w : L' & have splitL : SplittingField.axiom L. exists (cyclotomic w n); rewrite ?cyclotomic_over// -wfull. exact: splitting_Fadjoin_cyclotomic. - by exists (SplittingFieldType F L splitL), w. -pose Fo := [splittingFieldType F of F^o]. + pose lM := FieldExt_isSplittingField.Build F L splitL. + pose lT : splittingFieldType F := HB.pack L lM. + by exists lT, w. +pose Fo : splittingFieldType F := F^o. apply: classic_bind (@classic_cycloExt _ Fo n nN0). case=> [L [w [iota wfull wprim]]]; apply/classicW. exists L, w => //; apply/eqP; rewrite eqEsubv subvf/= -wfull. diff --git a/theories/xmathcomp/cyclotomic_ext.v b/theories/xmathcomp/cyclotomic_ext.v index ca46d08..35eb025 100644 --- a/theories/xmathcomp/cyclotomic_ext.v +++ b/theories/xmathcomp/cyclotomic_ext.v @@ -18,7 +18,7 @@ Qed. Lemma Cyclotomic2 : 'Phi_2 = 'X + 1. Proof. have := @prod_Cyclotomic 2%N isT; rewrite !big_cons big_nil mulr1/=. -rewrite Cyclotomic1 -(@expr1n [ringType of {poly int}] 2%N). +rewrite Cyclotomic1 -(@expr1n {poly int} 2%N). by rewrite subr_sqr expr1n => /mulfI->//; rewrite polyXsubC_eq0. Qed. @@ -134,7 +134,7 @@ Lemma galois_Fadjoin_cyclotomic : galois E <>. Proof. apply/splitting_galoisField; exists (cyclotomic w n). split; rewrite ?cyclotomic_over//; last exact: splitting_Fadjoin_cyclotomic. -rewrite /cyclotomic -(big_image _ _ _ (fun x => 'X - x%:P))/=. +rewrite /cyclotomic -(big_image _ _ _ _ (fun x => 'X - x%:P))/=. rewrite separable_prod_XsubC map_inj_uniq ?enum_uniq// => i j /eqP. by rewrite (eq_prim_root_expr w_is_nth_root) !modn_small// => /eqP/val_inj. Qed. diff --git a/theories/xmathcomp/map_gal.v b/theories/xmathcomp/map_gal.v index 10f8600..cddf7b5 100644 --- a/theories/xmathcomp/map_gal.v +++ b/theories/xmathcomp/map_gal.v @@ -1,3 +1,4 @@ +From HB Require Import structures. From mathcomp Require Import all_ssreflect all_fingroup all_algebra. From mathcomp Require Import all_solvable all_field. From Abel Require Import various char0. @@ -49,15 +50,13 @@ apply/trivgP/subsetP=> u uG; rewrite inE. by apply/gal_eqP => x xE; rewrite gal_id (fixed_gal _ uG). Qed. -Program Canonical prodv_aspace_law := - @Monoid.Law {subfield L} 1%AS (@prodv_aspace _ _) _ _ _. +Program Definition prodv_aspace_law_mixin := + Monoid.isComLaw.Build {subfield L} 1%AS (@prodv_aspace _ _) _ _ _. Next Obligation. by move=> *; apply/val_inj/prodvA. Qed. +Next Obligation. by move=> *; apply/val_inj/prodvC. Qed. Next Obligation. by move=> *; apply/val_inj/prod1v. Qed. -Next Obligation. by move=> *; apply/val_inj/prodv1. Qed. -Program Canonical prodv_aspace_com_law := - @Monoid.ComLaw {subfield L} 1%AS prodv_aspace_law _. -Next Obligation. by move=> *; apply/val_inj/prodvC. Qed. +HB.instance Definition _ := prodv_aspace_law_mixin. Lemma big_prodv_eq_aspace I (r : seq I) (P : {pred I}) (F : I -> {aspace L}) : (\big[@prodv _ _/1%VS]_(i <- r | P i) F i) = @@ -372,14 +371,17 @@ Proof. move=> /= k a b; apply/lfunP => x; rewrite /map_hom. by rewrite !(comp_lfunE, add_lfunE, scale_lfunE) linearP. Qed. -Canonical map_hom_linear := Linear map_hom_is_linear. +HB.instance Definition _ := GRing.isLinear.Build F0 'End(L) 'End(L') _ map_hom + map_hom_is_linear. Lemma inv_map_hom_is_linear : linear inv_map_hom. Proof. move=> /= k a b; apply/lfunP => x; rewrite /map_hom. by rewrite !(comp_lfunE, add_lfunE, scale_lfunE) linearP. Qed. -Canonical inv_map_hom_linear := Linear inv_map_hom_is_linear. +HB.instance Definition _ := + GRing.isLinear.Build F0 'End(L') 'End(L) _ inv_map_hom + inv_map_hom_is_linear. Lemma lker0_map_homC (f : 'End(L)) : lker iota == 0%VS -> (map_hom f \o iota = iota \o f)%VF. @@ -418,7 +420,7 @@ Lemma map_ahom_in (f : 'End(L)) (E : {vspace L}) : ahom_in (iota @: E) (map_hom iota f) = ahom_in E f. Proof. apply/ahom_inP/ahom_inP => -[mfM mf1]; last first. - split; last by rewrite -(rmorph1 [rmorphism of iota]) map_hom_algE mf1. + split; last by rewrite -(rmorph1 iota) map_hom_algE mf1. move=> _ _ /memv_imgP[u uE ->] /memv_imgP[v vE ->]. by rewrite !(map_hom_algE, =^~rmorphM)/= mfM. split=> [x y xE yE|]; last first. @@ -449,7 +451,7 @@ apply/kHomP/kHomP => -[/= fM s_id]. rewrite -!rmorphM/= -3?inv_map_homE ?memv_img ?memvf ?fiotaf ?rpredM//. by rewrite fM// rmorphM. by rewrite -inv_map_homE ?s_id// fiotaf//; apply: subv_trans EF. -split=> [x y xF yF|x xF]; apply: (fmorph_inj [rmorphism of iota]) => /=. +split=> [x y xF yF|x xF]; apply: (fmorph_inj iota) => /=. by rewrite rmorphM/= !inv_map_homE ?fiotaf ?rpredM// rmorphM fM ?memv_img. by rewrite inv_map_homE s_id ?memv_img ?memvf. Qed. @@ -512,7 +514,7 @@ rewrite !kAutE limg_map_ahom limg_ker0 ?AHom_lker0// [LHS]andbC [RHS]andbC. have [sF_sub_F|]//= := boolP (s @: F <= F)%VS. apply/kAHomP/kAHomP => [s_id x xE|s_id _/memv_imgP[x xE ->]]; last first. by rewrite map_ahomE s_id. -apply: (fmorph_inj [rmorphism of iota]). +apply: (fmorph_inj iota). by rewrite /= -map_ahomE s_id// memv_img. Qed. @@ -523,7 +525,7 @@ Proof. by rewrite !inE map_ahom_kAut. Qed. Lemma map_ahom_kEnd_img s : map_ahom s \in kAEnd 1 (iota @: {: L})%AS. Proof. rewrite inE -(aimg1 iota) map_ahom_kAut// kAutfE. -exact/kHom_lrmorphism/ahom_is_lrmorphism. +exact/kHom_lrmorphism/ahom_is_multiplicative. Qed. End map_ahom. @@ -672,7 +674,7 @@ Implicit Types (K E F : {subfield L}). Lemma separable_aimgr E F s : s \in kAEndf E -> separable E (s @: F) = separable E F. Proof. -rewrite inE => /kHom_kAut_sub/kAHomP s_id; rewrite -(separable_aimg _ _ s). +rewrite inE => /kHom_kAut_sub/kAHomP s_id; rewrite -[RHS](separable_aimg _ _ s). suff /eq_in_limg->: {in E, s =1 \1%VF} by rewrite lim1g. by move=> x xE; rewrite lfunE/= s_id. Qed. @@ -773,7 +775,8 @@ Lemma solvable_ext_refl E : solvable_ext E E. Proof. by apply/solvable_extP; exists E; rewrite subvv galois_refl/= galvv solvable1. Qed. -#[local] Hint Resolve solvable_ext_refl : core. +#[local] Hint Extern 0 (is_true (solvable_ext (asval _) (asval _))) => + (apply: solvable_ext_refl) : core. Lemma sub_solvable_ext F K E : (E <= F)%VS -> solvable_ext K F -> solvable_ext K E. @@ -837,10 +840,13 @@ Qed. End normalClosure. -#[global] Hint Resolve normalClosureSl : core. -#[global] Hint Resolve normalClosureSr : core. +#[global] Hint Extern 0 (is_true (subsetv (asval _) (normalClosure _ _))) => + (apply: normalClosureSl) : core. +#[global] Hint Extern 0 (is_true (subsetv (asval _) (normalClosure _ _))) => + (apply: normalClosureSr) : core. #[global] Hint Resolve normalClosure_normal : core. -#[global] Hint Resolve solvable_ext_refl : core. +#[global] Hint Extern 0 (is_true (solvable_ext (asval _) (asval _))) => + (apply: solvable_ext_refl) : core. Lemma aimg_normalClosure (F0 : fieldType) (L L' : splittingFieldType F0) (iota : 'AHom(L, L')) (K E : {subfield L}) : diff --git a/theories/xmathcomp/various.v b/theories/xmathcomp/various.v index 1702e11..a064fcc 100644 --- a/theories/xmathcomp/various.v +++ b/theories/xmathcomp/various.v @@ -1,3 +1,4 @@ +From HB Require Import structures. From mathcomp Require Import all_ssreflect all_fingroup all_algebra all_solvable. From mathcomp Require Import all_field. @@ -160,11 +161,8 @@ Proof. by move=> x; apply/ffunP => i; rewrite !ffunE mulVg. Qed. Lemma extnprod_mulgA : associative extnprod_mulg. Proof. by move=> x y z; apply/ffunP => i; rewrite !ffunE mulgA. Qed. -Definition extnprod_groupMixin := - Eval hnf in FinGroup.Mixin extnprod_mulgA extnprod_mul1g extnprod_mulVg. -Canonical extnprod_baseFinGroupType := - Eval hnf in BaseFinGroupType gTn extnprod_groupMixin. -Canonical prod_group := FinGroupType extnprod_mulVg. +HB.instance Definition _ := isMulGroup.Build gTn + extnprod_mulgA extnprod_mul1g extnprod_mulVg. End ExternalNDirProd. @@ -288,9 +286,9 @@ Section ssrnum. Import Num.Theory. Lemma CrealJ (C : numClosedFieldType) : - {mono (@conjC C) : x / x \is Num.real}. + {mono (@Num.conj_op C) : x / x \is Num.real}. Proof. -suff realK : {homo (@conjC C) : x / x \is Num.real}. +suff realK : {homo (@Num.conj_op C) : x / x \is Num.real}. by move=> x; apply/idP/idP => /realK//; rewrite conjCK. by move=> x xreal; rewrite conj_Creal. Qed. @@ -344,12 +342,12 @@ Lemma map_polyXsubC (aR rR : ringType) (f : {rmorphism aR -> rR}) x : map_poly f ('X - x%:P) = 'X - (f x)%:P. Proof. by rewrite rmorphB/= map_polyX map_polyC. Qed. -Lemma poly_XsubC_over {R : ringType} c (S : {pred R}) (addS : subringPred S) - (kS : keyed_pred addS): c \in kS -> 'X - c%:P \is a polyOver kS. +Lemma poly_XsubC_over {R : ringType} c (S : subringClosed R) : + c \in S -> 'X - c%:P \is a polyOver S. Proof. by move=> cS; rewrite rpredB ?polyOverC ?polyOverX. Qed. -Lemma poly_XnsubC_over {R : ringType} n c (S : {pred R}) (addS : subringPred S) - (kS : keyed_pred addS): c \in kS -> 'X^n - c%:P \is a polyOver kS. +Lemma poly_XnsubC_over {R : ringType} n c (S : subringClosed R) : + c \in S -> 'X^n - c%:P \is a polyOver S. Proof. by move=> cS; rewrite rpredB ?rpredX ?polyOverX ?polyOverC. Qed. Lemma lead_coef_prod {R : idomainType} (ps : seq {poly R}) : @@ -382,17 +380,17 @@ by rewrite rmorph_prod big_map; apply/eq_bigr => x /=; rewrite map_polyXsubC. Qed. Lemma eq_in_map_poly_id0 (aR rR : ringType) (f g : aR -> rR) - (S0 : {pred aR}) (addS : addrPred S0) (kS : keyed_pred addS) : + (S : addrClosed aR) : f 0 = 0 -> g 0 = 0 -> - {in kS, f =1 g} -> {in polyOver kS, map_poly f =1 map_poly g}. + {in S, f =1 g} -> {in polyOver S, map_poly f =1 map_poly g}. Proof. move=> f0 g0 eq_fg p pP; apply/polyP => i. by rewrite !coef_map_id0// eq_fg// (polyOverP _). Qed. Lemma eq_in_map_poly (aR rR : ringType) (f g : {additive aR -> rR}) - (S0 : {pred aR}) (addS : addrPred S0) (kS : keyed_pred addS) : - {in kS, f =1 g} -> {in polyOver kS, map_poly f =1 map_poly g}. + (S : addrClosed aR) : + {in S, f =1 g} -> {in polyOver S, map_poly f =1 map_poly g}. Proof. by move=> /eq_in_map_poly_id0; apply; rewrite //?raddf0. Qed. Lemma mapf_root (F : fieldType) (R : ringType) (f : {rmorphism F -> R}) @@ -404,7 +402,7 @@ Section multiplicity. Variable (L : fieldType). Definition mup (x : L) (p : {poly L}) := - [arg max_(n > 0 : 'I_(size p).+1 | ('X - x%:P) ^+ n %| p) n] : nat. + [arg max_(n > (0 : 'I_(size p).+1) | ('X - x%:P) ^+ n %| p) n] : nat. Lemma mup_geq x q n : q != 0 -> (n <= mup x q)%N = (('X - x%:P) ^+ n %| q). Proof. @@ -590,7 +588,7 @@ Proof. by apply/val_inj; rewrite /= vsprojK. Qed. (* falgebra *) (************) -Lemma adjoin_cat (K : fieldType) (aT : FalgType K) (V : {vspace aT}) +Lemma adjoin_cat (K : fieldType) (aT : falgType K) (V : {vspace aT}) (rs1 rs2 : seq aT) : <>%VS = <<<> & rs2>>%VS. Proof. @@ -599,14 +597,14 @@ elim: rs1 => /= [|r rs1 ih] in V *. - by rewrite !adjoin_cons ih. Qed. -Lemma eq_adjoin (K : fieldType) (aT : FalgType K) (U : {vspace aT}) +Lemma eq_adjoin (K : fieldType) (aT : falgType K) (U : {vspace aT}) (rs1 rs2 : seq aT) : rs1 =i rs2 -> <>%VS = <>%VS. Proof. by move=> rs12; apply/eqP; rewrite eqEsubv !adjoin_seqSr// => x; rewrite rs12. Qed. -Lemma memv_mulP (K : fieldType) (aT : FalgType K) (U V : {vspace aT}) w : +Lemma memv_mulP (K : fieldType) (aT : falgType K) (U V : {vspace aT}) w : reflect (exists n (us vs : n.-tuple aT), [/\ all (mem U) us, all (mem V) vs & w = \sum_(i < n) tnth us i * tnth vs i]) @@ -626,7 +624,7 @@ by apply: eq_bigr => i; rewrite !tnth_map/= tnth_ord_tuple; case: sig2_eqW. Qed. Lemma big_prodv_seqP (I : eqType) (r : seq I) (P : {pred I}) - (K : fieldType) (aT : FalgType K) (U : {vspace aT}) + (K : fieldType) (aT : falgType K) (U : {vspace aT}) (V : I -> {vspace aT}) (W : {vspace aT}) : uniq r -> reflect (forall u (v : I -> aT), u \in U -> (forall i, P i -> v i \in V i) -> \big[*%R/u]_(i <- r | P i) v i \in W) @@ -728,31 +726,27 @@ Arguments prodv_idPr {F0 L K F}. Section canonicals. Variables (F0 : fieldType) (L : fieldExtType F0). -Lemma vsproj_is_lrmorphism : lrmorphism (vsproj {:L}). -Proof. -split; last exact/linearZZ. -split; first exact/raddfB. +Lemma vsproj_is_multiplicative : multiplicative (vsproj {:L}). by split => [v w|]; apply/val_inj; rewrite /= !vsprojK ?memvf ?algid1. Qed. -Canonical vsproj_lrmorphism := LRMorphism vsproj_is_lrmorphism. -Canonical vsproj_rmorphism := RMorphism vsproj_is_lrmorphism. +HB.instance Definition _ := + GRing.isMultiplicative.Build L (subvs_of {:L}) (vsproj {:L}) + vsproj_is_multiplicative. Definition vssub (k K : {vspace L}) of (k <= K)%VS : subvs_of k -> subvs_of K := vsproj _ \o vsval. Variables (k K : {subfield L}) (kK : (k <= K)%VS). -Lemma vssub_is_lrmorphism : lrmorphism (vssub kK). -split; last exact/linearZZ. -split; first exact/raddfB. +Lemma vssub_is_multiplicative : multiplicative (vssub kK). split => [v w|]; apply/val_inj => /=; last first. by rewrite vsprojK ?algid1 ?rmorph1 ?rpred1//. by rewrite /= !vsprojK/= ?rpredM//= (subvP kK _ (subvsP _)) . Qed. -Canonical vssub_additive := Additive vssub_is_lrmorphism. -Canonical vssub_linear := Linear vssub_is_lrmorphism. -Canonical vssub_rmorphism := RMorphism vssub_is_lrmorphism. -Canonical vssub_lrmorphism := LRMorphism vssub_is_lrmorphism. +HB.instance Definition _ := GRing.Linear.on (vssub kK). +HB.instance Definition _ := + GRing.isMultiplicative.Build (subvs_of k) (subvs_of K) (vssub kK) + vssub_is_multiplicative. Lemma vsval_sub (v : subvs_of k) : vsval (vssub kK v) = vsval v. Proof. by rewrite vsprojK// (subvP kK)// subvsP. Qed. @@ -766,26 +760,35 @@ Lemma splitting_ahom (F0 : fieldType) (L L' : fieldExtType F0) {iota : 'AHom(L, L') | limg iota = E'}. Proof. do [suff init (p : {poly L}) (k : {subfield L}) - (K := [FalgType F0 of subvs_of k]) (f : 'AHom(K, L')) : + (K := subvs_of k : falgType F0) (f : 'AHom(K, L')) : p \is a polyOver k -> splittingFieldFor k p fullv -> splittingFieldFor (limg f) (p ^^ (f \o vsproj k)) E' -> {g : 'AHom(L, L') | limg g = E'}] in p *. - move=> pf pE'; pose K := [FalgType F0 of subvs_of (1%VS : {vspace L})]. + move=> pf pE'; pose K : falgType F0 := subvs_of (1%VS : {vspace L}). have [idF0 idF0E] : {f : 'AHom(K, L') | forall x : F0, f x%:A = x%:A}. - have flr : lrmorphism - (fun v : K => in_alg L' (projT1 (sig_eqW (vlineP _ _ (valP v))))). - do ![split] => [? ?|? ?||a ?]/=. - - case: sig_eqW => x; case: sig_eqW => /= v->; case: sig_eqW => /= w->. - by rewrite -!in_algE -raddfB => /fmorph_inj<-//; rewrite raddfB. + pose f (v : K) := in_alg L' (projT1 (sig_eqW (vlineP _ _ (valP v)))). + have fa : additive f. + move=> ? ?; rewrite /f. + case: sig_eqW => x; case: sig_eqW => /= v->; case: sig_eqW => /= w->. + by rewrite -!in_algE -raddfB => /fmorph_inj<-//; rewrite raddfB. + have fm : multiplicative f. + split=> [? ?|]; rewrite /f. - case: sig_eqW => x; case: sig_eqW => /= v->; case: sig_eqW => /= w->. by rewrite -!in_algE -rmorphM => /fmorph_inj<-//; rewrite rmorphM. - case: sig_eqW => /= one /esym/eqP; rewrite algid1. - by rewrite -in_algE fmorph_eq1 => /eqP->; rewrite scale1r. - - case: sig_eqW => x; case: sig_eqW => /= v->. - rewrite -mulr_algl -in_algE -rmorphM => /fmorph_inj<-. - by rewrite -in_algE rmorphM mulr_algl. - exists (linfun_ahom (LRMorphism flr)) => v; rewrite lfunE/=. - by case: sig_eqW => /= x; rewrite algid1 -in_algE => /fmorph_inj->. + by rewrite -[X in X == _]in_algE fmorph_eq1 => /eqP->; rewrite scale1r. + have fl : scalable f. + move=> a ? /=; rewrite /f. + case: sig_eqW => x; case: sig_eqW => /= v->. + rewrite -[_ *: _]mulr_algl -in_algE -rmorphM => /fmorph_inj<-. + by rewrite -in_algE rmorphM mulr_algl. + pose faM := GRing.isAdditive.Build _ _ _ fa. + pose fmM := GRing.isMultiplicative.Build _ _ _ fm. + pose flM := GRing.isScalable.Build _ _ _ _ _ fl. + pose fLRM : {lrmorphism _ -> _} := HB.pack f faM fmM flM. + exists (linfun_ahom fLRM) => v; rewrite lfunE/= /f. + case: sig_eqW => /= x. + by rewrite algid1 -[in X in X -> _]in_algE => /fmorph_inj->. apply: (init (p ^^ in_alg L) 1%AS idF0) => //. by apply/polyOver1P; exists p. suff -> : limg idF0 = 1%VS. @@ -803,11 +806,11 @@ move=> /sig2_eqW[rs prs rsf] /sig2_eqW [rs' prs' <-]{E'}; apply/sig_eqW. elim: rs => [|x rs IHrs]//= in k @K f p rs' prs rsf prs' *. rewrite ?Fadjoin_nil ?big_nil/= in rsf prs. move=> /(@val_inj _ _ _ k) in rsf; rewrite {k}rsf in K f p prs prs' *. - have: p %= 1 by rewrite -(eqp_map [rmorphism of vsval]) rmorph1. - rewrite -(eqp_map [rmorphism of f]) rmorph1 (eqp_ltrans prs')//. + have: p %= 1 by rewrite -(eqp_map vsval) rmorph1. + rewrite -(eqp_map f) rmorph1 (eqp_ltrans prs')//. move=> /eqp_size; rewrite size_prod_XsubC size_poly1 => -[]. case: {+}rs' => // _; rewrite Fadjoin_nil/=. - exists (linfun_ahom [lrmorphism of f \o vsproj _]). + exists (linfun_ahom (f \o vsproj _)). apply/vspaceP => v; apply/memv_imgP/memv_imgP => -[u _ ->]/=. by exists (vsproj fullv u); rewrite ?memvf//= lfunE/=. by exists (val u); rewrite ?memvf//= lfunE/= ?vsvalK. @@ -816,7 +819,7 @@ have [xk|xNk] := boolP (x \in k). rewrite adjoin_cons (Fadjoin_idP _) ?subvsP//= in rsf. have xrs' : f x \in rs'. rewrite -root_prod_XsubC -(eqp_root prs') mapf_root. - rewrite -(mapf_root [lrmorphism of vsval]) (eqp_root prs). + rewrite -(mapf_root vsval) (eqp_root prs). by rewrite root_prod_XsubC mem_head. have -> : <>%VS = <>%VS. rewrite (eq_adjoin _ (perm_mem (perm_to_rem xrs'))). @@ -838,7 +841,7 @@ have size_q : (size q > 1)%N. have [x' x'rs qx'0] : exists2 x', x' \in rs' & root (q ^^ f) x'. have : q ^^ vsval %| p ^^ vsval. by rewrite -eq_q minPoly_dvdp//; apply/polyOver_subvs; exists p. - rewrite dvdp_map -(dvdp_map [rmorphism of f]) (eqp_dvdr _ prs'). + rewrite dvdp_map -(dvdp_map f) (eqp_dvdr _ prs'). move=> /dvdp_prod_XsubC[m]; rewrite eqp_monic ?map_monic ?monic_prod_XsubC//. move=> /eqP; case rs'_eq : mask => [|x' rs'x]. move=> /(congr1 (psize _))/=. @@ -847,7 +850,7 @@ have [x' x'rs qx'0] : exists2 x', x' \in rs' & root (q ^^ f) x'. by rewrite (@mem_mask _ _ m)// rs'_eq mem_head. by rewrite q_eq rootE !hornerE subrr mul0r. have rpx' : root (p ^^ f) x' by rewrite (eqp_root prs') root_prod_XsubC. -pose Kx := [fieldExtType F0 of subvs_of <>]. +pose Kx : fieldExtType F0 := subvs_of <>. pose mpsI := map_inj_poly subvs_inj (rmorph0 _). pose x0 := Subvs (memv_adjoin k x). pose KKx := vssub (subv_adjoin k x). @@ -888,15 +891,21 @@ have polM (v w : Kx) : pol (val v * val w) = pol (val v) * pol (val w) %% q. - by rewrite -ltnS -size_minPoly ltn_modp ?monic_neq0 ?monic_minPoly//. rewrite -Fadjoin_poly_mod ?rpredM ?Fadjoin_polyOver//. by rewrite hornerM !Fadjoin_poly_eq//= ?rpredM ?subvsP. -have hlr : lrmorphism (fun v : Kx => (pol (val v) ^^ f).[x']). - do ![split] => [v w|v w||w v]/=. - - by rewrite -raddfB/= polB raddfB !hornerE. - - by rewrite -rmorphM/= polM map_modp/= horner_mod// rmorphM hornerE. - - by rewrite algid1 pol1 rmorph1 hornerE. - - by rewrite polZ linearZ/= rmorph_alg hornerE mulr_algl. -pose h := linfun_ahom (LRMorphism hlr). -exists h; first by rewrite lfunE/= polX map_polyX hornerX. -by move=> v; rewrite /comp lfunE/= vsval_sub/= polC map_polyC hornerC. +pose h (v : Kx) := (pol (val v) ^^ f).[x']. +have ha : additive h. + by move=> v w; rewrite /h/= -raddfB/= polB raddfB !hornerE. +have hm : multiplicative h. + split=> [v w|]. + - by rewrite /h /= -rmorphM/= polM map_modp/= horner_mod// rmorphM hornerE. + - by rewrite /h /= algid1 pol1 rmorph1 hornerE. +have hl : scalable h. + by move=> ? ?; rewrite /h /= polZ linearZ/= rmorph_alg hornerE mulr_algl. +pose haM := GRing.isAdditive.Build _ _ _ ha. +pose hmM := GRing.isMultiplicative.Build _ _ _ hm. +pose hlM := GRing.isScalable.Build _ _ _ _ _ hl. +pose hLRM : {lrmorphism _ -> _} := HB.pack h haM hmM hlM. +exists (linfun_ahom hLRM); first by rewrite lfunE/= /h polX map_polyX hornerX. +by move=> v; rewrite /comp lfunE/= /h/= vsval_sub/= polC map_polyC hornerC. Qed. Lemma lker0_img_cap (K : fieldType) (aT rT : vectType K) (f : 'Hom(aT, rT)) @@ -1108,7 +1117,9 @@ Lemma sol_setXn n (gT : 'I_n -> finGroupType) (G : forall i, {group gT i}) : Proof. elim: n => [|n IHn] in gT G * => solG; first by rewrite setX0 solvable1. pose gT' (i : 'I_n) := gT (lift ord0 i). -pose f (x : prod_group gT) : prod_group gT' := [ffun i => x (lift ord0 i)]. +pose prod_group_gT := [the finGroupType of {dffun forall i, gT i}]. +pose prod_group_gT' := [the finGroupType of {dffun forall i, gT' i}]. +pose f (x : prod_group_gT) : prod_group_gT' := [ffun i => x (lift ord0 i)]. have fm : morphic (setXn G) f. apply/'forall_implyP => -[a b]; rewrite !inE/=. by move=> /andP[/forallP aG /forallP bG]; apply/eqP/ffunP => i; rewrite !ffunE. @@ -1119,8 +1130,8 @@ have -> : (morphm fm @* setXn G)%g = setXn (fun i => G (lift ord0 i)). move=> /imsetP[/=x]; rewrite inE => /forallP/= xG ->. by move=> i; rewrite morphmE ffunE xG. move=> vG; apply/imsetP. - pose w : prod_group gT := [ffun i : 'I_n.+1 => - match unliftP ord0 i with + pose w := [ffun i : 'I_n.+1 => + match unliftP ord0 i return (gT i) : Type with | UnliftSome j i_eq => ecast i (gT i) (esym i_eq) (v j) | UnliftNone i0 => 1%g end]. @@ -1133,8 +1144,12 @@ have -> : (morphm fm @* setXn G)%g = setXn (fun i => G (lift ord0 i)). rewrite inE; apply/forallP => i. by case: (unliftP ord0 i) => [j|]->; rewrite ?wl ?w0 ?vG. rewrite IHn ?andbT//; last by move=> i; apply: solG. -pose k (x : gT ord0) : prod_group gT := - [ffun i : 'I_n.+1 => if (ord0 =P i) is ReflectT P then ecast i (gT i) P x else 1%g]. +pose k (x : gT ord0) : prod_group_gT := + [ffun i : 'I_n.+1 => + match (ord0 =P i) return (gT i) : Type with + | ReflectT P => ecast i (gT i) P x + | _ => 1%g + end]. have km : morphic (G ord0) k. apply/'forall_implyP => -[a b]; rewrite !inE/= => /andP[aG bG]. apply/eqP/ffunP => i; rewrite !ffunE; case: eqP => //; rewrite ?mulg1//. From 779f085df206314c7a00a0ee37c522e2c05d6eb9 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 11 May 2023 16:46:24 +0200 Subject: [PATCH 2/3] [CI] Update Nix --- .../workflows/nix-action-coq8.12+mc1.13.yml | 99 -------- .../workflows/nix-action-coq8.13+mc1.13.yml | 99 -------- .../workflows/nix-action-coq8.13+mc1.14.yml | 99 -------- .../workflows/nix-action-coq8.13+mcmaster.yml | 211 ----------------- .../workflows/nix-action-coq8.14+mc1.13.yml | 99 -------- .../workflows/nix-action-coq8.14+mc1.14.yml | 99 -------- .../workflows/nix-action-coq8.14+mcmaster.yml | 211 ----------------- .../workflows/nix-action-coq8.15+mc1.14.yml | 99 -------- .../workflows/nix-action-coq8.15+mcmaster.yml | 211 ----------------- .../nix-action-coq8.16+mcmathcomp-1.15.0.yml | 213 ----------------- ...> nix-action-coq8.16+mcmathcomp-2.1.0.yml} | 154 +++++++----- ...> nix-action-coq8.17+mcmathcomp-2.1.0.yml} | 154 +++++++----- ...> nix-action-coq8.18+mcmathcomp-2.1.0.yml} | 154 +++++++----- .../nix-action-coqmaster+mcmaster.yml | 219 +++++++++++++++--- .nix/config.nix | 11 +- .nix/coq-nix-toolbox.nix | 2 +- 16 files changed, 491 insertions(+), 1643 deletions(-) delete mode 100644 .github/workflows/nix-action-coq8.12+mc1.13.yml delete mode 100644 .github/workflows/nix-action-coq8.13+mc1.13.yml delete mode 100644 .github/workflows/nix-action-coq8.13+mc1.14.yml delete mode 100644 .github/workflows/nix-action-coq8.13+mcmaster.yml delete mode 100644 .github/workflows/nix-action-coq8.14+mc1.13.yml delete mode 100644 .github/workflows/nix-action-coq8.14+mc1.14.yml delete mode 100644 .github/workflows/nix-action-coq8.14+mcmaster.yml delete mode 100644 .github/workflows/nix-action-coq8.15+mc1.14.yml delete mode 100644 .github/workflows/nix-action-coq8.15+mcmaster.yml delete mode 100644 .github/workflows/nix-action-coq8.16+mcmathcomp-1.15.0.yml rename .github/workflows/{nix-action-coq8.13+mcmathcomp-1.15.0.yml => nix-action-coq8.16+mcmathcomp-2.1.0.yml} (57%) rename .github/workflows/{nix-action-coq8.15+mcmathcomp-1.15.0.yml => nix-action-coq8.17+mcmathcomp-2.1.0.yml} (57%) rename .github/workflows/{nix-action-coq8.14+mcmathcomp-1.15.0.yml => nix-action-coq8.18+mcmathcomp-2.1.0.yml} (57%) diff --git a/.github/workflows/nix-action-coq8.12+mc1.13.yml b/.github/workflows/nix-action-coq8.12+mc1.13.yml deleted file mode 100644 index de0e66b..0000000 --- a/.github/workflows/nix-action-coq8.12+mc1.13.yml +++ /dev/null @@ -1,99 +0,0 @@ -jobs: - coq: - needs: [] - runs-on: ubuntu-latest - steps: - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v2 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v16 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target coq - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.12+mc1.13\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.12+mc1.13" - --argstr job "coq" - mathcomp-abel: - needs: - - coq - runs-on: ubuntu-latest - steps: - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v2 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v16 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target mathcomp-abel - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.12+mc1.13\" --argstr job \"mathcomp-abel\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.12+mc1.13" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.12+mc1.13" - --argstr job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-real-closed' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.12+mc1.13" - --argstr job "mathcomp-real-closed" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.12+mc1.13" - --argstr job "mathcomp-abel" -name: Nix CI for bundle coq8.12+mc1.13 -'on': - pull_request: - paths: - - .github/workflows/** - pull_request_target: - types: - - opened - - synchronize - - reopened - push: - branches: - - master diff --git a/.github/workflows/nix-action-coq8.13+mc1.13.yml b/.github/workflows/nix-action-coq8.13+mc1.13.yml deleted file mode 100644 index b80478c..0000000 --- a/.github/workflows/nix-action-coq8.13+mc1.13.yml +++ /dev/null @@ -1,99 +0,0 @@ -jobs: - coq: - needs: [] - runs-on: ubuntu-latest - steps: - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v2 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v16 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target coq - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.13+mc1.13\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mc1.13" - --argstr job "coq" - mathcomp-abel: - needs: - - coq - runs-on: ubuntu-latest - steps: - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v2 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v16 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target mathcomp-abel - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.13+mc1.13\" --argstr job \"mathcomp-abel\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mc1.13" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mc1.13" - --argstr job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-real-closed' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mc1.13" - --argstr job "mathcomp-real-closed" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mc1.13" - --argstr job "mathcomp-abel" -name: Nix CI for bundle coq8.13+mc1.13 -'on': - pull_request: - paths: - - .github/workflows/** - pull_request_target: - types: - - opened - - synchronize - - reopened - push: - branches: - - master diff --git a/.github/workflows/nix-action-coq8.13+mc1.14.yml b/.github/workflows/nix-action-coq8.13+mc1.14.yml deleted file mode 100644 index 2d7e934..0000000 --- a/.github/workflows/nix-action-coq8.13+mc1.14.yml +++ /dev/null @@ -1,99 +0,0 @@ -jobs: - coq: - needs: [] - runs-on: ubuntu-latest - steps: - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v2 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v16 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target coq - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.13+mc1.14\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mc1.14" - --argstr job "coq" - mathcomp-abel: - needs: - - coq - runs-on: ubuntu-latest - steps: - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v2 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v16 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target mathcomp-abel - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.13+mc1.14\" --argstr job \"mathcomp-abel\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mc1.14" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mc1.14" - --argstr job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-real-closed' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mc1.14" - --argstr job "mathcomp-real-closed" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mc1.14" - --argstr job "mathcomp-abel" -name: Nix CI for bundle coq8.13+mc1.14 -'on': - pull_request: - paths: - - .github/workflows/** - pull_request_target: - types: - - opened - - synchronize - - reopened - push: - branches: - - master diff --git a/.github/workflows/nix-action-coq8.13+mcmaster.yml b/.github/workflows/nix-action-coq8.13+mcmaster.yml deleted file mode 100644 index 7db6988..0000000 --- a/.github/workflows/nix-action-coq8.13+mcmaster.yml +++ /dev/null @@ -1,211 +0,0 @@ -jobs: - coq: - needs: [] - runs-on: ubuntu-latest - steps: - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v2 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v16 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target coq - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.13+mcmaster\" --argstr job \"coq\" \\\n --dry-run 2>&1 >\ - \ /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ - \ | grep \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mcmaster" - --argstr job "coq" - mathcomp-abel: - needs: - - coq - - mathcomp-real-closed - runs-on: ubuntu-latest - steps: - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v2 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v16 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target mathcomp-abel - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.13+mcmaster\" --argstr job \"mathcomp-abel\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mcmaster" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mcmaster" - --argstr job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-real-closed' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mcmaster" - --argstr job "mathcomp-real-closed" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mcmaster" - --argstr job "mathcomp-abel" - mathcomp-bigenough: - needs: - - coq - runs-on: ubuntu-latest - steps: - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v2 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v16 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target mathcomp-bigenough - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.13+mcmaster\" --argstr job \"mathcomp-bigenough\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mcmaster" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mcmaster" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mcmaster" - --argstr job "mathcomp-bigenough" - mathcomp-real-closed: - needs: - - coq - - mathcomp-bigenough - runs-on: ubuntu-latest - steps: - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v2 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v16 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target mathcomp-real-closed - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.13+mcmaster\" --argstr job \"mathcomp-real-closed\" \\\n \ - \ --dry-run 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mcmaster" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mcmaster" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mcmaster" - --argstr job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mcmaster" - --argstr job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mcmaster" - --argstr job "mathcomp-fingroup" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-solvable' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mcmaster" - --argstr job "mathcomp-solvable" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mcmaster" - --argstr job "mathcomp-bigenough" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mcmaster" - --argstr job "mathcomp-real-closed" -name: Nix CI for bundle coq8.13+mcmaster -'on': - pull_request: - paths: - - .github/workflows/** - pull_request_target: - types: - - opened - - synchronize - - reopened - push: - branches: - - master diff --git a/.github/workflows/nix-action-coq8.14+mc1.13.yml b/.github/workflows/nix-action-coq8.14+mc1.13.yml deleted file mode 100644 index 4a65c92..0000000 --- a/.github/workflows/nix-action-coq8.14+mc1.13.yml +++ /dev/null @@ -1,99 +0,0 @@ -jobs: - coq: - needs: [] - runs-on: ubuntu-latest - steps: - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v2 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v16 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target coq - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.14+mc1.13\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mc1.13" - --argstr job "coq" - mathcomp-abel: - needs: - - coq - runs-on: ubuntu-latest - steps: - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v2 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v16 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target mathcomp-abel - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.14+mc1.13\" --argstr job \"mathcomp-abel\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mc1.13" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mc1.13" - --argstr job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-real-closed' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mc1.13" - --argstr job "mathcomp-real-closed" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mc1.13" - --argstr job "mathcomp-abel" -name: Nix CI for bundle coq8.14+mc1.13 -'on': - pull_request: - paths: - - .github/workflows/** - pull_request_target: - types: - - opened - - synchronize - - reopened - push: - branches: - - master diff --git a/.github/workflows/nix-action-coq8.14+mc1.14.yml b/.github/workflows/nix-action-coq8.14+mc1.14.yml deleted file mode 100644 index be90fa9..0000000 --- a/.github/workflows/nix-action-coq8.14+mc1.14.yml +++ /dev/null @@ -1,99 +0,0 @@ -jobs: - coq: - needs: [] - runs-on: ubuntu-latest - steps: - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v2 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v16 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target coq - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.14+mc1.14\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mc1.14" - --argstr job "coq" - mathcomp-abel: - needs: - - coq - runs-on: ubuntu-latest - steps: - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v2 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v16 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target mathcomp-abel - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.14+mc1.14\" --argstr job \"mathcomp-abel\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mc1.14" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mc1.14" - --argstr job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-real-closed' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mc1.14" - --argstr job "mathcomp-real-closed" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mc1.14" - --argstr job "mathcomp-abel" -name: Nix CI for bundle coq8.14+mc1.14 -'on': - pull_request: - paths: - - .github/workflows/** - pull_request_target: - types: - - opened - - synchronize - - reopened - push: - branches: - - master diff --git a/.github/workflows/nix-action-coq8.14+mcmaster.yml b/.github/workflows/nix-action-coq8.14+mcmaster.yml deleted file mode 100644 index 4583664..0000000 --- a/.github/workflows/nix-action-coq8.14+mcmaster.yml +++ /dev/null @@ -1,211 +0,0 @@ -jobs: - coq: - needs: [] - runs-on: ubuntu-latest - steps: - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v2 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v16 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target coq - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.14+mcmaster\" --argstr job \"coq\" \\\n --dry-run 2>&1 >\ - \ /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ - \ | grep \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mcmaster" - --argstr job "coq" - mathcomp-abel: - needs: - - coq - - mathcomp-real-closed - runs-on: ubuntu-latest - steps: - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v2 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v16 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target mathcomp-abel - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.14+mcmaster\" --argstr job \"mathcomp-abel\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mcmaster" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mcmaster" - --argstr job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-real-closed' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mcmaster" - --argstr job "mathcomp-real-closed" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mcmaster" - --argstr job "mathcomp-abel" - mathcomp-bigenough: - needs: - - coq - runs-on: ubuntu-latest - steps: - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v2 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v16 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target mathcomp-bigenough - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.14+mcmaster\" --argstr job \"mathcomp-bigenough\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mcmaster" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mcmaster" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mcmaster" - --argstr job "mathcomp-bigenough" - mathcomp-real-closed: - needs: - - coq - - mathcomp-bigenough - runs-on: ubuntu-latest - steps: - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v2 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v16 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target mathcomp-real-closed - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.14+mcmaster\" --argstr job \"mathcomp-real-closed\" \\\n \ - \ --dry-run 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mcmaster" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mcmaster" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mcmaster" - --argstr job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mcmaster" - --argstr job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mcmaster" - --argstr job "mathcomp-fingroup" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-solvable' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mcmaster" - --argstr job "mathcomp-solvable" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mcmaster" - --argstr job "mathcomp-bigenough" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mcmaster" - --argstr job "mathcomp-real-closed" -name: Nix CI for bundle coq8.14+mcmaster -'on': - pull_request: - paths: - - .github/workflows/** - pull_request_target: - types: - - opened - - synchronize - - reopened - push: - branches: - - master diff --git a/.github/workflows/nix-action-coq8.15+mc1.14.yml b/.github/workflows/nix-action-coq8.15+mc1.14.yml deleted file mode 100644 index 2dafc21..0000000 --- a/.github/workflows/nix-action-coq8.15+mc1.14.yml +++ /dev/null @@ -1,99 +0,0 @@ -jobs: - coq: - needs: [] - runs-on: ubuntu-latest - steps: - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v2 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v16 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target coq - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.15+mc1.14\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.15+mc1.14" - --argstr job "coq" - mathcomp-abel: - needs: - - coq - runs-on: ubuntu-latest - steps: - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v2 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v16 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target mathcomp-abel - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.15+mc1.14\" --argstr job \"mathcomp-abel\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.15+mc1.14" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.15+mc1.14" - --argstr job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-real-closed' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.15+mc1.14" - --argstr job "mathcomp-real-closed" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.15+mc1.14" - --argstr job "mathcomp-abel" -name: Nix CI for bundle coq8.15+mc1.14 -'on': - pull_request: - paths: - - .github/workflows/** - pull_request_target: - types: - - opened - - synchronize - - reopened - push: - branches: - - master diff --git a/.github/workflows/nix-action-coq8.15+mcmaster.yml b/.github/workflows/nix-action-coq8.15+mcmaster.yml deleted file mode 100644 index bfff4ca..0000000 --- a/.github/workflows/nix-action-coq8.15+mcmaster.yml +++ /dev/null @@ -1,211 +0,0 @@ -jobs: - coq: - needs: [] - runs-on: ubuntu-latest - steps: - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v2 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v16 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target coq - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.15+mcmaster\" --argstr job \"coq\" \\\n --dry-run 2>&1 >\ - \ /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ - \ | grep \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.15+mcmaster" - --argstr job "coq" - mathcomp-abel: - needs: - - coq - - mathcomp-real-closed - runs-on: ubuntu-latest - steps: - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v2 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v16 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target mathcomp-abel - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.15+mcmaster\" --argstr job \"mathcomp-abel\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.15+mcmaster" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.15+mcmaster" - --argstr job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-real-closed' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.15+mcmaster" - --argstr job "mathcomp-real-closed" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.15+mcmaster" - --argstr job "mathcomp-abel" - mathcomp-bigenough: - needs: - - coq - runs-on: ubuntu-latest - steps: - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v2 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v16 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target mathcomp-bigenough - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.15+mcmaster\" --argstr job \"mathcomp-bigenough\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.15+mcmaster" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.15+mcmaster" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.15+mcmaster" - --argstr job "mathcomp-bigenough" - mathcomp-real-closed: - needs: - - coq - - mathcomp-bigenough - runs-on: ubuntu-latest - steps: - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v2 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v16 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target mathcomp-real-closed - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.15+mcmaster\" --argstr job \"mathcomp-real-closed\" \\\n \ - \ --dry-run 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.15+mcmaster" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.15+mcmaster" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.15+mcmaster" - --argstr job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.15+mcmaster" - --argstr job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.15+mcmaster" - --argstr job "mathcomp-fingroup" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-solvable' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.15+mcmaster" - --argstr job "mathcomp-solvable" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.15+mcmaster" - --argstr job "mathcomp-bigenough" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.15+mcmaster" - --argstr job "mathcomp-real-closed" -name: Nix CI for bundle coq8.15+mcmaster -'on': - pull_request: - paths: - - .github/workflows/** - pull_request_target: - types: - - opened - - synchronize - - reopened - push: - branches: - - master diff --git a/.github/workflows/nix-action-coq8.16+mcmathcomp-1.15.0.yml b/.github/workflows/nix-action-coq8.16+mcmathcomp-1.15.0.yml deleted file mode 100644 index 4b5e58f..0000000 --- a/.github/workflows/nix-action-coq8.16+mcmathcomp-1.15.0.yml +++ /dev/null @@ -1,213 +0,0 @@ -jobs: - coq: - needs: [] - runs-on: ubuntu-latest - steps: - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v2 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v16 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target coq - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.16+mcmathcomp-1.15.0\" --argstr job \"coq\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.16+mcmathcomp-1.15.0" - --argstr job "coq" - mathcomp-abel: - needs: - - coq - - mathcomp-real-closed - runs-on: ubuntu-latest - steps: - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v2 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v16 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target mathcomp-abel - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.16+mcmathcomp-1.15.0\" --argstr job \"mathcomp-abel\" \\\n\ - \ --dry-run 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.16+mcmathcomp-1.15.0" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.16+mcmathcomp-1.15.0" - --argstr job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-real-closed' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.16+mcmathcomp-1.15.0" - --argstr job "mathcomp-real-closed" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.16+mcmathcomp-1.15.0" - --argstr job "mathcomp-abel" - mathcomp-bigenough: - needs: - - coq - runs-on: ubuntu-latest - steps: - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v2 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v16 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target mathcomp-bigenough - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.16+mcmathcomp-1.15.0\" --argstr job \"mathcomp-bigenough\"\ - \ \\\n --dry-run 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output\ - \ name=status::$(echo $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\"\ - )\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.16+mcmathcomp-1.15.0" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.16+mcmathcomp-1.15.0" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.16+mcmathcomp-1.15.0" - --argstr job "mathcomp-bigenough" - mathcomp-real-closed: - needs: - - coq - - mathcomp-bigenough - runs-on: ubuntu-latest - steps: - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v2 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v16 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target mathcomp-real-closed - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.16+mcmathcomp-1.15.0\" --argstr job \"mathcomp-real-closed\"\ - \ \\\n --dry-run 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output\ - \ name=status::$(echo $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\"\ - )\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.16+mcmathcomp-1.15.0" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.16+mcmathcomp-1.15.0" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.16+mcmathcomp-1.15.0" - --argstr job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.16+mcmathcomp-1.15.0" - --argstr job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.16+mcmathcomp-1.15.0" - --argstr job "mathcomp-fingroup" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-solvable' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.16+mcmathcomp-1.15.0" - --argstr job "mathcomp-solvable" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.16+mcmathcomp-1.15.0" - --argstr job "mathcomp-bigenough" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.16+mcmathcomp-1.15.0" - --argstr job "mathcomp-real-closed" -name: Nix CI for bundle coq8.16+mcmathcomp-1.15.0 -'on': - pull_request: - paths: - - .github/workflows/** - pull_request_target: - types: - - opened - - synchronize - - reopened - push: - branches: - - master diff --git a/.github/workflows/nix-action-coq8.13+mcmathcomp-1.15.0.yml b/.github/workflows/nix-action-coq8.16+mcmathcomp-2.1.0.yml similarity index 57% rename from .github/workflows/nix-action-coq8.13+mcmathcomp-1.15.0.yml rename to .github/workflows/nix-action-coq8.16+mcmathcomp-2.1.0.yml index 0a6a5c5..39ebbdd 100644 --- a/.github/workflows/nix-action-coq8.13+mcmathcomp-1.15.0.yml +++ b/.github/workflows/nix-action-coq8.16+mcmathcomp-2.1.0.yml @@ -3,24 +3,35 @@ jobs: needs: [] runs-on: ubuntu-latest steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} - name: Determine which commit to test run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - name: Git checkout - uses: actions/checkout@v2 + uses: actions/checkout@v3 with: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v16 + uses: cachix/install-nix-action@v20 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 + uses: cachix/cachix-action@v12 with: authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} extraPullNames: coq, coq-community @@ -28,12 +39,12 @@ jobs: - id: stepCheck name: Checking presence of CI target coq run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.13+mcmathcomp-1.15.0\" --argstr job \"coq\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + \ bundle \"coq8.16+mcmathcomp-2.1.0\" --argstr job \"coq\" \\\n --dry-run\ + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.16+mcmathcomp-2.1.0" --argstr job "coq" mathcomp-abel: needs: @@ -41,24 +52,35 @@ jobs: - mathcomp-real-closed runs-on: ubuntu-latest steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} - name: Determine which commit to test run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - name: Git checkout - uses: actions/checkout@v2 + uses: actions/checkout@v3 with: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v16 + uses: cachix/install-nix-action@v20 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 + uses: cachix/cachix-action@v12 with: authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} extraPullNames: coq, coq-community @@ -66,48 +88,59 @@ jobs: - id: stepCheck name: Checking presence of CI target mathcomp-abel run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.13+mcmathcomp-1.15.0\" --argstr job \"mathcomp-abel\" \\\n\ - \ --dry-run 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + \ bundle \"coq8.16+mcmathcomp-2.1.0\" --argstr job \"mathcomp-abel\" \\\n\ + \ --dry-run 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.16+mcmathcomp-2.1.0" --argstr job "coq" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.16+mcmathcomp-2.1.0" --argstr job "mathcomp-field" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-real-closed' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.16+mcmathcomp-2.1.0" --argstr job "mathcomp-real-closed" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.16+mcmathcomp-2.1.0" --argstr job "mathcomp-abel" mathcomp-bigenough: needs: - coq runs-on: ubuntu-latest steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} - name: Determine which commit to test run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - name: Git checkout - uses: actions/checkout@v2 + uses: actions/checkout@v3 with: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v16 + uses: cachix/install-nix-action@v20 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 + uses: cachix/cachix-action@v12 with: authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} extraPullNames: coq, coq-community @@ -115,21 +148,20 @@ jobs: - id: stepCheck name: Checking presence of CI target mathcomp-bigenough run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.13+mcmathcomp-1.15.0\" --argstr job \"mathcomp-bigenough\"\ - \ \\\n --dry-run 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output\ - \ name=status::$(echo $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\"\ - )\n" + \ bundle \"coq8.16+mcmathcomp-2.1.0\" --argstr job \"mathcomp-bigenough\"\ + \ \\\n --dry-run 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.16+mcmathcomp-2.1.0" --argstr job "coq" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.16+mcmathcomp-2.1.0" --argstr job "mathcomp-ssreflect" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.16+mcmathcomp-2.1.0" --argstr job "mathcomp-bigenough" mathcomp-real-closed: needs: @@ -137,24 +169,35 @@ jobs: - mathcomp-bigenough runs-on: ubuntu-latest steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} - name: Determine which commit to test run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - name: Git checkout - uses: actions/checkout@v2 + uses: actions/checkout@v3 with: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v16 + uses: cachix/install-nix-action@v20 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 + uses: cachix/cachix-action@v12 with: authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} extraPullNames: coq, coq-community @@ -162,48 +205,49 @@ jobs: - id: stepCheck name: Checking presence of CI target mathcomp-real-closed run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.13+mcmathcomp-1.15.0\" --argstr job \"mathcomp-real-closed\"\ - \ \\\n --dry-run 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output\ - \ name=status::$(echo $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\"\ - )\n" + \ bundle \"coq8.16+mcmathcomp-2.1.0\" --argstr job \"mathcomp-real-closed\"\ + \ \\\n --dry-run 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.16+mcmathcomp-2.1.0" --argstr job "coq" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.16+mcmathcomp-2.1.0" --argstr job "mathcomp-ssreflect" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.16+mcmathcomp-2.1.0" --argstr job "mathcomp-algebra" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.16+mcmathcomp-2.1.0" --argstr job "mathcomp-field" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.16+mcmathcomp-2.1.0" --argstr job "mathcomp-fingroup" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-solvable' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.16+mcmathcomp-2.1.0" --argstr job "mathcomp-solvable" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.16+mcmathcomp-2.1.0" --argstr job "mathcomp-bigenough" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.16+mcmathcomp-2.1.0" --argstr job "mathcomp-real-closed" -name: Nix CI for bundle coq8.13+mcmathcomp-1.15.0 +name: Nix CI for bundle coq8.16+mcmathcomp-2.1.0 'on': pull_request: paths: - .github/workflows/** pull_request_target: + paths-ignore: + - .github/workflows/nix-action-coq8.16+mcmathcomp-2.1.0.yml types: - opened - synchronize diff --git a/.github/workflows/nix-action-coq8.15+mcmathcomp-1.15.0.yml b/.github/workflows/nix-action-coq8.17+mcmathcomp-2.1.0.yml similarity index 57% rename from .github/workflows/nix-action-coq8.15+mcmathcomp-1.15.0.yml rename to .github/workflows/nix-action-coq8.17+mcmathcomp-2.1.0.yml index 9e8f46a..e7214ba 100644 --- a/.github/workflows/nix-action-coq8.15+mcmathcomp-1.15.0.yml +++ b/.github/workflows/nix-action-coq8.17+mcmathcomp-2.1.0.yml @@ -3,24 +3,35 @@ jobs: needs: [] runs-on: ubuntu-latest steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} - name: Determine which commit to test run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - name: Git checkout - uses: actions/checkout@v2 + uses: actions/checkout@v3 with: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v16 + uses: cachix/install-nix-action@v20 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 + uses: cachix/cachix-action@v12 with: authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} extraPullNames: coq, coq-community @@ -28,12 +39,12 @@ jobs: - id: stepCheck name: Checking presence of CI target coq run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.15+mcmathcomp-1.15.0\" --argstr job \"coq\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + \ bundle \"coq8.17+mcmathcomp-2.1.0\" --argstr job \"coq\" \\\n --dry-run\ + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.15+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.17+mcmathcomp-2.1.0" --argstr job "coq" mathcomp-abel: needs: @@ -41,24 +52,35 @@ jobs: - mathcomp-real-closed runs-on: ubuntu-latest steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} - name: Determine which commit to test run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - name: Git checkout - uses: actions/checkout@v2 + uses: actions/checkout@v3 with: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v16 + uses: cachix/install-nix-action@v20 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 + uses: cachix/cachix-action@v12 with: authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} extraPullNames: coq, coq-community @@ -66,48 +88,59 @@ jobs: - id: stepCheck name: Checking presence of CI target mathcomp-abel run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.15+mcmathcomp-1.15.0\" --argstr job \"mathcomp-abel\" \\\n\ - \ --dry-run 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + \ bundle \"coq8.17+mcmathcomp-2.1.0\" --argstr job \"mathcomp-abel\" \\\n\ + \ --dry-run 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.15+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.17+mcmathcomp-2.1.0" --argstr job "coq" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.15+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.17+mcmathcomp-2.1.0" --argstr job "mathcomp-field" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-real-closed' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.15+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.17+mcmathcomp-2.1.0" --argstr job "mathcomp-real-closed" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.15+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.17+mcmathcomp-2.1.0" --argstr job "mathcomp-abel" mathcomp-bigenough: needs: - coq runs-on: ubuntu-latest steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} - name: Determine which commit to test run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - name: Git checkout - uses: actions/checkout@v2 + uses: actions/checkout@v3 with: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v16 + uses: cachix/install-nix-action@v20 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 + uses: cachix/cachix-action@v12 with: authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} extraPullNames: coq, coq-community @@ -115,21 +148,20 @@ jobs: - id: stepCheck name: Checking presence of CI target mathcomp-bigenough run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.15+mcmathcomp-1.15.0\" --argstr job \"mathcomp-bigenough\"\ - \ \\\n --dry-run 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output\ - \ name=status::$(echo $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\"\ - )\n" + \ bundle \"coq8.17+mcmathcomp-2.1.0\" --argstr job \"mathcomp-bigenough\"\ + \ \\\n --dry-run 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.15+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.17+mcmathcomp-2.1.0" --argstr job "coq" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.15+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.17+mcmathcomp-2.1.0" --argstr job "mathcomp-ssreflect" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.15+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.17+mcmathcomp-2.1.0" --argstr job "mathcomp-bigenough" mathcomp-real-closed: needs: @@ -137,24 +169,35 @@ jobs: - mathcomp-bigenough runs-on: ubuntu-latest steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} - name: Determine which commit to test run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - name: Git checkout - uses: actions/checkout@v2 + uses: actions/checkout@v3 with: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v16 + uses: cachix/install-nix-action@v20 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 + uses: cachix/cachix-action@v12 with: authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} extraPullNames: coq, coq-community @@ -162,48 +205,49 @@ jobs: - id: stepCheck name: Checking presence of CI target mathcomp-real-closed run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.15+mcmathcomp-1.15.0\" --argstr job \"mathcomp-real-closed\"\ - \ \\\n --dry-run 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output\ - \ name=status::$(echo $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\"\ - )\n" + \ bundle \"coq8.17+mcmathcomp-2.1.0\" --argstr job \"mathcomp-real-closed\"\ + \ \\\n --dry-run 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.15+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.17+mcmathcomp-2.1.0" --argstr job "coq" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.15+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.17+mcmathcomp-2.1.0" --argstr job "mathcomp-ssreflect" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.15+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.17+mcmathcomp-2.1.0" --argstr job "mathcomp-algebra" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.15+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.17+mcmathcomp-2.1.0" --argstr job "mathcomp-field" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.15+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.17+mcmathcomp-2.1.0" --argstr job "mathcomp-fingroup" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-solvable' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.15+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.17+mcmathcomp-2.1.0" --argstr job "mathcomp-solvable" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.15+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.17+mcmathcomp-2.1.0" --argstr job "mathcomp-bigenough" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.15+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.17+mcmathcomp-2.1.0" --argstr job "mathcomp-real-closed" -name: Nix CI for bundle coq8.15+mcmathcomp-1.15.0 +name: Nix CI for bundle coq8.17+mcmathcomp-2.1.0 'on': pull_request: paths: - .github/workflows/** pull_request_target: + paths-ignore: + - .github/workflows/nix-action-coq8.17+mcmathcomp-2.1.0.yml types: - opened - synchronize diff --git a/.github/workflows/nix-action-coq8.14+mcmathcomp-1.15.0.yml b/.github/workflows/nix-action-coq8.18+mcmathcomp-2.1.0.yml similarity index 57% rename from .github/workflows/nix-action-coq8.14+mcmathcomp-1.15.0.yml rename to .github/workflows/nix-action-coq8.18+mcmathcomp-2.1.0.yml index 7c4cc7a..f39105d 100644 --- a/.github/workflows/nix-action-coq8.14+mcmathcomp-1.15.0.yml +++ b/.github/workflows/nix-action-coq8.18+mcmathcomp-2.1.0.yml @@ -3,24 +3,35 @@ jobs: needs: [] runs-on: ubuntu-latest steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} - name: Determine which commit to test run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - name: Git checkout - uses: actions/checkout@v2 + uses: actions/checkout@v3 with: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v16 + uses: cachix/install-nix-action@v20 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 + uses: cachix/cachix-action@v12 with: authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} extraPullNames: coq, coq-community @@ -28,12 +39,12 @@ jobs: - id: stepCheck name: Checking presence of CI target coq run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.14+mcmathcomp-1.15.0\" --argstr job \"coq\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + \ bundle \"coq8.18+mcmathcomp-2.1.0\" --argstr job \"coq\" \\\n --dry-run\ + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18+mcmathcomp-2.1.0" --argstr job "coq" mathcomp-abel: needs: @@ -41,24 +52,35 @@ jobs: - mathcomp-real-closed runs-on: ubuntu-latest steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} - name: Determine which commit to test run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - name: Git checkout - uses: actions/checkout@v2 + uses: actions/checkout@v3 with: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v16 + uses: cachix/install-nix-action@v20 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 + uses: cachix/cachix-action@v12 with: authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} extraPullNames: coq, coq-community @@ -66,48 +88,59 @@ jobs: - id: stepCheck name: Checking presence of CI target mathcomp-abel run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.14+mcmathcomp-1.15.0\" --argstr job \"mathcomp-abel\" \\\n\ - \ --dry-run 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + \ bundle \"coq8.18+mcmathcomp-2.1.0\" --argstr job \"mathcomp-abel\" \\\n\ + \ --dry-run 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18+mcmathcomp-2.1.0" --argstr job "coq" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18+mcmathcomp-2.1.0" --argstr job "mathcomp-field" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-real-closed' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18+mcmathcomp-2.1.0" --argstr job "mathcomp-real-closed" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18+mcmathcomp-2.1.0" --argstr job "mathcomp-abel" mathcomp-bigenough: needs: - coq runs-on: ubuntu-latest steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} - name: Determine which commit to test run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - name: Git checkout - uses: actions/checkout@v2 + uses: actions/checkout@v3 with: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v16 + uses: cachix/install-nix-action@v20 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 + uses: cachix/cachix-action@v12 with: authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} extraPullNames: coq, coq-community @@ -115,21 +148,20 @@ jobs: - id: stepCheck name: Checking presence of CI target mathcomp-bigenough run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.14+mcmathcomp-1.15.0\" --argstr job \"mathcomp-bigenough\"\ - \ \\\n --dry-run 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output\ - \ name=status::$(echo $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\"\ - )\n" + \ bundle \"coq8.18+mcmathcomp-2.1.0\" --argstr job \"mathcomp-bigenough\"\ + \ \\\n --dry-run 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18+mcmathcomp-2.1.0" --argstr job "coq" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18+mcmathcomp-2.1.0" --argstr job "mathcomp-ssreflect" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18+mcmathcomp-2.1.0" --argstr job "mathcomp-bigenough" mathcomp-real-closed: needs: @@ -137,24 +169,35 @@ jobs: - mathcomp-bigenough runs-on: ubuntu-latest steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} - name: Determine which commit to test run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - name: Git checkout - uses: actions/checkout@v2 + uses: actions/checkout@v3 with: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v16 + uses: cachix/install-nix-action@v20 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 + uses: cachix/cachix-action@v12 with: authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} extraPullNames: coq, coq-community @@ -162,48 +205,49 @@ jobs: - id: stepCheck name: Checking presence of CI target mathcomp-real-closed run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.14+mcmathcomp-1.15.0\" --argstr job \"mathcomp-real-closed\"\ - \ \\\n --dry-run 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output\ - \ name=status::$(echo $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\"\ - )\n" + \ bundle \"coq8.18+mcmathcomp-2.1.0\" --argstr job \"mathcomp-real-closed\"\ + \ \\\n --dry-run 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18+mcmathcomp-2.1.0" --argstr job "coq" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18+mcmathcomp-2.1.0" --argstr job "mathcomp-ssreflect" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18+mcmathcomp-2.1.0" --argstr job "mathcomp-algebra" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18+mcmathcomp-2.1.0" --argstr job "mathcomp-field" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18+mcmathcomp-2.1.0" --argstr job "mathcomp-fingroup" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-solvable' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18+mcmathcomp-2.1.0" --argstr job "mathcomp-solvable" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18+mcmathcomp-2.1.0" --argstr job "mathcomp-bigenough" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mcmathcomp-1.15.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18+mcmathcomp-2.1.0" --argstr job "mathcomp-real-closed" -name: Nix CI for bundle coq8.14+mcmathcomp-1.15.0 +name: Nix CI for bundle coq8.18+mcmathcomp-2.1.0 'on': pull_request: paths: - .github/workflows/** pull_request_target: + paths-ignore: + - .github/workflows/nix-action-coq8.18+mcmathcomp-2.1.0.yml types: - opened - synchronize diff --git a/.github/workflows/nix-action-coqmaster+mcmaster.yml b/.github/workflows/nix-action-coqmaster+mcmaster.yml index b1f3cfa..695da0c 100644 --- a/.github/workflows/nix-action-coqmaster+mcmaster.yml +++ b/.github/workflows/nix-action-coqmaster+mcmaster.yml @@ -3,24 +3,35 @@ jobs: needs: [] runs-on: ubuntu-latest steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} - name: Determine which commit to test run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - name: Git checkout - uses: actions/checkout@v2 + uses: actions/checkout@v3 with: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v16 + uses: cachix/install-nix-action@v20 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 + uses: cachix/cachix-action@v12 with: authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} extraPullNames: coq, coq-community @@ -29,36 +40,156 @@ jobs: name: Checking presence of CI target coq run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coqmaster+mcmaster\" --argstr job \"coq\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ - \ | grep \"built:\" | sed \"s/.*/built/\")\n" + \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ + built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coqmaster+mcmaster" --argstr job "coq" + coq-elpi: + needs: + - coq + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target coq-elpi + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coqmaster+mcmaster\" --argstr job \"coq-elpi\" \\\n --dry-run\ + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coqmaster+mcmaster" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coqmaster+mcmaster" + --argstr job "coq-elpi" + hierarchy-builder: + needs: + - coq + - coq-elpi + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target hierarchy-builder + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coqmaster+mcmaster\" --argstr job \"hierarchy-builder\" \\\n \ + \ --dry-run 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coqmaster+mcmaster" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq-elpi' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coqmaster+mcmaster" + --argstr job "coq-elpi" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coqmaster+mcmaster" + --argstr job "hierarchy-builder" mathcomp-abel: needs: - coq - mathcomp-real-closed runs-on: ubuntu-latest steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} - name: Determine which commit to test run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - name: Git checkout - uses: actions/checkout@v2 + uses: actions/checkout@v3 with: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v16 + uses: cachix/install-nix-action@v20 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 + uses: cachix/cachix-action@v12 with: authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} extraPullNames: coq, coq-community @@ -67,8 +198,8 @@ jobs: name: Checking presence of CI target mathcomp-abel run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coqmaster+mcmaster\" --argstr job \"mathcomp-abel\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coqmaster+mcmaster" @@ -90,24 +221,35 @@ jobs: - coq runs-on: ubuntu-latest steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} - name: Determine which commit to test run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - name: Git checkout - uses: actions/checkout@v2 + uses: actions/checkout@v3 with: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v16 + uses: cachix/install-nix-action@v20 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 + uses: cachix/cachix-action@v12 with: authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} extraPullNames: coq, coq-community @@ -116,8 +258,8 @@ jobs: name: Checking presence of CI target mathcomp-bigenough run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coqmaster+mcmaster\" --argstr job \"mathcomp-bigenough\" \\\n \ - \ --dry-run 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + \ --dry-run 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coqmaster+mcmaster" @@ -136,24 +278,35 @@ jobs: - mathcomp-bigenough runs-on: ubuntu-latest steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} - name: Determine which commit to test run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - name: Git checkout - uses: actions/checkout@v2 + uses: actions/checkout@v3 with: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v16 + uses: cachix/install-nix-action@v20 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup math-comp - uses: cachix/cachix-action@v10 + uses: cachix/cachix-action@v12 with: authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} extraPullNames: coq, coq-community @@ -162,8 +315,8 @@ jobs: name: Checking presence of CI target mathcomp-real-closed run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coqmaster+mcmaster\" --argstr job \"mathcomp-real-closed\" \\\n\ - \ --dry-run 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + \ --dry-run 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coqmaster+mcmaster" @@ -202,6 +355,8 @@ name: Nix CI for bundle coqmaster+mcmaster paths: - .github/workflows/** pull_request_target: + paths-ignore: + - .github/workflows/nix-action-coqmaster+mcmaster.yml types: - opened - synchronize diff --git a/.nix/config.nix b/.nix/config.nix index 42998fe..b0f0e26 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -31,7 +31,7 @@ ## select an entry to build in the following `bundles` set ## defaults to "default" - default-bundle = "coq8.16+mcmathcomp-2.0.0"; + default-bundle = "coq8.18+mcmathcomp-2.1.0"; ## write one `bundles.name` attribute set per ## alternative configuration @@ -45,17 +45,18 @@ mathcomp.job = false; } // (if (coqv == "master") then { coq-elpi.override.version = "coq-master"; - hierarchy-builder.override.version = "proux01:coq-master"; + hierarchy-builder.override.version = "master"; } else {}) // (if (mcv == "master") then { mathcomp-real-closed.override.version = "master"; mathcomp-bigenough.override.version = "1.0.1"; - } else {}) // (if (mcv == "mathcomp-2.0.0") then { + } else {}) // (if (mcv == "mathcomp-2.1.0") then { mathcomp-real-closed.override.version = "master"; mathcomp-bigenough.override.version = "1.0.1"; } else {}); }; in - gen "8.16" "mathcomp-2.0.0" // - gen "8.17" "mathcomp-2.0.0" // + gen "8.16" "mathcomp-2.1.0" // + gen "8.17" "mathcomp-2.1.0" // + gen "8.18" "mathcomp-2.1.0" // gen "master" "master"; ## Cachix caches to use in CI diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index dd2bd93..5b6bf1f 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"be976db262f1dc9f6e013153f263182e14372246" +"e7a39f47847edcde691d7bf8f423e4806a1b660f" From dbb88d88fd95898995fc53f278bc6690843794ea Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 11 May 2023 16:47:47 +0200 Subject: [PATCH 3/3] [CI] Update Docker --- .github/workflows/docker-action.yml | 18 +++++------------- 1 file changed, 5 insertions(+), 13 deletions(-) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index e51049f..735b50b 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -17,20 +17,12 @@ jobs: strategy: matrix: image: - - 'mathcomp/mathcomp:1.13.0-coq-8.11' - - 'mathcomp/mathcomp:1.13.0-coq-8.12' - - 'mathcomp/mathcomp:1.13.0-coq-8.13' - - 'mathcomp/mathcomp:1.14.0-coq-8.13' - - 'mathcomp/mathcomp:1.14.0-coq-8.14' - - 'mathcomp/mathcomp:1.14.0-coq-8.15' - - 'mathcomp/mathcomp:1.14.0-coq-8.14' - - 'mathcomp/mathcomp:1.15.0-coq-8.14' - - 'mathcomp/mathcomp:1.15.0-coq-8.15' - - 'mathcomp/mathcomp:1.15.0-coq-8.16' - - 'mathcomp/mathcomp-dev:coq-8.13' - - 'mathcomp/mathcomp-dev:coq-8.14' - - 'mathcomp/mathcomp-dev:coq-8.15' + - 'mathcomp/mathcomp:2.1.0-coq-8.16' + - 'mathcomp/mathcomp:2.1.0-coq-8.17' + - 'mathcomp/mathcomp:2.1.0-coq-8.18' - 'mathcomp/mathcomp-dev:coq-8.16' + - 'mathcomp/mathcomp-dev:coq-8.17' + - 'mathcomp/mathcomp-dev:coq-8.18' - 'mathcomp/mathcomp-dev:coq-dev' fail-fast: false steps: