From 1df017027bfb2c28cb3e72d0c06890cf775712f0 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Mon, 5 Aug 2024 16:36:43 +0200 Subject: [PATCH 1/6] adapt to MC#1256 --- theories/BGappendixC.v | 2 +- theories/PFsection10.v | 2 +- theories/PFsection11.v | 4 ++-- theories/PFsection13.v | 6 +++--- theories/PFsection14.v | 4 ++-- theories/PFsection2.v | 2 +- theories/PFsection5.v | 3 ++- theories/PFsection6.v | 6 ++++-- theories/PFsection7.v | 11 ++++++----- theories/PFsection9.v | 4 ++-- 10 files changed, 24 insertions(+), 20 deletions(-) diff --git a/theories/BGappendixC.v b/theories/BGappendixC.v index 0ac92b4..e39078b 100644 --- a/theories/BGappendixC.v +++ b/theories/BGappendixC.v @@ -181,7 +181,7 @@ Proof. have fP v: in_alg F (uval v) \is a GRing.unit by rewrite rmorph_unit ?(valP v). pose f (v : {unit 'F_p}) := FinRing.unit F (fP v). have fM: {in setT &, {morph f: v1 v2 / (v1 * v2)%g}}. - by move=> v1 v2 _ _; apply: val_inj; rewrite /= -in_algE rmorphM. + by move=> v1 v2 _ _; apply: val_inj; rewrite /= -1?in_algE rmorphM. pose galFpU := Morphism fM @* [set: {unit 'F_p}]. have ->: [set u | uval u \in Fp] = galFpU. apply/setP=> u; rewrite inE /galFpU morphimEdom. diff --git a/theories/PFsection10.v b/theories/PFsection10.v index 030eaed..2f48dcf 100644 --- a/theories/PFsection10.v +++ b/theories/PFsection10.v @@ -767,7 +767,7 @@ have ub_G1: #|G1|%:R / #|G|%:R <= #|H|%:R / #|S|%:R + #|V|%:R / #|W|%:R :> algC. rewrite !oTI // !card_conjugates defNH defNV /= leq_add2r ?leq_mul //. by rewrite subset_leq_card ?subsetDl. rewrite le_gtF // addrAC lerBrDl -lerBrDr (le_trans ub_G1) //. -rewrite -(sdprod_card defS) -(sdprod_card defHU) addrC. +rewrite -(sdprod_card defS) -(sdprod_card defHU) [leLHS]addrC. rewrite -mulnA !natrM invfM mulVKf ?natrG_neq0 // -/w1 -/w2. have sW12_W: W1 :|: W2 \subset W by rewrite -(dprodWY defW) sub_gen. rewrite cardsD (setIidPr sW12_W) natrB ?subset_leq_card // mulrBl. diff --git a/theories/PFsection11.v b/theories/PFsection11.v index 25c00c8..502be74 100644 --- a/theories/PFsection11.v +++ b/theories/PFsection11.v @@ -889,7 +889,7 @@ have tau_alpha i: tau (alpha_ i j) = eta_ i j - eta_ i 0 - n *: zeta1. rewrite cfnorm_map_orthonormal // -Dn Itau1 ?mem_zchar ?n1S1 // mulr1. rewrite scaler_sumr cfproj_sum_orthonormal // rmorphN addrAC. rewrite Dn rmorphM/= !intr_normK ?rpred_nat // !rmorph_nat conj_intr // -Dn. - by rewrite -mulr2n mulrC mulrA -mulr_natr mulNr -mulrBr. + by rewrite -mulr2n mulrC mulrA -[in LHS]mulr_natr mulNr -mulrBr. have{a_even} Da: (a == 0) || (a == 2%:R). (* Second part of (11.8.2). *) suffices (b := a - 1): b ^+ 2 == 1. by rewrite -!(can_eq (subrK 1) a) add0r addrK orbC -eqf_sqr expr1n. @@ -1002,7 +1002,7 @@ Lemma FTtype34_structure (eta0row := \sum_j eta_ 0 j) : (*b*) (p < q)%N & (*c*) FTtype M == 3%N /\ typeP_Galois MtypeP]. Proof. -have sum_etaW F: \sum_(eta <- etaW) F eta = \sum_i \sum_j F (eta_ i j). +have sum_etaW (t : nmodType) (F : _ -> t): \sum_(eta <- etaW) F eta = \sum_i \sum_j F (eta_ i j). rewrite big_map big_tuple (reindex (dprod_Iirr defW)) /=. by rewrite pair_bigA; apply: eq_bigr => -[i j]. by exists (inv_dprod_Iirr defW) => ij; rewrite ?dprod_IirrK ?inv_dprod_IirrK. diff --git a/theories/PFsection13.v b/theories/PFsection13.v index 1bbaa3f..98621a4 100644 --- a/theories/PFsection13.v +++ b/theories/PFsection13.v @@ -663,7 +663,7 @@ have{} Deta10: {in H^#, eta10 =1 alpha}. set a1_2 := alpha 1%g ^+ 2 in ub_alpha. have Dsum_alpha: \sum_(x in H^#) `|alpha x| ^+ 2 = #|H|%:R * '[alpha] - a1_2. rewrite (cfnormE (cfun_onG _)) mulVKf ?neq0CG // (big_setD1 _ (group1 H)) /=. - by rewrite addrC intr_normK ?addKr ?Cint_vchar1. + by rewrite [RHS]addrC intr_normK ?addKr ?Cint_vchar1. have [/mulG_sub[sPH _] [_ _ _ [_ _ sW2P _ _] _]] := (dprodW defH, StypeP). have nz_alpha: alpha != 0. have [[x W2x ntx] [y W1y nty]] := (trivgPn _ ntW2, trivgPn _ ntW1). @@ -1164,7 +1164,7 @@ rewrite Dv natf_div ?dvdn_pred_predX // oQ. rewrite invfM invrK -mulrA -subn1 mulVKf ?gt_eqF ?ltr0n //; last first. by rewrite subn_gt0 -(exp1n p) ltn_exp2r ltnW // ltnW. rewrite -oQ natrB ?cardG_gt0 // !mulrBl mul1r mulrC mulKf ?neq0CG // -invfM. -by rewrite -natrM oQ opprD opprK addrA addrAC. +by rewrite -natrM oQ opprD opprK addrA [LHS]addrAC. Qed. End Thirteen_4_10. @@ -1218,7 +1218,7 @@ apply: le_trans; rewrite addnS /f /d; set x := (3 + r)%N. rewrite ler_pdivrMr ?ltr0n ?expn_gt0 // mulrAC (expnS 3) (natrM _ 3). rewrite mulrA mulfK ?gt_eqF ?ltr0n ?expn_gt0 //. rewrite -ler_pdivrMl ?ltr0n // !natrX -exprVn -exprMn. -rewrite mulrS mulrDr mulr1 mulVf ?pnatr_eq0 //. +rewrite [X in _ * X]mulrS mulrDr mulr1 mulVf ?pnatr_eq0 //. apply: le_trans (_ : (3%:R^-1 + 1) ^+ 2 <= _); last by rewrite -!CratrE; reflexivity. rewrite ler_sqr ?rpredD ?rpred1 ?rpredV ?rpred_nat // lerD2r. by rewrite lef_pV2 ?qualifE/= ?ltr0n ?leC_nat. diff --git a/theories/PFsection14.v b/theories/PFsection14.v index dcb7adc..ac73785 100644 --- a/theories/PFsection14.v +++ b/theories/PFsection14.v @@ -999,7 +999,7 @@ have{rho sumG0 sumG0_diff ub_rho lb_rho} []: rewrite /sumG0_diff -!addnA natrD opprD [in leLHS]addrA mulrBr opprB. rewrite [in leLHS]addrA lerBlDr ler_wpDr //. by rewrite mulr_ge0 ?invr_ge0 ?ler0n // subr_ge0 -sumr_const ler_sum. - rewrite mulrDl -!addrA addrCA [1 + _]addrA [_ + (_ - _)]addrA lerD //. + rewrite mulrDl -!addrA [leRHS]addrCA [1 + _]addrA [_ + (_ - _)]addrA lerD //. rewrite -(Lagrange (normal_sub nsKM)) natrM invfM mulrA -/k -/e /pq -De. rewrite ler_pM2r ?invr_gt0 ?gt0CiG // ler_pdivrMr ?gt0CG //. by rewrite mul1r leC_nat leq_pred. @@ -1015,7 +1015,7 @@ rewrite -!addrA ler_ltD //; last first. pose q2 : algC := (q ^ 2)%:R. apply: lt_le_trans (_ : 2%:R / q2 + (2%:R * q2)^-1 *+ 2 <= _); last first. rewrite addrC -[_ *+ 2]mulr_natl invfM mulVKf ?pnatr_eq0 //. - rewrite mulr_natl -mulrS -mulr_natl [q2]natrM. + rewrite mulr_natl -mulrS -[leLHS]mulr_natl [q2]natrM. by rewrite ler_pdivrMr ?mulr_gt0 ?gt0CG // mulKf ?neq0CG ?leC_nat. rewrite -natrM !addrA ltrD ?(FTtypeP_complV_ltr _ TtypeP) 1?ltnW //. rewrite ltrD ?(FTtypeP_complV_ltr _ StypeP) // /pq mulnC /q2 !natrM !invfM. diff --git a/theories/PFsection2.v b/theories/PFsection2.v index 1d8eee3..d1ed67d 100644 --- a/theories/PFsection2.v +++ b/theories/PFsection2.v @@ -370,7 +370,7 @@ apply: eq_bigr => a /sTA=> {T sTA}Aa. have [La def_Ca] := (subsetP sAL a Aa, defCA Aa). rewrite (eq_bigr (fun _ => alpha a * (psi a)^*)) => [|ax]; last first. by case/imsetP=> x Lx ->{ax}; rewrite !cfunJ. -rewrite sumr_const -index_cent1 mulrC -mulr_natr -!mulrA. +rewrite sumr_const -index_cent1 mulrC -[_ *+ #|_|]mulr_natr -!mulrA. rewrite (eq_bigr (fun xa => alpha a * (phi xa)^*)) => [|xa Fa_xa]; last first. by rewrite (DadeE _ Aa). rewrite -big_distrr /= -rmorph_sum; congr (_ * _). diff --git a/theories/PFsection5.v b/theories/PFsection5.v index 7e2812b..a8d249f 100644 --- a/theories/PFsection5.v +++ b/theories/PFsection5.v @@ -1035,7 +1035,8 @@ case/andP=> /(zchar_expansion (free_uniq (orthogonal_free oS3)))[b Zb {eta}->]. pose bS Si := \sum_(xi <- Si) b xi *: xi. have ZbS Si: bS Si \in 'Z[Si]. by rewrite /bS big_seq rpred_sum // => eta /mem_zchar/rpredZ_int->. -rewrite big_cat /= -!/(bS _) cfunE addrC addr_eq0 linearD => /eqP-bS2_1. +rewrite big_cat /= -!/(bS _) cfunE [X in X == 0]addrC addr_eq0 linearD. +move=> /eqP-bS2_1. transitivity (tau1 (bS S1) + tau2 (bS S2)). by rewrite !raddf_sum; congr (_ + _); apply/eq_big_seq=> xi Si_xi /=; rewrite !raddfZ_int // -(defY1, defY2). diff --git a/theories/PFsection6.v b/theories/PFsection6.v index 36ce84c..942d875 100644 --- a/theories/PFsection6.v +++ b/theories/PFsection6.v @@ -828,7 +828,8 @@ have{odd_frobL1} caseA_cohXY: caseA -> coherent (X ++ Y) L^# tau. have DsumXd: sumXd = (xi1 1%g)^-1 *: (cfReg L - cfReg (L / Z) %% Z)%CF. apply/(canRL (scalerK nz_xi1_1))/(canRL (addrK _)); rewrite !cfReg_sum. pose kerZ := [pred i : Iirr L | Z \subset cfker 'chi_i]. - rewrite 2!linear_sum (bigID kerZ) (reindex _ (mod_Iirr_bij nsZL)) /= addrC. + rewrite 2!linear_sum (bigID kerZ) (reindex _ (mod_Iirr_bij nsZL)) /=. + rewrite [LHS]addrC. congr (_ + _). apply: eq_big => [i | i _]; first by rewrite mod_IirrE ?cfker_mod. by rewrite linearZ mod_IirrE // cfMod1. @@ -1027,7 +1028,8 @@ have{caseA_cohXY Itau1 Ztau1 Dtau1 oYYt} cohXY: coherent (X ++ Y) L^# tau. exists (tau (gamma i) + #|H : Z|%:R *: Y1); last by rewrite addrK. apply/orthoPl=> _ /mapP[eta Yeta ->]. rewrite scalerN cfdotBl cfdotZl cfproj_sum_orthonormal // [x]addrAC. - rewrite -addrA mulrDr mulrBr mulrC -Dx0 -Da opprD addrA -!raddfB /=. + rewrite -[_ + 1 - _]addrA mulrDr mulrBr mulrC -Dx0 -Da opprD addrA. + rewrite -!raddfB /=. have Yeta_1: eta - eta1 \in 'Z[Y, L^#]. by rewrite zcharD1E rpredB ?seqInd_zcharW //= !cfunE !uniY ?subrr. rewrite Dtau1 ?Itau // ?(zchar_subset sYS) // cfdotBl cfdotZl. diff --git a/theories/PFsection7.v b/theories/PFsection7.v index 178c5a5..5d1b99c 100644 --- a/theories/PFsection7.v +++ b/theories/PFsection7.v @@ -330,7 +330,7 @@ rewrite exchange_big; apply: eq_bigr => xi _; rewrite exchange_big /=. apply: eq_big_seq => mu Smu; have Tmu := sST mu Smu. rewrite /u eh (cfdotEr _ (seqInd_on nsHL Tmu)) (mulrC _^-1) -mulrBl mulrA. rewrite -mulr_suml -mulr_sumr (big_setD1 1%g (group1 H)) /=; congr (_ * _ * _). -by rewrite addrC conj_natr ?addKr // (Cnat_seqInd1 Tmu). +by rewrite [RHS]addrC conj_natr ?addKr // (Cnat_seqInd1 Tmu). Qed. End InvDadeSeqInd. @@ -460,7 +460,7 @@ split=> // [ | chi /irrP[t def_chi] o_chiSnu]. do 2!apply: canRL (addrK _) _; rewrite -addrA; congr (_ + _). rewrite defX (addrC (- nu _)) cfnormB cfnormZ intr_normK // InuS //. rewrite cfdotZl cfproj_sum_orthogonal // Nzeta1 zeta1 divff // divr1. - rewrite !mulr1 aut_intr // mulrBr mulrDr mulVKf // addrAC. + rewrite !mulr1 aut_intr // mulrBr mulrDr mulVKf // [RHS]addrAC. rewrite mulrA mulrC hu -[e^-1](divfK nze) -expr2; congr (_ * _ - _ + 1). rewrite -mulrA -sum_seqIndC1_square // mulr_sumr cfnorm_sum_orthogonal //. apply: eq_big_seq => xi Sxi. @@ -722,8 +722,9 @@ have nzh2: h + 2%:R != 0 by rewrite -natrD addnC pnatr_eq0. have{lhs} ->: lhs = 1 - e / h - (h - 1) / (e * h) - (e - 1) / (h + 2%:R). rewrite {}/lhs -{2}(addrK h 2%:R) !invfM (mulrBl _ _ h) mulVKf ?nzh //. rewrite addrCA (addrC _ h) mulrCA mulrA addrA mulrBr; congr (_ - _). - rewrite mulfK // mulrDr addrAC addrC mulrC mulrBl -mulrA mulVKf ?nze //. - rewrite mulrC mulrBr mulrBl mul1r addrAC addrC addrA; congr (_ - _). + rewrite mulfK // mulrDr addrAC [LHS]addrC mulrC mulrBl -mulrA mulVKf ?nze //. + rewrite mulrC mulrBr mulrBl mul1r [X in X + _]addrAC addrC addrA. + congr (_ - _). rewrite mulrCA mulVKf ?nze // addrCA mulrCA mulr_natl opprD addNKr. by rewrite !mulrBl opprB addrA subrK divff ?nzh. pose beta i := tau i ('Ind[L i, H i] 1 - 'chi_(r i)). @@ -755,7 +756,7 @@ suffices{min_rho1} sumB_max: sumB <= (e - 1) / (h + 2%:R). apply: (le_trans (y := \sum_i ('[rho i 'chi_t] - ea i))); last first. rewrite -subr_ge0 -opprB oppr_ge0 -mulNr opprB addrC mulrC. by rewrite /sumG0 defG0 Dade_cover_inequality ?cfnorm_irr. - rewrite (bigID (mem calB)) /= addrC lerD //. + rewrite (bigID (mem calB)) /= [leLHS]addrC lerD //. rewrite -subr_ge0 opprK -big_split sumr_ge0 //= => i _. by rewrite def_h1 eh subrK cfnorm_ge0. rewrite (bigD1 i1) ?inE ?eqxx ?andbF //= -lerBlDl. diff --git a/theories/PFsection9.v b/theories/PFsection9.v index 69d8458..969cc8a 100644 --- a/theories/PFsection9.v +++ b/theories/PFsection9.v @@ -1828,7 +1828,7 @@ have oS4: (q * u * size S4 + p.-1 * (q + u))%N = (p ^ q).-1. have /S3qu/eqP: 'Ind 'chi_s \in S3. by rewrite mem_filter /= S2's sH0CC' ?mem_seqInd. by rewrite natrM cfInd1 // -(index_sdprod defM) => /(mulfI (neq0CG _)). - rewrite sumr_const -mulr_natl natrM natrX -nb_mu; congr (_%:R * _). + rewrite sumr_const -[LHS]mulr_natl natrM natrX -nb_mu; congr (_%:R * _). have [_ s_mu_H0C] := nb_redM_H0. rewrite (size_red_subseq_seqInd_typeP MtypeP _ s_mu_H0C); last first. - by apply/allP; apply: filter_all. @@ -2202,7 +2202,7 @@ have{x Zx X defX Delta Dalpha oD1} b_mod_ua: (b == 0 %[mod u %/ a])%C. - by rewrite memv_span ?inE. - apply: subvP (zchar_span S4_Gamma); apply: sub_span; apply: mem_subseq. by rewrite map_subseq ?filter_subseq. - rewrite Dalpha addrC cfdotDl (span_orthogonal oD1); first 1 last. + rewrite Dalpha [X + _]addrC cfdotDl (span_orthogonal oD1); first 1 last. - by rewrite memv_span ?inE. - rewrite addrC rpredB ?rpredZ //; last by rewrite memv_span ?map_f. by rewrite big_seq rpred_sum // => psi S1psi; rewrite memv_span ?map_f. From 02a190fc95162b59cb591838f86f6f693c6d6622 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Tue, 13 Aug 2024 10:53:30 +0200 Subject: [PATCH 2/6] update nix --- .github/workflows/nix-action-8.16.yml | 12 +- .github/workflows/nix-action-8.17.yml | 12 +- .github/workflows/nix-action-8.18.yml | 12 +- .github/workflows/nix-action-8.19.yml | 12 +- .github/workflows/nix-action-8.20.yml | 228 ++++++++++++++++++++++++ .github/workflows/nix-action-master.yml | 20 +-- .nix/config.nix | 4 + .nix/coq-nix-toolbox.nix | 2 +- 8 files changed, 267 insertions(+), 35 deletions(-) create mode 100644 .github/workflows/nix-action-8.20.yml diff --git a/.github/workflows/nix-action-8.16.yml b/.github/workflows/nix-action-8.16.yml index a38e315..67f83a1 100644 --- a/.github/workflows/nix-action-8.16.yml +++ b/.github/workflows/nix-action-8.16.yml @@ -8,7 +8,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@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -22,7 +22,7 @@ jobs: \ \"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 }} @@ -56,7 +56,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@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -70,7 +70,7 @@ jobs: \ \"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 }} @@ -141,7 +141,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@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -155,7 +155,7 @@ jobs: \ \"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 }} diff --git a/.github/workflows/nix-action-8.17.yml b/.github/workflows/nix-action-8.17.yml index af7aad8..d928fa1 100644 --- a/.github/workflows/nix-action-8.17.yml +++ b/.github/workflows/nix-action-8.17.yml @@ -8,7 +8,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@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -22,7 +22,7 @@ jobs: \ \"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 }} @@ -56,7 +56,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@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -70,7 +70,7 @@ jobs: \ \"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 }} @@ -141,7 +141,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@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -155,7 +155,7 @@ jobs: \ \"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 }} diff --git a/.github/workflows/nix-action-8.18.yml b/.github/workflows/nix-action-8.18.yml index 1fb9a1e..e771506 100644 --- a/.github/workflows/nix-action-8.18.yml +++ b/.github/workflows/nix-action-8.18.yml @@ -8,7 +8,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@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -22,7 +22,7 @@ jobs: \ \"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 }} @@ -56,7 +56,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@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -70,7 +70,7 @@ jobs: \ \"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 }} @@ -141,7 +141,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@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -155,7 +155,7 @@ jobs: \ \"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 }} diff --git a/.github/workflows/nix-action-8.19.yml b/.github/workflows/nix-action-8.19.yml index 7632398..3a239d3 100644 --- a/.github/workflows/nix-action-8.19.yml +++ b/.github/workflows/nix-action-8.19.yml @@ -8,7 +8,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@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -22,7 +22,7 @@ jobs: \ \"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 }} @@ -56,7 +56,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@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -70,7 +70,7 @@ jobs: \ \"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 }} @@ -141,7 +141,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@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -155,7 +155,7 @@ jobs: \ \"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 }} diff --git a/.github/workflows/nix-action-8.20.yml b/.github/workflows/nix-action-8.20.yml new file mode 100644 index 0000000..9803b38 --- /dev/null +++ b/.github/workflows/nix-action-8.20.yml @@ -0,0 +1,228 @@ +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@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" + - name: Git checkout + uses: actions/checkout@v4 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v27 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v15 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target coq + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"8.20\" --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 "8.20" --argstr + job "coq" + 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@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" + - name: Git checkout + uses: actions/checkout@v4 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v27 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v15 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - 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 \"8.20\" --argstr job \"mathcomp\" \\\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 previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr + job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq-elpi' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr + job "coq-elpi" + - 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 "8.20" --argstr + job "hierarchy-builder" + - 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 "8.20" --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 "8.20" --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 "8.20" --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 "8.20" --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 "8.20" --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 "8.20" --argstr + job "mathcomp-character" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr + job "mathcomp" + odd-order: + needs: + - coq + - mathcomp + 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@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" + - name: Git checkout + uses: actions/checkout@v4 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v27 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v15 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target odd-order + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"8.20\" --argstr job \"odd-order\" \\\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 previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr + job "coq" + - 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 "8.20" --argstr + job "mathcomp-character" + - 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 "8.20" --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 "8.20" --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 "8.20" --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 "8.20" --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 "8.20" --argstr + job "mathcomp-field" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr + job "mathcomp" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr + job "odd-order" +name: Nix CI for bundle 8.20 +'on': + pull_request: + paths: + - .github/workflows/nix-action-8.20.yml + pull_request_target: + paths-ignore: + - .github/workflows/nix-action-8.20.yml + types: + - opened + - synchronize + - reopened + push: + branches: + - master diff --git a/.github/workflows/nix-action-master.yml b/.github/workflows/nix-action-master.yml index d598384..e5a2c3b 100644 --- a/.github/workflows/nix-action-master.yml +++ b/.github/workflows/nix-action-master.yml @@ -8,7 +8,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@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -22,7 +22,7 @@ jobs: \ \"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 }} @@ -56,7 +56,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@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -70,7 +70,7 @@ jobs: \ \"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 }} @@ -109,7 +109,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@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -123,7 +123,7 @@ jobs: \ \"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 }} @@ -167,7 +167,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@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -181,7 +181,7 @@ jobs: \ \"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 }} @@ -252,7 +252,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@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -266,7 +266,7 @@ jobs: \ \"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 }} diff --git a/.nix/config.nix b/.nix/config.nix index 1657666..babe0af 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -51,6 +51,10 @@ coq.override.version = "8.19"; mathcomp.override.version = "mathcomp-2.2.0"; }; + bundles."8.20".coqPackages = { + coq.override.version = "8.20"; + mathcomp.override.version = "mathcomp-2.2.0"; + }; bundles."master".coqPackages = { coq.override.version = "master"; coq-elpi.override.version = "coq-master"; diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index b5a006a..5dfe651 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"281be33f1e42a92e5c47f30907819aad1a45e5f2" +"208d8cd3c82113f719ae67d7652203da3fbbcbe4" From 1c1d652060e710539e65e896622b8af63b5c57f3 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 14 Aug 2024 11:43:49 +0200 Subject: [PATCH 3/6] fix nix and CI for coq-master --- .nix/config.nix | 2 +- .nix/coq-overlays/coq-elpi/default.nix | 85 ++++++++++++++++++++++++++ 2 files changed, 86 insertions(+), 1 deletion(-) create mode 100644 .nix/coq-overlays/coq-elpi/default.nix diff --git a/.nix/config.nix b/.nix/config.nix index babe0af..c0e1256 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -57,7 +57,7 @@ }; bundles."master".coqPackages = { coq.override.version = "master"; - coq-elpi.override.version = "coq-master"; + coq-elpi.override.version = "master"; hierarchy-builder.override.version = "master"; mathcomp.override.version = "master"; }; diff --git a/.nix/coq-overlays/coq-elpi/default.nix b/.nix/coq-overlays/coq-elpi/default.nix new file mode 100644 index 0000000..9a7879f --- /dev/null +++ b/.nix/coq-overlays/coq-elpi/default.nix @@ -0,0 +1,85 @@ +{ lib, mkCoqDerivation, which, coq, version ? null }: + +let + elpi = coq.ocamlPackages.elpi.override (lib.switch coq.coq-version [ + { case = "8.11"; out = { version = "1.11.4"; };} + { case = "8.12"; out = { version = "1.12.0"; };} + { case = "8.13"; out = { version = "1.13.7"; };} + { case = "8.14"; out = { version = "1.13.7"; };} + { case = "8.15"; out = { version = "1.15.0"; };} + { case = "8.16"; out = { version = "1.17.0"; };} + { case = "8.17"; out = { version = "1.17.0"; };} + { case = "8.18"; out = { version = "1.18.1"; };} + { case = "8.20"; out = { version = "1.19.2"; };} + ] { version = "v1.19.4"; } ); +in (mkCoqDerivation { + pname = "elpi"; + repo = "coq-elpi"; + owner = "LPCIC"; + inherit version; + defaultVersion = lib.switch coq.coq-version [ + { case = "8.20"; out = "2.2.0"; } + { case = "8.19"; out = "2.0.1"; } + { case = "8.18"; out = "2.0.0"; } + { case = "8.17"; out = "1.18.0"; } + { case = "8.16"; out = "1.15.6"; } + { case = "8.15"; out = "1.14.0"; } + { case = "8.14"; out = "1.11.2"; } + { case = "8.13"; out = "1.11.1"; } + { case = "8.12"; out = "1.8.3_8.12"; } + { case = "8.11"; out = "1.6.3_8.11"; } + ] null; + release."2.2.0".sha256 = "sha256-rADEoqTXM7/TyYkUKsmCFfj6fjpWdnZEOK++5oLfC/I="; + release."2.0.1".sha256 = "sha256-cuoPsEJ+JRLVc9Golt2rJj4P7lKltTrrmQijjoViooc="; + release."2.0.0".sha256 = "sha256-A/cH324M21k3SZ7+YWXtaYEbu6dZQq3K0cb1RMKjbsM="; + release."1.19.0".sha256 = "sha256-kGoo61nJxeG/BqV+iQaV3iinwPStND+7+fYMxFkiKrQ="; + release."1.18.0".sha256 = "sha256-2fCOlhqi4YkiL5n8SYHuc3pLH+DArf9zuMH7IhpBc2Y="; + release."1.17.0".sha256 = "sha256-J8GatRKFU0ekNCG3V5dBI+FXypeHcLgC5QJYGYzFiEM="; + release."1.15.6".sha256 = "sha256-qc0q01tW8NVm83801HHOBHe/7H1/F2WGDbKO6nCXfno="; + release."1.15.1".sha256 = "sha256-NT2RlcIsFB9AvBhMxil4ZZIgx+KusMqDflj2HgQxsZg="; + release."1.14.0".sha256 = "sha256:1v2p5dlpviwzky2i14cj7gcgf8cr0j54bdm9fl5iz1ckx60j6nvp"; + release."1.13.0".sha256 = "1j7s7dlnjbw222gnbrsjgmjck1yrx7h6hwm8zikcyxi0zys17w7n"; + release."1.12.1".sha256 = "sha256-4mO6/co7NcIQSGIQJyoO8lNWXr6dqz+bIYPO/G0cPkY="; + release."1.11.2".sha256 = "0qk5cfh15y2zrja7267629dybd3irvxk1raz7z8qfir25a81ckd4"; + release."1.11.1".sha256 = "10j076vc2hdcbm15m6s7b6xdzibgfcbzlkgjnlkr2vv9k13qf8kc"; + release."1.10.1".sha256 = "1zsyx26dvj7pznfd2msl2w7zbw51q1nsdw0bdvdha6dga7ijf7xk"; + release."1.9.7".sha256 = "0rvn12h9dpk9s4pxy32p8j0a1h7ib7kg98iv1cbrdg25y5vs85n1"; + release."1.9.5".sha256 = "0gjdwmb6bvb5gh0a6ra48bz5fb3pr5kpxijb7a8mfydvar5i9qr6"; + release."1.9.4".sha256 = "0nii7238mya74f9g6147qmpg6gv6ic9b54x5v85nb6q60d9jh0jq"; + release."1.9.3".sha256 = "198irm800fx3n8n56vx1c6f626cizp1d7jfkrc6ba4iqhb62ma0z"; + release."1.9.2".sha256 = "1rr2fr8vjkc0is7vh1461aidz2iwkigdkp6bqss4hhv0c3ijnn07"; + release."1.8.3_8.12".sha256 = "15z2l4zy0qpw0ws7bvsmpmyv543aqghrfnl48nlwzn9q0v89p557"; + release."1.8.3_8.12".version = "1.8.3"; + release."1.8.2_8.12".sha256 = "1n6jwcdazvjgj8vsv2r9zgwpw5yqr5a1ndc2pwhmhqfl04b5dk4y"; + release."1.8.2_8.12".version = "1.8.2"; + release."1.8.1".sha256 = "1fbbdccdmr8g4wwpihzp4r2xacynjznf817lhijw6kqfav75zd0r"; + release."1.8.0".sha256 = "13ywjg94zkbki22hx7s4gfm9rr87r4ghsgan23xyl3l9z8q0idd1"; + release."1.7.0".sha256 = "1ws5cqr0xawv69prgygbl3q6dgglbaw0vc397h9flh90kxaqgyh8"; + release."1.6.3_8.11".sha256 = "1j340cr2bv95clzzkkfmsjkklham1mj84cmiyprzwv20q89zr1hp"; + release."1.6.3_8.11".version = "1.6.3"; + release."1.6.2_8.11".sha256 = "06xrx0ljilwp63ik2sxxr7h617dgbch042xfcnfpy5x96br147rn"; + release."1.6.2_8.11".version = "1.6.2"; + release."1.6.1_8.11".sha256 = "0yyyh35i1nb3pg4hw7cak15kj4y6y9l84nwar9k1ifdsagh5zq53"; + release."1.6.1_8.11".version = "1.6.1"; + release."1.6.0_8.11".sha256 = "0ahxjnzmd7kl3gl38kyjqzkfgllncr2ybnw8bvgrc6iddgga7bpq"; + release."1.6.0_8.11".version = "1.6.0"; + release."1.6.0".sha256 = "0kf99i43mlf750fr7fric764mm495a53mg5kahnbp6zcjcxxrm0b"; + releaseRev = v: "v${v}"; + + buildFlags = [ "OCAMLWARN=" ]; + + mlPlugin = true; + useDuneifVersion = v: lib.versions.isGe "2.2.0" v || v == "dev"; + propagatedBuildInputs = [ coq.ocamlPackages.findlib elpi ]; + + meta = { + description = "Coq plugin embedding ELPI"; + maintainers = [ lib.maintainers.cohencyril ]; + license = lib.licenses.lgpl21Plus; + }; +}).overrideAttrs (o: + lib.optionalAttrs (o.version != null + && (o.version == "dev" || lib.versions.isGe "2.2.0" o.version)) + { + propagatedBuildInputs = o.propagatedBuildInputs ++ [ coq.ocamlPackages.ppx_optcomp ]; + }) From 720ecbc9cc0f8d32cd5ec7f25de4f26984b28fd1 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 14 Aug 2024 11:50:11 +0200 Subject: [PATCH 4/6] outdated mathcomp --- .nix/coq-overlays/mathcomp/default.nix | 122 ------------------------- 1 file changed, 122 deletions(-) delete mode 100644 .nix/coq-overlays/mathcomp/default.nix diff --git a/.nix/coq-overlays/mathcomp/default.nix b/.nix/coq-overlays/mathcomp/default.nix deleted file mode 100644 index dbaf587..0000000 --- a/.nix/coq-overlays/mathcomp/default.nix +++ /dev/null @@ -1,122 +0,0 @@ -############################################################################ -# This file mainly provides the `mathcomp` derivation, which is # -# essentially a meta-package containing all core mathcomp libraries # -# (ssreflect fingroup algebra solvable field character). They can be # -# accessed individually through the passthrough attributes of mathcomp # -# bearing the same names (mathcomp.ssreflect, etc). # -############################################################################ -# Compiling a custom version of mathcomp using `mathcomp.override`. # -# This is the replacement for the former `mathcomp_ config` function. # -# See the documentation at doc/languages-frameworks/coq.section.md. # -############################################################################ - -{ lib, ncurses, graphviz, lua, fetchzip, - coq-elpi, hierarchy-builder, - mkCoqDerivation, recurseIntoAttrs, withDoc ? false, single ? false, - coqPackages, coq, version ? null }@args: -with builtins // lib; -let - repo = "math-comp"; - owner = "math-comp"; - withDoc = single && (args.withDoc or false); - defaultVersion = with versions; switch coq.coq-version [ - { case = isGe "8.11"; out = "1.14.0"; } - { case = range "8.11" "8.15"; out = "1.13.0"; } - { case = range "8.10" "8.13"; out = "1.12.0"; } - { case = range "8.7" "8.12"; out = "1.11.0"; } - { case = range "8.7" "8.11"; out = "1.10.0"; } - { case = range "8.7" "8.11"; out = "1.9.0"; } - { case = range "8.7" "8.9"; out = "1.8.0"; } - { case = range "8.6" "8.9"; out = "1.7.0"; } - { case = range "8.5" "8.7"; out = "1.6.4"; } - ] null; - release = { - "1.14.0".sha256 = "07yamlp1c0g5nahkd2gpfhammcca74ga2s6qr7a3wm6y6j5pivk9"; - "1.13.0".sha256 = "0j4cz2y1r1aw79snkcf1pmicgzf8swbaf9ippz0vg99a572zqzri"; - "1.12.0".sha256 = "1ccfny1vwgmdl91kz5xlmhq4wz078xm4z5wpd0jy5rn890dx03wp"; - "1.11.0".sha256 = "06a71d196wd5k4wg7khwqb7j7ifr7garhwkd54s86i0j7d6nhl3c"; - "1.10.0".sha256 = "1b9m6pwxxyivw7rgx82gn5kmgv2mfv3h3y0mmjcjfypi8ydkrlbv"; - "1.9.0".sha256 = "0lid9zaazdi3d38l8042lczb02pw5m9wq0yysiilx891hgq2p81r"; - "1.8.0".sha256 = "07l40is389ih8bi525gpqs3qp4yb2kl11r9c8ynk1ifpjzpnabwp"; - "1.7.0".sha256 = "0wnhj9nqpx2bw6n1l4i8jgrw3pjajvckvj3lr4vzjb3my2lbxdd1"; - "1.6.4".sha256 = "09ww48qbjsvpjmy1g9yhm0rrkq800ffq21p6fjkbwd34qvd82raz"; - "1.6.1".sha256 = "1ilw6vm4dlsdv9cd7kmf0vfrh2kkzr45wrqr8m37miy0byzr4p9i"; - }; - releaseRev = v: "mathcomp-${v}"; - - # list of core mathcomp packages sorted by dependency order - packages = [ "ssreflect" "fingroup" "algebra" "solvable" "field" "character" "all" ]; - - mathcomp_ = package: let - mathcomp-deps = if package == "single" then [] - else map mathcomp_ (head (splitList (pred.equal package) packages)); - pkgpath = if package == "single" then "mathcomp" else "mathcomp/${package}"; - pname = if package == "single" then "mathcomp" else "mathcomp-${package}"; - pkgallMake = '' - echo "all.v" > Make - echo "-I ." >> Make - echo "-R . mathcomp.all" >> Make - ''; - derivation = mkCoqDerivation ({ - inherit version pname defaultVersion release releaseRev repo owner; - - mlPlugin = versions.isLe "8.6" coq.coq-version; - nativeBuildInputs = optionals withDoc [ graphviz lua ]; - buildInputs = [ ncurses ]; - propagatedBuildInputs = [ coq-elpi hierarchy-builder ] ++ mathcomp-deps; - - buildFlags = optional withDoc "doc"; - - preBuild = '' - if [[ -f etc/utils/ssrcoqdep ]] - then patchShebangs etc/utils/ssrcoqdep - fi - if [[ -f etc/buildlibgraph ]] - then patchShebangs etc/buildlibgraph - fi - '' + '' - cd ${pkgpath} - '' + optionalString (package == "all") pkgallMake; - - meta = { - homepage = "https://math-comp.github.io/"; - license = licenses.cecill-b; - maintainers = with maintainers; [ vbgl jwiegley cohencyril ]; - }; - } // optionalAttrs (package != "single") - { passthru = genAttrs packages mathcomp_; } - // optionalAttrs withDoc { - htmldoc_template = - fetchzip { - url = "https://github.com/math-comp/math-comp.github.io/archive/doc-1.12.0.zip"; - sha256 = "0y1352ha2yy6k2dl375sb1r68r1qi9dyyy7dyzj5lp9hxhhq69x8"; - }; - postBuild = '' - cp -rf _build_doc/* . - rm -r _build_doc - ''; - postInstall = - let tgt = "$out/share/coq/${coq.coq-version}/"; in - optionalString withDoc '' - mkdir -p ${tgt} - cp -r htmldoc ${tgt} - cp -r $htmldoc_template/htmldoc_template/* ${tgt}/htmldoc/ - ''; - buildTargets = "doc"; - extraInstallFlags = [ "-f Makefile.coq" ]; - }); - patched-derivation1 = derivation.overrideAttrs (o: - optionalAttrs (o.pname != null && o.pname == "mathcomp-all" && - o.version != null && o.version != "dev" && versions.isLt "1.7" o.version) - { preBuild = ""; buildPhase = ""; installPhase = "echo doing nothing"; } - ); - patched-derivation = patched-derivation1.overrideAttrs (o: - optionalAttrs (versions.isLe "8.7" coq.coq-version || - (o.version != "dev" && versions.isLe "1.7" o.version)) - { - installFlags = o.installFlags ++ [ "-f Makefile.coq" ]; - } - ); - in patched-derivation; -in -mathcomp_ (if single then "single" else "all") From 273285b63b942d53feb32661f4ad7d450cc023fb Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 14 Aug 2024 12:01:16 +0200 Subject: [PATCH 5/6] fix --- .nix/coq-overlays/coq-elpi/default.nix | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.nix/coq-overlays/coq-elpi/default.nix b/.nix/coq-overlays/coq-elpi/default.nix index 9a7879f..0c4eef4 100644 --- a/.nix/coq-overlays/coq-elpi/default.nix +++ b/.nix/coq-overlays/coq-elpi/default.nix @@ -10,7 +10,8 @@ let { case = "8.16"; out = { version = "1.17.0"; };} { case = "8.17"; out = { version = "1.17.0"; };} { case = "8.18"; out = { version = "1.18.1"; };} - { case = "8.20"; out = { version = "1.19.2"; };} + { case = "8.19"; out = { version = "1.19.4"; };} + { case = "8.20"; out = { version = "1.19.4"; };} ] { version = "v1.19.4"; } ); in (mkCoqDerivation { pname = "elpi"; From e37c7056cf6c3232c27b0027c36de5e3a31c477a Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 14 Aug 2024 12:06:04 +0200 Subject: [PATCH 6/6] fix --- .nix/coq-overlays/coq-elpi/default.nix | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.nix/coq-overlays/coq-elpi/default.nix b/.nix/coq-overlays/coq-elpi/default.nix index 0c4eef4..372cef1 100644 --- a/.nix/coq-overlays/coq-elpi/default.nix +++ b/.nix/coq-overlays/coq-elpi/default.nix @@ -10,8 +10,8 @@ let { case = "8.16"; out = { version = "1.17.0"; };} { case = "8.17"; out = { version = "1.17.0"; };} { case = "8.18"; out = { version = "1.18.1"; };} - { case = "8.19"; out = { version = "1.19.4"; };} - { case = "8.20"; out = { version = "1.19.4"; };} + { case = "8.19"; out = { version = "1.18.1"; };} + { case = "8.20"; out = { version = "1.19.2"; };} ] { version = "v1.19.4"; } ); in (mkCoqDerivation { pname = "elpi";