From c67fdf492744fa11200f0e2a45b647c217d74f88 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 26 Jun 2026 10:33:07 +0200 Subject: [PATCH 1/2] Compile with MathComp master --- 3rdparty/ALEA/Qmeasure.v | 4 +++- theories/Basic/combclass.v | 1 + theories/Basic/congr.v | 1 + theories/Basic/ordtype.v | 1 + theories/Basic/unitriginv.v | 1 + theories/Combi/Dyckword.v | 1 + theories/Combi/Yamanouchi.v | 1 + theories/Combi/bintree.v | 1 + theories/Combi/composition.v | 1 + theories/Combi/partition.v | 1 + theories/Combi/permuted.v | 1 + theories/Combi/setpartition.v | 1 + theories/Combi/skewpart.v | 1 + theories/Combi/skewtab.v | 1 + theories/Combi/std.v | 1 + theories/Combi/stdtab.v | 1 + theories/Combi/subseq.v | 1 + theories/Combi/tableau.v | 1 + theories/Combi/vectNK.v | 1 + theories/Erdos_Szekeres/Erdos_Szekeres.v | 1 + theories/HookFormula/Frobenius_ident.v | 1 + theories/HookFormula/hook.v | 1 + theories/LRrule/Greene.v | 1 + theories/LRrule/Greene_inv.v | 1 + theories/LRrule/Schensted.v | 1 + theories/LRrule/Yam_plact.v | 1 + theories/LRrule/freeSchur.v | 1 + theories/LRrule/implem.v | 1 + theories/LRrule/plactic.v | 1 + theories/LRrule/shuffle.v | 1 + theories/LRrule/stdplact.v | 1 + theories/LRrule/therule.v | 1 + theories/MPoly/Cauchy.v | 6 +++--- theories/MPoly/MurnaghanNakayama.v | 3 ++- theories/MPoly/Schur_altdef.v | 1 + theories/MPoly/Schur_mpoly.v | 1 + theories/MPoly/antisym.v | 1 + theories/MPoly/homogsym.v | 3 ++- theories/MPoly/sympoly.v | 3 ++- theories/SSRcomplements/sorted.v | 1 + theories/SSRcomplements/tools.v | 1 + theories/SymGroup/Frobenius_char.v | 1 + theories/SymGroup/cycles.v | 1 + theories/SymGroup/cycletype.v | 1 + theories/SymGroup/permcent.v | 1 + theories/SymGroup/presentSn.v | 1 + theories/SymGroup/towerSn.v | 1 + theories/SymGroup/weak_order.v | 1 + 48 files changed, 55 insertions(+), 7 deletions(-) diff --git a/3rdparty/ALEA/Qmeasure.v b/3rdparty/ALEA/Qmeasure.v index 3732c3f..4d42011 100644 --- a/3rdparty/ALEA/Qmeasure.v +++ b/3rdparty/ALEA/Qmeasure.v @@ -31,6 +31,8 @@ Import GRing. Import Order.Theory. Import Num.Theory. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) + Delimit Scope order_scope with Omc. #[local] Open Scope O_scope. Delimit Scope O_scope with O. @@ -939,7 +941,7 @@ congr *%R. rewrite -big_filter (bigD1_seq a) /=. - rewrite (eq_refl a) mulr1. transitivity (coeff d a + 0)%R; last by rewrite addr0. - congr +%R; apply big1 => i. + congr +%R; apply: big1 => i. by case (i == a); rewrite //= ?mulr0 ?addr0. - by rewrite mem_filter Hain Hap. - by rewrite filter_uniq. diff --git a/theories/Basic/combclass.v b/theories/Basic/combclass.v index afe523c..10e55f9 100644 --- a/theories/Basic/combclass.v +++ b/theories/Basic/combclass.v @@ -25,6 +25,7 @@ From HB Require Import structures. From mathcomp Require Import all_boot. Require Import tools. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/Basic/congr.v b/theories/Basic/congr.v index d32541b..99188c4 100644 --- a/theories/Basic/congr.v +++ b/theories/Basic/congr.v @@ -72,6 +72,7 @@ From mathcomp Require Import all_boot. From Stdlib Require Import Recdef. Require Import permcomp permuted multinomial vectNK. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/Basic/ordtype.v b/theories/Basic/ordtype.v index 9f2c0c1..985ed97 100644 --- a/theories/Basic/ordtype.v +++ b/theories/Basic/ordtype.v @@ -44,6 +44,7 @@ From mathcomp Require Import all_boot. From mathcomp Require Import order. Require Import tools. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/Basic/unitriginv.v b/theories/Basic/unitriginv.v index 9c385fc..afb5386 100644 --- a/theories/Basic/unitriginv.v +++ b/theories/Basic/unitriginv.v @@ -36,6 +36,7 @@ From mathcomp Require Import finset fingroup perm matrix. Require ordtype. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/Combi/Dyckword.v b/theories/Combi/Dyckword.v index da0a081..f2baffe 100644 --- a/theories/Combi/Dyckword.v +++ b/theories/Combi/Dyckword.v @@ -71,6 +71,7 @@ From mathcomp Require Import all_boot order. From mathcomp Require Import div ssralg ssrint ssrnum binomial. Require Import tools combclass bintree. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/Combi/Yamanouchi.v b/theories/Combi/Yamanouchi.v index 817463d..4a23272 100644 --- a/theories/Combi/Yamanouchi.v +++ b/theories/Combi/Yamanouchi.v @@ -54,6 +54,7 @@ From HB Require Import structures. From mathcomp Require Import all_boot. Require Import tools combclass partition. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/Combi/bintree.v b/theories/Combi/bintree.v index ace6541..eee0b4d 100644 --- a/theories/Combi/bintree.v +++ b/theories/Combi/bintree.v @@ -84,6 +84,7 @@ From HB Require Import structures. From mathcomp Require Import all_boot order. Require Import tools combclass ordtype. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/Combi/composition.v b/theories/Combi/composition.v index 7a319af..20e5706 100644 --- a/theories/Combi/composition.v +++ b/theories/Combi/composition.v @@ -51,6 +51,7 @@ From HB Require Import structures. From mathcomp Require Import all_boot order. Require Import tools combclass sorted partition subseq ordtype. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/Combi/partition.v b/theories/Combi/partition.v index 20d7235..57883fd 100644 --- a/theories/Combi/partition.v +++ b/theories/Combi/partition.v @@ -118,6 +118,7 @@ From mathcomp Require Import all_boot order. From mathcomp Require Import div ssralg ssrint ssrnum binomial. Require Import tools combclass sorted ordtype. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/Combi/permuted.v b/theories/Combi/permuted.v index 28966f1..03d0b73 100644 --- a/theories/Combi/permuted.v +++ b/theories/Combi/permuted.v @@ -41,6 +41,7 @@ Require Import tools combclass sorted partition composition multinomial. Require Import permcomp cycles. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/Combi/setpartition.v b/theories/Combi/setpartition.v index 4d8e1ee..31ced5b 100644 --- a/theories/Combi/setpartition.v +++ b/theories/Combi/setpartition.v @@ -33,6 +33,7 @@ From mathcomp Require Import all_boot order. From mathcomp Require Import div ssralg ssrint ssrnum binomial. Require Import tools combclass sorted ordtype partition. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/Combi/skewpart.v b/theories/Combi/skewpart.v index 7bc8bf1..5adade7 100644 --- a/theories/Combi/skewpart.v +++ b/theories/Combi/skewpart.v @@ -61,6 +61,7 @@ From HB Require Import structures. From mathcomp Require Import all_boot. Require Import tools sorted partition. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/Combi/skewtab.v b/theories/Combi/skewtab.v index 2f4d685..9f1f7ba 100644 --- a/theories/Combi/skewtab.v +++ b/theories/Combi/skewtab.v @@ -30,6 +30,7 @@ From mathcomp Require Import all_boot order. Require Import tools partition skewpart Yamanouchi ordtype tableau std stdtab. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/Combi/std.v b/theories/Combi/std.v index e06fa9d..71414d1 100644 --- a/theories/Combi/std.v +++ b/theories/Combi/std.v @@ -54,6 +54,7 @@ From mathcomp Require Import perm fingroup. Require Import tools combclass ordtype permcomp. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/Combi/stdtab.v b/theories/Combi/stdtab.v index 8da03c9..db36ef6 100644 --- a/theories/Combi/stdtab.v +++ b/theories/Combi/stdtab.v @@ -86,6 +86,7 @@ From mathcomp Require Import perm fingroup. Require Import tools combclass partition Yamanouchi ordtype std tableau. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/Combi/subseq.v b/theories/Combi/subseq.v index acdd8b8..08c06ee 100644 --- a/theories/Combi/subseq.v +++ b/theories/Combi/subseq.v @@ -27,6 +27,7 @@ From HB Require Import structures. From mathcomp Require Import all_boot. Require Import tools combclass sorted. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/Combi/tableau.v b/theories/Combi/tableau.v index c8b7823..31737ff 100644 --- a/theories/Combi/tableau.v +++ b/theories/Combi/tableau.v @@ -47,6 +47,7 @@ From HB Require Import structures. From mathcomp Require Import all_boot order. Require Import tools partition ordtype sorted. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/Combi/vectNK.v b/theories/Combi/vectNK.v index 79d8c69..d9af221 100644 --- a/theories/Combi/vectNK.v +++ b/theories/Combi/vectNK.v @@ -27,6 +27,7 @@ From Corelib Require Import Setoid. From mathcomp Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq. Require Import tools. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/Erdos_Szekeres/Erdos_Szekeres.v b/theories/Erdos_Szekeres/Erdos_Szekeres.v index 0ab737b..749e539 100644 --- a/theories/Erdos_Szekeres/Erdos_Szekeres.v +++ b/theories/Erdos_Szekeres/Erdos_Szekeres.v @@ -30,6 +30,7 @@ From mathcomp Require Import tuple finfun finset bigop path order. Require Import partition tableau Schensted ordtype Greene Greene_inv. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/HookFormula/Frobenius_ident.v b/theories/HookFormula/Frobenius_ident.v index dc4dcce..d514fc3 100644 --- a/theories/HookFormula/Frobenius_ident.v +++ b/theories/HookFormula/Frobenius_ident.v @@ -32,6 +32,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype choice ssrnat seq ssrint div rat fintype finset bigop path ssralg ssrnum order. (* Import bigop before ssralg/ssrnum to get correct printing of \sum \prod*) +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/HookFormula/hook.v b/theories/HookFormula/hook.v index 67395dc..07981a5 100644 --- a/theories/HookFormula/hook.v +++ b/theories/HookFormula/hook.v @@ -87,6 +87,7 @@ Require Import tools subseq partition Yamanouchi stdtab Qmeasure. Set Warnings "hiding-delimiting-key". +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/LRrule/Greene.v b/theories/LRrule/Greene.v index 5eb6ba5..809ab1d 100644 --- a/theories/LRrule/Greene.v +++ b/theories/LRrule/Greene.v @@ -72,6 +72,7 @@ From mathcomp Require Import perm. Require Import sorted tools subseq partition tableau. Require Import Schensted congr plactic ordcast. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/LRrule/Greene_inv.v b/theories/LRrule/Greene_inv.v index f41d82a..123d912 100644 --- a/theories/LRrule/Greene_inv.v +++ b/theories/LRrule/Greene_inv.v @@ -132,6 +132,7 @@ From mathcomp Require Import perm. Require Import tools ordcast ordtype subseq partition tableau Yamanouchi stdtab. Require Import Schensted congr plactic Greene. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/LRrule/Schensted.v b/theories/LRrule/Schensted.v index bdcb807..bd7eb35 100644 --- a/theories/LRrule/Schensted.v +++ b/theories/LRrule/Schensted.v @@ -127,6 +127,7 @@ From mathcomp Require Import all_boot order. From mathcomp Require Import perm fingroup. Require Import tools partition Yamanouchi ordtype subseq tableau std stdtab. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/LRrule/Yam_plact.v b/theories/LRrule/Yam_plact.v index 3bd8221..c5993d2 100644 --- a/theories/LRrule/Yam_plact.v +++ b/theories/LRrule/Yam_plact.v @@ -43,6 +43,7 @@ From mathcomp Require Import tuple finfun finset path bigop order. Require Import tools partition Yamanouchi ordtype std tableau stdtab. Require Import Schensted congr plactic Greene_inv stdplact. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/LRrule/freeSchur.v b/theories/LRrule/freeSchur.v index 1afe2ac..1028bda 100644 --- a/theories/LRrule/freeSchur.v +++ b/theories/LRrule/freeSchur.v @@ -87,6 +87,7 @@ Require Import tools ordtype partition Yamanouchi std tableau stdtab. Require Import Schensted congr plactic stdplact Yam_plact Greene_inv shuffle. Require Import Schur_mpoly. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/LRrule/implem.v b/theories/LRrule/implem.v index e8d66ef..089c8e5 100644 --- a/theories/LRrule/implem.v +++ b/theories/LRrule/implem.v @@ -35,6 +35,7 @@ Require Import tools combclass partition Yamanouchi ordtype tableau. Require Import skewtab Schur_mpoly freeSchur therule. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/LRrule/plactic.v b/theories/LRrule/plactic.v index 7f3a45f..010ad5c 100644 --- a/theories/LRrule/plactic.v +++ b/theories/LRrule/plactic.v @@ -62,6 +62,7 @@ From mathcomp Require Import perm. Require Import tools partition ordtype tableau stdtab Schensted congr. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/LRrule/shuffle.v b/theories/LRrule/shuffle.v index a47f2ab..e8292f2 100644 --- a/theories/LRrule/shuffle.v +++ b/theories/LRrule/shuffle.v @@ -66,6 +66,7 @@ From mathcomp Require Import order seq tuple finfun finset perm binomial bigop. Require Import tools vectNK subseq partition Yamanouchi ordtype std tableau stdtab. Require Import Schensted plactic Greene_inv stdplact. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/LRrule/stdplact.v b/theories/LRrule/stdplact.v index 28cec6d..e9b31bb 100644 --- a/theories/LRrule/stdplact.v +++ b/theories/LRrule/stdplact.v @@ -36,6 +36,7 @@ From mathcomp Require Import perm fingroup. Require Import tools combclass ordcast partition Yamanouchi ordtype std tableau. Require Import stdtab sorted Schensted congr plactic Greene Greene_inv. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/LRrule/therule.v b/theories/LRrule/therule.v index 57173eb..3547a40 100644 --- a/theories/LRrule/therule.v +++ b/theories/LRrule/therule.v @@ -68,6 +68,7 @@ Require Import tools ordcast combclass partition skewpart Yamanouchi ordtype. Require Import std tableau stdtab Schensted congr plactic Greene_inv. Require Import stdplact Yam_plact skewtab shuffle Schur_mpoly freeSchur. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/MPoly/Cauchy.v b/theories/MPoly/Cauchy.v index 2bf2f80..b750361 100644 --- a/theories/MPoly/Cauchy.v +++ b/theories/MPoly/Cauchy.v @@ -59,6 +59,7 @@ Require Import antisym Schur_mpoly Schur_altdef sympoly homogsym permcent. Require ordtype. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -302,7 +303,7 @@ Qed. Lemma evalXY_homog d p : p \is d.-homog -> p(XY) \is d.-homog. Proof. move/pihomog_dE <-; rewrite pihomogE. -rewrite rmorph_sum /=; apply rpred_sum => mon /eqP Hdeg. +rewrite rmorph_sum /=; apply: rpred_sum => mon /eqP Hdeg. rewrite linearZ /= scale_polXYE; apply: rpredZ. rewrite evalXY_XE -rmorph_prod /= polyXY_scale /=; apply: rpredZ. by rewrite /polX_XY map_mpolyX dhomogX /= mdeg_monX Hdeg. @@ -475,7 +476,7 @@ Qed. (** Unused lemma *) Lemma Cauchy_kernel_symmetric : Cauchy_kernel d \is symmetric. Proof. -rewrite Cauchy_symm_symh; apply rpred_sum => la _. +rewrite Cauchy_symm_symh; apply: rpred_sum => la _. by apply: rpredZ; apply sympolP. Qed. @@ -702,4 +703,3 @@ by rewrite homsymdotss (inj_eq (injectiveP _ hs_uniq)). Qed. End Scalar. - diff --git a/theories/MPoly/MurnaghanNakayama.v b/theories/MPoly/MurnaghanNakayama.v index c490eea..fa5e903 100644 --- a/theories/MPoly/MurnaghanNakayama.v +++ b/theories/MPoly/MurnaghanNakayama.v @@ -48,11 +48,12 @@ We provide the following definitions: From HB Require Import structures. From mathcomp Require Import all_boot. From mathcomp Require Import ssralg ssrint perm fingroup tuple vector rat. -From mathcomp Require Import ssrcomplements freeg mpoly monalg. +From mathcomp Require Import ssrcomplements mpoly. Require Import sorted tools ordtype permuted partition skewpart. Require Import antisym Schur_mpoly Schur_altdef sympoly homogsym. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/MPoly/Schur_altdef.v b/theories/MPoly/Schur_altdef.v index 27c5fb6..ba57b34 100644 --- a/theories/MPoly/Schur_altdef.v +++ b/theories/MPoly/Schur_altdef.v @@ -90,6 +90,7 @@ Require Import tools combclass ordtype sorted partition tableau. Require Import skewpart skewtab antisym Schur_mpoly freeSchur therule. Require Import std stdtab unitriginv presentSn. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/MPoly/Schur_mpoly.v b/theories/MPoly/Schur_mpoly.v index 09e1c13..dbdcb47 100644 --- a/theories/MPoly/Schur_mpoly.v +++ b/theories/MPoly/Schur_mpoly.v @@ -29,6 +29,7 @@ From mathcomp Require Import ssrcomplements freeg mpoly. Require Import tools ordtype partition tableau. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/MPoly/antisym.v b/theories/MPoly/antisym.v index f930c8d..4d07089 100644 --- a/theories/MPoly/antisym.v +++ b/theories/MPoly/antisym.v @@ -52,6 +52,7 @@ From mathcomp Require Import ssrcomplements freeg mpoly. Require Import tools permcomp presentSn sorted partition. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/MPoly/homogsym.v b/theories/MPoly/homogsym.v index 5a7b064..ff9cc16 100644 --- a/theories/MPoly/homogsym.v +++ b/theories/MPoly/homogsym.v @@ -84,6 +84,7 @@ From mathcomp Require Import ssrcomplements freeg mpoly. Require Import tools sorted ordtype permuted partition permcent. Require Import antisym Schur_mpoly Schur_altdef sympoly. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -259,7 +260,7 @@ exists (fun r : 'rV[R]_(#|b|) => - move=> r /=; apply/matrixP=> i j. rewrite mxE !raddf_sum ord1 /= (bigD1 j) //=. rewrite !linearZ /= mcoeff_symm ?sztntht //. - rewrite perm_refl mulr1 big1 ?addr0 //. + rewrite perm_refl mulr1 big1 ?addr0 ?ord1 //. move=> k Hkj. rewrite !linearZ /= mcoeff_symm ?sztntht //. suff : ~~(perm_eq (mpart (n := n) (tnth t k)) (mpart (n := n) (tnth t j))). diff --git a/theories/MPoly/sympoly.v b/theories/MPoly/sympoly.v index c709ad4..47a07ea 100644 --- a/theories/MPoly/sympoly.v +++ b/theories/MPoly/sympoly.v @@ -93,6 +93,7 @@ Require Import sorted tools ordtype permuted partition skewpart composition. Require Import Yamanouchi std tableau stdtab skewtab permcent. Require Import antisym Schur_mpoly therule Schur_altdef unitriginv. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -271,7 +272,7 @@ Canonical symh d : {sympoly R[n]} := SymPoly (symh_sym d). Lemma mcoeff_symh d m : 'h_d@_m = (mdeg m == d)%:R. Proof. exact: mcoeff_symh_pol. Qed. Lemma symh_homog d : sympol 'h_d \is d.-homog. -Proof using. by apply rpred_sum => m /eqP H; rewrite dhomogX /= H. Qed. +Proof using. by apply: rpred_sum => m /eqP H; rewrite dhomogX /= H. Qed. (** ** Power sum symmetric polynomials *) diff --git a/theories/SSRcomplements/sorted.v b/theories/SSRcomplements/sorted.v index 7dd60d2..2ca4cf7 100644 --- a/theories/SSRcomplements/sorted.v +++ b/theories/SSRcomplements/sorted.v @@ -22,6 +22,7 @@ From Corelib Require Import Setoid. From mathcomp Require Import ssreflect ssrbool ssrfun ssrnat eqtype fintype choice seq. From mathcomp Require Import path order. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/SSRcomplements/tools.v b/theories/SSRcomplements/tools.v index e5dd690..6310716 100644 --- a/theories/SSRcomplements/tools.v +++ b/theories/SSRcomplements/tools.v @@ -23,6 +23,7 @@ From Corelib Require Import Setoid. From mathcomp Require Import ssreflect ssrbool ssrfun ssrnat eqtype fintype choice. From mathcomp Require Import seq finset bigop path binomial order. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/SymGroup/Frobenius_char.v b/theories/SymGroup/Frobenius_char.v index 92a097c..fe35b97 100644 --- a/theories/SymGroup/Frobenius_char.v +++ b/theories/SymGroup/Frobenius_char.v @@ -63,6 +63,7 @@ Require Import MurnaghanNakayama. Require ordtype. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/SymGroup/cycles.v b/theories/SymGroup/cycles.v index d7929cd..8205eac 100644 --- a/theories/SymGroup/cycles.v +++ b/theories/SymGroup/cycles.v @@ -43,6 +43,7 @@ From mathcomp Require finmodule. Require Import tools permcomp. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/SymGroup/cycletype.v b/theories/SymGroup/cycletype.v index d35ffee..9d8d899 100644 --- a/theories/SymGroup/cycletype.v +++ b/theories/SymGroup/cycletype.v @@ -70,6 +70,7 @@ From mathcomp Require Import ssralg matrix mxalgebra algC classfun. Require Import partition tools sorted. Require Import permcomp fibered_set cycles. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/SymGroup/permcent.v b/theories/SymGroup/permcent.v index 90f75ae..6df083b 100644 --- a/theories/SymGroup/permcent.v +++ b/theories/SymGroup/permcent.v @@ -78,6 +78,7 @@ Require Import tools partition permcomp cycles cycletype. Import GroupScope. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/SymGroup/presentSn.v b/theories/SymGroup/presentSn.v index 19e0649..1199311 100644 --- a/theories/SymGroup/presentSn.v +++ b/theories/SymGroup/presentSn.v @@ -110,6 +110,7 @@ From mathcomp Require Import ssralg poly ssrint. Require Import permcomp tools permuted combclass congr. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/SymGroup/towerSn.v b/theories/SymGroup/towerSn.v index 5c8caa4..3e63bb2 100644 --- a/theories/SymGroup/towerSn.v +++ b/theories/SymGroup/towerSn.v @@ -73,6 +73,7 @@ Notation "''SG_' n" := [set: 'S_n] Import LeqGeqOrder. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/SymGroup/weak_order.v b/theories/SymGroup/weak_order.v index 0a4f857..e4841e9 100644 --- a/theories/SymGroup/weak_order.v +++ b/theories/SymGroup/weak_order.v @@ -33,6 +33,7 @@ From mathcomp Require Import fingroup perm morphism presentation. Require Import permcomp tools permuted combclass congr presentSn ordtype. +Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. From 12dbf967392572f04cfaca4fe3b7712a5d79f5c0 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sat, 27 Jun 2026 14:11:36 +0200 Subject: [PATCH 2/2] [CI] Update Nix toolbox --- ....0.yml => nix-action-rocq-9.0-mc2.5.0.yml} | 125 +++++------ .../workflows/nix-action-rocq-9.1-mc2.5.0.yml | 200 ++++++++++++++++++ .../nix-action-rocq-9.1-mcmaster.yml | 196 +++++++++++++++++ .nix/config.nix | 67 ++++-- .nix/coq-nix-toolbox.nix | 2 +- .nix/coq-overlays/coq-combi/default.nix | 74 +++++-- 6 files changed, 550 insertions(+), 114 deletions(-) rename .github/workflows/{nix-action-rocq-9.0-mc2.4.0.yml => nix-action-rocq-9.0-mc2.5.0.yml} (71%) create mode 100644 .github/workflows/nix-action-rocq-9.1-mc2.5.0.yml create mode 100644 .github/workflows/nix-action-rocq-9.1-mcmaster.yml diff --git a/.github/workflows/nix-action-rocq-9.0-mc2.4.0.yml b/.github/workflows/nix-action-rocq-9.0-mc2.5.0.yml similarity index 71% rename from .github/workflows/nix-action-rocq-9.0-mc2.4.0.yml rename to .github/workflows/nix-action-rocq-9.0-mc2.5.0.yml index 9853468..e894f10 100644 --- a/.github/workflows/nix-action-rocq-9.0-mc2.4.0.yml +++ b/.github/workflows/nix-action-rocq-9.0-mc2.5.0.yml @@ -1,6 +1,7 @@ jobs: - coq-combi: - needs: [] + coq: + needs: + - rocq-core runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -8,7 +9,7 @@ jobs: 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@v4 + uses: actions/checkout@v6 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -22,7 +23,7 @@ jobs: }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ \ fi\nfi\n" - name: Git checkout - uses: actions/checkout@v4 + uses: actions/checkout@v6 with: fetch-depth: 0 ref: ${{ env.tested_commit }} @@ -30,17 +31,18 @@ jobs: uses: cachix/install-nix-action@v31 with: nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq + - name: Cachix setup math-comp uses: cachix/cachix-action@v16 with: - extraPullNames: coq-community, math-comp - name: coq + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp - id: stepGetDerivation - name: Getting derivation for current job (coq-combi) + name: Getting derivation for current job (coq) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"rocq-9.0-mc2.4.0\" --argstr job \"coq-combi\" \\\n --dry-run 2> err > - out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: - getting derivation failed\"; exit 1; fi\n" + \"rocq-9.0-mc2.5.0\" --argstr job \"coq\" \\\n --dry-run 2> err > out || + (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting + derivation failed\"; exit 1; fi\n" - id: stepCheck name: Checking presence of CI target for current job run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs @@ -49,39 +51,16 @@ jobs: \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.0-mc2.4.0" --argstr job "coq" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.0-mc2.4.0" --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.0-mc2.4.0" --argstr job "mathcomp-fingroup" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.0-mc2.4.0" --argstr job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: multinomials' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.0-mc2.4.0" --argstr job "multinomials" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-character' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.0-mc2.4.0" --argstr job "mathcomp-character" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-field' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.0-mc2.4.0" --argstr job "mathcomp-field" + "rocq-9.0-mc2.5.0" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.0-mc2.4.0" --argstr job "coq-combi" - mathcomp: - needs: [] + "rocq-9.0-mc2.5.0" --argstr job "coq" + coq-combi: + needs: + - coq runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -89,7 +68,7 @@ jobs: 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@v4 + uses: actions/checkout@v6 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -103,7 +82,7 @@ jobs: }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ \ fi\nfi\n" - name: Git checkout - uses: actions/checkout@v4 + uses: actions/checkout@v6 with: fetch-depth: 0 ref: ${{ env.tested_commit }} @@ -111,17 +90,18 @@ jobs: uses: cachix/install-nix-action@v31 with: nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq + - name: Cachix setup math-comp uses: cachix/cachix-action@v16 with: - extraPullNames: coq-community, math-comp - name: coq + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp - id: stepGetDerivation - name: Getting derivation for current job (mathcomp) + name: Getting derivation for current job (coq-combi) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"rocq-9.0-mc2.4.0\" --argstr job \"mathcomp\" \\\n --dry-run 2> err > out - || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting - derivation failed\"; exit 1; fi\n" + \"rocq-9.0-mc2.5.0\" --argstr job \"coq-combi\" \\\n --dry-run 2> err > + out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: + getting derivation failed\"; exit 1; fi\n" - id: stepCheck name: Checking presence of CI target for current job run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs @@ -132,20 +112,24 @@ jobs: - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.0-mc2.4.0" --argstr job "coq" + "rocq-9.0-mc2.5.0" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-character' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.0-mc2.4.0" --argstr job "mathcomp-character" + "rocq-9.0-mc2.5.0" --argstr job "mathcomp-character" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: hierarchy-builder' + name: 'Building/fetching previous CI target: multinomials' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.0-mc2.4.0" --argstr job "hierarchy-builder" + "rocq-9.0-mc2.5.0" --argstr job "multinomials" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: stdlib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.0-mc2.5.0" --argstr job "stdlib" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.0-mc2.4.0" --argstr job "mathcomp" - rocq: + "rocq-9.0-mc2.5.0" --argstr job "coq-combi" + rocq-core: needs: [] runs-on: ubuntu-latest steps: @@ -154,7 +138,7 @@ jobs: 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@v4 + uses: actions/checkout@v6 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -168,7 +152,7 @@ jobs: }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ \ fi\nfi\n" - name: Git checkout - uses: actions/checkout@v4 + uses: actions/checkout@v6 with: fetch-depth: 0 ref: ${{ env.tested_commit }} @@ -176,17 +160,18 @@ jobs: uses: cachix/install-nix-action@v31 with: nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq + - name: Cachix setup math-comp uses: cachix/cachix-action@v16 with: - extraPullNames: coq-community, math-comp - name: coq + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp - id: stepGetDerivation - name: Getting derivation for current job (rocq) + name: Getting derivation for current job (rocq-core) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"rocq-9.0-mc2.4.0\" --argstr job \"rocq\" \\\n --dry-run 2> err > out || - (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting - derivation failed\"; exit 1; fi\n" + \"rocq-9.0-mc2.5.0\" --argstr job \"rocq-core\" \\\n --dry-run 2> err > + out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: + getting derivation failed\"; exit 1; fi\n" - id: stepCheck name: Checking presence of CI target for current job run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs @@ -194,22 +179,18 @@ jobs: ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.0-mc2.4.0" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.0-mc2.4.0" --argstr job "rocq" -name: Nix CI for bundle rocq-9.0-mc2.4.0 + "rocq-9.0-mc2.5.0" --argstr job "rocq-core" +name: Nix CI for bundle rocq-9.0-mc2.5.0 on: pull_request: paths: - - .github/workflows/nix-action-rocq-9.0-mc2.4.0.yml + - .github/workflows/nix-action-rocq-9.0-mc2.5.0.yml pull_request_target: paths-ignore: - - .github/workflows/nix-action-rocq-9.0-mc2.4.0.yml + - .github/workflows/nix-action-rocq-9.0-mc2.5.0.yml types: - opened - synchronize diff --git a/.github/workflows/nix-action-rocq-9.1-mc2.5.0.yml b/.github/workflows/nix-action-rocq-9.1-mc2.5.0.yml new file mode 100644 index 0000000..e6f6653 --- /dev/null +++ b/.github/workflows/nix-action-rocq-9.1-mc2.5.0.yml @@ -0,0 +1,200 @@ +jobs: + coq: + needs: + - rocq-core + 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@v6 + 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@v6 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v31 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepGetDerivation + name: Getting derivation for current job (coq) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-9.1-mc2.5.0\" --argstr job \"coq\" \\\n --dry-run 2> err > out || + (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting + derivation failed\"; exit 1; fi\n" + - id: stepCheck + name: Checking presence of CI target for current job + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: rocq-core' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1-mc2.5.0" --argstr job "rocq-core" + - if: steps.stepCheck.outputs.status != 'fetched' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1-mc2.5.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@v6 + 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@v6 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v31 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepGetDerivation + name: Getting derivation for current job (coq-combi) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-9.1-mc2.5.0\" --argstr job \"coq-combi\" \\\n --dry-run 2> err > + out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: + getting derivation failed\"; exit 1; fi\n" + - id: stepCheck + name: Checking presence of CI target for current job + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1-mc2.5.0" --argstr job "coq" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-character' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1-mc2.5.0" --argstr job "mathcomp-character" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: multinomials' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1-mc2.5.0" --argstr job "multinomials" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: stdlib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1-mc2.5.0" --argstr job "stdlib" + - if: steps.stepCheck.outputs.status != 'fetched' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1-mc2.5.0" --argstr job "coq-combi" + rocq-core: + 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@v6 + 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@v6 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v31 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepGetDerivation + name: Getting derivation for current job (rocq-core) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-9.1-mc2.5.0\" --argstr job \"rocq-core\" \\\n --dry-run 2> err > + out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: + getting derivation failed\"; exit 1; fi\n" + - id: stepCheck + name: Checking presence of CI target for current job + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1-mc2.5.0" --argstr job "rocq-core" +name: Nix CI for bundle rocq-9.1-mc2.5.0 +on: + pull_request: + paths: + - .github/workflows/nix-action-rocq-9.1-mc2.5.0.yml + pull_request_target: + paths-ignore: + - .github/workflows/nix-action-rocq-9.1-mc2.5.0.yml + types: + - opened + - synchronize + - reopened + push: + branches: + - master diff --git a/.github/workflows/nix-action-rocq-9.1-mcmaster.yml b/.github/workflows/nix-action-rocq-9.1-mcmaster.yml new file mode 100644 index 0000000..dfe0a60 --- /dev/null +++ b/.github/workflows/nix-action-rocq-9.1-mcmaster.yml @@ -0,0 +1,196 @@ +jobs: + coq: + needs: + - rocq-core + 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@v6 + 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@v6 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v31 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepGetDerivation + name: Getting derivation for current job (coq) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-9.1-mcmaster\" --argstr job \"coq\" \\\n --dry-run 2> err > out || + (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting + derivation failed\"; exit 1; fi\n" + - id: stepCheck + name: Checking presence of CI target for current job + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: rocq-core' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1-mcmaster" --argstr job "rocq-core" + - if: steps.stepCheck.outputs.status != 'fetched' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1-mcmaster" --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@v6 + 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@v6 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v31 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepGetDerivation + name: Getting derivation for current job (coq-combi) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-9.1-mcmaster\" --argstr job \"coq-combi\" \\\n --dry-run 2> err > + out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: + getting derivation failed\"; exit 1; fi\n" + - id: stepCheck + name: Checking presence of CI target for current job + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1-mcmaster" --argstr job "coq" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-character' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1-mcmaster" --argstr job "mathcomp-character" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: stdlib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1-mcmaster" --argstr job "stdlib" + - if: steps.stepCheck.outputs.status != 'fetched' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1-mcmaster" --argstr job "coq-combi" + rocq-core: + 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@v6 + 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@v6 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v31 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepGetDerivation + name: Getting derivation for current job (rocq-core) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-9.1-mcmaster\" --argstr job \"rocq-core\" \\\n --dry-run 2> err > + out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: + getting derivation failed\"; exit 1; fi\n" + - id: stepCheck + name: Checking presence of CI target for current job + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1-mcmaster" --argstr job "rocq-core" +name: Nix CI for bundle rocq-9.1-mcmaster +on: + pull_request: + paths: + - .github/workflows/nix-action-rocq-9.1-mcmaster.yml + pull_request_target: + paths-ignore: + - .github/workflows/nix-action-rocq-9.1-mcmaster.yml + types: + - opened + - synchronize + - reopened + push: + branches: + - master diff --git a/.nix/config.nix b/.nix/config.nix index 4b8bb3b..989a506 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -25,25 +25,66 @@ ## /!\ Manual overlays in `.nix/coq-overlays` should be preferred then. # buildInputs = [ ]; + ## Set this when the package has no rocqPackages version yet + ## (either in nixpkgs or in .nix/rocq-overlays) + no-rocq-yet = true; + ## Indicate the relative location of your _CoqProject ## If not specified, it defaults to "_CoqProject" # coqproject = "_CoqProject"; ## select an entry to build in the following `bundles` set ## defaults to "default" - default-bundle = "rocq-9.0-mc2.4.0"; + default-bundle = "rocq-9.1-mc2.5.0"; ## write one `bundles.name` attribute set per ## alternative configuration ## When generating GitHub Action CI, one workflow file ## will be created per bundle - bundles."rocq-9.0-mc2.4.0" = { + bundles = { + "rocq-9.0-mc2.5.0" = { + rocqPackages = { + rocq-core.override.version = "9.0"; + mathcomp.override.version = "2.5.0"; + mathcomp.job = false; + }; + coqPackages = { + coq.override.version = "9.0"; + mathcomp.override.version = "2.5.0"; + }; + }; + "rocq-9.1-mc2.5.0" = { + rocqPackages = { + rocq-core.override.version = "9.1"; + mathcomp.override.version = "2.5.0"; + mathcomp.job = false; + }; + coqPackages = { + coq.override.version = "9.1"; + mathcomp.override.version = "2.5.0"; + }; + }; + "rocq-9.1-mcmaster" = { + rocqPackages = { + rocq-core.override.version = "9.1"; + mathcomp.override.version = "master"; + mathcomp-finmap.override.version = "master"; + multinomials.override.version = "master"; + mathcomp.job = false; + multinomials.job = false; + mathcomp-finmap.job = false; + }; + coqPackages = { + coq.override.version = "9.1"; + mathcomp.override.version = "master"; + mathcomp-finmap.override.version = "master"; + multinomials.override.version = "master"; + }; + }; ## You can override Coq and other Coq coqPackages ## through the following attribute # coqPackages.coq.override.version = "8.11"; - coqPackages.rocq.override.version = "9.0"; - coqPackages.mathcomp.override.version = "2.4.0"; ## In some cases, light overrides are not available/enough ## in which case you can use either @@ -83,32 +124,22 @@ # push-branches = [ "master" "branch2" ]; }; - # bundles."rocq-9.0-mc2.4.0" = { - # coqPackages.coq.override.version = "8.19"; - # coqPackages.mathcomp.override.version = "2.4.0"; - # }; - - # bundles."coq8.20-mc2.4.0" = { - # coqPackages.coq.override.version = "8.20"; - # coqPackages.mathcomp.override.version = "2.4.0"; - # }; - ## Cachix caches to use in CI ## Below we list some standard ones cachix.coq = {}; - cachix.math-comp = {}; + cachix.math-comp.authToken = "CACHIX_AUTH_TOKEN"; cachix.coq-community = {}; - + ## If you have write access to one of these caches you can ## provide the auth token or signing key through a secret ## variable on GitHub. Then, you should give the variable ## name here. For instance, coq-community projects can use ## the following line instead of the one above: # cachix.coq-community.authToken = "CACHIX_AUTH_TOKEN"; - + ## Or if you have a signing key for a given Cachix cache: # cachix.my-cache.signingKey = "CACHIX_SIGNING_KEY" - + ## Note that here, CACHIX_AUTH_TOKEN and CACHIX_SIGNING_KEY ## are the names of secret variables. They are set in ## GitHub's web interface. diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index 65931b4..c4fe2e9 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"0ab08603eabcfd0dd4b98ec4bec9dc05ab361ba2" +"d7d07e70842253ad4fb71fd0d55742d15e347775" diff --git a/.nix/coq-overlays/coq-combi/default.nix b/.nix/coq-overlays/coq-combi/default.nix index 5ebc399..eb5c897 100644 --- a/.nix/coq-overlays/coq-combi/default.nix +++ b/.nix/coq-overlays/coq-combi/default.nix @@ -4,31 +4,50 @@ ## but the full doc is on nixos / nix packages website: ## https://nixos.org/manual/nixpkgs/stable/#sec-language-coq -{ lib, mkCoqDerivation, which, coq - , mathcomp-ssreflect, mathcomp-fingroup - , mathcomp-algebra, multinomials - , mathcomp-character, mathcomp-field, hierarchy-builder +{ + lib, + coq, + mkCoqDerivation, + mathcomp, + multinomials, + stdlib, ## declare extra dependencies here, to be used in propagateBuildInputs e.g. # , mathcomp, coq-elpi - , version ? null }: + version ? null, +}: -with lib; mkCoqDerivation { - pname = "coq-combi"; - ## you can configure the domain, owner and repository, the default are: - # repo = "coq-combi"; - # owner = "coq-community"; - # domain = "github.com"; +let + derivation = mkCoqDerivation { + pname = "coq-combi"; + repo = "Coq-Combi"; + owner = "math-comp"; + ## you can configure the domain, owner and repository, the default are: + # repo = "coq-combi"; + # owner = "coq-community"; + # domain = "github.com"; - inherit version; + inherit version; ## The `defaultVersion` attribute is important for nixpkgs but can be kept unchanged ## for local usage since it will be ignored locally if ## - this derivation corresponds to the main attribute, ## - or its version is overridden (by a branch, PR, url or path) in `.nix/config.nix`. - defaultVersion = with versions; switch coq.coq-version [ - ## Example of possible dependencies - # { case = range "8.13" "8.14"; out = "1.2.0"; } - ## other predicates are `isLe v`, `isLt v`, `isGe v`, `isGt v`, `isEq v` etc - ] null; + defaultVersion = + let + case = coq: mc: out: { + cases = [ + coq + mc + ]; + inherit out; + }; + in + with lib.versions; + lib.switch + [ coq.version mathcomp.version ] + [ + (case (range "9.0" "9.1") (isGe "2.5.0") "2.0.3") + ] + null; ## Declare existing releases ## leave sha256 empty at first and then copy paste @@ -37,22 +56,30 @@ with lib; mkCoqDerivation { ## if the tag is not exactly the version number you can amend like this # release."1.1.1".rev = "v1.1.1"; ## if a consistent scheme gives the tag from the release number, you can do like this: - # releaseRev = v: "v${v}"; + release = { + "2.0.3".hash = ""; + }; + releaseRev = v: "v${v}"; ## Add dependencies in here. In particular you can add ## - arbitrary nix packages (you need to require them at the beginning of the file) ## - Coq packages (require them at the beginning of the file) ## - OCaml packages (use `coq.ocamlPackages.xxx`, no need to require them at the beginning of the file) - propagatedBuildInputs = - [ mathcomp-ssreflect mathcomp-fingroup mathcomp-algebra multinomials - mathcomp-character mathcomp-field]; + propagatedBuildInputs = [ + mathcomp.character + multinomials + stdlib + ]; ## Does the package contain OCaml code? # mlPlugin = false; ## Give some meta data ## This is needed for submitting the package to nixpkgs but not required for local use. - meta = { + meta = { + description = "Formalisation of (algebraic) combinatorics in Coq/MathComp."; + license = lib.licenses.gpl3Only; + }; ## Describe your package in one sentence # description = ""; ## Kindly ask one of these people if they want to be an official maintainer. @@ -62,4 +89,5 @@ with lib; mkCoqDerivation { ## https://github.com/NixOS/nixpkgs/blob/master/lib/licenses.nix # license = licenses.mit; }; -} +in +derivation