From a3d2439fb5052f5589dfa29c57da5776dc6af990 Mon Sep 17 00:00:00 2001 From: Florent Hivert Date: Fri, 3 Jan 2025 10:28:02 +0100 Subject: [PATCH 1/8] MathComp 2.3 compat --- Makefile | 44 +++------------------ README.md | 16 ++++---- _CoqProject | 1 + theories/Basic/ordtype.v | 49 ++++++++++++------------ theories/Basic/unitriginv.v | 6 +-- theories/Combi/Dyckword.v | 13 ++++--- theories/Combi/bintree.v | 6 +-- theories/Combi/composition.v | 10 ++--- theories/Combi/multinomial.v | 3 +- theories/Combi/partition.v | 21 +++++----- theories/Combi/setpartition.v | 6 +-- theories/Combi/skewtab.v | 21 +++++----- theories/Combi/std.v | 35 +++++++---------- theories/Combi/stdtab.v | 8 ++-- theories/Combi/subseq.v | 4 +- theories/Combi/tableau.v | 12 +++--- theories/Erdos_Szekeres/Erdos_Szekeres.v | 3 +- theories/HookFormula/hook.v | 4 +- theories/LRrule/Greene.v | 8 ++-- theories/LRrule/Greene_inv.v | 22 +++++------ theories/LRrule/Schensted.v | 4 +- theories/LRrule/freeSchur.v | 9 ++--- theories/LRrule/plactic.v | 22 +++++------ theories/LRrule/shuffle.v | 4 +- theories/LRrule/stdplact.v | 12 +++--- theories/LRrule/therule.v | 7 ++-- theories/MPoly/Cauchy.v | 4 +- theories/MPoly/homogsym.v | 2 + theories/MPoly/sympoly.v | 10 ++--- theories/SSRcomplements/sorted.v | 2 +- theories/SSRcomplements/tools.v | 4 +- theories/SymGroup/Frobenius_char.v | 4 +- theories/SymGroup/cycletype.v | 2 +- theories/SymGroup/presentSn.v | 20 +++++----- theories/SymGroup/weak_order.v | 2 +- 35 files changed, 176 insertions(+), 224 deletions(-) diff --git a/Makefile b/Makefile index 38bfd4d..e8b12fe 100644 --- a/Makefile +++ b/Makefile @@ -7,7 +7,7 @@ ## # GNU Lesser General Public License Version 2.1 ## ## # (see LICENSE file for the text of the license) ## ########################################################################## -## GNUMakefile for Coq 8.19.2 +## GNUMakefile for Coq 8.20.0 # For debugging purposes (must stay here, don't move below) INITIAL_VARS := $(.VARIABLES) @@ -278,7 +278,7 @@ COQDOCLIBS?=$(COQLIBS_NOML) # The version of Coq being run and the version of coq_makefile that # generated this makefile COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1) -COQMAKEFILE_VERSION:=8.19.2 +COQMAKEFILE_VERSION:=8.20.0 # COQ_SRC_SUBDIRS is for user-overriding, usually to add # `user-contrib/Foo` to the includes, we keep COQCORE_SRC_SUBDIRS for @@ -309,7 +309,7 @@ endif ifneq (,$(PROFILING)) PROFILE_ARG=-profile $<.prof.json - PROFILE_ZIP=gzip $<.prof.json + PROFILE_ZIP=gzip -f $<.prof.json else PROFILE_ARG= PROFILE_ZIP=true @@ -503,37 +503,6 @@ bytefiles: $(CMOFILES) $(CMAFILES) optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES)) .PHONY: optfiles -# FIXME, see Ralf's bugreport -# quick is deprecated, now renamed vio -vio: $(VOFILES:.vo=.vio) -.PHONY: vio -quick: vio - $(warning "'make quick' is deprecated, use 'make vio' or consider using 'vos' files") -.PHONY: quick - -vio2vo: - $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \ - -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio) -.PHONY: vio2vo - -# quick2vo is undocumented -quick2vo: - $(HIDE)make -j $(J) vio - $(HIDE)VIOFILES=$$(for vofile in $(VOFILES); do \ - viofile="$$(echo "$$vofile" | sed "s/\.vo$$/.vio/")"; \ - if [ "$$vofile" -ot "$$viofile" -o ! -e "$$vofile" ]; then printf "$$viofile "; fi; \ - done); \ - echo "VIO2VO: $$VIOFILES"; \ - if [ -n "$$VIOFILES" ]; then \ - $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -schedule-vio2vo $(J) $$VIOFILES; \ - fi -.PHONY: quick2vo - -checkproofs: - $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \ - -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio) -.PHONY: checkproofs - vos: $(VOFILES:%.vo=%.vos) .PHONY: vos @@ -711,9 +680,10 @@ clean:: $(HIDE)rm -f $(NATIVEFILES) $(HIDE)find . -name .coq-native -type d -empty -delete $(HIDE)rm -f $(VOFILES) - $(HIDE)rm -f $(VOFILES:.vo=.vio) $(HIDE)rm -f $(VOFILES:.vo=.vos) $(HIDE)rm -f $(VOFILES:.vo=.vok) + $(HIDE)rm -f $(VOFILES:.vo=.v.prof.json) + $(HIDE)rm -f $(VOFILES:.vo=.v.prof.json.gz) $(HIDE)rm -f $(BEAUTYFILES) $(VFILES:=.old) $(HIDE)rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob all-mli.tex $(HIDE)rm -f $(VFILES:.v=.glob) @@ -846,10 +816,6 @@ endif $(foreach vfile,$(VFILES:.v=),$(eval $(call globvorule,$(vfile)))) -$(VFILES:.v=.vio): %.vio: %.v - $(SHOW)COQC -vio $< - $(HIDE)$(TIMER) $(COQC) -vio $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< - $(VFILES:.v=.vos): %.vos: %.v $(SHOW)COQC -vos $< $(HIDE)$(TIMER) $(COQC) -vos $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< diff --git a/README.md b/README.md index 6e5fb96..2b5fd6e 100644 --- a/README.md +++ b/README.md @@ -163,15 +163,15 @@ Installation This library is based on * [SSReflect/MathComp 2]([https://github.com/math-comp/math-comp]) - Library version 2.2.0 or more recent. + Library version 2.3.0 or more recent. Here are the Opam packages I'm using ``` -coq-hierarchy-builder 1.7.0 -coq-mathcomp-ssreflect 2.2.0 -coq-mathcomp-algebra 2.2.0 -coq-mathcomp-field 2.2.0 -coq-mathcomp-fingroup 2.2.0 -coq-mathcomp-character 2.2.0 -coq-mathcomp-multinomials 2.2.0 +coq-hierarchy-builder 1.8.0 +coq-mathcomp-ssreflect 2.3.0 +coq-mathcomp-algebra 2.3.0 +coq-mathcomp-field 2.3.0 +coq-mathcomp-fingroup 2.3.0 +coq-mathcomp-character 2.3.0 +coq-mathcomp-multinomials 2.3.0 ``` diff --git a/_CoqProject b/_CoqProject index d0c43a3..685ba48 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,6 +1,7 @@ -docroot Combi -R theories Combi -arg -w -arg -notation-overridden +-arg -w -arg -notation-incompatible-prefix -arg -w -arg -ambiguous-paths -arg -w -arg -redundant-canonical-projection -arg -w -arg -projection-no-head-constant diff --git a/theories/Basic/ordtype.v b/theories/Basic/ordtype.v index b62030c..e61aa2b 100644 --- a/theories/Basic/ordtype.v +++ b/theories/Basic/ordtype.v @@ -55,7 +55,7 @@ Import Order.Theory. (** * Induction on partially ordered types *) (******************************************************************************) -Lemma finord_wf (disp : unit) (T : finPOrderType disp) (P : T -> Type) : +Lemma finord_wf disp (T : finPOrderType disp) (P : T -> Type) : (forall x, (forall y, y < x -> P y) -> P x) -> forall x, P x. Proof. move=> IH x. @@ -67,7 +67,7 @@ rewrite -{}eqcn; apply proper_card; apply/andP; split; apply/subsetP. - by move/(_ y); rewrite !inE => /(_ ltxy); rewrite ltxx. Qed. -Lemma finord_wf_down (disp : unit) (T : finPOrderType disp) (P : T -> Type) : +Lemma finord_wf_down disp (T : finPOrderType disp) (P : T -> Type) : (forall x, (forall y, y > x -> P y) -> P x) -> forall x, P x. Proof. exact: (finord_wf (T := T^d : finPOrderType _)). Qed. @@ -78,12 +78,12 @@ Proof. exact: (finord_wf (T := T^d : finPOrderType _)). Qed. (** We only define covering relation for finite type, since it cannot be *) (** decided and it is not very useful for infinite orders. *) -Definition covers {disp : unit} {T : finPOrderType disp} := +Definition covers {disp} {T : finPOrderType disp} := [rel x y : T | (x < y) && [forall z, ~~(x < z < y)]]. Section CoversFinPOrder. -Variable (disp : unit) (T : finPOrderType disp). +Variable (disp : _) (T : finPOrderType disp). Implicit Type (x y : T). Lemma coversP x y : reflect (x < y /\ (forall z, ~(x < z < y))) (covers x y). @@ -148,7 +148,7 @@ Proof. by rewrite -covers_connect; apply: (iffP connectP). Qed. End CoversFinPOrder. -Lemma covers_rind (disp : unit) (T : finPOrderType disp) (P : T -> Type) : +Lemma covers_rind disp (T : finPOrderType disp) (P : T -> Type) : (forall x y, covers y x -> P x -> P y) -> forall x, P x -> forall y, x >= y -> P y. Proof. @@ -168,12 +168,12 @@ HB.structure Definition Inhabited := {T of isInhabited T & Choice T}. HB.factory Record isInhabitedType T := { x : T }. HB.builders Context T of isInhabitedType T. -HB.instance Definition _ := isInhabited.Build T (ex_intro _ x is_true_true). +#[warning="-HB.no-new-instance"] +HB.instance Definition _ := isInhabited.Build T (ex_intro _ x is_true_true). HB.end. HB.instance Definition _ := isInhabitedType.Build unit tt. HB.instance Definition _ := isInhabitedType.Build bool false. -HB.instance Definition _ := isInhabitedType.Build Prop False. HB.instance Definition _ := isInhabitedType.Build nat 0. HB.instance Definition _ (n : nat) := isInhabitedType.Build 'I_n.+1 ord0. @@ -207,19 +207,19 @@ HB.structure Definition InhFinite := { T of isInhabited T & Finite T }. (** ** Inhabited ordered types *) (******************************************************************************) #[short(type=inhPOrderType)] -HB.structure Definition InhPOrder (d : unit) := +HB.structure Definition InhPOrder d := {T of isInhabited T & Order.POrder d T}. #[short(type=inhLatticeType)] -HB.structure Definition InhLattice (d : unit) := +HB.structure Definition InhLattice d := {T of isInhabited T & Order.Lattice d T}. #[short(type=inhTBLatticeType)] -HB.structure Definition InhTBLattice (d : unit) := +HB.structure Definition InhTBLattice d := {T of isInhabited T & Order.TBLattice d T}. #[short(type=inhOrderType)] -HB.structure Definition InhOrder (d : unit) := +HB.structure Definition InhOrder d := {T of isInhabited T & Order.Total d T}. @@ -227,15 +227,15 @@ HB.structure Definition InhOrder (d : unit) := (** ** Inhabited finite partially ordered types *) (******************************************************************************) #[short(type=inhFinPOrderType)] -HB.structure Definition InhFinPOrder (d : unit) := +HB.structure Definition InhFinPOrder d := {T of isInhabited T & Order.POrder d T & Finite T}. #[short(type=inhFinLatticeType)] -HB.structure Definition InhFinLattice (d : unit) := +HB.structure Definition InhFinLattice d := {T of isInhabited T & Order.FinLattice d T}. #[short(type=inhFinOrderType)] -HB.structure Definition InhFinOrder (d : unit) := +HB.structure Definition InhFinOrder d := {T of isInhabited T & Order.FinTotal d T}. HB.instance Definition _ := Inhabited.on bool. @@ -246,15 +246,14 @@ Section Dual. HB.instance Definition _ (T : inhType) := isInhabitedType.Build (Order.dual T) (@inh T). -Variable d : unit. -HB.instance Definition _ (T : inhPOrderType d) := InhPOrder.on (T^d). -HB.instance Definition _ (T : inhLatticeType d) := InhLattice.on (T^d). -HB.instance Definition _ (T : inhTBLatticeType d) := InhTBLattice.on (T^d). -HB.instance Definition _ (T : inhOrderType d) := InhOrder.on (T^d). +HB.instance Definition _ d (T : inhPOrderType d) := InhPOrder.on (T^d). +HB.instance Definition _ d (T : inhLatticeType d) := InhLattice.on (T^d). +HB.instance Definition _ d (T : inhTBLatticeType d) := InhTBLattice.on (T^d). +HB.instance Definition _ d (T : inhOrderType d) := InhOrder.on (T^d). -HB.instance Definition _ (T : inhFinPOrderType d) := InhFinPOrder.on (T^d). -HB.instance Definition _ (T : inhFinLatticeType d) := InhFinLattice.on (T^d). -HB.instance Definition _ (T : inhFinOrderType d) := InhFinOrder.on (T^d). +HB.instance Definition _ d (T : inhFinPOrderType d) := InhFinPOrder.on (T^d). +HB.instance Definition _ d (T : inhFinLatticeType d) := InhFinLattice.on (T^d). +HB.instance Definition _ d (T : inhFinOrderType d) := InhFinOrder.on (T^d). End Dual. @@ -264,7 +263,7 @@ End Dual. (** *** Maximum of a sequence *) Section MaxSeq. -Variables (disp : unit) (T : orderType disp). +Variables (disp : _) (T : orderType disp). Implicit Type a b c : T. Implicit Type u v : seq T. @@ -300,7 +299,7 @@ End MaxSeq. (** *** Comparison of the elements of a sequence to an element *) Section AllLeqLtn. -Variables (disp : unit) (T : orderType disp). +Variables (disp : _) (T : orderType disp). Implicit Type a b c : T. Implicit Type u v : seq T. @@ -453,7 +452,7 @@ End AllLeqLtn. (** *** Removing the largest letter of a sequence *) Section RemoveBig. -Variables (disp : unit) (T : orderType disp). +Variables (disp : _) (T : orderType disp). Variable Z : T. Implicit Type a b c : T. Implicit Type u v w r : seq T. diff --git a/theories/Basic/unitriginv.v b/theories/Basic/unitriginv.v index c5cc725..3d99a69 100644 --- a/theories/Basic/unitriginv.v +++ b/theories/Basic/unitriginv.v @@ -47,8 +47,7 @@ Import GRing.Theory. Section UniTriangular. Variable R : comUnitRingType. -Variable disp : unit. -Variable T : finPOrderType disp. +Variables (disp : _) (T : finPOrderType disp). Implicit Type M : T -> T -> R. Implicit Types t u v : T. @@ -151,8 +150,7 @@ End UniTriangular. Section TriangularInv. Variable R : comUnitRingType. -Variable disp : unit. -Variable T : finPOrderType disp. +Variable (disp : _) (T : finPOrderType disp). Variable M : T -> T -> R. Implicit Types t u v : T. diff --git a/theories/Combi/Dyckword.v b/theories/Combi/Dyckword.v index 2be93a7..3ed616a 100644 --- a/theories/Combi/Dyckword.v +++ b/theories/Combi/Dyckword.v @@ -350,14 +350,17 @@ Canonical join_Dyck D1 D2 := DyckWord (Dyck_word_OwCw D1 D2). End DyckType. -Notation "[ 'Dyck' 'of' s ]" := (dyck (fun sP => @DyckWord s sP)) +#[warning="-notation-incompatible-prefix"] +Notation "'[' 'Dyck' 'of' s ]" := (dyck (fun sP => @DyckWord s sP)) (at level 9, format "[ 'Dyck' 'of' s ]") : form_scope. -Notation "[ 'Dyck' 'of' s 'by' pf ]" := (@DyckWord s pf) +#[warning="-notation-incompatible-prefix"] +Notation "'[' 'Dyck' 'of' s 'by' pf ]" := (@DyckWord s pf) (at level 9, format "[ 'Dyck' 'of' s 'by' pf ]") : form_scope. -Notation "[ 'Dyck' {{ D1 }} D2 ]" := (join_Dyck D1 D2) - (at level 8, format "[ 'Dyck' {{ D1 }} D2 ]", +#[warning="-notation-incompatible-prefix"] +Notation "'[' 'Dyck' '{{' D1 '}}' D2 ]" := (join_Dyck D1 D2) + (at level 8, format "[ 'Dyck' '{{' D1 '}}' D2 ]", D1 at next level) : form_scope. @@ -467,7 +470,7 @@ Implicit Type D : Dyck. Variable P : Dyck -> Type. Hypotheses (Pnil : P nil_Dyck) - (Pcons : forall D1 D2, P D1 -> P D2 -> P ([Dyck {{ D1 }} D2])). + (Pcons : forall D1 D2, P D1 -> P D2 -> P [Dyck {{ D1 }} D2]). Theorem Dyck_ind D : P D. Proof. diff --git a/theories/Combi/bintree.v b/theories/Combi/bintree.v index 02d0030..d594edc 100644 --- a/theories/Combi/bintree.v +++ b/theories/Combi/bintree.v @@ -1362,7 +1362,7 @@ apply/anti_leq/andP; split. Qed. -Fact Tamari_display : unit. Proof. exact: tt. Qed. +Fact Tamari_display : Order.disp_t. Proof. by []. Qed. Notation "x <=T y" := (@Order.le Tamari_display _ x y). Notation "x T'; f' : T' -> T; @@ -77,7 +77,7 @@ HB.end. HB.factory Record IsoTop disp T of Order.POrder disp T := { - disp' : unit; + disp' : Order.disp_t; T' : tPOrderType disp'; f : T -> T'; f' : T' -> T; @@ -652,7 +652,7 @@ Implicit Types (c : 'CRef) (d : {set 'I_n.-1}). #[export] HB.instance Definition _ := SubType.copy 'CRef (intcompn n). #[export] HB.instance Definition _ := Finite.copy 'CRef (intcompn n). -Fact compnref_display : unit. Proof. exact: tt. Qed. +Fact compnref_display : Order.disp_t. Proof. by []. Qed. #[export] HB.instance Definition _ : Order.isPOrder compnref_display 'CRef := Order.CanIsPartial compnref_display (@descsetK n). #[export] HB.instance Definition _ := @@ -696,10 +696,10 @@ Qed. IsoTop.Build compnref_display 'CRef (@descsetK n) (@from_descsetK n) descset_mono. -Lemma topEcompnref : 1%O = colcompn n :> 'CRef. +Lemma topEcompnref : \top%O = colcompn n :> 'CRef. Proof. by apply: descset_inj; rewrite from_descsetK descset_colcompn. Qed. -Lemma botEcompnref : 0%O = rowcompn n :> 'CRef. +Lemma botEcompnref : \bot%O = rowcompn n :> 'CRef. Proof. by apply: descset_inj; rewrite from_descsetK descset_rowcompn. Qed. Lemma compnref_rev c1 c2 : diff --git a/theories/Combi/multinomial.v b/theories/Combi/multinomial.v index a4d1d9e..ee9cd60 100644 --- a/theories/Combi/multinomial.v +++ b/theories/Combi/multinomial.v @@ -39,7 +39,8 @@ Implicit Type (i a b : nat) (s t : seq nat). Fixpoint multinomial_rec s := if s is i :: s' then 'C(sumn s, i) * (multinomial_rec s') else 1. Arguments multinomial_rec : simpl nomatch. -Definition multinomial := nosimpl multinomial_rec. +Definition multinomial := multinomial_rec. +Arguments multinomial : simpl never. Notation "''C' [ s ]" := (multinomial s) (at level 8, format "''C' [ s ]") : nat_scope. diff --git a/theories/Combi/partition.v b/theories/Combi/partition.v index 88e7f44..7ec1abd 100644 --- a/theories/Combi/partition.v +++ b/theories/Combi/partition.v @@ -1695,15 +1695,15 @@ exact: (part_nseq1P Hpart Hhead). Qed. #[export] HB.instance Definition _ := - Order.hasBottom.Build Order.lexi_display 'PLexi colpartn_bot. + Order.hasBottom.Build _ 'PLexi colpartn_bot. #[export] HB.instance Definition _ := - Order.hasTop.Build Order.lexi_display 'PLexi rowpartn_top. + Order.hasTop.Build _ 'PLexi rowpartn_top. #[export] HB.instance Definition _ := isInhabitedType.Build 'PLexi (rowpartn d). -Lemma botEintpartnlexi : 0%O = colpartn d :> 'PLexi. +Lemma botEintpartnlexi : \bot%O = colpartn d :> 'PLexi. Proof. by []. Qed. -Lemma topEintpartnlexi : 1%O = rowpartn d :> 'PLexi. +Lemma topEintpartnlexi : \top%O = rowpartn d :> 'PLexi. Proof. by []. Qed. End IntPartNLexi. @@ -2016,7 +2016,7 @@ Qed. #[export] HB.instance Definition _ := Countable.copy 'YL intpart. #[export] HB.instance Definition _ := Inhabited.copy 'YL intpart. -Fact Young_display : unit. Proof. exact: tt. Qed. +Fact Young_display : Order.disp_t. Proof. by []. Qed. #[export] HB.instance Definition _ := Order.Le_isPOrder.Build Young_display 'YL le_Young_refl le_Young_anti le_Young_trans. @@ -2153,11 +2153,8 @@ Fact emptypart_bottom sh : (empty_intpart <= sh :> 'YL)%O. Proof. by apply/includedP; split => //= i; rewrite nth_nil. Qed. HB.instance Definition _ := Order.hasBottom.Build Young_display 'YL emptypart_bottom. -HB.instance Definition _ := - isInhabitedType.Build 'YL empty_intpart. - -Lemma bottom_YoungE : 0%O = empty_intpart :> 'YL. +Lemma bottom_YoungE : \bot%O = empty_intpart :> 'YL. Proof. by []. Qed. Fact Young_meetUl : @left_distributive 'YL 'YL Order.meet Order.join. @@ -2379,7 +2376,7 @@ Proof. by move=> x y /andP[Hxy Hyx]; apply val_inj => /=; apply: partdom_anti. Qed. -Lemma partdom_display : unit. Proof. exact: tt. Qed. +Lemma partdom_display : Order.disp_t. Proof. by []. Qed. #[export] HB.instance Definition _ := Order.Le_isPOrder.Build partdom_display 'PDom partdom_refl partdom_antisym partdom_trans. @@ -2672,9 +2669,9 @@ Proof. by rewrite -partdom_conj_intpartn conj_colpartn partdom_rowpartn. Qed. #[export] HB.instance Definition _ := Order.hasTop.Build partdom_display 'PDom partdom_rowpartn. -Lemma botEintpartndom : 0%O = colpartn d :> 'PDom. +Lemma botEintpartndom : \bot%O = colpartn d :> 'PDom. Proof. by []. Qed. -Lemma topEintpartndom : 1%O = rowpartn d :> 'PDom. +Lemma topEintpartndom : \top%O = rowpartn d :> 'PDom. Proof. by []. Qed. End IntPartNTopBottom. diff --git a/theories/Combi/setpartition.v b/theories/Combi/setpartition.v index b1db52e..bcb8367 100644 --- a/theories/Combi/setpartition.v +++ b/theories/Combi/setpartition.v @@ -304,7 +304,7 @@ have -> : pblock P x = pblock Q x. by apply/eqP; rewrite eqEsubset ?PsQ ?QsP. by apply pblock_mem; rewrite (cover_setpart Q). Qed. -Lemma setpartfiner_display : unit. Proof. exact: tt. Qed. +Lemma setpartfiner_display : Order.disp_t. Proof. by []. Qed. #[export] HB.instance Definition _ := Order.Le_isPOrder.Build setpartfiner_display (setpart S) @@ -527,9 +527,9 @@ exists (fun B => [set A | (A \in P) && (A \subset B)]). by exists B=> //; rewrite inE AinP AsB. Qed. -Lemma setpart_bottomE : 0%O = setpart1 S. +Lemma setpart_bottomE : \bot%O = setpart1 S. Proof. by []. Qed. -Lemma setpart_topE : 1%O = trivsetpart S. +Lemma setpart_topE : \top%O = trivsetpart S. Proof. by []. Qed. Definition mem_meet_finerP P Q X : reflect (meet_spec P Q X) (X \in P `&` Q)%O diff --git a/theories/Combi/skewtab.v b/theories/Combi/skewtab.v index 391a009..b1c93a5 100644 --- a/theories/Combi/skewtab.v +++ b/theories/Combi/skewtab.v @@ -134,7 +134,7 @@ Qed. (** ** Skew tableaux *) Section Dominate. -Variables (disp : unit) (T : inhOrderType disp). +Variables (disp : _) (T : inhOrderType disp). Implicit Type u v : seq T. Definition skew_dominate sh u v := dominate (drop sh u) v. @@ -375,7 +375,7 @@ End Dominate. (** ** Skewing and joining tableaux *) Section FilterLeqGeq. -Variables (disp : unit) (T : inhOrderType disp). +Variables (disp : _) (T : inhOrderType disp). Implicit Type l : T. Implicit Type r w : seq T. Implicit Type t : seq (seq T). @@ -646,7 +646,7 @@ End FilterLeqGeq. Section EqInvSkewTab. Lemma eq_inv_skew_dominate - (d1 d2 : unit) (T1 : inhOrderType d1) (T2 : inhOrderType d2) + d1 d2 (T1 : inhOrderType d1) (T2 : inhOrderType d2) (u1 v1 : seq T1) (u2 v2 : seq T2) s : eq_inv (u1 ++ v1) (u2 ++ v2) -> size u1 = size u2 -> @@ -673,8 +673,7 @@ rewrite leq_add2r ltn_add2l; apply/andP; split. Qed. Lemma eq_inv_is_skew_tableau_reshape_size - inner outer - (d1 d2 : unit) (T1 : inhOrderType d1) (T2 : inhOrderType d2) + inner outer d1 d2 (T1 : inhOrderType d1) (T2 : inhOrderType d2) (u1 : seq T1) (u2 : seq T2) : size inner = size outer -> (* complete with 0 if needed *) eq_inv u1 u2 -> size u1 = sumn (outer / inner) -> @@ -728,7 +727,7 @@ apply (eq_inv_catr (u1 := take (sumn d) u1) (u2 := take (sumn d) u2) ). Qed. Lemma is_skew_tableau_skew_reshape_pad0 inner outer - (d : unit) (T : inhOrderType d) (u : seq T) : + d (T : inhOrderType d) (u : seq T) : is_skew_tableau inner (skew_reshape inner outer u) = is_skew_tableau ((pad 0 (size outer)) inner) (skew_reshape ((pad 0 (size outer)) inner) outer u). @@ -740,8 +739,7 @@ by rewrite /skew_reshape diff_shape_pad0. Qed. Theorem eq_inv_is_skew_tableau_reshape - inner outer - (d1 d2 : unit) (T1 : inhOrderType d1) (T2 : inhOrderType d2) + inner outer d1 d2 (T1 : inhOrderType d1) (T2 : inhOrderType d2) (u1 : seq T1) (u2 : seq T2) : size inner <= size outer -> eq_inv u1 u2 -> @@ -761,7 +759,7 @@ apply eq_inv_is_skew_tableau_reshape_size. Qed. Theorem is_skew_tableau_reshape_std inner outer - (d : unit) (T : inhOrderType d) (u : seq T) : + d (T : inhOrderType d) (u : seq T) : size inner <= size outer -> size u = sumn (outer / inner) -> is_skew_tableau inner (skew_reshape inner outer u) = @@ -774,8 +772,7 @@ apply/idP/idP; apply eq_inv_is_skew_tableau_reshape => //=. - by rewrite size_std. Qed. -Theorem is_tableau_reshape_std sh - (d : unit) (T : inhOrderType d) (u : seq T) : +Theorem is_tableau_reshape_std sh d (T : inhOrderType d) (u : seq T) : size u = sumn sh -> is_tableau (skew_reshape [::] sh u) = is_tableau (skew_reshape [::] sh (std u)). @@ -784,7 +781,7 @@ move=> Hsz. by rewrite -!is_skew_tableau0; rewrite is_skew_tableau_reshape_std. Qed. -Theorem is_tableau_std (d : unit) (T : inhOrderType d) (t : seq (seq T)) : +Theorem is_tableau_std d (T : inhOrderType d) (t : seq (seq T)) : is_tableau t = is_tableau (skew_reshape [::] (shape t) (std (to_word t))). Proof. rewrite -{1}(to_wordK t); apply is_tableau_reshape_std. diff --git a/theories/Combi/std.v b/theories/Combi/std.v index 2e23000..6309427 100644 --- a/theories/Combi/std.v +++ b/theories/Combi/std.v @@ -238,7 +238,7 @@ End StdCombClass. (** * Standardisation of a word over a totally ordered alphabet *) Section Standardisation. -Context {disp : unit} {Alph : orderType disp}. +Context {disp : _} {Alph : orderType disp}. Implicit Type s u v w : seq Alph. Fixpoint std_rec n s := @@ -345,8 +345,7 @@ move Hn : (size s) => n; elim: n s Hn => [/= | n IHn] s Hsz. exact: posbig_take_dropE. Qed. -Lemma std_stdE (disp : unit) (T : orderType disp) - (s : seq T) : std (std s) = std s. +Lemma std_stdE disp (T : orderType disp) (s : seq T) : std (std s) = std s. Proof. apply: std_std; exact: std_is_std. Qed. @@ -360,10 +359,10 @@ Definition eq_inv d1 d2 (T1 : inhOrderType d1) (T2 : inhOrderType d2) (w1 : seq T1) (w2 : seq T2) := (versions w1) =2 (versions w2). -Variables (disp1 disp2 disp3 : unit). -Variables (S : inhOrderType disp1) - (T : inhOrderType disp2) - (U : inhOrderType disp3). +Variables (disp1 disp2 disp3 : _) + (S : inhOrderType disp1) + (T : inhOrderType disp2) + (U : inhOrderType disp3). Lemma eq_inv_refl (w : seq T) : eq_inv w w. Proof. by []. Qed. @@ -402,8 +401,8 @@ Qed. Section EqInvAltDef. -Variables (disp1 disp2 disp3 : unit). -Variables (S : inhOrderType disp1) +Variables (disp1 disp2 disp3 : _) + (S : inhOrderType disp1) (T : inhOrderType disp2) (U : inhOrderType disp3). @@ -480,9 +479,7 @@ Qed. Section EqInvPosRemBig. -Variables (disp1 disp2 : unit). -Variables (S : inhOrderType disp1) - (T : inhOrderType disp2). +Variables (disp1 disp2 : _) (S : inhOrderType disp1) (T : inhOrderType disp2). Lemma eq_inv_posbig (u : seq S) (v : seq T) : eq_inv u v -> posbig u = posbig v. @@ -604,9 +601,7 @@ End EqInvPosRemBig. Section Spec. -Variables (disp1 disp2 : unit). -Variables (S : inhOrderType disp1) - (T : inhOrderType disp2). +Variables (disp1 disp2 : _) (S : inhOrderType disp1) (T : inhOrderType disp2). Variant std_spec (s : seq T) (p : seq nat) : Prop := | StdSpec : is_std p -> eq_inv s p -> std_spec s p. @@ -677,9 +672,7 @@ End Spec. Section StdTakeDrop. -Variables (disp1 disp2 : unit). -Variables (S : inhOrderType disp1) - (T : inhOrderType disp2). +Variables (disp1 disp2 : _) (S : inhOrderType disp1) (T : inhOrderType disp2). Implicit Type u v : seq T. Lemma std_take_std u v : std (take (size u) (std (u ++ v))) = std u. @@ -707,8 +700,7 @@ End StdTakeDrop. Section PermEq. -Variable disp : unit. -Variable Alph : orderType disp. +Variable (disp : _) (Alph : orderType disp). Implicit Type u v : seq Alph. Theorem perm_stdE u v : perm_eq u v -> std u = std v -> u = v. @@ -737,8 +729,7 @@ End PermEq. (** ** Standardization and elementary transpositions of a word *) Section Transp. -Variable disp : unit. -Variable Alph : inhOrderType disp. +Variable (disp : _) (Alph : inhOrderType disp). Implicit Type u v : seq Alph. Lemma nth_transp u v a b i : diff --git a/theories/Combi/stdtab.v b/theories/Combi/stdtab.v index eebf1db..a441b45 100644 --- a/theories/Combi/stdtab.v +++ b/theories/Combi/stdtab.v @@ -96,7 +96,7 @@ Import Order.Theory. (** ** Appending on the n-th row *) Section AppendNth. -Variables (disp :unit) (T : inhOrderType disp). +Variables (disp : _) (T : inhOrderType disp). Implicit Type b : T. Implicit Type t : seq (seq T). @@ -599,7 +599,7 @@ Qed. End Bijection. -Lemma eq_inv_is_row (d1 d2 : unit) (T1 : inhOrderType d1) (T2 : inhOrderType d2) +Lemma eq_inv_is_row (d1 d2 : _) (T1 : inhOrderType d1) (T2 : inhOrderType d2) (u1 : seq T1) (u2 : seq T2) : eq_inv u1 u2 -> is_row u1 -> is_row u2. Proof. @@ -609,7 +609,7 @@ rewrite -(Hinv i j Hij). exact: Hrow. Qed. -Lemma is_row_stdE (d : unit) (T : inhOrderType d) (w : seq T) : +Lemma is_row_stdE (d : _) (T : inhOrderType d) (w : seq T) : is_row (std w) = is_row w. Proof. by apply/idP/idP; apply eq_inv_is_row; first apply eq_inv_sym; apply: eq_inv_std. @@ -755,7 +755,7 @@ End StdtabnOfStdtabsh. (** * Conjugate of a standard tableau *) Section ConjTab. -Variables (disp: unit) (T : inhOrderType disp). +Variables (disp: _) (T : inhOrderType disp). Definition conj_tab (t : seq (seq T)) : seq (seq T) := let c := conj_part (shape t) in diff --git a/theories/Combi/subseq.v b/theories/Combi/subseq.v index 3f86656..1cd9c7a 100644 --- a/theories/Combi/subseq.v +++ b/theories/Combi/subseq.v @@ -287,7 +287,7 @@ by congr (_ * _); rewrite -big_mkcond. Qed. Lemma big_subseqs_undup (F : seq T -> R) (s : seq T) : - idempotent op -> + idempotent_op op -> \big[*%M/1]_(i : subseqs s) F i = \big[*%M/1]_(m : (size s).-tuple bool) F (mask m s). Proof. @@ -297,7 +297,7 @@ by rewrite big_map big_enum; exact: eq_bigr. Qed. Lemma big_subseqs_undup_cond (F : seq T -> R) (P : pred (seq T)) (s : seq T) : - idempotent op -> + idempotent_op op -> \big[*%M/1]_(i : subseqs s | P i) F i = \big[*%M/1]_(m : (size s).-tuple bool | P (mask m s)) F (mask m s). Proof. diff --git a/theories/Combi/tableau.v b/theories/Combi/tableau.v index 726ded8..5d64b1c 100644 --- a/theories/Combi/tableau.v +++ b/theories/Combi/tableau.v @@ -58,7 +58,7 @@ Import Order.Theory. (** ** Specialization of sorted Lemmas *) Section Rows. -Variables (disp : unit) (T : inhOrderType disp). +Variables (disp : _) (T : inhOrderType disp). Implicit Type l : T. Implicit Type r : seq T. @@ -92,7 +92,7 @@ Notation is_row := (sorted <=%O). (** ** Dominance order for rows *) Section Dominate. -Context {disp : unit} {T : inhOrderType disp}. +Context {disp : _} {T : inhOrderType disp}. Implicit Type l : T. Implicit Type r u v : seq T. @@ -205,7 +205,7 @@ Arguments dominate_rev_trans {disp T}. (** * Tableaux : definition and basic properties *) Section Tableau. -Variables (disp : unit) (T : inhOrderType disp). +Variables (disp : _) (T : inhOrderType disp). Implicit Type l : T. Implicit Type r w : seq T. @@ -522,7 +522,7 @@ Prenex Implicits is_tableau to_word size_tab. (** ** Tableaux from their row reading *) Section TableauReading. -Variables (disp : unit) (A : inhOrderType disp). +Variables (disp : _) (A : inhOrderType disp). Definition tabsh_reading (sh : seq nat) (w : seq A) := (size w == sumn sh) && (is_tableau (rev (reshape (rev sh) w))). @@ -550,7 +550,7 @@ End TableauReading. (** ** Sigma type for tableaux *) Section FinType. -Context {disp : unit} {T : inhFinOrderType disp}. +Context {disp : _} {T : inhFinOrderType disp}. Variables (d : nat) (sh : 'P_d). Definition is_tab_of_shape (sh : seq nat) := @@ -704,7 +704,7 @@ End OrdTableau. (** ** Tableaux and increasing maps *) Section IncrMap. -Context (disp1 disp2 : unit) +Context (disp1 disp2 : _) (T1 : inhOrderType disp1) (T2 : inhOrderType disp2). Variable F : T1 -> T2. diff --git a/theories/Erdos_Szekeres/Erdos_Szekeres.v b/theories/Erdos_Szekeres/Erdos_Szekeres.v index ceda0d4..b934b2f 100644 --- a/theories/Erdos_Szekeres/Erdos_Szekeres.v +++ b/theories/Erdos_Szekeres/Erdos_Szekeres.v @@ -67,8 +67,7 @@ exists sol; repeat split. + by rewrite /sol size_extract /= /cover big_set1. Qed. -Theorem Erdos_Szekeres - (disp : unit) (T : inhOrderType disp) (m n : nat) (s : seq T) : +Theorem Erdos_Szekeres disp (T : inhOrderType disp) (m n : nat) (s : seq T) : size s > m * n -> (exists t, subseq t s /\ sorted <=%O t /\ size t > m) \/ (exists t, subseq t s /\ sorted >%O t /\ size t > n). diff --git a/theories/HookFormula/hook.v b/theories/HookFormula/hook.v index 6b3c7ab..a45da18 100644 --- a/theories/HookFormula/hook.v +++ b/theories/HookFormula/hook.v @@ -395,7 +395,7 @@ Open Scope ring_scope. Lemma hook_length_pred sh rc : (hook_length sh rc)%:~R - 1 = ((hook_length sh rc).-1)%:~R :> rat. -Proof. by rewrite predn_int // !mulrzDr_tmp. Qed. +Proof. by rewrite predn_int // !mulrzDr. Qed. Lemma prod_hook_length_quot_row p Alpha Beta : is_part p -> corner_box p (Alpha, Beta) -> @@ -1032,7 +1032,7 @@ move=> /or3P[] /andP[HA HB]. have:= @addf_div rat 1 Alen%:Q 1 Blen%:Q. rewrite addrC !div1r !mul1r => ->; rewrite ?intr_eq0 ?eqz_nat //. rewrite addrC [LHS]mulrC mulrA mulVf; first by rewrite mul1r invfM mulrC. - rewrite -mulrzDr_tmp /= intr_eq0 eqz_nat. + rewrite -mulrzDr /= intr_eq0 eqz_nat. by rewrite addn_eq0 negb_and Alen0 Blen0. - move: HA => /eqP HA; subst A. rewrite [X in (_ + X)]walk_to_corner_emptyl // addr0. diff --git a/theories/LRrule/Greene.v b/theories/LRrule/Greene.v index 37b53c6..62df025 100644 --- a/theories/LRrule/Greene.v +++ b/theories/LRrule/Greene.v @@ -896,7 +896,7 @@ End Rev. (** * Greene number for tableaux *) Section GreeneRec. -Context {disp : unit} {Alph : inhOrderType disp}. +Context {disp : _} {Alph : inhOrderType disp}. Implicit Type u v w : seq Alph. Implicit Type t : seq (seq Alph). @@ -1529,7 +1529,7 @@ End GreeneRec. (** ** Greene numbers of a tableau *) Section GreeneTab. -Context {disp : unit} {Alph : inhOrderType disp}. +Context {disp : _} {Alph : inhOrderType disp}. Implicit Type t : seq (seq Alph). @@ -1648,7 +1648,7 @@ End GreeneTab. (** ** Recovering a shape from Greene numbers on tableaux *) Theorem Greene_row_tab_eq_shape - (d1 d2 : unit) (T1 : inhOrderType d1) (T2 : inhOrderType d2) + d1 d2 (T1 : inhOrderType d1) (T2 : inhOrderType d2) (t1 : seq (seq T1)) (t2 : seq (seq T2)) : is_tableau t1 -> is_tableau t2 -> (forall k, Greene_row (to_word t1) k = Greene_row (to_word t2) k) -> @@ -1662,7 +1662,7 @@ exact: Heq. Qed. Theorem Greene_col_tab_eq_shape - (d1 d2 : unit) (T1 : inhOrderType d1) (T2 : inhOrderType d2) + d1 d2 (T1 : inhOrderType d1) (T2 : inhOrderType d2) (t1 : seq (seq T1)) (t2 : seq (seq T2)) : is_tableau t1 -> is_tableau t2 -> (forall k, Greene_col (to_word t1) k = Greene_col (to_word t2) k) -> diff --git a/theories/LRrule/Greene_inv.v b/theories/LRrule/Greene_inv.v index b77b7e1..9bfb4ad 100644 --- a/theories/LRrule/Greene_inv.v +++ b/theories/LRrule/Greene_inv.v @@ -140,7 +140,7 @@ Open Scope bool. Section Duality. -Context {disp : unit} {Alph : inhOrderType disp}. +Context {disp : _} {Alph : inhOrderType disp}. Let word := seq Alph. Lemma extract_cut (N : nat) (wt : N.-tuple Alph) (i : 'I_N) (S : {set 'I_N}) : @@ -348,7 +348,7 @@ End Duality. Module Swap. Section Swap. -Context {disp : unit} {Alph : inhOrderType disp}. +Context {disp : _} {Alph : inhOrderType disp}. Let word := seq Alph. Implicit Type a b c : Alph. @@ -486,7 +486,7 @@ Module NoSetContainingBoth. Section Case. -Context {disp : unit} {Alph : inhOrderType disp}. +Context {disp : _} {Alph : inhOrderType disp}. Let word := seq Alph. Implicit Type a b c : Alph. @@ -645,7 +645,7 @@ Module SetContainingBothLeft. (** *** Generic order hypothesis *) Section RelHypothesis. -Context {disp : unit} {Alph : inhOrderType disp}. +Context {disp : _} {Alph : inhOrderType disp}. Implicit Type a b c : Alph. Record hypRabc R a b c := HypRabc { @@ -683,7 +683,7 @@ End RelHypothesis. Section Case. -Context {disp : unit} {Alph : inhOrderType disp}. +Context {disp : _} {Alph : inhOrderType disp}. Let word := seq Alph. Implicit Type u v w r : word. @@ -1287,7 +1287,7 @@ End SetContainingBothLeft. (** * Greene numbers are invariant by each plactic rules *) Section GreeneInvariantsRule. -Context {disp : unit} {Alph : inhOrderType disp}. +Context {disp : _} {Alph : inhOrderType disp}. Let word := seq Alph. Variable u v1 w v2 : word. @@ -1470,7 +1470,7 @@ End GreeneInvariantsRule. (** ** Deducing the other comparisons by duality *) Section GreeneInvariantsDual. -Context {disp : unit} {Alph : inhOrderType disp}. +Context {disp : _} {Alph : inhOrderType disp}. Let word := seq Alph. Implicit Type u v w : word. @@ -1590,7 +1590,7 @@ End GreeneInvariantsDual. (** * Main theorem *) Section GreeneInvariants. -Context {disp : unit} {Alph : inhOrderType disp}. +Context {disp : _} {Alph : inhOrderType disp}. Let word := seq Alph. Implicit Type a b c : Alph. @@ -1692,7 +1692,7 @@ Qed. End GreeneInvariants. Corollary Greene_row_eq_shape_RS - (d1 d2 : unit) (S : inhOrderType d1) (T : inhOrderType d2) + d1 d2 (S : inhOrderType d1) (T : inhOrderType d2) (s : seq S) (t : seq T) : (forall k, Greene_row s k = Greene_row t k) -> (shape (RS s) = shape (RS t)). Proof. @@ -1704,7 +1704,7 @@ exact: HGreene. Qed. Corollary Greene_col_eq_shape_RS - (d1 d2 : unit) (S : inhOrderType d1) (T : inhOrderType d2) + d1 d2 (S : inhOrderType d1) (T : inhOrderType d2) (s : seq S) (t : seq T) : (forall k, Greene_col s k = Greene_col t k) -> (shape (RS s) = shape (RS t)). Proof. @@ -1719,7 +1719,7 @@ Qed. (** ** Reverting uniq words *) Section RevConj. -Context {disp : unit} {Alph : inhOrderType disp}. +Context {disp : _} {Alph : inhOrderType disp}. Implicit Type s : seq Alph. Theorem RS_rev_uniq s : uniq s -> RS (rev s) = conj_tab (RS s). diff --git a/theories/LRrule/Schensted.v b/theories/LRrule/Schensted.v index 1258885..8ebb5a8 100644 --- a/theories/LRrule/Schensted.v +++ b/theories/LRrule/Schensted.v @@ -137,7 +137,7 @@ Import Order.Theory. Section NonEmpty. -Variables (disp : unit) (T : inhOrderType disp). +Variables (disp : _) (T : inhOrderType disp). (** * Schensted's algorithm *) (** ** Row insertion *) @@ -1390,7 +1390,7 @@ by apply/idP/idP => Hstd; apply: (perm_std Hstd); Qed. Section QTableau. -Variables (disp : unit) (T : inhOrderType disp). +Variables (disp : _) (T : inhOrderType disp). Notation TabPair := (seq (seq T) * seq (seq nat) : Type). diff --git a/theories/LRrule/freeSchur.v b/theories/LRrule/freeSchur.v index 6ebe242..11f2715 100644 --- a/theories/LRrule/freeSchur.v +++ b/theories/LRrule/freeSchur.v @@ -152,7 +152,7 @@ End CommutativeImage. (** ** Row reading of tableau *) Section TableauReading. -Context {disp : unit} {A : inhOrderType disp}. +Context {disp : _} {A : inhOrderType disp}. Definition tabsh_reading_RS (sh : seq nat) (w : seq A) := (to_word (RS w) == w) && (shape (RS (w)) == sh). @@ -441,8 +441,7 @@ rewrite sumr_const; congr (_ *+ _). by apply: eq_card => i /=; rewrite unfold_in inE. Qed. -Lemma size_RSmapinv2_yam d - (disp : unit) (Typ : inhOrderType disp) +Lemma size_RSmapinv2_yam d disp (Typ : inhOrderType disp) (tab : seq (seq Typ)) (T : stdtabn d) : size (RSmapinv2 (tab, yam_of_stdtab T)) = d. Proof using . @@ -464,7 +463,7 @@ Hypothesis Hsh2 : shape U2 = shape T2. Section TakeDrop. -Context {disp : unit} {T : inhOrderType disp}. +Context {disp : _} {T : inhOrderType disp}. Lemma RStabE (w : seq T) : (RStab w).1 = (RS w). Proof using . by rewrite RStabmapE. Qed. @@ -526,7 +525,7 @@ Qed. End TakeDrop. -Lemma changeUTK (disp : unit) (T : inhOrderType disp) (w : seq T) : +Lemma changeUTK disp (T : inhOrderType disp) (w : seq T) : (take d1 w) \in langQ U1 -> (drop d1 w) \in langQ U2 -> changeUT U1 U2 (changeUT T1 T2 w) = w. diff --git a/theories/LRrule/plactic.v b/theories/LRrule/plactic.v index b7d6968..ba54fa8 100644 --- a/theories/LRrule/plactic.v +++ b/theories/LRrule/plactic.v @@ -73,7 +73,7 @@ Import Order.Theory. (** * Definition of the Plactic monoid *) Section Defs. -Variables (disp : unit) (Alph : inhOrderType disp). +Variables (disp : _) (Alph : inhOrderType disp). Let word := seq Alph. Implicit Type a b c : Alph. @@ -275,7 +275,7 @@ Notation "a =Pl b" := (plactcongr a b) (at level 70). Section RowsAndCols. -Variables (disp : unit) (Alph : inhOrderType disp). +Variables (disp : _) (Alph : inhOrderType disp). Let word := seq Alph. Implicit Type u v w : word. @@ -329,7 +329,7 @@ End RowsAndCols. (** ** Plactic equivalence and reversal *) Section Rev. -Variables (disp : unit) (Alph : inhOrderType disp). +Variables (disp : _) (Alph : inhOrderType disp). Let word := seq Alph. Implicit Type u v w : word. @@ -386,7 +386,7 @@ End Rev. (** ** Plactic equivalence and order duality *) Section DualRule. -Variables (disp : unit) (Alph : inhOrderType disp). +Variables (disp : _) (Alph : inhOrderType disp). Let word := seq Alph. Implicit Type u v w : word. @@ -439,7 +439,7 @@ Arguments from_revdual {disp Alph}. Section PlactDual. -Variables (disp : unit) (Alph : inhOrderType disp). +Variables (disp : _) (Alph : inhOrderType disp). Let word := seq Alph. Implicit Type u v w : word. @@ -490,7 +490,7 @@ End PlactDual. (** * Plactic monoid and Robinson-Schensted map *) Section RSToPlactic. -Variables (disp : unit) (Alph : inhOrderType disp). +Variables (disp : _) (Alph : inhOrderType disp). Let word := seq Alph. Implicit Type a b c : Alph. @@ -622,7 +622,7 @@ End RSToPlactic. (** ** Removing the last big letter and plactic congruence *) Section RemoveBig. -Variables (disp : unit) (Alph : inhOrderType disp). +Variables (disp : _) (Alph : inhOrderType disp). Let word := seq Alph. Implicit Type a b c : Alph. @@ -830,7 +830,7 @@ End RemoveBig. Section RestrIntervSmall. -Variables (disp : unit) (Alph : inhOrderType disp). +Variables (disp : _) (Alph : inhOrderType disp). Let word := seq Alph. Implicit Type a b c : Alph. @@ -910,7 +910,7 @@ End RestrIntervSmall. Section RestrIntervBig. -Variables (disp : unit) (Alph : inhOrderType disp). +Variables (disp : _) (Alph : inhOrderType disp). Let word := seq Alph. Implicit Type a b c : Alph. @@ -955,9 +955,7 @@ End RestrIntervBig. (** ** Plactic congruence and increasing maps *) Section IncrMap. -Variables (disp1 disp2 : unit) - (T1 : inhOrderType disp1) - (T2 : inhOrderType disp2). +Variables (disp1 disp2 : _) (T1 : inhOrderType disp1) (T2 : inhOrderType disp2). Variable F : T1 -> T2. Variable u v : seq T1. diff --git a/theories/LRrule/shuffle.v b/theories/LRrule/shuffle.v index fd227cb..a9e16ec 100644 --- a/theories/LRrule/shuffle.v +++ b/theories/LRrule/shuffle.v @@ -415,7 +415,7 @@ End ShiftedShuffle. (** * Shifted shuffle and inverse standardized *) Section LRTriple. -Context {disp : unit} {Alph : inhOrderType disp}. +Context {disp : _} {Alph : inhOrderType disp}. Let word := seq Alph. Implicit Type a b c : Alph. @@ -628,7 +628,7 @@ apply: (iffP idP) => /=. + rewrite /= -Hp2 RSmapE; exact: mem_RSclass. Qed. -Lemma filter_gt_RS (d : unit) (T : inhOrderType d) (w : seq T) n : +Lemma filter_gt_RS d (T : inhOrderType d) (w : seq T) n : RS (filter (>%O n) w) = filter_gt_tab n (RS w). Proof using . apply/eqP. diff --git a/theories/LRrule/stdplact.v b/theories/LRrule/stdplact.v index a6cb353..2eaf507 100644 --- a/theories/LRrule/stdplact.v +++ b/theories/LRrule/stdplact.v @@ -46,7 +46,7 @@ Import Order.TTheory. (** ** Plactic congruence and standardization *) Section StdRS. -Context {disp : unit} {Alph : inhOrderType disp}. +Context {disp : _} {Alph : inhOrderType disp}. Implicit Type s u v w : seq Alph. Implicit Type p : seq nat. Implicit Type t : seq (seq Alph). @@ -209,11 +209,11 @@ Proof using. by apply: Greene_row_eq_shape_RS; exact: Greene_std. Qed. End StdRS. -Theorem RSmap_std (d : unit) (T : inhOrderType d) (w : seq T) : +Theorem RSmap_std disp (T : inhOrderType disp) (w : seq T) : (RSmap (std w)).2 = (RSmap w).2. Proof. move Hn : (size w) => n. -elim: n d T w Hn => [/= | n IHn] d T w; first by move/eqP/nilP => ->. +elim: n disp T w Hn => [/= | n IHn] d T w; first by move/eqP/nilP => ->. case/lastP Hw : w => [// | w' wn] Hn. have:= shape_RS_std (rcons w' wn). rewrite -!RSmapE !shape_RSmap_eq. @@ -240,7 +240,7 @@ case HRS : (RSmap st) => [t0 rows]. by case Hins : (instabnrow t0 stn) => [tr irow] /= /incr_nth_inj ->. Qed. -Corollary RStabmap_std (d : unit) (T : inhOrderType d) (w : seq T) : +Corollary RStabmap_std disp (T : inhOrderType disp) (w : seq T) : (RStabmap (std w)).2 = (RStabmap w).2. Proof. rewrite /RStabmap. @@ -538,14 +538,14 @@ case H : (RStabmap (invstd s)) => [P Q]. by rewrite (invseqRSE (invseq_invstd Hstd)) H. Qed. -Corollary RSTabmapstdE (disp : unit) (T : inhOrderType disp) (w : seq T) : +Corollary RSTabmapstdE disp (T : inhOrderType disp) (w : seq T) : (RStabmap (invstd (std w))).1 = (RStabmap (std w)).2. Proof. have := invstdRSE (std_is_std w). by case (RStabmap (invstd (std w))) => [P Q] /= ->. Qed. -Corollary RSinvstdE (disp : unit) (T : inhOrderType disp) (w : seq T) : +Corollary RSinvstdE disp (T : inhOrderType disp) (w : seq T) : RS (invstd (std w)) = (RStabmap w).2. Proof. rewrite -RStabmapE RSTabmapstdE /RStabmap. diff --git a/theories/LRrule/therule.v b/theories/LRrule/therule.v index e82b4c5..1a7ee11 100644 --- a/theories/LRrule/therule.v +++ b/theories/LRrule/therule.v @@ -219,7 +219,7 @@ apply: (plactic_filter_le d1). exact: congr_RS. Qed. -Lemma filter_gt_to_word (d : unit) (T : inhOrderType d) n (t : seq (seq T)) : +Lemma filter_gt_to_word disp (T : inhOrderType disp) n (t : seq (seq T)) : filter (>%O n) (to_word t) = to_word (filter_gt_tab n t). Proof using . elim: t => [// | t0 t IHt] /=. @@ -229,7 +229,7 @@ case: (filter (>%O n) t0 =P [::]) => [->|_] /=. - by rewrite to_word_cons IHt. Qed. -Lemma filter_le_to_word (d : unit) (T : inhOrderType d) n (t : seq (seq T)) : +Lemma filter_le_to_word disp (T : inhOrderType disp) n (t : seq (seq T)) : filter (<=%O n) (to_word t) = to_word (filter_le_tab n t). Proof using . elim: t => [// | t0 t IHt] /=. @@ -553,8 +553,7 @@ Qed. End OneCoeff. -Lemma included_shape_filter_gt_tab - (d : unit) (T : inhOrderType d) (n : T) t : +Lemma included_shape_filter_gt_tab disp (T : inhOrderType disp) (n : T) t : is_tableau t -> included (shape (filter_gt_tab n t)) (shape t). Proof using . elim: t => [// | r0 t /= IHt] /= /and4P[Hnnil Hrow Hdom Htab]. diff --git a/theories/MPoly/Cauchy.v b/theories/MPoly/Cauchy.v index 9720b35..31cf98d 100644 --- a/theories/MPoly/Cauchy.v +++ b/theories/MPoly/Cauchy.v @@ -71,9 +71,11 @@ Proof. exact: Num.Theory.char_num. Qed. Proof. exact: Num.Theory.char_num. Qed. #[local] Hint Resolve char0_algC char0_rat : core. - +#[warning="-postfix-notation-not-level-1"] Reserved Notation "p '(Y)'" (at level 20, format "p '(Y)'"). +#[warning="-postfix-notation-not-level-1"] Reserved Notation "p '(X)'" (at level 20, format "p '(X)'"). +#[warning="-postfix-notation-not-level-1"] Reserved Notation "p '(XY)'" (at level 20, format "p '(XY)'"). diff --git a/theories/MPoly/homogsym.v b/theories/MPoly/homogsym.v index 87652da..bacf9e8 100644 --- a/theories/MPoly/homogsym.v +++ b/theories/MPoly/homogsym.v @@ -94,8 +94,10 @@ Import ssrnum algC GRing.Theory Num.Theory. Reserved Notation "{ 'homsym' T [ n , d ] }" (at level 0, T, n, d at level 2, format "{ 'homsym' T [ n , d ] }"). +#[warning="-closed-notation-not-level-0"] Reserved Notation "'[ p | q ]" (at level 2, format "'[hv' ''[' p | '/ ' q ] ']'"). +#[warning="-closed-notation-not-level-0"] Reserved Notation "'[ p | q ] _( R , n )" (at level 2, format "'[hv' ''[' p | '/ ' q ] ']' '_(' R , n )"). diff --git a/theories/MPoly/sympoly.v b/theories/MPoly/sympoly.v index 7100edb..b9cb880 100644 --- a/theories/MPoly/sympoly.v +++ b/theories/MPoly/sympoly.v @@ -133,11 +133,11 @@ Reserved Notation "{ 'sympoly' T [ n ] }" Reserved Notation "''e_' k" (at level 8, k at level 2, format "''e_' k"). Reserved Notation "''h_' k" (at level 8, k at level 2, format "''h_' k"). Reserved Notation "''p_' k" (at level 8, k at level 2, format "''p_' k"). -Reserved Notation "''e[' k ]" (at level 8, format "''e[' k ]"). -Reserved Notation "''h[' k ]" (at level 8, format "''h[' k ]"). -Reserved Notation "''p[' k ]" (at level 8, format "''p[' k ]"). -Reserved Notation "''m[' k ]" (at level 8, format "''m[' k ]"). -Reserved Notation "''s[' k ]" (at level 8, format "''s[' k ]"). +Reserved Notation "''e[' k ]" (at level 0, format "''e[' k ]"). +Reserved Notation "''h[' k ]" (at level 0, format "''h[' k ]"). +Reserved Notation "''p[' k ]" (at level 0, format "''p[' k ]"). +Reserved Notation "''m[' k ]" (at level 0, format "''m[' k ]"). +Reserved Notation "''s[' k ]" (at level 0, format "''s[' k ]"). Section DefType. diff --git a/theories/SSRcomplements/sorted.v b/theories/SSRcomplements/sorted.v index 76073a7..c4d5066 100644 --- a/theories/SSRcomplements/sorted.v +++ b/theories/SSRcomplements/sorted.v @@ -20,7 +20,7 @@ (******************************************************************************) Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import ssrbool ssrfun ssrnat eqtype fintype choice seq. -From mathcomp Require Import path. +From mathcomp Require Import path order. Set Implicit Arguments. Unset Strict Implicit. diff --git a/theories/SSRcomplements/tools.v b/theories/SSRcomplements/tools.v index c9bc3ca..977acdf 100644 --- a/theories/SSRcomplements/tools.v +++ b/theories/SSRcomplements/tools.v @@ -21,7 +21,7 @@ TODO: these probably should be contributed to SSReflect itself ****************************************************************************) Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import ssrbool ssrfun ssrnat eqtype fintype choice seq. -From mathcomp Require Import finset bigop path binomial. +From mathcomp Require Import finset bigop path binomial order. Set Implicit Arguments. Unset Strict Implicit. @@ -214,7 +214,7 @@ Proof. by rewrite -sumn_take => /take_oversize ->. Qed. (** ** [iota] related lemmas *) Lemma binomial_sumn_iota n : 'C(n, 2) = sumn (iota 0 n). -Proof. by rewrite -triangular_sum sumnE /index_iota subn0. Qed. +Proof. by rewrite -bin2_sum sumnE /index_iota subn0. Qed. Lemma sumn_pred1_iota a b x : sumn [seq ((i == x) : nat) | i <- iota a b] = (a <= x < a + b). diff --git a/theories/SymGroup/Frobenius_char.v b/theories/SymGroup/Frobenius_char.v index e4f6c3f..95bb97e 100644 --- a/theories/SymGroup/Frobenius_char.v +++ b/theories/SymGroup/Frobenius_char.v @@ -71,9 +71,9 @@ Import GroupScope GRing.Theory Num.Theory. Open Scope ring_scope. Reserved Notation "''irrSG[' l ']'" - (at level 8, l at level 2, format "''irrSG[' l ]"). + (at level 0, l at level 2, format "''irrSG[' l ]"). Reserved Notation "''M[' l ']'" - (at level 8, l at level 2, format "''M[' l ]"). + (at level 0, l at level 2, format "''M[' l ]"). #[local] Lemma char0_rat : [char rat] =i pred0. diff --git a/theories/SymGroup/cycletype.v b/theories/SymGroup/cycletype.v index 3f756f1..506d25f 100644 --- a/theories/SymGroup/cycletype.v +++ b/theories/SymGroup/cycletype.v @@ -79,7 +79,7 @@ Import LeqGeqOrder. #[local] Hint Resolve porbit_id : core. Reserved Notation "''1_[' G ]" - (at level 8, G at level 2, format "''1_[' G ]"). + (at level 0, G at level 2, format "''1_[' G ]"). Section CanPorbit. diff --git a/theories/SymGroup/presentSn.v b/theories/SymGroup/presentSn.v index cccbd38..1cd941b 100644 --- a/theories/SymGroup/presentSn.v +++ b/theories/SymGroup/presentSn.v @@ -147,8 +147,8 @@ Notation "''SG_' n" := [set: 'S_n] Reserved Notation "''s_' i" (at level 8, i at level 2, format "''s_' i"). -Reserved Notation "''s_' [ w ] " - (at level 8, w at level 100, format "''s_' [ w ]"). +Reserved Notation "''s_[' w ] " + (at level 0, w at level 100, format "''s_[' w ]"). #[local] Reserved Notation "''II_' n" (at level 8, n at level 2). #[local] Reserved Notation "a =Br b" (at level 70). @@ -321,11 +321,11 @@ End FinType. Lemma card_codesz n : #|{:codesz n}| = n`!. Proof. -rewrite factE /= cardE -(size_map val) enum_codeszE. +rewrite /= cardE -(size_map val) enum_codeszE. elim: n => [//=| n IHn]. rewrite size_flatten -/enum_codesz /shape -map_comp. -rewrite (eq_map (g := fun => fact_rec n)); first last. - by move=> i /=; rewrite size_map. +rewrite (eq_map (g := fun => n`!)); first last. + by move=> i /=; rewrite size_map IHn. by rewrite sumnE big_map big_const_seq count_predT size_iota iter_addn_0 mulnC. Qed. @@ -719,7 +719,7 @@ Notation n := n0.+1. Definition eltr i : 'S_n0.+1 := tperm (inord i) (inord i.+1). Notation "''s_' i" := (eltr i). -Notation "''s_' [ w ]" := (\prod_(i <- w) 's_i). +Notation "''s_[' w ]" := (\prod_(i <- w) 's_i). Implicit Type s t : 'S_n. @@ -875,7 +875,7 @@ Local Notation n := n0.+1. Implicit Type s t : 'S_n. Notation "''s_' i" := (eltr _ i). -Notation "''s_' [ w ]" := (\prod_(i <- w) 's_i). +Notation "''s_[' w ]" := (\prod_(i <- w) 's_i). Lemma eltr_exchange i (a b : 'I_n) : i < n0 -> a < b -> 's_i a < 's_i b = (i != a) || (i.+1 != b). @@ -970,7 +970,7 @@ Variable n0 : nat. Notation n := n0.+1. Notation "''s_' i" := (eltr n0 i). -Notation "''s_' [ w ]" := (\prod_(i <- w) 's_i). +Notation "''s_[' w ]" := (\prod_(i <- w) 's_i). Implicit Type s t u : 'S_n. @@ -1424,7 +1424,7 @@ Variable n : nat. Implicit Type u v w : seq 'I_n. Notation "''s_' i" := (eltr n i). -Notation "''s_' [ w ]" := (\prod_(i <- w) 's_i). +Notation "''s_[' w ]" := (\prod_(i <- w) 's_i). Definition reduced_word := [qualify w : seq 'I_n | length 's_[w] == size w ]. Notation reduced := reduced_word. @@ -1732,7 +1732,7 @@ Section CanWord. Variable (n0 : nat). #[local] Notation n := n0.+1. #[local] Notation "''s_' i" := (eltr n i) : group_scope. -#[local] Notation "''s_' [ w ]" := (\prod_(i <- w) 's_i). +#[local] Notation "''s_[' w ]" := (\prod_(i <- w) 's_i). #[local] Notation "a =Br b" := (braidcongr a b). Fixpoint inscode (c : seq nat) (i : 'I_n) := diff --git a/theories/SymGroup/weak_order.v b/theories/SymGroup/weak_order.v index 7642044..fee6591 100644 --- a/theories/SymGroup/weak_order.v +++ b/theories/SymGroup/weak_order.v @@ -49,7 +49,7 @@ Reserved Notation "s '/\R' t" (at level 70, t at next level). Reserved Notation "s '\/R' t" (at level 70, t at next level). -Fact perm_display : unit. Proof. exact: tt. Qed. +Fact perm_display : Order.disp_t. Proof. by []. Qed. Module WeakOrder. From fded7427bbbc3bfa548c2f8e88ed4a1f285cdf77 Mon Sep 17 00:00:00 2001 From: Florent Hivert Date: Fri, 3 Jan 2025 17:14:24 +0100 Subject: [PATCH 2/8] Nix for MathComp 2.3 --- .../workflows/nix-action-coq8.18-mc2.2.0.yml | 216 ------------------ ...1.0.yml => nix-action-coq8.18-mc2.3.0.yml} | 50 ++-- .../workflows/nix-action-coq8.19-mc2.2.0.yml | 216 ------------------ ...2.0.yml => nix-action-coq8.19-mc2.3.0.yml} | 50 ++-- ...1.0.yml => nix-action-coq8.20-mc2.3.0.yml} | 52 ++--- .nix/config.nix | 24 +- README.md | 2 +- 7 files changed, 76 insertions(+), 534 deletions(-) delete mode 100644 .github/workflows/nix-action-coq8.18-mc2.2.0.yml rename .github/workflows/{nix-action-coq8.17-mc2.1.0.yml => nix-action-coq8.18-mc2.3.0.yml} (90%) delete mode 100644 .github/workflows/nix-action-coq8.19-mc2.2.0.yml rename .github/workflows/{nix-action-coq8.17-mc2.2.0.yml => nix-action-coq8.19-mc2.3.0.yml} (90%) rename .github/workflows/{nix-action-coq8.18-mc2.1.0.yml => nix-action-coq8.20-mc2.3.0.yml} (88%) diff --git a/.github/workflows/nix-action-coq8.18-mc2.2.0.yml b/.github/workflows/nix-action-coq8.18-mc2.2.0.yml deleted file mode 100644 index faa1fb1..0000000 --- a/.github/workflows/nix-action-coq8.18-mc2.2.0.yml +++ /dev/null @@ -1,216 +0,0 @@ -jobs: - coq: - 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 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 coq - uses: cachix/cachix-action@v12 - with: - extraPullNames: coq-community, math-comp - name: coq - - 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.18-mc2.2.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.18-mc2.2.0" - --argstr job "coq" - coq-combi: - 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 coq - uses: cachix/cachix-action@v12 - with: - extraPullNames: coq-community, math-comp - name: coq - - id: stepCheck - name: Checking presence of CI target coq-combi - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.18-mc2.2.0\" --argstr job \"coq-combi\" \\\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.18-mc2.2.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.18-mc2.2.0" - --argstr job "mathcomp-ssreflect" - - 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.18-mc2.2.0" - --argstr job "mathcomp-fingroup" - - 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.18-mc2.2.0" - --argstr job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: multinomials' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18-mc2.2.0" - --argstr job "multinomials" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-character' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18-mc2.2.0" - --argstr job "mathcomp-character" - - 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.18-mc2.2.0" - --argstr job "mathcomp-field" - - 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.18-mc2.2.0" - --argstr job "coq-combi" - mathcomp: - 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 coq - uses: cachix/cachix-action@v12 - with: - extraPullNames: coq-community, math-comp - name: coq - - id: stepCheck - name: Checking presence of CI target mathcomp - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.18-mc2.2.0\" --argstr job \"mathcomp\" \\\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.18-mc2.2.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.18-mc2.2.0" - --argstr job "mathcomp-ssreflect" - - 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.18-mc2.2.0" - --argstr job "mathcomp-fingroup" - - 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.18-mc2.2.0" - --argstr job "mathcomp-algebra" - - 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.18-mc2.2.0" - --argstr job "mathcomp-solvable" - - 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.18-mc2.2.0" - --argstr job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-character' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18-mc2.2.0" - --argstr job "mathcomp-character" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18-mc2.2.0" - --argstr job "hierarchy-builder" - - 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.18-mc2.2.0" - --argstr job "mathcomp" -name: Nix CI for bundle coq8.18-mc2.2.0 -'on': - pull_request: - paths: - - .github/workflows/nix-action-coq8.18-mc2.2.0.yml - pull_request_target: - paths-ignore: - - .github/workflows/nix-action-coq8.18-mc2.2.0.yml - types: - - opened - - synchronize - - reopened - push: - branches: - - master diff --git a/.github/workflows/nix-action-coq8.17-mc2.1.0.yml b/.github/workflows/nix-action-coq8.18-mc2.3.0.yml similarity index 90% rename from .github/workflows/nix-action-coq8.17-mc2.1.0.yml rename to .github/workflows/nix-action-coq8.18-mc2.3.0.yml index fdfd25c..bd985fb 100644 --- a/.github/workflows/nix-action-coq8.17-mc2.1.0.yml +++ b/.github/workflows/nix-action-coq8.18-mc2.3.0.yml @@ -38,12 +38,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.17-mc2.1.0\" --argstr job \"coq\" \\\n --dry-run 2>&1 >\ + \ bundle \"coq8.18-mc2.3.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.17-mc2.1.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18-mc2.3.0" --argstr job "coq" coq-combi: needs: @@ -85,40 +85,36 @@ jobs: - id: stepCheck name: Checking presence of CI target coq-combi run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.17-mc2.1.0\" --argstr job \"coq-combi\" \\\n --dry-run 2>&1\ + \ bundle \"coq8.18-mc2.3.0\" --argstr job \"coq-combi\" \\\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.17-mc2.1.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18-mc2.3.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.17-mc2.1.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18-mc2.3.0" --argstr job "mathcomp-ssreflect" - 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.17-mc2.1.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18-mc2.3.0" --argstr job "mathcomp-fingroup" - 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.17-mc2.1.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18-mc2.3.0" --argstr job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: multinomials' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.17-mc2.1.0" - --argstr job "multinomials" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-character' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.17-mc2.1.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18-mc2.3.0" --argstr job "mathcomp-character" - 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.17-mc2.1.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18-mc2.3.0" --argstr job "mathcomp-field" - 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.17-mc2.1.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18-mc2.3.0" --argstr job "coq-combi" mathcomp: needs: @@ -160,53 +156,53 @@ jobs: - id: stepCheck name: Checking presence of CI target mathcomp run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.17-mc2.1.0\" --argstr job \"mathcomp\" \\\n --dry-run 2>&1\ + \ bundle \"coq8.18-mc2.3.0\" --argstr job \"mathcomp\" \\\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.17-mc2.1.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18-mc2.3.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.17-mc2.1.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18-mc2.3.0" --argstr job "mathcomp-ssreflect" - 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.17-mc2.1.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18-mc2.3.0" --argstr job "mathcomp-fingroup" - 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.17-mc2.1.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18-mc2.3.0" --argstr job "mathcomp-algebra" - 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.17-mc2.1.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18-mc2.3.0" --argstr job "mathcomp-solvable" - 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.17-mc2.1.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18-mc2.3.0" --argstr job "mathcomp-field" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-character' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.17-mc2.1.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18-mc2.3.0" --argstr job "mathcomp-character" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.17-mc2.1.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18-mc2.3.0" --argstr job "hierarchy-builder" - 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.17-mc2.1.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18-mc2.3.0" --argstr job "mathcomp" -name: Nix CI for bundle coq8.17-mc2.1.0 +name: Nix CI for bundle coq8.18-mc2.3.0 'on': pull_request: paths: - - .github/workflows/nix-action-coq8.17-mc2.1.0.yml + - .github/workflows/nix-action-coq8.18-mc2.3.0.yml pull_request_target: paths-ignore: - - .github/workflows/nix-action-coq8.17-mc2.1.0.yml + - .github/workflows/nix-action-coq8.18-mc2.3.0.yml types: - opened - synchronize diff --git a/.github/workflows/nix-action-coq8.19-mc2.2.0.yml b/.github/workflows/nix-action-coq8.19-mc2.2.0.yml deleted file mode 100644 index 739dd6a..0000000 --- a/.github/workflows/nix-action-coq8.19-mc2.2.0.yml +++ /dev/null @@ -1,216 +0,0 @@ -jobs: - coq: - 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 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 coq - uses: cachix/cachix-action@v12 - with: - extraPullNames: coq-community, math-comp - name: coq - - 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.19-mc2.2.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.19-mc2.2.0" - --argstr job "coq" - coq-combi: - 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 coq - uses: cachix/cachix-action@v12 - with: - extraPullNames: coq-community, math-comp - name: coq - - id: stepCheck - name: Checking presence of CI target coq-combi - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.19-mc2.2.0\" --argstr job \"coq-combi\" \\\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.19-mc2.2.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.19-mc2.2.0" - --argstr job "mathcomp-ssreflect" - - 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.19-mc2.2.0" - --argstr job "mathcomp-fingroup" - - 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.19-mc2.2.0" - --argstr job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: multinomials' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.19-mc2.2.0" - --argstr job "multinomials" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-character' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.19-mc2.2.0" - --argstr job "mathcomp-character" - - 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.19-mc2.2.0" - --argstr job "mathcomp-field" - - 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.19-mc2.2.0" - --argstr job "coq-combi" - mathcomp: - 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 coq - uses: cachix/cachix-action@v12 - with: - extraPullNames: coq-community, math-comp - name: coq - - id: stepCheck - name: Checking presence of CI target mathcomp - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.19-mc2.2.0\" --argstr job \"mathcomp\" \\\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.19-mc2.2.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.19-mc2.2.0" - --argstr job "mathcomp-ssreflect" - - 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.19-mc2.2.0" - --argstr job "mathcomp-fingroup" - - 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.19-mc2.2.0" - --argstr job "mathcomp-algebra" - - 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.19-mc2.2.0" - --argstr job "mathcomp-solvable" - - 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.19-mc2.2.0" - --argstr job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-character' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.19-mc2.2.0" - --argstr job "mathcomp-character" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.19-mc2.2.0" - --argstr job "hierarchy-builder" - - 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.19-mc2.2.0" - --argstr job "mathcomp" -name: Nix CI for bundle coq8.19-mc2.2.0 -'on': - pull_request: - paths: - - .github/workflows/nix-action-coq8.19-mc2.2.0.yml - pull_request_target: - paths-ignore: - - .github/workflows/nix-action-coq8.19-mc2.2.0.yml - types: - - opened - - synchronize - - reopened - push: - branches: - - master diff --git a/.github/workflows/nix-action-coq8.17-mc2.2.0.yml b/.github/workflows/nix-action-coq8.19-mc2.3.0.yml similarity index 90% rename from .github/workflows/nix-action-coq8.17-mc2.2.0.yml rename to .github/workflows/nix-action-coq8.19-mc2.3.0.yml index f4382ff..cc17bba 100644 --- a/.github/workflows/nix-action-coq8.17-mc2.2.0.yml +++ b/.github/workflows/nix-action-coq8.19-mc2.3.0.yml @@ -38,12 +38,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.17-mc2.2.0\" --argstr job \"coq\" \\\n --dry-run 2>&1 >\ + \ bundle \"coq8.19-mc2.3.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.17-mc2.2.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.19-mc2.3.0" --argstr job "coq" coq-combi: needs: @@ -85,40 +85,36 @@ jobs: - id: stepCheck name: Checking presence of CI target coq-combi run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.17-mc2.2.0\" --argstr job \"coq-combi\" \\\n --dry-run 2>&1\ + \ bundle \"coq8.19-mc2.3.0\" --argstr job \"coq-combi\" \\\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.17-mc2.2.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.19-mc2.3.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.17-mc2.2.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.19-mc2.3.0" --argstr job "mathcomp-ssreflect" - 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.17-mc2.2.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.19-mc2.3.0" --argstr job "mathcomp-fingroup" - 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.17-mc2.2.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.19-mc2.3.0" --argstr job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: multinomials' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.17-mc2.2.0" - --argstr job "multinomials" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-character' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.17-mc2.2.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.19-mc2.3.0" --argstr job "mathcomp-character" - 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.17-mc2.2.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.19-mc2.3.0" --argstr job "mathcomp-field" - 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.17-mc2.2.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.19-mc2.3.0" --argstr job "coq-combi" mathcomp: needs: @@ -160,53 +156,53 @@ jobs: - id: stepCheck name: Checking presence of CI target mathcomp run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.17-mc2.2.0\" --argstr job \"mathcomp\" \\\n --dry-run 2>&1\ + \ bundle \"coq8.19-mc2.3.0\" --argstr job \"mathcomp\" \\\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.17-mc2.2.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.19-mc2.3.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.17-mc2.2.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.19-mc2.3.0" --argstr job "mathcomp-ssreflect" - 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.17-mc2.2.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.19-mc2.3.0" --argstr job "mathcomp-fingroup" - 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.17-mc2.2.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.19-mc2.3.0" --argstr job "mathcomp-algebra" - 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.17-mc2.2.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.19-mc2.3.0" --argstr job "mathcomp-solvable" - 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.17-mc2.2.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.19-mc2.3.0" --argstr job "mathcomp-field" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-character' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.17-mc2.2.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.19-mc2.3.0" --argstr job "mathcomp-character" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.17-mc2.2.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.19-mc2.3.0" --argstr job "hierarchy-builder" - 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.17-mc2.2.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.19-mc2.3.0" --argstr job "mathcomp" -name: Nix CI for bundle coq8.17-mc2.2.0 +name: Nix CI for bundle coq8.19-mc2.3.0 'on': pull_request: paths: - - .github/workflows/nix-action-coq8.17-mc2.2.0.yml + - .github/workflows/nix-action-coq8.19-mc2.3.0.yml pull_request_target: paths-ignore: - - .github/workflows/nix-action-coq8.17-mc2.2.0.yml + - .github/workflows/nix-action-coq8.19-mc2.3.0.yml types: - opened - synchronize diff --git a/.github/workflows/nix-action-coq8.18-mc2.1.0.yml b/.github/workflows/nix-action-coq8.20-mc2.3.0.yml similarity index 88% rename from .github/workflows/nix-action-coq8.18-mc2.1.0.yml rename to .github/workflows/nix-action-coq8.20-mc2.3.0.yml index edfb658..d805f16 100644 --- a/.github/workflows/nix-action-coq8.18-mc2.1.0.yml +++ b/.github/workflows/nix-action-coq8.20-mc2.3.0.yml @@ -38,12 +38,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.18-mc2.1.0\" --argstr job \"coq\" \\\n --dry-run 2>&1 >\ + \ bundle \"coq8.20-mc2.3.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.18-mc2.1.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.20-mc2.3.0" --argstr job "coq" coq-combi: needs: @@ -85,40 +85,36 @@ jobs: - id: stepCheck name: Checking presence of CI target coq-combi run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.18-mc2.1.0\" --argstr job \"coq-combi\" \\\n --dry-run 2>&1\ + \ bundle \"coq8.20-mc2.3.0\" --argstr job \"coq-combi\" \\\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.18-mc2.1.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.20-mc2.3.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.18-mc2.1.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.20-mc2.3.0" --argstr job "mathcomp-ssreflect" - 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.18-mc2.1.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.20-mc2.3.0" --argstr job "mathcomp-fingroup" - 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.18-mc2.1.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.20-mc2.3.0" --argstr job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: multinomials' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18-mc2.1.0" - --argstr job "multinomials" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-character' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18-mc2.1.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.20-mc2.3.0" --argstr job "mathcomp-character" - 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.18-mc2.1.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.20-mc2.3.0" --argstr job "mathcomp-field" - 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.18-mc2.1.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.20-mc2.3.0" --argstr job "coq-combi" mathcomp: needs: @@ -160,53 +156,49 @@ jobs: - id: stepCheck name: Checking presence of CI target mathcomp run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.18-mc2.1.0\" --argstr job \"mathcomp\" \\\n --dry-run 2>&1\ + \ bundle \"coq8.20-mc2.3.0\" --argstr job \"mathcomp\" \\\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.18-mc2.1.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.20-mc2.3.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.18-mc2.1.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.20-mc2.3.0" --argstr job "mathcomp-ssreflect" - 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.18-mc2.1.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.20-mc2.3.0" --argstr job "mathcomp-fingroup" - 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.18-mc2.1.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.20-mc2.3.0" --argstr job "mathcomp-algebra" - 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.18-mc2.1.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.20-mc2.3.0" --argstr job "mathcomp-solvable" - 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.18-mc2.1.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.20-mc2.3.0" --argstr job "mathcomp-field" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-character' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18-mc2.1.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.20-mc2.3.0" --argstr job "mathcomp-character" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18-mc2.1.0" - --argstr job "hierarchy-builder" - 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.18-mc2.1.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.20-mc2.3.0" --argstr job "mathcomp" -name: Nix CI for bundle coq8.18-mc2.1.0 +name: Nix CI for bundle coq8.20-mc2.3.0 'on': pull_request: paths: - - .github/workflows/nix-action-coq8.18-mc2.1.0.yml + - .github/workflows/nix-action-coq8.20-mc2.3.0.yml pull_request_target: paths-ignore: - - .github/workflows/nix-action-coq8.18-mc2.1.0.yml + - .github/workflows/nix-action-coq8.20-mc2.3.0.yml types: - opened - synchronize diff --git a/.nix/config.nix b/.nix/config.nix index 067c902..be419f0 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -31,19 +31,19 @@ ## select an entry to build in the following `bundles` set ## defaults to "default" - default-bundle = "coq8.18-mc2.1.0"; + default-bundle = "coq8.19-mc2.3.0"; ## write one `bundles.name` attribute set per ## alternative configuration ## When generating GitHub Action CI, one workflow file ## will be created per bundle - bundles."coq8.18-mc2.1.0" = { + bundles."coq8.18-mc2.3.0" = { ## You can override Coq and other Coq coqPackages ## through the following attribute # coqPackages.coq.override.version = "8.11"; coqPackages.coq.override.version = "8.18"; - coqPackages.mathcomp.override.version = "2.2.0"; + coqPackages.mathcomp.override.version = "2.3.0"; ## In some cases, light overrides are not available/enough ## in which case you can use either @@ -83,23 +83,13 @@ # push-branches = [ "master" "branch2" ]; }; - bundles."coq8.17-mc2.2.0" = { - coqPackages.coq.override.version = "8.17"; - coqPackages.mathcomp.override.version = "2.2.0"; - }; - - bundles."coq8.18-mc2.2.0" = { - coqPackages.coq.override.version = "8.18"; - coqPackages.mathcomp.override.version = "2.2.0"; - }; - - bundles."coq8.19-mc2.2.0" = { + bundles."coq8.19-mc2.3.0" = { coqPackages.coq.override.version = "8.19"; - coqPackages.mathcomp.override.version = "2.2.0"; + coqPackages.mathcomp.override.version = "2.3.0"; }; - bundles."coq8.19-mc2.3.0" = { - coqPackages.coq.override.version = "8.19"; + bundles."coq8.20-mc2.3.0" = { + coqPackages.coq.override.version = "8.20"; coqPackages.mathcomp.override.version = "2.3.0"; }; diff --git a/README.md b/README.md index 2b5fd6e..db78922 100644 --- a/README.md +++ b/README.md @@ -3,7 +3,7 @@ Coq-Combi Formalisation of (algebraic) combinatorics in Coq/MathComp. -[![Nix CI for coq8.17-mc2.2.0](https://github.com/math-comp/Coq-Combi/actions/workflows/nix-action-coq8.17-mc2.2.0.yml/badge.svg)](https://github.com/math-comp/Coq-Combi/actions/workflows/nix-action-coq8.17-mc2.2.0.yml) [![Nix CI for coq8.18-mc2.2.0](https://github.com/math-comp/Coq-Combi/actions/workflows/nix-action-coq8.18-mc2.2.0.yml/badge.svg)](https://github.com/math-comp/Coq-Combi/actions/workflows/nix-action-coq8.18-mc2.2.0.yml) [![Nix CI for coq8.19-mc2.2.0](https://github.com/math-comp/Coq-Combi/actions/workflows/nix-action-coq8.19-mc2.2.0.yml/badge.svg)](https://github.com/math-comp/Coq-Combi/actions/workflows/nix-action-coq8.19-mc2.2.0.yml) +[![Nix CI for coq8.18-mc2.3.0](https://github.com/math-comp/Coq-Combi/actions/workflows/nix-action-coq8.18-mc2.3.0.yml/badge.svg)](https://github.com/math-comp/Coq-Combi/actions/workflows/nix-action-coq8.18-mc2.3.0.yml) [![Nix CI for coq8.19-mc2.3.0](https://github.com/math-comp/Coq-Combi/actions/workflows/nix-action-coq8.19-mc2.3.0.yml/badge.svg)](https://github.com/math-comp/Coq-Combi/actions/workflows/nix-action-coq8.19-mc2.3.0.yml) [![Nix CI for coq8.20-mc2.3.0](https://github.com/math-comp/Coq-Combi/actions/workflows/nix-action-coq8.20-mc2.3.0.yml/badge.svg)](https://github.com/math-comp/Coq-Combi/actions/workflows/nix-action-coq8.20-mc2.3.0.yml) Authors ======================================================================== From 3324d958f3694b17833a52dc91d72a65cb715af6 Mon Sep 17 00:00:00 2001 From: Florent Hivert Date: Sat, 4 Jan 2025 18:05:33 +0100 Subject: [PATCH 3/8] Used bilinear maps from new MC 2.0 sesquilinear --- theories/MPoly/Cauchy.v | 4 +- theories/MPoly/homogsym.v | 140 +++++++++++++---------------- theories/SymGroup/Frobenius_char.v | 6 +- theories/SymGroup/towerSn.v | 60 ++++++------- 4 files changed, 94 insertions(+), 116 deletions(-) diff --git a/theories/MPoly/Cauchy.v b/theories/MPoly/Cauchy.v index 31cf98d..c986ed3 100644 --- a/theories/MPoly/Cauchy.v +++ b/theories/MPoly/Cauchy.v @@ -549,12 +549,12 @@ Hypothesis Hd : (d <= n)%N. Definition co_hp (la : 'P_d) : pol -> algC := - homsymdotr 'hp[la] \o in_homsym d (R := algC). + homsymdot^~ 'hp[la] \o in_homsym d (R := algC). Definition co_hpXY (la mu : 'P_d) : polXY -> algC := locked (co_hp la \o map_mpoly (co_hp mu)). Fact co_hp_is_additive la : additive (co_hp la). -Proof. by rewrite /co_hp => p q; rewrite raddfB. Qed. +Proof. by rewrite /co_hp => p q; rewrite /= raddfB homsymdotBl. Qed. HB.instance Definition _ la := GRing.isAdditive.Build pol algC _ (co_hp_is_additive la). diff --git a/theories/MPoly/homogsym.v b/theories/MPoly/homogsym.v index bacf9e8..58c64a1 100644 --- a/theories/MPoly/homogsym.v +++ b/theories/MPoly/homogsym.v @@ -76,6 +76,7 @@ of the scalar product. From HB Require Import structures. From mathcomp Require Import all_ssreflect. From mathcomp Require Import ssralg matrix vector ssrnum algC archimedean. +From mathcomp Require Import sesquilinear. From mathcomp Require Import fingroup perm. From mathcomp Require Import ssrcomplements freeg mpoly. @@ -279,63 +280,53 @@ Fact homsymprod_subproof (p : {homsym R[n, c]}) (q : {homsym R[n, d]}) : Proof. by apply: dhomogM => /=; apply: homsym_is_dhomog. Qed. Canonical homsymprod p q : {homsym R[n, c + d]} := HomogSym (homsymprod_subproof p q). -Definition homsymprodr_head k p q := let: tt := k in homsymprod q p. - -Notation homsymprodr := (homsymprodr_head tt). -#[local] Notation "p *h q" := (homsymprod p q) - (at level 20, format "p *h q"). - -Fact homsymprod_is_linear p : linear (homsymprod p). +Fact homsymprod_is_bilinear : bilinear_for *:%R *:%R homsymprod. Proof. -by move=> a /= u v; apply val_inj; rewrite /= mulrDr -scalerAr. +split => /= p r /= u v; apply val_inj => /=. +- by rewrite mulrDl -scalerAl. +- by rewrite mulrDr -scalerAr. Qed. -HB.instance Definition _ p := - GRing.isLinear.Build - R {homsym R[n, d]} {homsym R[n, (c + d)]} _ _ (homsymprod_is_linear p). +HB.instance Definition _ := + bilinear_isBilinear.Build + R {homsym R[n, c]} {homsym R[n, d]} {homsym R[n, c + d]} + *:%R *:%R homsymprod homsymprod_is_bilinear. -Lemma homsymprodrE p q : homsymprodr p q = q *h p. Proof. by []. Qed. -Fact homsymprodr_is_linear p : linear (homsymprodr p). -Proof. -by move=> a /= u v; apply val_inj; rewrite /= mulrDl -scalerAl. -Qed. -HB.instance Definition _ p := - GRing.isLinear.Build - R {homsym R[n, c]} {homsym R[n, (c + d)]} _ _ (homsymprodr_is_linear p). +#[local] Notation "p *h q" := (homsymprod p q) + (at level 20, format "p *h q"). -Lemma homsymprod0r p : p *h 0 = 0. Proof. exact: raddf0. Qed. +Lemma homsymprod0r p : p *h 0 = 0. Proof. exact: linear0r. Qed. Lemma homsymprodBr p q1 q2 : p *h (q1 - q2) = p *h q1 - p *h q2. -Proof. exact: raddfB. Qed. +Proof. exact: linearBr. Qed. Lemma homsymprodNr p q : p *h (- q) = - p *h q. -Proof. exact: raddfN. Qed. +Proof. exact: linearNr. Qed. Lemma homsymprodDr p q1 q2 : p *h (q1 + q2) = p *h q1 + p *h q2. -Proof. exact: raddfD. Qed. +Proof. exact: linearDr. Qed. Lemma homsymprodMnr p q m : p *h (q *+ m) = (p *h q) *+ m. -Proof. exact: raddfMn. Qed. +Proof. exact: linearMnr. Qed. Lemma homsymprod_sumr p I r (P : pred I) (q : I -> {homsym R[n, d]}) : p *h (\sum_(i <- r | P i) q i) = \sum_(i <- r | P i) p *h q i. -Proof. exact: raddf_sum. Qed. +Proof. exact: linear_sumr. Qed. Lemma homsymprodZr a p q : p *h (a *: q) = a *: (p *h q). -Proof. by rewrite linearZ. Qed. +Proof. by rewrite linearZr. Qed. Lemma homsymprod0l p : 0 *h p = 0. -Proof. by rewrite -homsymprodrE linear0. Qed. +Proof. by rewrite linear0l. Qed. Lemma homsymprodNl p q : (- q) *h p = - q *h p. -Proof. by rewrite -!homsymprodrE linearN. Qed. +Proof. by rewrite linearNl. Qed. Lemma homsymprodDl p q1 q2 : (q1 + q2) *h p = q1 *h p + q2 *h p. -Proof. by rewrite -!homsymprodrE linearD. Qed. +Proof. by rewrite linearDl. Qed. Lemma homsymprodBl p q1 q2 : (q1 - q2) *h p = q1 *h p - q2 *h p. -Proof. by rewrite -!homsymprodrE linearB. Qed. +Proof. by rewrite linearBl. Qed. Lemma homsymprodMnl p q m : (q *+ m) *h p = q *h p *+ m. -Proof. by rewrite -!homsymprodrE linearMn. Qed. +Proof. by rewrite linearMnl. Qed. Lemma homsymprod_suml p I r (P : pred I) (q : I -> {homsym R[n, c]}) : (\sum_(i <- r | P i) q i) *h p = \sum_(i <- r | P i) q i *h p. -Proof. by rewrite -!homsymprodrE linear_sum. Qed. +Proof. by rewrite linear_sumlz. Qed. Lemma homsymprodZl p a q : (a *: q) *h p = a *: q *h p. -Proof. by rewrite -!homsymprodrE linearZ. Qed. +Proof. by rewrite linearZl. Qed. End HomogSymProd. -Notation homsymprodr := (homsymprodr_head tt). Notation "p *h q" := (homsymprod p q) (at level 20, format "p *h q"). @@ -837,18 +828,14 @@ Proof. exact: char_num. Qed. (** * The scalar product *) Section ScalarProduct. -Variable n0 d : nat. +Context {n0 d : nat}. #[local] Notation n := (n0.+1). #[local] Notation HSF := {homsym algC[n, d]}. Definition homsymdot (p q : HSF) : algC := \sum_(i < #|{:'P_d}|) (zcard (enum_val i))%:R * (coord 'hp i p) * (coord 'hp i q)^*. -Definition homsymdotr_head k p q := let: tt := k in homsymdot q p. - -Notation homsymdotr := (homsymdotr_head tt). Notation "''[' u | v ]" := (homsymdot u v) : ring_scope. - Lemma homsymdotE p q : '[ p | q ] = \sum_(la : 'P_d) (zcard la)%:R * @@ -857,63 +844,61 @@ Proof. rewrite /homsymdot [RHS](reindex _ (onW_bij _ (@enum_val_bij _))) /=. by apply/eq_bigr => i _; rewrite enum_valK. Qed. -Lemma homsymdotrE p q : homsymdotr p q = '[q | p]. Proof. by []. Qed. - -Fact homsymdotr_is_scalar p : scalar (homsymdotr p). +Lemma homsymdotC p q : '[p | q] = ('[q | p])^*. +Proof. +rewrite /homsymdot rmorph_sum /=. +apply: eq_bigr=> x _. +rewrite [in RHS]rmorphM [X in _ = X * _]rmorphM conjCK -!mulrA. +have /geC0_conj -> : 0 <= ((zcard (enum_val x))%:R : algC). + by rewrite -nnegrE ?nnegrE ?ler01 ?ler0n ?oner_neq0. +by congr (_ * _); rewrite mulrC. +Qed. +Fact homsymdot_is_bilinear : bilinear_for *%R (Num.conj_op \; *%R) homsymdot. Proof. -move=> a /= u v. -rewrite mulr_sumr /= -big_split; apply: eq_bigr => x _ /=. -rewrite linearD linearZ /= mulrDr mulrDl !mulrA; congr (_ + _). -by rewrite [_ * a]mulrC -!mulrA. +have lin r p u v : '[r *: u + v | p] = r * '[u | p] + '[v | p]. + rewrite !homsymdotE mulr_sumr /= -big_split; apply: eq_bigr => x _ /=. + rewrite linearD linearZ /= mulrDr mulrDl !mulrA; congr (_ + _). + by rewrite [_ * r]mulrC -!mulrA. +split => /= p r /= u v; first exact: lin. +by rewrite !(homsymdotC p) lin rmorphD rmorphM. Qed. -HB.instance Definition _ p := - GRing.isLinear.Build - algC {homsym algC[n, d]} algC _ _ (homsymdotr_is_scalar p). +HB.instance Definition _ := + bilinear_isBilinear.Build algC HSF HSF algC *%R (Num.conj_op \; *%R) + homsymdot homsymdot_is_bilinear. +Notation "''[' u | v ]" := (homsymdot u v) : ring_scope. Lemma homsymdot0l p : '[0 | p] = 0. -Proof. by rewrite -homsymdotrE linear0. Qed. +Proof. exact: linear0l. Qed. Lemma homsymdotNl p q : '[- q | p] = - '[q | p]. -Proof. by rewrite -!homsymdotrE linearN. Qed. +Proof. exact: linearNl. Qed. Lemma homsymdotDl p q1 q2 : '[q1 + q2 | p] = '[q1 | p] + '[q2 | p]. -Proof. by rewrite -!homsymdotrE linearD. Qed. +Proof. exact: linearDl. Qed. Lemma homsymdotBl p q1 q2 : '[q1 - q2 | p] = '[q1 | p] - '[q2 | p]. -Proof. by rewrite -!homsymdotrE linearB. Qed. +Proof. exact: linearBl. Qed. Lemma homsymdotMnl p q n : '[q *+ n | p] = '[q | p] *+ n. -Proof. by rewrite -!homsymdotrE linearMn. Qed. +Proof. exact: linearMnl. Qed. Lemma homsymdot_suml p I r (P : pred I) (q : I -> HSF) : '[\sum_(i <- r | P i) q i | p] = \sum_(i <- r | P i) '[q i | p]. -Proof. by rewrite -!homsymdotrE linear_sum. Qed. +Proof. exact: linear_sumlz. Qed. Lemma homsymdotZl p a q : '[a *: q | p] = a * '[q | p]. -Proof. by rewrite -!homsymdotrE linearZ. Qed. - -Lemma homsymdotC p q : '[p | q] = ('[q | p])^*. -Proof. -rewrite /homsymdot rmorph_sum /=. -apply: eq_bigr=> x _. -rewrite [in RHS]rmorphM [X in _ = X * _]rmorphM conjCK -!mulrA. -have /geC0_conj -> : 0 <= ((zcard (enum_val x))%:R : algC). - by rewrite -nnegrE ?nnegrE ?ler01 ?ler0n ?oner_neq0. -by congr (_ * _); rewrite mulrC. -Qed. +Proof. exact: linearZl. Qed. -Lemma homsymdotBr p q1 q2 : '[p | q1 - q2] = '[p | q1] - '[p | q2]. -Proof. by rewrite !(homsymdotC p) -rmorphB homsymdotBl. Qed. -HB.instance Definition _ p := - GRing.isAdditive.Build - {homsym algC[n, d]} algC _ (homsymdotBr p). -Lemma homsymdot0r p : '[p | 0] = 0. Proof. exact: raddf0. Qed. +Lemma homsymdot0r p : '[p | 0] = 0. +Proof. exact: linear0r. Qed. Lemma homsymdotNr p q : '[p | - q] = - '[p | q]. -Proof. exact: raddfN. Qed. +Proof. exact: linearNr. Qed. Lemma homsymdotDr p q1 q2 : '[p | q1 + q2] = '[p | q1] + '[p | q2]. -Proof. exact: raddfD. Qed. +Proof. exact: linearDr. Qed. +Lemma homsymdotBr p q1 q2 : '[p | q1 - q2] = '[p | q1] - '[p | q2]. +Proof. exact: linearBr. Qed. Lemma homsymdotMnr p q n : '[p | q *+ n] = '[p | q] *+ n. -Proof. exact: raddfMn. Qed. +Proof. exact: linearMnr. Qed. Lemma homsymdot_sumr p I r (P : pred I) (q : I -> HSF) : '[p | \sum_(i <- r | P i) q i] = \sum_(i <- r | P i) '[p | q i]. -Proof. exact: raddf_sum. Qed. +Proof. exact: linear_sumr. Qed. Lemma homsymdotZr a p q : '[p | a *: q] = a^* * '[p | q]. -Proof. by rewrite !(homsymdotC p) homsymdotZl rmorphM. Qed. +Proof. exact: linearZr. Qed. Lemma homsymdotpp (Hd : (d <= n)%N) la mu : '[ 'hp[la] | 'hp[mu] ] = (zcard la)%:R * (la == mu)%:R. @@ -947,7 +932,6 @@ Qed. End ScalarProduct. -Notation homsymdotr := (homsymdotr_head tt). Notation "''[' u | v ]" := (homsymdot u v) : ring_scope. Notation "''[' u | v ] _( n , d )" := (@homsymdot n d u v) (only parsing) : ring_scope. diff --git a/theories/SymGroup/Frobenius_char.v b/theories/SymGroup/Frobenius_char.v index 95bb97e..c147420 100644 --- a/theories/SymGroup/Frobenius_char.v +++ b/theories/SymGroup/Frobenius_char.v @@ -52,6 +52,7 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect. From mathcomp Require Import fingroup perm morphism gproduct. From mathcomp Require Import rat ssralg ssrint ssrnum algC vector archimedean. +From mathcomp Require Import sesquilinear. From mathcomp Require Import mxrepresentation classfun character. From mathcomp Require Import mpoly. @@ -253,7 +254,8 @@ dependent equality but I'm not sure this is really needed. Theorem Fchar_ind_morph m n (f : 'CF('SG_m)) (g : 'CF('SG_n)) : Fchar ('Ind['SG_(m + n)] (f \o^ g)) = Fchar f *h Fchar g. Proof using. -rewrite (ncfuniCT_gen f) (ncfuniCT_gen g) !linear_sum; apply eq_bigr => /= l _. +rewrite (ncfuniCT_gen f) (ncfuniCT_gen g). +rewrite !(linear_sum, linear_sumr); apply eq_bigr => /= l _. rewrite cfextprod_suml homsymprod_suml !linear_sum; apply eq_bigr => /= k _. do 2 rewrite [in RHS]linearZ /= Fchar_ncfuniCT. rewrite cfextprodZr cfextprodZl homsymprodZr homsymprodZl !scalerA. @@ -492,7 +494,7 @@ Qed. Theorem Murnaghan_Nakayama_char n la (sigma : 'S_n) : 'irrSG[la] sigma = (MN_coeff la (cycle_typeSn sigma))%:~R. Proof. -rewrite Frobenius_char_homsymdot MN_coeff_homogP raddf_sum /=. +rewrite Frobenius_char_homsymdot MN_coeff_homogP homsymdot_sumr /=. rewrite (bigD1 la) //= big1 ?addr0 //; first last => [i /negbTE Hi|]. by rewrite homsymdotZr homsymdotss // eq_sym Hi mulr0. rewrite homsymdotZr homsymdotss // eqxx mulr1. diff --git a/theories/SymGroup/towerSn.v b/theories/SymGroup/towerSn.v index 3b2fdde..756e209 100644 --- a/theories/SymGroup/towerSn.v +++ b/theories/SymGroup/towerSn.v @@ -63,6 +63,7 @@ From mathcomp Require Import all_ssreflect. From mathcomp Require Import ssralg fingroup morphism perm gproduct. From mathcomp Require Import ssrnum matrix vector mxalgebra algC. From mathcomp Require Import classfun character mxrepresentation. +From mathcomp Require Import sesquilinear. Require Import tools ordcast partition sorted. Require Import permcomp cycles cycletype permcent. @@ -134,12 +135,11 @@ rewrite genGid; apply intro_class_fun => [x y|]. + by rewrite [h _]cfun0gen ?mulr0 ?genGid. Qed. Definition cfextprod g h := Cfun 0 (cfextprod_subproof g h). -Definition cfextprodr_head k g h := let: tt := k in cfextprod h g. End CFExtProdDefs. Notation "f \ox g" := (cfextprod f g) (at level 40, left associativity). -Notation cfextprodr := (cfextprodr_head tt). + Section CFExtProdTheory. @@ -149,58 +149,50 @@ Implicit Type (g : 'CF(G)) (h : 'CF(H)). #[local] Open Scope ring_scope. -Lemma cfextprodrE h g : cfextprodr h g = g \ox h. -Proof using. by []. Qed. - -Fact cfextprod_is_linear g : linear (cfextprod g : 'CF(H) -> 'CF(setX G H)). -Proof using. -move=> /= a h1 h2. -apply/cfunP=> /= x. -by rewrite !cfunE !mulrDr mulrA [g _ * _]mulrC mulrA. +Fact cfextprod_is_bilinear : + bilinear_for *:%R *:%R (cfextprod (G := G) (H := H)). +Proof. +split => /= g r /= h1 h2; apply/cfunP => /= x. +- by rewrite !cfunE !mulrDl -mulrA. +- by rewrite !cfunE !mulrDr mulrA [g _ * _]mulrC mulrA. Qed. -HB.instance Definition _ g := - GRing.isLinear.Build algC 'CF(H) 'CF(setX G H) _ _ (cfextprod_is_linear g). +HB.instance Definition _ := + bilinear_isBilinear.Build + algC 'CF(G) 'CF(H) 'CF(setX G H) + *:%R *:%R (cfextprod (G := G) (H := H)) cfextprod_is_bilinear. Lemma cfextprod0r g : g \ox (0 : 'CF(H)) = 0. -Proof using. by rewrite linear0. Qed. +Proof using. by rewrite linear0r. Qed. Lemma cfextprodNr g h : g \ox - h = - (g \ox h). -Proof using. by rewrite linearN. Qed. +Proof using. by rewrite linearNr. Qed. Lemma cfextprodDr g h1 h2 : g \ox (h1 + h2) = g \ox h1 + g \ox h2. -Proof using. by rewrite linearD. Qed. +Proof using. by rewrite linearDr. Qed. Lemma cfextprodBr g h1 h2 : g \ox (h1 - h2) = g \ox h1 - g \ox h2. -Proof using. by rewrite linearB. Qed. +Proof using. by rewrite linearBr. Qed. Lemma cfextprodMnr h g n : g \ox (h *+ n) = (g \ox h) *+ n. -Proof using. by rewrite linearMn. Qed. +Proof using. by rewrite linearMnr. Qed. Lemma cfextprod_sumr g I r (P : pred I) (phi : I -> 'CF(H)) : g \ox (\sum_(i <- r | P i) phi i) = \sum_(i <- r | P i) g \ox phi i. -Proof using. by rewrite linear_sum. Qed. +Proof using. by rewrite linear_sumr. Qed. Lemma cfextprodZr g a h : g \ox (a *: h) = a *: (g \ox h). -Proof using. by rewrite linearZ. Qed. +Proof using. by rewrite linearZr. Qed. -Fact cfextprodr_is_linear h : linear (cfextprodr h : 'CF(G) -> 'CF(setX G H)). -Proof using. -move=> /= a g1 g2; rewrite !cfextprodrE. -apply/cfunP=> /= x. -by rewrite !cfunE !mulrDl -mulrA. -Qed. -HB.instance Definition _ h := - GRing.isLinear.Build algC 'CF(G) 'CF(setX G H) _ _ (cfextprodr_is_linear h). Lemma cfextprod0l h : (0 : 'CF(G)) \ox h = 0. -Proof using. by rewrite -cfextprodrE linear0. Qed. +Proof using. by rewrite linear0l. Qed. Lemma cfextprodNl h g : - g \ox h = - g \ox h. -Proof using. by rewrite -!cfextprodrE linearN. Qed. +Proof using. by rewrite linearNl. Qed. Lemma cfextprodDl h g1 g2 : (g1 + g2) \ox h = g1 \ox h + g2 \ox h. -Proof using. by rewrite -!cfextprodrE linearD. Qed. +Proof using. by rewrite linearDl. Qed. Lemma cfextprodBl h g1 g2 : (g1 - g2) \ox h = g1 \ox h - g2 \ox h. -Proof using. by rewrite -!cfextprodrE linearB. Qed. +Proof using. by rewrite linearBl. Qed. Lemma cfextprodMnl h g n : g *+ n \ox h = g \ox h *+ n. -Proof using. by rewrite -!cfextprodrE linearMn. Qed. +Proof using. by rewrite linearMnl. Qed. Lemma cfextprod_suml h I r (P : pred I) (phi : I -> 'CF(G)) : (\sum_(i <- r | P i) phi i) \ox h = \sum_(i <- r | P i) phi i \ox h. -Proof using. by rewrite -!cfextprodrE linear_sum. Qed. +Proof using. by rewrite linear_sumlz. Qed. Lemma cfextprodZl h a g : (a *: g) \ox h = a *: (g \ox h). -Proof using. by rewrite -!cfextprodrE linearZ. Qed. +Proof using. by rewrite linearZl. Qed. Section ReprExtProd. From 68bf88a54fbab21513f21478c57d2dedc5f17797 Mon Sep 17 00:00:00 2001 From: Florent Hivert Date: Sun, 5 Jan 2025 12:27:49 +0100 Subject: [PATCH 4/8] Orthogonal and orthonormal from sesquilinear --- theories/MPoly/Cauchy.v | 38 ++++--- theories/MPoly/homogsym.v | 160 +++++++++++++++++++++-------- theories/SymGroup/Frobenius_char.v | 4 +- 3 files changed, 140 insertions(+), 62 deletions(-) diff --git a/theories/MPoly/Cauchy.v b/theories/MPoly/Cauchy.v index c986ed3..c4f0cb1 100644 --- a/theories/MPoly/Cauchy.v +++ b/theories/MPoly/Cauchy.v @@ -50,6 +50,7 @@ orthonormal for the scalar product. From HB Require Import structures. From mathcomp Require Import all_ssreflect. From mathcomp Require Import ssrint rat ssralg ssrnum algC matrix vector. +From mathcomp Require Import sesquilinear. From mathcomp Require Import mpoly. Require Import tools partition ordtype. @@ -71,12 +72,11 @@ Proof. exact: Num.Theory.char_num. Qed. Proof. exact: Num.Theory.char_num. Qed. #[local] Hint Resolve char0_algC char0_rat : core. -#[warning="-postfix-notation-not-level-1"] +Set Warnings "-postfix-notation-not-level-1". Reserved Notation "p '(Y)'" (at level 20, format "p '(Y)'"). -#[warning="-postfix-notation-not-level-1"] Reserved Notation "p '(X)'" (at level 20, format "p '(X)'"). -#[warning="-postfix-notation-not-level-1"] Reserved Notation "p '(XY)'" (at level 20, format "p '(XY)'"). +Set Warnings "postfix-notation-not-level-1". (** ** Polynomials in two sets of variables *) @@ -534,18 +534,13 @@ Variable n0 d : nat. Hypothesis Hd : (d <= n)%N. #[local] Notation HSC := {homsym algC[n, d]}. -#[local] Notation HSQ := {homsym rat[n, d]}. #[local] Notation polXY := (polXY n0 n0 algC). #[local] Notation pol := {mpoly algC[n]}. -#[local] Notation "p '(Y)'" := (@polY_XY n0 n0 _ p) - (at level 20, format "p '(Y)'"). -#[local] Notation "p '(X)'" := (@polX_XY n0 n0 _ p) - (at level 20, format "p '(X)'"). +#[local] Notation "p '(Y)'" := (@polY_XY n0 n0 _ p). +#[local] Notation "p '(X)'" := (@polX_XY n0 n0 _ p). #[local] Notation "''hsC[' la ]" := ('hs[la] : HSC). -#[local] Notation "''hsQ[' la ]" := ('hs[la] : HSQ). #[local] Notation "''hpC[' la ]" := ('hp[la] : HSC). -#[local] Notation "''hpQ[' la ]" := ('hp[la] : HSQ). Definition co_hp (la : 'P_d) : pol -> algC := @@ -653,10 +648,10 @@ Lemma coord_zsymspsp (la mu : 'P_d) : ((zcard nu)%:R * coord 'hp (enum_rank nu) 'hsC[mu])) = (la == mu)%:R. Proof using Hd. -pose matsp : 'M[algC]_#|{:'P_d}| := - \matrix_(i, j < #|{:'P_d}|) (coord 'hp i 'hsC[enum_val j]). -pose matzsp : 'M[algC]_#|{:'P_d}| := - \matrix_(i, j < #|{:'P_d}|) +pose matsp : 'M[algC]_#|{: 'P_d}| := + \matrix_(i, j < #|{: 'P_d}|) (coord 'hp i 'hsC[enum_val j]). +pose matzsp : 'M[algC]_#|{: 'P_d}| := + \matrix_(i, j < #|{: 'P_d}|) ((zcard (enum_val j))%:R * (coord 'hp j 'hsC[enum_val i])). have: matsp *m matzsp = 1%:M. apply/matrixP => i j /=. @@ -688,7 +683,7 @@ transitivity rewrite homsymdot_suml; apply eq_bigr => /= l _. rewrite homsymdotZl homsymdot_sumr -mulrA; congr (_ * _). transitivity - (\sum_(i < #|{:'P_d}|) + (\sum_(i < #|{: 'P_d}|) (coord 'hp i 'hsC[mu])^* * (zcard (enum_val l))%:R * (i == l)%:R). apply: eq_bigr => i _; rewrite homsymdotZr -mulrA; congr (_ * _). rewrite !(nth_map inh _ (fun l => 'hp[l])) -?cardE ?ltn_ord //. @@ -698,5 +693,18 @@ rewrite eq_refl mulr1 mulrC; congr (_ * _). by rewrite -coord_map_homsym ?map_homsymbp ?symbp_basis // map_homsyms. Qed. +Theorem homsyms_orthonormal : orthonormal homsymdot ('hs : seq HSC). +Proof. +have hs_uniq := free_uniq (basis_free (symbs_basis algC Hd)). +apply/orthonormalP; split => /=; first exact: hs_uniq. +have {hs_uniq} hs_inj : injective (fun la : 'P_d => 'hs[la] : HSC). + move=> /= la mu. + have /tnthP[i /[dup] eqla ->] : la \in enum {: 'P_d} by rewrite mem_enum. + have /tnthP[j /[dup] eqmu ->] : mu \in enum {: 'P_d} by rewrite mem_enum. + by rewrite -!['hs[_]]tnth_map => /(tuple_uniqP _ hs_uniq) ->. +move=> f g /mapP[/= la _ {f}->]/mapP[/= mu _ {g}->]. +by rewrite homsymdotss (inj_eq hs_inj). +Qed. + End Scalar. diff --git a/theories/MPoly/homogsym.v b/theories/MPoly/homogsym.v index 58c64a1..6207108 100644 --- a/theories/MPoly/homogsym.v +++ b/theories/MPoly/homogsym.v @@ -93,15 +93,35 @@ Import ssrnum algC GRing.Theory Num.Theory. #[local] Open Scope nat_scope. #[local] Open Scope ring_scope. +Reserved Notation "d .-homsym" (at level 1, format "d .-homsym"). +Reserved Notation "[ 'in' R [ n ] , d .-homsym ]" + (at level 0, R, n at level 2, d at level 0, + format "[ 'in' R [ n ] , d .-homsym ]"). Reserved Notation "{ 'homsym' T [ n , d ] }" (at level 0, T, n, d at level 2, format "{ 'homsym' T [ n , d ] }"). -#[warning="-closed-notation-not-level-0"] + +Set Warnings "-closed-notation-not-level-0". +Reserved Notation "''he[' k ]" (at level 8, k at level 2, format "''he[' k ]"). +Reserved Notation "''hh[' k ]" (at level 8, k at level 2, format "''hh[' k ]"). +Reserved Notation "''hp[' k ]" (at level 8, k at level 2, format "''hp[' k ]"). +Reserved Notation "''hm[' k ]" (at level 8, k at level 2, format "''hm[' k ]"). +Reserved Notation "''hs[' k ]" (at level 8, k at level 2, format "''hs[' k ]"). + +Reserved Notation "''he'" (at level 8, format "''he'"). +Reserved Notation "''hh'" (at level 8, format "''hh'"). +Reserved Notation "''hp'" (at level 8, format "''hp'"). +Reserved Notation "''hm'" (at level 8, format "''hm'"). +Reserved Notation "''hs'" (at level 8, format "''hs'"). + +Reserved Notation "p *h q" (at level 20, format "p *h q"). + Reserved Notation "'[ p | q ]" (at level 2, format "'[hv' ''[' p | '/ ' q ] ']'"). -#[warning="-closed-notation-not-level-0"] Reserved Notation "'[ p | q ] _( R , n )" (at level 2, format "'[hv' ''[' p | '/ ' q ] ']' '_(' R , n )"). +Set Warnings "closed-notation-not-level-0". + Definition ishomogsym1 {n} {R : ringType} (d : nat) : qualifier 0 {sympoly R[n]} := [qualify p | sympol p \is d.-homog]. @@ -113,11 +133,9 @@ Definition homogsym1_keyed {n R} d := KeyedQualifier (@homogsym1_key n R d). End SymPolyHomogKey. Canonical SymPolyHomogKey.homogsym1_keyed. -Notation "d .-homsym" := (@ishomogsym1 _ _ d) - (at level 1, format "d .-homsym") : form_scope. -Notation "[ 'in' R [ n ] , d .-homsym ]" := (@ishomogsym1 n R d) - (at level 0, R, n at level 2, d at level 0, - format "[ 'in' R [ n ] , d .-homsym ]") : form_scope. +Notation "d .-homsym" := (@ishomogsym1 _ _ d) : form_scope. +Notation "[ 'in' R [ n ] , d .-homsym ]" := (@ishomogsym1 n R d) : form_scope. + (** ** Homogeneous symmetric polynomials *) Section DefType. @@ -151,7 +169,6 @@ Bind Scope ring_scope with homogsym. (* Arguments homogsym n%_N R%_R. *) (* Arguments homsym_inj n%_N R%_R d%_N. *) - Notation "{ 'homsym' T [ n , d ] }" := (homogsym n T d). Section HomogSymLModType. @@ -256,16 +273,11 @@ HB.instance Definition _ := Lmodule_hasFinDim.Build R {homsym R[n, d]} End Vector. -Notation "''he[' k ]" := (homsyme _ _ k) - (at level 8, k at level 2, format "''he[' k ]"). -Notation "''hh[' k ]" := (homsymh _ _ k) - (at level 8, k at level 2, format "''hh[' k ]"). -Notation "''hp[' k ]" := (homsymp _ _ k) - (at level 8, k at level 2, format "''hp[' k ]"). -Notation "''hm[' k ]" := (homsymm _ _ k) - (at level 8, k at level 2, format "''hm[' k ]"). -Notation "''hs[' k ]" := (homsyms _ _ k) - (at level 8, k at level 2, format "''hs[' k ]"). +Notation "''he[' k ]" := (homsyme _ _ k). +Notation "''hh[' k ]" := (homsymh _ _ k). +Notation "''hp[' k ]" := (homsymp _ _ k). +Notation "''hm[' k ]" := (homsymm _ _ k). +Notation "''hs[' k ]" := (homsyms _ _ k). (** ** Products of homogeneous symmetric polynomials *) @@ -291,8 +303,8 @@ HB.instance Definition _ := R {homsym R[n, c]} {homsym R[n, d]} {homsym R[n, c + d]} *:%R *:%R homsymprod homsymprod_is_bilinear. -#[local] Notation "p *h q" := (homsymprod p q) - (at level 20, format "p *h q"). +#[local] Notation "p *h q" := (homsymprod p q). + Lemma homsymprod0r p : p *h 0 = 0. Proof. exact: linear0r. Qed. Lemma homsymprodBr p q1 q2 : p *h (q1 - q2) = p *h q1 - p *h q2. @@ -327,8 +339,8 @@ Proof. by rewrite linearZl. Qed. End HomogSymProd. -Notation "p *h q" := (homsymprod p q) - (at level 20, format "p *h q"). +Notation "p *h q" := (homsymprod p q). + Section HomSymProdGen. @@ -337,20 +349,31 @@ Variable n0 : nat. Variable R : comRingType. #[local] Notation HSF := {homsym R[n, _]}. -Import LeqGeqOrder. +Section Merge. +Variables (d1 d2 : nat) (la : 'P_d1) (mu : 'P_d2). +Lemma homsymprod_hh : 'hh[la] *h 'hh[mu] = 'hh[la +|+ mu] :> HSF. +Proof. by apply val_inj; rewrite /= prod_genM. Qed. +Lemma homsymprod_he : 'he[la] *h 'he[mu] = 'he[la +|+ mu] :> HSF. +Proof. by apply val_inj; rewrite /= prod_genM. Qed. +Lemma homsymprod_hp : 'hp[la] *h 'hp[mu] = 'hp[la +|+ mu] :> HSF. +Proof. by apply val_inj; rewrite /= prod_genM. Qed. +End Merge. + +Section Cons. Variables (d l0 : nat) (la : seq nat). Hypotheses (Hla : is_part_of_n d la) (Hlla : is_part_of_n (l0 + d)%N (l0 :: la)). Notation Plla := (IntPartN Hlla). Notation Pla := (IntPartN Hla). -Lemma homsymprod_hh : 'hh[Plla] = 'hh[rowpartn l0] *h 'hh[Pla] :> HSF. +Lemma homsymprod_h1h : 'hh[Plla] = 'hh[rowpartn l0] *h 'hh[Pla] :> HSF. Proof. by apply val_inj; rewrite /= prod_genM intpartn_cons. Qed. -Lemma homsymprod_he : 'he[Plla] = 'he[rowpartn l0] *h 'he[Pla] :> HSF. +Lemma homsymprod_h1e : 'he[Plla] = 'he[rowpartn l0] *h 'he[Pla] :> HSF. Proof. by apply val_inj; rewrite /= prod_genM intpartn_cons. Qed. -Lemma homsymprod_hp : 'hp[Plla] = 'hp[rowpartn l0] *h 'hp[Pla] :> HSF. +Lemma homsymprod_h1p : 'hp[Plla] = 'hp[rowpartn l0] *h 'hp[Pla] :> HSF. Proof. by apply val_inj; rewrite /= prod_genM intpartn_cons. Qed. +End Cons. End HomSymProdGen. @@ -463,7 +486,7 @@ Variable R : fieldType. #[local] Notation HSF := {homsym R[n, d]}. -#[local] Notation Basis := (#|{:'P_d}|.-tuple HSF). +#[local] Notation Basis := (#|{: 'P_d}|.-tuple HSF). Definition symbe : Basis := [tuple of [seq 'he[la] | la : 'P_d]]. Definition symbh : Basis := [tuple of [seq 'hh[la] | la : 'P_d]]. Definition symbm : Basis := [tuple of [seq 'hm[la] | la : 'P_d]]. @@ -472,7 +495,7 @@ Definition symbp : Basis := [tuple of [seq 'hp[la] | la : 'P_d]]. Hypothesis Hd : (d <= n)%N. -Lemma basis_homsym : [set p : 'P_d | (size p <= n)%N] =i {:'P_d}. +Lemma basis_homsym : [set p : 'P_d | (size p <= n)%N] =i {: 'P_d}. Proof using Hd. move=> la. rewrite !inE; apply: (leq_trans _ Hd). @@ -480,7 +503,7 @@ by rewrite -[X in (_ <= X)%N](sumn_intpartn la); apply: size_part. Qed. Lemma dim_homsym : - \dim (fullv (vT := HSF)) = #|{:'P_d}|. + \dim (fullv (vT := HSF)) = #|{: 'P_d}|. Proof using Hd. by rewrite dimvf /=; apply eq_card; apply basis_homsym. Qed. Lemma symbm_free : free symbm. @@ -651,11 +674,11 @@ Proof. by move=> Hchar; apply/basis_free/symbp_basis. Qed. End HomSymField. -Notation "''he'" := (symbe _ _ _) (at level 8, format "''he'"). -Notation "''hh'" := (symbh _ _ _) (at level 8, format "''hh'"). -Notation "''hp'" := (symbp _ _ _) (at level 8, format "''hp'"). -Notation "''hm'" := (symbm _ _ _) (at level 8, format "''hm'"). -Notation "''hs'" := (symbs _ _ _) (at level 8, format "''hs'"). +Notation "''he'" := (symbe _ _ _). +Notation "''hh'" := (symbh _ _ _). +Notation "''hp'" := (symbp _ _ _). +Notation "''hm'" := (symbm _ _ _). +Notation "''hs'" := (symbs _ _ _). (** ** Changing the base field *) @@ -694,7 +717,7 @@ HB.instance Definition _ := _ _ map_homsym_is_scalable. -Lemma coord_map_homsym (b : #|{:'P_d}|.-tuple HSFR) j (f : HSFR) : +Lemma coord_map_homsym (b : #|{: 'P_d}|.-tuple HSFR) j (f : HSFR) : basis_of fullv b -> basis_of fullv (map_tuple map_homsym b) -> coord (map_tuple map_homsym b) j (map_homsym f) = mor (coord b j f). @@ -703,7 +726,7 @@ move=> Hbasis Hmap_basis. have toSf : f \in span b by rewrite (span_basis Hbasis) // memvf. rewrite {1}(coord_span toSf) raddf_sum /=. rewrite (eq_bigr - (fun i : 'I_#|{:'P_d}| => + (fun i : 'I_#|{: 'P_d}| => (mor (coord b i f)) *: (map_tuple map_homsym b)`_i )). by rewrite coord_sum_free //; apply: (basis_free Hmap_basis). move=> i _; rewrite linearZ /=. @@ -832,10 +855,13 @@ Context {n0 d : nat}. #[local] Notation n := (n0.+1). #[local] Notation HSF := {homsym algC[n, d]}. -Definition homsymdot (p q : HSF) : algC := - \sum_(i < #|{:'P_d}|) +Implicit Type (p q u v : HSF). + +Definition homsymdot p q : algC := + \sum_(i < #|{: 'P_d}|) (zcard (enum_val i))%:R * (coord 'hp i p) * (coord 'hp i q)^*. Notation "''[' u | v ]" := (homsymdot u v) : ring_scope. + Lemma homsymdotE p q : '[ p | q ] = \sum_(la : 'P_d) (zcard la)%:R * @@ -867,6 +893,12 @@ HB.instance Definition _ := homsymdot homsymdot_is_bilinear. Notation "''[' u | v ]" := (homsymdot u v) : ring_scope. +Fact homsymdot_is_hermitian p q : '[p | q] = (-1) ^+ false * '[q | p]^*. +Proof. by rewrite expr0 mul1r -homsymdotC. Qed. +HB.instance Definition _ := + isHermitianSesquilinear.Build + algC HSF false Num.conj_op homsymdot homsymdot_is_hermitian. + Lemma homsymdot0l p : '[0 | p] = 0. Proof. exact: linear0l. Qed. Lemma homsymdotNl p q : '[- q | p] = - '[q | p]. @@ -883,7 +915,6 @@ Proof. exact: linear_sumlz. Qed. Lemma homsymdotZl p a q : '[a *: q | p] = a * '[q | p]. Proof. exact: linearZl. Qed. - Lemma homsymdot0r p : '[p | 0] = 0. Proof. exact: linear0r. Qed. Lemma homsymdotNr p q : '[p | - q] = - '[p | q]. @@ -900,8 +931,36 @@ Proof. exact: linear_sumr. Qed. Lemma homsymdotZr a p q : '[p | a *: q] = a^* * '[p | q]. Proof. exact: linearZr. Qed. -Lemma homsymdotpp (Hd : (d <= n)%N) la mu : - '[ 'hp[la] | 'hp[mu] ] = (zcard la)%:R * (la == mu)%:R. + +Hypothesis (Hd : (d <= n)%N). + +Fact homsymdot_is_dot f : f != 0 -> 0 < '[f | f]. +Proof. +rewrite lt0r andbC. +pose co (la : 'P_d) := + (zcard la)%:R * coord 'hp (enum_rank la) f * (coord 'hp (enum_rank la) f)^*. +have le0zcc (la : 'P_d) : 0 <= co la. + by rewrite /co -mulrA mulr_ge0 // mul_conjC_ge0. +have -> /= : 0 <= '[f | f]. + by rewrite homsymdotE; apply: sumr_ge0 => /= la _; apply: le0zcc. +have /andP[/eqP Hfull Hfree]:= symbp_basis Hd char0_algC. +have:= memvf f; rewrite -Hfull => /coord_span {1}->. +apply contra; rewrite homsymdotE => /eqP H. +have {H le0zcc} eq0zcc (la : 'P_d) : co la = 0. + by apply/(psumr_eq0P _ H) => //= mu _; apply le0zcc. +suff allc0 i : coord 'hp i f = 0. + by apply/eqP/big1 => /= i _; rewrite allc0 scale0r. +have {eq0zcc} /eqP := eq0zcc (enum_val i). +rewrite {}/co enum_valK -mulrA mulf_eq0 pnatr_eq0 (negbTE (neq0zcard _)) /=. +by rewrite mul_conjC_eq0 => /eqP. +Qed. +HB.instance Definition _ := + isDotProduct.Build algC HSF homsymdot homsymdot_is_dot. + + +(** Formulas for other bases will be proved in Cauchy *) +Lemma homsymdotpp la mu : + '['hp[la] | 'hp[mu]] = (zcard la)%:R * (la == mu)%:R. Proof. rewrite homsymdotE (bigD1 mu) //= big1 ?addr0 => [| nu /negbTE Hneq]. - rewrite !(coord_symbp Hd) // eq_refl /= conjC1 mulr1. @@ -910,12 +969,12 @@ rewrite homsymdotE (bigD1 mu) //= big1 ?addr0 => [| nu /negbTE Hneq]. Qed. Lemma homsymdot_omegasf f g : - (d <= n)%N -> '[ omegahomsym f | omegahomsym g ] = '[ f | g ]. + '[omegahomsym f |omegahomsym g ] = '[f | g]. Proof. -move=> Hd; have /andP[/eqP Hfull Hfree]:= symbp_basis Hd char0_algC. -have:= (memvf g); rewrite -Hfull => /coord_span ->. +have /andP[/eqP Hfull Hfree]:= symbp_basis Hd char0_algC. +have:= memvf g; rewrite -Hfull => /coord_span ->. rewrite raddf_sum /= !homsymdot_sumr; apply eq_bigr => i _. -have:= (memvf f); rewrite -Hfull => /coord_span ->. +have:= memvf f; rewrite -Hfull => /coord_span ->. rewrite raddf_sum /= !homsymdot_suml; apply eq_bigr => j _. rewrite !linearZ /= !homsymdotZl !homsymdotZr; congr (_ * (_ * _)). rewrite ![_`_i](nth_map (rowpartn d)) -?cardE //. @@ -930,6 +989,17 @@ have /Num.Theory.conj_intr -> : by rewrite -exprD addnn -muln2 exprM sqrr_sign mul1r. Qed. +Lemma homsymp_orthogonal : pairwise_orthogonal homsymdot 'hp. +Proof. +apply/pairwise_orthogonalP => /=; split. + have pfree := basis_free (symbp_basis Hd char0_algC). + rewrite free_uniq // andbT. + by move: pfree; rewrite free_directv /= => /andP[]. +move=> f g /mapP[/= la _ {f}->]/mapP[/= mu _ {g}->]. +rewrite homsymdotpp. +by case: (altP (la =P mu)) => [->|_]; rewrite /= ?mulr0 // eqxx. +Qed. + End ScalarProduct. Notation "''[' u | v ]" := (homsymdot u v) : ring_scope. diff --git a/theories/SymGroup/Frobenius_char.v b/theories/SymGroup/Frobenius_char.v index c147420..ec6256e 100644 --- a/theories/SymGroup/Frobenius_char.v +++ b/theories/SymGroup/Frobenius_char.v @@ -149,7 +149,7 @@ rewrite FcharE; congr (_ *: _). rewrite (reindex _ (onW_bij _ (@enum_val_bij _))) /=. transitivity (coord 'hp (enum_rank la) - (\sum_(j < #|{:'P_n}|) + (\sum_(j < #|{: 'P_n}|) (f (permCT (enum_val j)) / 'z_(enum_val j)) *: ('hp`_j : HS))). congr coord; apply eq_bigr => /= i _; congr (_ *: _). rewrite (nth_map inh); last by rewrite -cardE ltn_ord. @@ -285,7 +285,7 @@ have Hla : (sumn la == sumn la) && is_part la. by rewrite eq_refl /=; have:= Hlla => /andP[_ /is_part_consK ->]. have Hdla : (sumn la <= nvar)%N by apply: (leq_trans _ Hd); rewrite /= leq_addl. have {IHla} Hrec := IHla Hla Hdla. -rewrite homsymprod_hh -Fchar_triv -(Fchar_invK Hdla 'hh[(IntPartN Hla)]). +rewrite homsymprod_h1h -Fchar_triv -(Fchar_invK Hdla 'hh[(IntPartN Hla)]). rewrite -Fchar_ind_morph (FcharK Hd). apply cfInd_char; rewrite cfIsom_char. exact: (cfextprod_char (cfun1_char _) Hrec). From 65e8e3c14e263b6e3dbfe92b84bc507fbaf76c8b Mon Sep 17 00:00:00 2001 From: Florent Hivert Date: Sun, 5 Jan 2025 12:34:36 +0100 Subject: [PATCH 5/8] Cosmetic --- theories/Combi/Yamanouchi.v | 4 ++-- theories/Combi/composition.v | 4 ++-- theories/Combi/partition.v | 4 ++-- theories/Combi/std.v | 2 +- theories/Combi/stdtab.v | 6 +++--- theories/Combi/tableau.v | 2 +- theories/HookFormula/Frobenius_ident.v | 2 +- theories/HookFormula/hook.v | 20 ++++++++++---------- theories/SymGroup/presentSn.v | 6 +++--- theories/SymGroup/reprSn.v | 2 +- 10 files changed, 26 insertions(+), 26 deletions(-) diff --git a/theories/Combi/Yamanouchi.v b/theories/Combi/Yamanouchi.v index 79e24d7..daa640c 100644 --- a/theories/Combi/Yamanouchi.v +++ b/theories/Combi/Yamanouchi.v @@ -412,7 +412,7 @@ Proof using. by case: y => /= y /andP[_ /eqP]. Qed. Lemma size_yameval (y : yameval) : size y = sumn ev. Proof using. by rewrite -evalseq_eq_size eval_yameval. Qed. -Lemma enum_yamevalE : map val (enum {:yameval}) = enum_yameval ev. +Lemma enum_yamevalE : map val (enum {: yameval}) = enum_yameval ev. Proof using. by rewrite /=; exact: enum_subE. Qed. Definition hyper_yameval := YamEval (hyper_yam_of_eval (intpartP ev)). @@ -457,7 +457,7 @@ Proof using. by case: y => /= y /andP[_ /eqP]. Qed. (** Check of disjoint union enumeration *) Lemma enum_yamnE : - map val (enum {:yamn}) = flatten [seq enum_yameval p | p <- enum_partn n]. + map val (enum {: yamn}) = flatten [seq enum_yameval p | p <- enum_partn n]. Proof using. rewrite enum_unionE /=; congr flatten. rewrite [LHS](eq_map (g := enum_yameval \o val)). diff --git a/theories/Combi/composition.v b/theories/Combi/composition.v index ea30627..ffb7b95 100644 --- a/theories/Combi/composition.v +++ b/theories/Combi/composition.v @@ -275,10 +275,10 @@ Coercion intcomp_of_intcompn : intcompn >-> intcomp. Lemma intcompn_sumn c : sumn c = n. Proof using. by case: c => /= c /andP[/eqP]. Qed. -Lemma enum_intcompnE : map val (enum {:intcompn}) = enum_compn n. +Lemma enum_intcompnE : map val (enum {: intcompn}) = enum_compn n. Proof using. exact: enum_subE. Qed. -Lemma card_intcompn : #|{:intcompn}| = 2 ^ n.-1. +Lemma card_intcompn : #|{: intcompn}| = 2 ^ n.-1. Proof. rewrite /= !cardT -!(size_map val) !enumT. rewrite unlock !subType_seqP ?enum_compn_allP //=. diff --git a/theories/Combi/partition.v b/theories/Combi/partition.v index 7ec1abd..a05e655 100644 --- a/theories/Combi/partition.v +++ b/theories/Combi/partition.v @@ -1340,7 +1340,7 @@ move=> /intpartn_leq_head /leq_trans; apply. by rewrite -(sumn_intpartn p); apply: leq_head_sumn. Qed. -Lemma enum_intpartnE : map val (enum {:'P}) = enum_partn n. +Lemma enum_intpartnE : map val (enum {: 'P}) = enum_partn n. Proof using. by rewrite /=; exact: enum_subE. Qed. Fact conj_intpartnP p : is_part_of_n n (conj_part p). @@ -1756,7 +1756,7 @@ rewrite -{1}[n.+1]addn1 iotaD add0n !map_cat sumn_cat IHn /= addn0. by rewrite size_enum_partns. Qed. -Lemma card_intpartn sm : #|{:'P_sm}| = intpartn_nb sm. +Lemma card_intpartn sm : #|{: 'P_sm}| = intpartn_nb sm. Proof. by rewrite [#|_|]cardT -(size_map val) /= enum_intpartnE -size_enum_partn. Qed. diff --git a/theories/Combi/std.v b/theories/Combi/std.v index 6309427..1832ee7 100644 --- a/theories/Combi/std.v +++ b/theories/Combi/std.v @@ -229,7 +229,7 @@ HB.instance Definition _ := Finite.copy stdwordn (uniq_finType stdwordn enum_stdwordnE enum_stdwordn_uniq). -Lemma card_stdwordn : #|{:stdwordn}| = n`!. +Lemma card_stdwordn : #|{: stdwordn}| = n`!. Proof using. by rewrite card_subE size_map -card_Sn cardE. Qed. End StdCombClass. diff --git a/theories/Combi/stdtab.v b/theories/Combi/stdtab.v index a441b45..0ca4bb9 100644 --- a/theories/Combi/stdtab.v +++ b/theories/Combi/stdtab.v @@ -660,7 +660,7 @@ Proof using. by case: t => /= t /andP[]. Qed. Lemma shape_stdtabsh (t : stdtabsh) : shape t = sh. Proof using. by case: t => /= t /andP[_ /eqP]. Qed. -Lemma enum_stdtabshE : map val (enum {:stdtabsh}) = enum_stdtabsh sh. +Lemma enum_stdtabshE : map val (enum {: stdtabsh}) = enum_stdtabsh sh. Proof. rewrite enumT unlock /= /stdtabsh_enum /enum_stdtabsh. elim: (enum_yameval sh) (enum_yamevalP (intpartP sh)) => //= y ly IHly. @@ -691,7 +691,7 @@ HB.instance Definition _ := [isSub of stdtabn for stdtabnval]. HB.instance Definition _ := [Countable of stdtabn by <:]. Definition enum_stdtabn : seq (seq (seq nat)) := - map (stdtab_of_yam \o val) (enum ({:yamn n})). + map (stdtab_of_yam \o val) (enum ({: yamn n})). Let stdtabn_enum : seq stdtabn := pmap insub enum_stdtabn. Fact finite_stdtabn : Finite.axiom stdtabn_enum. @@ -947,7 +947,7 @@ by exists (stdtabshcast (conj_intpartK sh) \o conj_stdtabsh) => t; Qed. Lemma card_stdtabsh_conj_part (sh : intpart) : - #|{:stdtabsh (conj_part sh)}| = #|{:stdtabsh sh}|. + #|{: stdtabsh (conj_part sh)}| = #|{: stdtabsh sh}|. Proof. by symmetry; apply: (bij_eq_card (conj_stdtabsh_bij sh)). Qed. #[export] Hint Resolve stdtabnP stdtabshP : core. diff --git a/theories/Combi/tableau.v b/theories/Combi/tableau.v index 5d64b1c..7716d6e 100644 --- a/theories/Combi/tableau.v +++ b/theories/Combi/tableau.v @@ -574,7 +574,7 @@ Proof using. by rewrite /= -(shape_tabsh t); apply: to_wordK. Qed. Let tabsh_enum : seq tabsh := pmap insub - [seq rev (reshape (rev sh) (val w)) | w in {:d.-tuple T}]. + [seq rev (reshape (rev sh) (val w)) | w in {: d.-tuple T}]. Lemma finite_tabsh : Finite.axiom tabsh_enum. Proof using. diff --git a/theories/HookFormula/Frobenius_ident.v b/theories/HookFormula/Frobenius_ident.v index 0b1069e..80ccc9e 100644 --- a/theories/HookFormula/Frobenius_ident.v +++ b/theories/HookFormula/Frobenius_ident.v @@ -46,7 +46,7 @@ Variable n : nat. #[local] Notation stpn := (stdtabn n * stdtabn n)%type. Lemma card_stpn_shape : #|[set p : stpn | shape p.1 == shape p.2]| = - \sum_(sh : 'P_n) #|{:stdtabsh sh}|^2. + \sum_(sh : 'P_n) #|{: stdtabsh sh}|^2. Proof. pose pairsh (sh : intpartn n) := [set p : stpn | (shape_deg p.1 == sh) && (shape_deg p.2 == sh)]. diff --git a/theories/HookFormula/hook.v b/theories/HookFormula/hook.v index a45da18..94fa59d 100644 --- a/theories/HookFormula/hook.v +++ b/theories/HookFormula/hook.v @@ -72,7 +72,7 @@ Finally the main Theorem is stated as: [[ Theorem HookLengthFormula (p : intpart) : - #|{:stdtabsh p}| = (sumn p)`! %/ (hook_length_prod p). + #|{: stdtabsh p}| = (sumn p)`! %/ (hook_length_prod p). ]] **********) @@ -99,8 +99,8 @@ Import Num.Theory. (** * Recursion for the number of Yamanouchi words and standard tableaux *) Lemma card_yama_rec (p : intpart) : p != empty_intpart -> - #|{:yameval p}| = - \sum_(i <- rem_corners p) #|{:yameval (decr_nth_intpart p i)}|. + #|{: yameval p}| = + \sum_(i <- rem_corners p) #|{: yameval (decr_nth_intpart p i)}|. Proof. move=> H. rewrite cardE -(size_map val) enum_yamevalE /enum_yameval. @@ -116,11 +116,11 @@ rewrite /enum_yameval /= /= Hcorn. by rewrite (sumn_decr_nth (intpartP p) Hcorn) Hn' /=. Qed. -Lemma card_yama0 : #|{:yameval empty_intpart}| = 1. +Lemma card_yama0 : #|{: yameval empty_intpart}| = 1. Proof. by rewrite cardE -(size_map val) enum_yamevalE. Qed. Lemma card_yam_stdtabE (p : intpart) : - #|{:yameval p}| = #|{:stdtabsh p}|. + #|{: yameval p}| = #|{: stdtabsh p}|. Proof. by rewrite !cardE -!(size_map val) enum_yamevalE enum_stdtabshE size_map. Qed. @@ -132,7 +132,7 @@ Lemma card_stdtabsh_rat_rec (F : intpart -> rat) : ( forall p : intpart, p != empty_intpart -> F p = \sum_(i <- rem_corners p) F (decr_nth_intpart p i) ) -> - forall p : intpart, F p = #|{:stdtabsh p}|%:Q. + forall p : intpart, F p = #|{: stdtabsh p}|%:Q. Proof. move=> H0 Hrec. elim/intpart_rem_corner_ind => [| p IHp] /=. @@ -1370,7 +1370,7 @@ Qed. End FindCorner. Theorem HookLengthFormula_rat (p : intpart) : - ( (#|{:stdtabsh p}|)%:Q = HLF p )%R. + ( (#|{: stdtabsh p}|)%:Q = HLF p )%R. Proof. apply esym; move: p; apply card_stdtabsh_rat_rec. - by rewrite /= /hook_length_prod /= big_box_skew /= big_nil factE. @@ -1386,7 +1386,7 @@ by apply/prodf_neq0 => [] [] [r c]. Qed. Lemma hook_length_prod_nat (p : intpart) : - #|{:stdtabsh p}| * (hook_length_prod p) = (sumn p)`!. + #|{: stdtabsh p}| * (hook_length_prod p) = (sumn p)`!. Proof. apply /eqP; rewrite -eqz_nat PoszM. rewrite -(@eqr_int rat) intrM /=. @@ -1398,11 +1398,11 @@ Qed. Lemma hook_length_prod_div (p : intpart) : (hook_length_prod p) %| (sumn p)`!. Proof. -by apply/dvdnP; exists #|{:stdtabsh p}|; rewrite hook_length_prod_nat. +by apply/dvdnP; exists #|{: stdtabsh p}|; rewrite hook_length_prod_nat. Qed. Theorem HookLengthFormula (p : intpart) : - #|{:stdtabsh p}| = (sumn p)`! %/ (hook_length_prod p). + #|{: stdtabsh p}| = (sumn p)`! %/ (hook_length_prod p). Proof. by rewrite -hook_length_prod_nat mulnK // lt0n; exact: hook_length_prod_non0. Qed. diff --git a/theories/SymGroup/presentSn.v b/theories/SymGroup/presentSn.v index 1cd941b..fd7f4cc 100644 --- a/theories/SymGroup/presentSn.v +++ b/theories/SymGroup/presentSn.v @@ -313,13 +313,13 @@ Proof using. by case: c => c /= /andP[]. Qed. Lemma size_codesz c : size c = n. Proof using. by case: c => c /= /andP[_ /eqP]. Qed. -Lemma enum_codeszE : map val (enum {:codesz}) = enum_codesz n. +Lemma enum_codeszE : map val (enum {: codesz}) = enum_codesz n. Proof using. by rewrite /=; exact: enum_subE. Qed. End FinType. -Lemma card_codesz n : #|{:codesz n}| = n`!. +Lemma card_codesz n : #|{: codesz n}| = n`!. Proof. rewrite /= cardE -(size_map val) enum_codeszE. elim: n => [//=| n IHn]. @@ -1355,7 +1355,7 @@ Lemma prods_codesz_bij : bijective prods_codesz. Proof using. apply inj_card_bij => [/= c1 c2 Heq|]; last by rewrite card_codesz card_Sn. suff {c1 c2 Heq} /image_injP Hinj : - #|image prods_codesz {:codesz n}| == #|{:codesz n}| by exact: (Hinj c1 c2). + #|image prods_codesz {: codesz n}| == #|{: codesz n}| by exact: (Hinj c1 c2). rewrite card_codesz (eq_card (B := 'S_n)) ?card_Sn // => /= s. rewrite !inE; apply/mapP. have Hcode : is_code_of_size n (cocode s). diff --git a/theories/SymGroup/reprSn.v b/theories/SymGroup/reprSn.v index c8b53a5..194c4a9 100644 --- a/theories/SymGroup/reprSn.v +++ b/theories/SymGroup/reprSn.v @@ -84,7 +84,7 @@ Qed. End LinRepr. -Lemma NirrSn n : Nirr 'SG_n = #|{:'P_n}|. +Lemma NirrSn n : Nirr 'SG_n = #|{: 'P_n}|. Proof using. by rewrite NirrE card_classes_perm card_ord. Qed. Section EltrConj. From 049cc63d0159ea03eec0faf1727ee724d0953a76 Mon Sep 17 00:00:00 2001 From: Florent Hivert Date: Sun, 5 Jan 2025 21:12:19 +0100 Subject: [PATCH 6/8] Hermitian product on class function + isometry --- theories/MPoly/Cauchy.v | 7 +----- theories/SymGroup/Frobenius_char.v | 40 +++++++++++++++++++++++++++--- 2 files changed, 37 insertions(+), 10 deletions(-) diff --git a/theories/MPoly/Cauchy.v b/theories/MPoly/Cauchy.v index c4f0cb1..f8cb9b6 100644 --- a/theories/MPoly/Cauchy.v +++ b/theories/MPoly/Cauchy.v @@ -697,13 +697,8 @@ Theorem homsyms_orthonormal : orthonormal homsymdot ('hs : seq HSC). Proof. have hs_uniq := free_uniq (basis_free (symbs_basis algC Hd)). apply/orthonormalP; split => /=; first exact: hs_uniq. -have {hs_uniq} hs_inj : injective (fun la : 'P_d => 'hs[la] : HSC). - move=> /= la mu. - have /tnthP[i /[dup] eqla ->] : la \in enum {: 'P_d} by rewrite mem_enum. - have /tnthP[j /[dup] eqmu ->] : mu \in enum {: 'P_d} by rewrite mem_enum. - by rewrite -!['hs[_]]tnth_map => /(tuple_uniqP _ hs_uniq) ->. move=> f g /mapP[/= la _ {f}->]/mapP[/= mu _ {g}->]. -by rewrite homsymdotss (inj_eq hs_inj). +by rewrite homsymdotss (inj_eq (injectiveP _ hs_uniq)). Qed. End Scalar. diff --git a/theories/SymGroup/Frobenius_char.v b/theories/SymGroup/Frobenius_char.v index ec6256e..4ce7d38 100644 --- a/theories/SymGroup/Frobenius_char.v +++ b/theories/SymGroup/Frobenius_char.v @@ -52,8 +52,8 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect. From mathcomp Require Import fingroup perm morphism gproduct. From mathcomp Require Import rat ssralg ssrint ssrnum algC vector archimedean. -From mathcomp Require Import sesquilinear. From mathcomp Require Import mxrepresentation classfun character. +From mathcomp Require Import sesquilinear. From mathcomp Require Import mpoly. Require Import sorted ordtype tools partition antisym sympoly homogsym Cauchy @@ -84,6 +84,38 @@ Proof. exact: char_num. Qed. #[local] Hint Resolve char0_algC char0_rat : core. +(** TODO: contribute to mathcomp *) +Section CharDotProduct. + +Variable (gT : finGroupType) (G : {group gT}). + +#[local] Notation cfdot := (cfdot (B := G)). + +Fact cfdot_is_bilinear : + bilinear_for *%R (Num.conj_op \; *%R) cfdot. +Proof. +split => /= p r /= u v; first by rewrite cfdotDl cfdotZl. +by rewrite cfdotDr cfdotZr. +Qed. +HB.instance Definition _ := + bilinear_isBilinear.Build algC 'CF(G) 'CF(G) algC *%R (Num.conj_op \; *%R) + cfdot cfdot_is_bilinear. + +Fact cfdot_is_hermitian (phi psi : 'CF(G)) : + '[phi, psi] = (-1) ^+ false * '[psi, phi]^*. +Proof. by rewrite expr0 mul1r -cfdotC. Qed. +HB.instance Definition _ := + isHermitianSesquilinear.Build + algC 'CF(G) false Num.conj_op cfdot cfdot_is_hermitian. + +Fact cfdot_is_dot (phi : 'CF(G)) : phi != 0 -> 0 < '[phi]. +Proof. by rewrite cfnorm_gt0. Qed. +HB.instance Definition _ := + isDotProduct.Build algC 'CF(G) cfdot cfdot_is_dot. + +End CharDotProduct. + + (** * Definition and basic properties *) Section NVar. @@ -220,11 +252,11 @@ Qed. (** ** The Frobenius Characteristic is an isometry *) -Theorem Fchar_isometry f g : '[Fchar f | Fchar g] = '[f, g]. +Corollary Fchar_isometry : isometry homsymdot cfdot Fchar. Proof using Hn. -rewrite (ncfuniCT_gen f) (ncfuniCT_gen g) !linear_sum /=. +move=> f g. +rewrite (ncfuniCT_gen f) (ncfuniCT_gen g) !linear_sum /=; apply eq_bigr => mu _. rewrite homsymdot_suml cfdot_suml; apply eq_bigr => la _. -rewrite homsymdot_sumr cfdot_sumr; apply eq_bigr => mu _. rewrite ![Fchar (_ *: '1z_[_])]linearZ /= !Fchar_ncfuniCT. rewrite homsymdotZl homsymdotZr cfdotZl cfdotZr; congr (_ * (_ * _)). rewrite homsymdotpp // cfdotZl cfdotZr cfdot_classfun_part. From 8c9c820b18acd46ad50ac146c4b922afe5108060 Mon Sep 17 00:00:00 2001 From: Florent Hivert Date: Wed, 8 Jan 2025 14:58:12 +0100 Subject: [PATCH 7/8] Updated README.txt --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index c44d91a..50c3c35 100644 --- a/README.md +++ b/README.md @@ -165,7 +165,7 @@ This library is based on * [SSReflect/MathComp 2](https://github.com/math-comp/math-comp) Library version 2.3.0 or more recent. -* For MathComp 2.2.0, use the [MathComp-2.2.0 branch](https://github.com/math-comp/Coq-Combi/tree/MathComp-2.2.0) +* For MathComp 2.2.0, use the [MathComp-2.2.0](https://github.com/math-comp/Coq-Combi/tree/MathComp-2.2.0) branch. Here are the Opam packages I'm using ``` From 097d9f4e440dbbdcd27a36ea005f45d3e7dd7282 Mon Sep 17 00:00:00 2001 From: Florent Hivert Date: Wed, 8 Jan 2025 19:46:27 +0100 Subject: [PATCH 8/8] New coq-nix-toolbox.ni --- .../workflows/nix-action-coq8.18-mc2.3.0.yml | 124 +++++++++-------- .../workflows/nix-action-coq8.19-mc2.3.0.yml | 124 +++++++++-------- .../workflows/nix-action-coq8.20-mc2.3.0.yml | 128 ++++++++++-------- .nix/coq-nix-toolbox.nix | 2 +- 4 files changed, 203 insertions(+), 175 deletions(-) diff --git a/.github/workflows/nix-action-coq8.18-mc2.3.0.yml b/.github/workflows/nix-action-coq8.18-mc2.3.0.yml index bd985fb..0f1616e 100644 --- a/.github/workflows/nix-action-coq8.18-mc2.3.0.yml +++ b/.github/workflows/nix-action-coq8.18-mc2.3.0.yml @@ -4,43 +4,43 @@ jobs: 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" + 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 + uses: actions/checkout@v4 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" + 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 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v20 + uses: cachix/install-nix-action@v30 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup coq - uses: cachix/cachix-action@v12 + uses: cachix/cachix-action@v15 with: extraPullNames: coq-community, math-comp name: coq - 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.18-mc2.3.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" + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"coq8.18-mc2.3.0\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n + echo $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.18-mc2.3.0" @@ -51,43 +51,43 @@ jobs: 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" + 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 + uses: actions/checkout@v4 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" + 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 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v20 + uses: cachix/install-nix-action@v30 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup coq - uses: cachix/cachix-action@v12 + uses: cachix/cachix-action@v15 with: extraPullNames: coq-community, math-comp name: coq - id: stepCheck name: Checking presence of CI target coq-combi - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.18-mc2.3.0\" --argstr job \"coq-combi\" \\\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" + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"coq8.18-mc2.3.0\" --argstr job \"coq-combi\" \\\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.18-mc2.3.0" @@ -104,6 +104,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-algebra' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18-mc2.3.0" --argstr job "mathcomp-algebra" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: multinomials' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18-mc2.3.0" + --argstr job "multinomials" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-character' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18-mc2.3.0" @@ -122,47 +126,51 @@ jobs: 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" + 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 + uses: actions/checkout@v4 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" + 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 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v20 + uses: cachix/install-nix-action@v30 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup coq - uses: cachix/cachix-action@v12 + uses: cachix/cachix-action@v15 with: extraPullNames: coq-community, math-comp name: coq - id: stepCheck name: Checking presence of CI target mathcomp - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.18-mc2.3.0\" --argstr job \"mathcomp\" \\\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" + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"coq8.18-mc2.3.0\" --argstr job \"mathcomp\" \\\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.18-mc2.3.0" --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: stdlib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18-mc2.3.0" + --argstr job "stdlib" - 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.18-mc2.3.0" @@ -196,7 +204,7 @@ jobs: run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18-mc2.3.0" --argstr job "mathcomp" name: Nix CI for bundle coq8.18-mc2.3.0 -'on': +on: pull_request: paths: - .github/workflows/nix-action-coq8.18-mc2.3.0.yml diff --git a/.github/workflows/nix-action-coq8.19-mc2.3.0.yml b/.github/workflows/nix-action-coq8.19-mc2.3.0.yml index cc17bba..df6f51d 100644 --- a/.github/workflows/nix-action-coq8.19-mc2.3.0.yml +++ b/.github/workflows/nix-action-coq8.19-mc2.3.0.yml @@ -4,43 +4,43 @@ jobs: 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" + 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 + uses: actions/checkout@v4 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" + 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 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v20 + uses: cachix/install-nix-action@v30 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup coq - uses: cachix/cachix-action@v12 + uses: cachix/cachix-action@v15 with: extraPullNames: coq-community, math-comp name: coq - 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.19-mc2.3.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" + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"coq8.19-mc2.3.0\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n + echo $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.19-mc2.3.0" @@ -51,43 +51,43 @@ jobs: 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" + 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 + uses: actions/checkout@v4 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" + 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 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v20 + uses: cachix/install-nix-action@v30 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup coq - uses: cachix/cachix-action@v12 + uses: cachix/cachix-action@v15 with: extraPullNames: coq-community, math-comp name: coq - id: stepCheck name: Checking presence of CI target coq-combi - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.19-mc2.3.0\" --argstr job \"coq-combi\" \\\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" + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"coq8.19-mc2.3.0\" --argstr job \"coq-combi\" \\\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.19-mc2.3.0" @@ -104,6 +104,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-algebra' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.19-mc2.3.0" --argstr job "mathcomp-algebra" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: multinomials' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.19-mc2.3.0" + --argstr job "multinomials" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-character' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.19-mc2.3.0" @@ -122,47 +126,51 @@ jobs: 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" + 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 + uses: actions/checkout@v4 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" + 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 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v20 + uses: cachix/install-nix-action@v30 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup coq - uses: cachix/cachix-action@v12 + uses: cachix/cachix-action@v15 with: extraPullNames: coq-community, math-comp name: coq - id: stepCheck name: Checking presence of CI target mathcomp - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.19-mc2.3.0\" --argstr job \"mathcomp\" \\\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" + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"coq8.19-mc2.3.0\" --argstr job \"mathcomp\" \\\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.19-mc2.3.0" --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: stdlib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.19-mc2.3.0" + --argstr job "stdlib" - 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.19-mc2.3.0" @@ -196,7 +204,7 @@ jobs: run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.19-mc2.3.0" --argstr job "mathcomp" name: Nix CI for bundle coq8.19-mc2.3.0 -'on': +on: pull_request: paths: - .github/workflows/nix-action-coq8.19-mc2.3.0.yml diff --git a/.github/workflows/nix-action-coq8.20-mc2.3.0.yml b/.github/workflows/nix-action-coq8.20-mc2.3.0.yml index d805f16..1369769 100644 --- a/.github/workflows/nix-action-coq8.20-mc2.3.0.yml +++ b/.github/workflows/nix-action-coq8.20-mc2.3.0.yml @@ -4,43 +4,43 @@ jobs: 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" + 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 + uses: actions/checkout@v4 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" + 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 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v20 + uses: cachix/install-nix-action@v30 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup coq - uses: cachix/cachix-action@v12 + uses: cachix/cachix-action@v15 with: extraPullNames: coq-community, math-comp name: coq - 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.20-mc2.3.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" + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"coq8.20-mc2.3.0\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n + echo $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.20-mc2.3.0" @@ -51,43 +51,43 @@ jobs: 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" + 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 + uses: actions/checkout@v4 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" + 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 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v20 + uses: cachix/install-nix-action@v30 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup coq - uses: cachix/cachix-action@v12 + uses: cachix/cachix-action@v15 with: extraPullNames: coq-community, math-comp name: coq - id: stepCheck name: Checking presence of CI target coq-combi - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.20-mc2.3.0\" --argstr job \"coq-combi\" \\\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" + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"coq8.20-mc2.3.0\" --argstr job \"coq-combi\" \\\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.20-mc2.3.0" @@ -104,6 +104,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-algebra' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.20-mc2.3.0" --argstr job "mathcomp-algebra" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: multinomials' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.20-mc2.3.0" + --argstr job "multinomials" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-character' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.20-mc2.3.0" @@ -122,47 +126,51 @@ jobs: 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" + 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 + uses: actions/checkout@v4 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" + 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 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v20 + uses: cachix/install-nix-action@v30 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup coq - uses: cachix/cachix-action@v12 + uses: cachix/cachix-action@v15 with: extraPullNames: coq-community, math-comp name: coq - id: stepCheck name: Checking presence of CI target mathcomp - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq8.20-mc2.3.0\" --argstr job \"mathcomp\" \\\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" + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"coq8.20-mc2.3.0\" --argstr job \"mathcomp\" \\\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.20-mc2.3.0" --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: stdlib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.20-mc2.3.0" + --argstr job "stdlib" - 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.20-mc2.3.0" @@ -187,12 +195,16 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-character' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.20-mc2.3.0" --argstr job "mathcomp-character" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.20-mc2.3.0" + --argstr job "hierarchy-builder" - 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.20-mc2.3.0" --argstr job "mathcomp" name: Nix CI for bundle coq8.20-mc2.3.0 -'on': +on: pull_request: paths: - .github/workflows/nix-action-coq8.20-mc2.3.0.yml diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index 2ca1468..dd5f8ff 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"dd771a5001cd955514f2462cad7cdd90377530e3" +"98bf866ef64cd2f9c4ba6a9eb73b16c5019fcde7"