From ee19f9f59956661e3b1eb8a2a1502988db425d2c Mon Sep 17 00:00:00 2001 From: Davide Fissore Date: Thu, 9 Nov 2023 10:55:40 +0100 Subject: [PATCH 01/16] Locality can be charged to coq.elpi.add-predicate --- Changelog.md | 15 +++++++++++++++ apps/tc/elpi/create_tc_predicate.elpi | 25 ++++++++++++++++--------- apps/tc/src/coq_elpi_tc_register.ml | 12 +++++++++--- apps/tc/tests/section_in_out.v | 11 +++++++++-- coq-builtin.elpi | 11 +++++++---- src/coq_elpi_builtins.ml | 18 ++++++++++++++---- src/coq_elpi_builtins.mli | 2 +- src/coq_elpi_programs.ml | 4 ++-- 8 files changed, 73 insertions(+), 25 deletions(-) diff --git a/Changelog.md b/Changelog.md index 98d9ecfc4..eb8dda8ba 100644 --- a/Changelog.md +++ b/Changelog.md @@ -1,5 +1,20 @@ # Changelog +## Unreleased - 09/11/2023 + +### API +- Change `coq.elpi.add-predicate` now locality can be charged +- Experimental `coq.toposort` returns a valid topological ordering of the nodes + of a graph +- Change `coq.TC.db-for`, now instances are returned sorted wrt their priority +- New `tc-priority`, contains the priority of an instance and if the priority + has been given by the user or computed by `coq` +- Change `tc-instance`, now the type is `gref -> tc-priority -> tc-instance` + +### Apps +- New `tc`app providing an implementation of a type class solver written in elpi. + This app is experimental + ## [1.19.3] - 12/10/2023 Requires Elpi 1.16.5 and Coq 8.18. diff --git a/apps/tc/elpi/create_tc_predicate.elpi b/apps/tc/elpi/create_tc_predicate.elpi index ec12a888b..66c8887c7 100644 --- a/apps/tc/elpi/create_tc_predicate.elpi +++ b/apps/tc/elpi/create_tc_predicate.elpi @@ -26,15 +26,21 @@ modes-of-class ClassGr Modes :- N is {coq.count-prods ClassTy} + 1, % + 1 for the solution list-init N (x\r\ r = (pr out "term")) Modes. +pred get-class-locality o:list prop. +get-class-locality [@local!] :- coq.env.current-section-path [_ | _], !. +get-class-locality [@global!]. + pred add-class-gr i:search-mode, i:gref. add-class-gr SearchMode ClassGR :- std.assert! (coq.TC.class? ClassGR) "Only gref of type classes can be added as new predicates", if (class ClassGR _ _) true (modes-of-class ClassGR Modes, gref->pred-name ClassGR PredName, - coq.elpi.add-predicate "tc.db" _ PredName Modes, - add-tc-db _ _ (tc-mode ClassGR Modes), - @global! => add-tc-db _ _ (class ClassGR PredName SearchMode)). + get-class-locality Locality, + Locality => ( + add-tc-db _ _ (tc-mode ClassGR Modes), + coq.elpi.add-predicate "tc.db" _ PredName Modes, + add-tc-db _ _ (class ClassGR PredName SearchMode))). pred add-class-str i:search-mode, i:string. add-class-str SearchMode ClassStr :- @@ -43,9 +49,9 @@ add-class-str SearchMode ClassStr :- % Following are predicates for TC.declare -pred attr->deterministic o:search-mode. -attr->deterministic deterministic :- get-option "deterministic" tt, !. -attr->deterministic classic. +pred attr->search-mode o:search-mode. +attr->search-mode deterministic :- get-option "deterministic" tt, !. +attr->search-mode classic. pred attr->modes o:list hint-mode. attr->modes CoqModes :- @@ -62,11 +68,12 @@ pred declare-class-in-coq i:gref. declare-class-in-coq ClassGR :- attr->modes CoqModes, if (CoqModes = []) true - (@global! => coq.hints.add-mode ClassGR "typeclass_instances" CoqModes), + (coq.hints.add-mode ClassGR "typeclass_instances" CoqModes), coq.TC.declare-class ClassGR, - attr->deterministic SearchMode, + attr->search-mode SearchMode, gref->pred-name ClassGR PredName, - @global! => add-tc-db _ (after "0") (class ClassGR PredName SearchMode). + get-class-locality Locality, + Locality => add-tc-db _ (after "0") (class ClassGR PredName SearchMode). pred declare-class i:indt-decl. declare-class D :- !, diff --git a/apps/tc/src/coq_elpi_tc_register.ml b/apps/tc/src/coq_elpi_tc_register.ml index 702d58a2f..6ec035370 100644 --- a/apps/tc/src/coq_elpi_tc_register.ml +++ b/apps/tc/src/coq_elpi_tc_register.ml @@ -51,7 +51,13 @@ let observer_instance ({locality; instance; info; class_name} : instance) : Coq_ let inObservation = Libobject.declare_object @@ - Libobject.local_object "TC_HACK_OBSERVER2" + Libobject.local_object "TC_HACK_OBSERVER_CLASSES" + ~cache:(fun (run,cl) -> run @@ observer_class cl) + ~discharge:(fun x -> Some x) + +let inObservation1 = + Libobject.declare_object @@ + Libobject.local_object "TC_HACK_OBSERVER_INSTANCE" ~cache:(fun (run,inst) -> run @@ observer_instance inst) ~discharge:(fun (_,inst as x) -> if inst.locality = Local then None else Some x) @@ -59,8 +65,8 @@ let observer_evt ((loc, name, atts) : loc_name_atts) (x : Event.t) = let open Coq_elpi_vernacular in let run_program e = run_program loc name ~atts e in match x with - | Event.NewClass cl -> run_program @@ observer_class cl - | Event.NewInstance inst -> Lib.add_leaf (inObservation (run_program,inst)) + | Event.NewClass cl -> Lib.add_leaf (inObservation (run_program,cl)) + | Event.NewInstance inst -> Lib.add_leaf (inObservation1 (run_program,inst)) module StringMap = Map.Make(String) diff --git a/apps/tc/tests/section_in_out.v b/apps/tc/tests/section_in_out.v index 45d11cff5..5b6fae08e 100644 --- a/apps/tc/tests/section_in_out.v +++ b/apps/tc/tests/section_in_out.v @@ -52,5 +52,12 @@ End A. Elpi len_test 4. - - +Section ClassPersistence. + Section S1. + Context (X : Type) (A : X). + Class class (A : X). + Definition x : class A. apply Build_class. Qed. + Elpi TC.AddInstances x. + Goal exists x, class x. eexists. apply _. Qed. + End S1. +End ClassPersistence. \ No newline at end of file diff --git a/coq-builtin.elpi b/coq-builtin.elpi index 9787d4f50..3e4ddc084 100644 --- a/coq-builtin.elpi +++ b/coq-builtin.elpi @@ -1739,10 +1739,13 @@ type in argument_mode. type out argument_mode. % [coq.elpi.add-predicate Db Indexing PredName Spec] Declares a new -% predicate PredName in the data base Db. Indexing can be left unspecified. -% Spec gathers a mode and a type for each argument. CAVEAT: types and -% indexing are strings instead of proper data types; beware parsing errors -% are fatal +% predicate PredName in the data base Db. +% Indexing can be left unspecified. Spec gathers a mode and a +% type for each argument. CAVEAT: types and indexing are strings +% instead of proper data types; beware parsing errors are fatal. +% Supported attributes: +% - @local! (default: false, discard at the end of section or module) +% - @global! (default: false, always active external pred coq.elpi.add-predicate i:string, i:string, i:string, i:list (pair argument_mode string). diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index d09bb7931..f1b173f92 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -604,7 +604,7 @@ let argument_mode = let open Conv in let open API.AlgebraicData in declare { let set_accumulate_text_to_db, get_accumulate_text_to_db = - let f = ref (fun _ _ -> assert false) in + let f = ref (fun _ _ _ -> assert false) in (fun x -> f := x), (fun () -> !f) @@ -4084,10 +4084,19 @@ Supported attributes: In(B.unspec B.string,"Indexing", In(B.string,"PredName", In(B.list (B.pair argument_mode B.string),"Spec", - Full(global,"Declares a new predicate PredName in the data base Db. Indexing can be left unspecified. Spec gathers a mode and a type for each argument. CAVEAT: types and indexing are strings instead of proper data types; beware parsing errors are fatal"))))), - (fun dbname indexing predname spec ~depth _ _ state -> + Full(global,{|Declares a new predicate PredName in the data base Db. +Indexing can be left unspecified. Spec gathers a mode and a +type for each argument. CAVEAT: types and indexing are strings +instead of proper data types; beware parsing errors are fatal. +Supported attributes: +- @local! (default: false, discard at the end of section or module) +- @global! (default: false, always active|}))))), + (fun dbname indexing predname spec ~depth ctx _ state -> let dbname = Coq_elpi_utils.string_split_on_char '.' dbname in let f = get_accumulate_text_to_db () in + let local = ctx.options.local = Some true in + let super_global = ctx.options.local = Some false in + if local && super_global then CErrors.user_err Pp.(str "coq.elpi.add-predicate: @global! incompatible with @local!"); let indexing = match indexing with | B.Given str -> ":index ("^str^") " @@ -4100,7 +4109,8 @@ Supported attributes: mode ^ "(" ^ ty ^ ")") in let spec = String.concat ", " spec in let text = indexing ^ "pred " ^ predname ^ " " ^ spec ^ "." in - f dbname text; + let scope = if local then Local else if super_global then SuperGlobal else Regular in + f dbname text scope; state, (), [] )), DocAbove); diff --git a/src/coq_elpi_builtins.mli b/src/coq_elpi_builtins.mli index eb717489c..055204608 100644 --- a/src/coq_elpi_builtins.mli +++ b/src/coq_elpi_builtins.mli @@ -13,7 +13,7 @@ val clauses_for_later : (qualified_name * Ast.program * Names.Id.t list * Coq_elpi_utils.clause_scope) list State.component val set_accumulate_to_db : (((qualified_name * Ast.program * Names.Id.t list * Coq_elpi_utils.clause_scope) list -> unit)) -> unit -val set_accumulate_text_to_db : ((string list -> string -> unit)) -> unit +val set_accumulate_text_to_db : ((string list -> string -> Coq_elpi_utils.clause_scope -> unit)) -> unit type attribute_data = | AttributeString of string diff --git a/src/coq_elpi_programs.ml b/src/coq_elpi_programs.ml index f2793efb4..022dc8c64 100644 --- a/src/coq_elpi_programs.ml +++ b/src/coq_elpi_programs.ml @@ -629,8 +629,8 @@ let () = Coq_elpi_builtins.set_accumulate_to_db (fun clauses_to_add -> clauses_to_add |> List.iter (fun (dbname,units,vs,scope) -> accumulate_to_db dbname units vs ~scope)) -let () = Coq_elpi_builtins.set_accumulate_text_to_db (fun n txt -> +let () = Coq_elpi_builtins.set_accumulate_text_to_db (fun n txt scope -> let elpi = ensure_initialized () in let loc = API.Ast.Loc.initial "(elpi.add_predicate)" in let u = unit_from_string ~elpi loc txt in - accumulate_to_db n [u] [] ~scope:Regular) + accumulate_to_db n [u] [] ~scope) From ea5dc16bc3609864857079d137fe8f4de7c7f666 Mon Sep 17 00:00:00 2001 From: qvermande Date: Wed, 8 Nov 2023 09:55:45 +0100 Subject: [PATCH 02/16] fix installation of tc --- _CoqProject | 2 +- apps/tc/Makefile.coq.local | 6 +++++- apps/tc/_CoqProject | 2 +- 3 files changed, 7 insertions(+), 3 deletions(-) diff --git a/_CoqProject b/_CoqProject index f6956fa6a..563bd9ebf 100644 --- a/_CoqProject +++ b/_CoqProject @@ -29,7 +29,7 @@ -I apps/coercion/src # Type classes --R apps/tc/theories elpi.apps +-R apps/tc/theories elpi.apps.tc -R apps/tc/tests elpi.apps.tc.tests -R apps/tc/elpi elpi.apps.tc -I apps/tc/src diff --git a/apps/tc/Makefile.coq.local b/apps/tc/Makefile.coq.local index f120308b2..0c6b3ef31 100644 --- a/apps/tc/Makefile.coq.local +++ b/apps/tc/Makefile.coq.local @@ -1,3 +1,7 @@ CAMLPKGS+= -package coq-elpi.elpi OCAMLPATH:=../../src/:$(OCAMLPATH) -export OCAMLPATH \ No newline at end of file +export OCAMLPATH + +install-extra:: + df="`$(COQMKFILE) -destination-of theories/tc.vo $(COQLIBS)`";\ + install -m 0644 $(wildcard elpi/*.elpi) "$(COQLIBINSTALL)/$$df" diff --git a/apps/tc/_CoqProject b/apps/tc/_CoqProject index 50e07f4cf..7898332a8 100644 --- a/apps/tc/_CoqProject +++ b/apps/tc/_CoqProject @@ -3,7 +3,7 @@ -I ../../src -docroot elpi.apps --R theories elpi.apps +-R theories elpi.apps.tc -R elpi elpi.apps.tc -R tests elpi.apps.tc.tests From 3e8aaa8129ab5dc04b3dcc8b3c481d2b310a6e6b Mon Sep 17 00:00:00 2001 From: qvermande Date: Wed, 8 Nov 2023 11:30:44 +0100 Subject: [PATCH 03/16] fix apps/tc/_CoqProject.test --- apps/tc/_CoqProject.test | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/apps/tc/_CoqProject.test b/apps/tc/_CoqProject.test index ed130c2f6..6d683f46f 100644 --- a/apps/tc/_CoqProject.test +++ b/apps/tc/_CoqProject.test @@ -5,7 +5,7 @@ -I ../../src -Q elpi elpi.apps.tc --R theories elpi.apps +-R theories elpi.apps.tc -R tests elpi.apps.tc.tests -I src @@ -50,4 +50,4 @@ tests/indt_to_inst.v tests/bigTest.v -examples/tutorial.v \ No newline at end of file +examples/tutorial.v From 470a9fb183bd23f177301130645f66dfbdd234f6 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 8 Nov 2023 13:42:02 +0100 Subject: [PATCH 04/16] fixup attribute parsing --- apps/tc/elpi/create_tc_predicate.elpi | 4 +++- apps/tc/tests/classes_declare.v | 13 +++++++++++++ 2 files changed, 16 insertions(+), 1 deletion(-) diff --git a/apps/tc/elpi/create_tc_predicate.elpi b/apps/tc/elpi/create_tc_predicate.elpi index 66c8887c7..6b85ed829 100644 --- a/apps/tc/elpi/create_tc_predicate.elpi +++ b/apps/tc/elpi/create_tc_predicate.elpi @@ -61,7 +61,9 @@ attr->modes CoqModes :- attr->modes []. pred get-key-from-option i:prop, o:string. -get-key-from-option (get-option A _) A :- !. +get-key-from-option (get-option A tt) A :- !. +get-key-from-option (get-option "i" ff) "o" :- !. +get-key-from-option (get-option "o" ff) "i" :- !. get-key-from-option A _ :- coq.error A "should be an option". pred declare-class-in-coq i:gref. diff --git a/apps/tc/tests/classes_declare.v b/apps/tc/tests/classes_declare.v index 56d10a5e2..db1f9f1b3 100644 --- a/apps/tc/tests/classes_declare.v +++ b/apps/tc/tests/classes_declare.v @@ -59,4 +59,17 @@ Section S3. End S3. +Section S31. + #[mode(o=ff)] TC.Declare Class class31 (n : nat). + Instance inst31 : class31 0. Proof. apply Build_class31. Qed. + + Goal exists x, class31 x. + Proof. + eexists. + Succeed apply inst31. + Fail apply _. + Abort. + +End S31. + From 337246c0c7348920db64a91f03e7ba56023e6b31 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 8 Nov 2023 13:46:37 +0100 Subject: [PATCH 05/16] syntax for coq modes that parses as a coq attribute --- apps/tc/elpi/create_tc_predicate.elpi | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/apps/tc/elpi/create_tc_predicate.elpi b/apps/tc/elpi/create_tc_predicate.elpi index 6b85ed829..794715c67 100644 --- a/apps/tc/elpi/create_tc_predicate.elpi +++ b/apps/tc/elpi/create_tc_predicate.elpi @@ -1,17 +1,16 @@ /* license: GNU Lesser General Public License Version 2.1 or later */ /* ------------------------------------------------------------------------- */ pred string->coq-mode i:string, o:hint-mode. -string->coq-mode "!" mode-ground :- !. -string->coq-mode "+" mode-input :- !. -string->coq-mode "-" mode-output :- !. - -string->coq-mode "i" mode-ground :- !. +string->coq-mode "bang" mode-ground :- !. +string->coq-mode "plus" mode-input :- !. +string->coq-mode "minus" mode-output :- !. +string->coq-mode "i" mode-input :- !. string->coq-mode "o" mode-output :- !. string->coq-mode A _ :- coq.error A "is not a valid mode". pred coq-mode->elpi i:hint-mode, o:pair argument_mode string. :name "coq-mode->elpi" -coq-mode->elpi mode-ground (pr in "term"). +coq-mode->elpi mode-ground (pr in "term"). % approximation coq-mode->elpi mode-input (pr in "term"). coq-mode->elpi mode-output (pr out "term"). From b89ffa1d2e3a13690a60dcbf53e02ea85f97a3c6 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 8 Nov 2023 13:59:30 +0100 Subject: [PATCH 06/16] only one class predicate per class --- apps/tc/elpi/create_tc_predicate.elpi | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/apps/tc/elpi/create_tc_predicate.elpi b/apps/tc/elpi/create_tc_predicate.elpi index 794715c67..77ef64d7f 100644 --- a/apps/tc/elpi/create_tc_predicate.elpi +++ b/apps/tc/elpi/create_tc_predicate.elpi @@ -70,11 +70,14 @@ declare-class-in-coq ClassGR :- attr->modes CoqModes, if (CoqModes = []) true (coq.hints.add-mode ClassGR "typeclass_instances" CoqModes), + % CAVEAT: this triggers the observer coq.TC.declare-class ClassGR, attr->search-mode SearchMode, gref->pred-name ClassGR PredName, + % HACK: we override the clauses added by the observer, since it does not know + % the SearchMode. get-class-locality Locality, - Locality => add-tc-db _ (after "0") (class ClassGR PredName SearchMode). + Locality => add-tc-db _ (after "0") (class ClassGR PredName SearchMode :- !). pred declare-class i:indt-decl. declare-class D :- !, From 801b3305a6f2558b1e1f4dbe11bf96480613dc6e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 9 Nov 2023 11:48:09 +0100 Subject: [PATCH 07/16] Apply suggestions from code review --- Changelog.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Changelog.md b/Changelog.md index eb8dda8ba..00d7a5b15 100644 --- a/Changelog.md +++ b/Changelog.md @@ -3,16 +3,16 @@ ## Unreleased - 09/11/2023 ### API -- Change `coq.elpi.add-predicate` now locality can be charged +- Change `coq.elpi.add-predicate` now locality can be changed - Experimental `coq.toposort` returns a valid topological ordering of the nodes of a graph - Change `coq.TC.db-for`, now instances are returned sorted wrt their priority - New `tc-priority`, contains the priority of an instance and if the priority has been given by the user or computed by `coq` -- Change `tc-instance`, now the type is `gref -> tc-priority -> tc-instance` +- Change `tc-instance`, now the type is `gref -> tc-priority -> tc-instance` i.e. the priority is not an integer anymore ### Apps -- New `tc`app providing an implementation of a type class solver written in elpi. +- New `tc` app providing an implementation of a type class solver written in elpi. This app is experimental ## [1.19.3] - 12/10/2023 From b2ff63846ff3d4202b47149c9b3201718e034e9e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 8 Nov 2023 13:59:30 +0100 Subject: [PATCH 08/16] only one class predicate per class --- apps/tc/elpi/create_tc_predicate.elpi | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/apps/tc/elpi/create_tc_predicate.elpi b/apps/tc/elpi/create_tc_predicate.elpi index 77ef64d7f..eb5b092ea 100644 --- a/apps/tc/elpi/create_tc_predicate.elpi +++ b/apps/tc/elpi/create_tc_predicate.elpi @@ -69,7 +69,7 @@ pred declare-class-in-coq i:gref. declare-class-in-coq ClassGR :- attr->modes CoqModes, if (CoqModes = []) true - (coq.hints.add-mode ClassGR "typeclass_instances" CoqModes), + (@global! => coq.hints.add-mode ClassGR "typeclass_instances" CoqModes), % CAVEAT: this triggers the observer coq.TC.declare-class ClassGR, attr->search-mode SearchMode, From 1b276fe9a96e7293f4906d2df2bafd9eb18afe9a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Oct 2023 10:38:07 +0200 Subject: [PATCH 09/16] ci: re-enable nix --- .github/workflows/nix-action-coq-8.18.yml | 1213 +++++++++++++++++++++ .nix/config.nix | 5 +- 2 files changed, 1215 insertions(+), 3 deletions(-) create mode 100644 .github/workflows/nix-action-coq-8.18.yml diff --git a/.github/workflows/nix-action-coq-8.18.yml b/.github/workflows/nix-action-coq-8.18.yml new file mode 100644 index 000000000..7d08d1256 --- /dev/null +++ b/.github/workflows/nix-action-coq-8.18.yml @@ -0,0 +1,1213 @@ +jobs: + addition-chains: + needs: + - mathcomp-ssreflect + - mathcomp-algebra + - mathcomp-fingroup + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target addition-chains + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.18\" --argstr job \"addition-chains\" \\\n --dry-run 2>&1\ + \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-algebra" + - 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 "coq-8.18" + --argstr job "mathcomp-fingroup" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: paramcoq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "paramcoq" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "addition-chains" + category-theory: + needs: + - mathcomp-ssreflect + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target category-theory + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.18\" --argstr job \"category-theory\" \\\n --dry-run 2>&1\ + \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: equations' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "equations" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "category-theory" + coq-elpi: + needs: [] + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target coq-elpi + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.18\" --argstr job \"coq-elpi\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coq-elpi" + coquelicot: + needs: + - mathcomp-ssreflect + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target coquelicot + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.18\" --argstr job \"coquelicot\" \\\n --dry-run 2>&1 >\ + \ /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coquelicot" + hierarchy-builder: + needs: + - coq-elpi + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target hierarchy-builder + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.18\" --argstr job \"hierarchy-builder\" \\\n --dry-run\ + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --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 "coq-8.18" + --argstr job "coq-elpi" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "hierarchy-builder" + interval: + needs: + - coquelicot + - mathcomp-ssreflect + - mathcomp-fingroup + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target interval + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.18\" --argstr job \"interval\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: bignums' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "bignums" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coquelicot' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coquelicot" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: flocq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "flocq" + - 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 "coq-8.18" + --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 "coq-8.18" + --argstr job "mathcomp-fingroup" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "interval" + mathcomp: + needs: + - mathcomp-ssreflect + - mathcomp-fingroup + - mathcomp-algebra + - mathcomp-solvable + - mathcomp-field + - mathcomp-character + - hierarchy-builder + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - 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 \"coq-8.18\" --argstr job \"mathcomp\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --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 "coq-8.18" + --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 "coq-8.18" + --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 "coq-8.18" + --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 "coq-8.18" + --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 "coq-8.18" + --argstr job "mathcomp-character" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "hierarchy-builder" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp" + mathcomp-algebra: + needs: + - mathcomp-ssreflect + - mathcomp-fingroup + - hierarchy-builder + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target mathcomp-algebra + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.18\" --argstr job \"mathcomp-algebra\" \\\n --dry-run 2>&1\ + \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --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 "coq-8.18" + --argstr job "mathcomp-fingroup" + - 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 "coq-8.18" + --argstr job "hierarchy-builder" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-algebra" + mathcomp-analysis: + needs: + - mathcomp-classical + - mathcomp-field + - mathcomp-bigenough + - hierarchy-builder + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target mathcomp-analysis + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.18\" --argstr job \"mathcomp-analysis\" \\\n --dry-run\ + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-classical' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-classical" + - 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 "coq-8.18" + --argstr job "mathcomp-field" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-bigenough' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-bigenough" + - 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 "coq-8.18" + --argstr job "hierarchy-builder" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-analysis" + mathcomp-bigenough: + needs: + - mathcomp-ssreflect + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target mathcomp-bigenough + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.18\" --argstr job \"mathcomp-bigenough\" \\\n --dry-run\ + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-bigenough" + mathcomp-character: + needs: + - mathcomp-ssreflect + - mathcomp-fingroup + - mathcomp-algebra + - mathcomp-solvable + - mathcomp-field + - hierarchy-builder + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target mathcomp-character + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.18\" --argstr job \"mathcomp-character\" \\\n --dry-run\ + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --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 "coq-8.18" + --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 "coq-8.18" + --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 "coq-8.18" + --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 "coq-8.18" + --argstr job "mathcomp-field" + - 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 "coq-8.18" + --argstr job "hierarchy-builder" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-character" + mathcomp-classical: + needs: + - mathcomp-algebra + - hierarchy-builder + - hierarchy-builder + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target mathcomp-classical + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.18\" --argstr job \"mathcomp-classical\" \\\n --dry-run\ + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coq" + - 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 "coq-8.18" + --argstr job "mathcomp-algebra" + - 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 "coq-8.18" + --argstr job "hierarchy-builder" + - 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 "coq-8.18" + --argstr job "hierarchy-builder" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-classical" + mathcomp-field: + needs: + - mathcomp-ssreflect + - mathcomp-fingroup + - mathcomp-algebra + - mathcomp-solvable + - hierarchy-builder + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target mathcomp-field + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.18\" --argstr job \"mathcomp-field\" \\\n --dry-run 2>&1\ + \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --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 "coq-8.18" + --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 "coq-8.18" + --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 "coq-8.18" + --argstr job "mathcomp-solvable" + - 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 "coq-8.18" + --argstr job "hierarchy-builder" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-field" + mathcomp-fingroup: + needs: + - mathcomp-ssreflect + - hierarchy-builder + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target mathcomp-fingroup + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.18\" --argstr job \"mathcomp-fingroup\" \\\n --dry-run\ + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-ssreflect" + - 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 "coq-8.18" + --argstr job "hierarchy-builder" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-fingroup" + mathcomp-solvable: + needs: + - mathcomp-ssreflect + - mathcomp-fingroup + - mathcomp-algebra + - hierarchy-builder + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target mathcomp-solvable + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.18\" --argstr job \"mathcomp-solvable\" \\\n --dry-run\ + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --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 "coq-8.18" + --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 "coq-8.18" + --argstr job "mathcomp-algebra" + - 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 "coq-8.18" + --argstr job "hierarchy-builder" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-solvable" + mathcomp-ssreflect: + needs: + - hierarchy-builder + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target mathcomp-ssreflect + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.18\" --argstr job \"mathcomp-ssreflect\" \\\n --dry-run\ + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coq" + - 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 "coq-8.18" + --argstr job "hierarchy-builder" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-ssreflect" + odd-order: + needs: + - mathcomp-character + - mathcomp-ssreflect + - mathcomp-fingroup + - mathcomp-algebra + - mathcomp-solvable + - mathcomp-field + - 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@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - 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 \"coq-8.18\" --argstr job \"odd-order\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --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 "coq-8.18" + --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 "coq-8.18" + --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 "coq-8.18" + --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 "coq-8.18" + --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 "coq-8.18" + --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 "coq-8.18" + --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 "coq-8.18" + --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 "coq-8.18" + --argstr job "odd-order" + trakt: + needs: + - coq-elpi + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target trakt + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.18\" --argstr job \"trakt\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --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 "coq-8.18" + --argstr job "coq-elpi" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "trakt" +name: Nix CI for bundle coq-8.18 +'on': + pull_request: + paths: + - .github/workflows/** + pull_request_target: + types: + - opened + - synchronize + - reopened + push: + branches: + - master diff --git a/.nix/config.nix b/.nix/config.nix index ead6869ee..d39bea2e4 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -1,11 +1,10 @@ { format = "1.0.0"; attribute = "coq-elpi"; - default-bundle = "coq-8.17"; + default-bundle = "coq-8.18"; bundles = { - "coq-8.17".coqPackages = { - coq.override.version = "8.17"; + "coq-8.18".coqPackages = { hierarchy-builder.override.version = "master"; hierarchy-builder-shim.job = false; From 873530b59ccb388891afc13866a7ea3a8cc76868 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Fri, 13 Oct 2023 14:57:30 +0200 Subject: [PATCH 10/16] update toolbox --- .nix/coq-nix-toolbox.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index ff29c1895..de2cac5a4 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"e2a21e50cd134b50c7e590b66ad14ec4905e16cd" +"95c6764e932cd20d037ad13fead23f2540f0ac7c" From 07073a290fb4fb7f7518dc1539b9cead2ab0d2fa Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Fri, 13 Oct 2023 14:59:14 +0200 Subject: [PATCH 11/16] regen action --- .github/workflows/nix-action-coq-8.18.yml | 255 +++++++++++++++------- 1 file changed, 174 insertions(+), 81 deletions(-) diff --git a/.github/workflows/nix-action-coq-8.18.yml b/.github/workflows/nix-action-coq-8.18.yml index 7d08d1256..2fbc8f05c 100644 --- a/.github/workflows/nix-action-coq-8.18.yml +++ b/.github/workflows/nix-action-coq-8.18.yml @@ -1,4 +1,68 @@ jobs: + Verdi: + needs: + - mathcomp-ssreflect + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target Verdi + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.18\" --argstr job \"Verdi\" \\\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 "coq-8.18" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: Cheerios' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "Cheerios" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: InfSeqExt' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "InfSeqExt" + - 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 "coq-8.18" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "Verdi" addition-chains: needs: - mathcomp-ssreflect @@ -43,8 +107,8 @@ jobs: name: Checking presence of CI target addition-chains run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coq-8.18\" --argstr job \"addition-chains\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ - \ | grep \"built:\" | sed \"s/.*/built/\")\n" + \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ + built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" @@ -69,7 +133,7 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" --argstr job "addition-chains" - category-theory: + autosubst: needs: - mathcomp-ssreflect runs-on: ubuntu-latest @@ -108,11 +172,11 @@ jobs: extraPullNames: coq, coq-community, math-comp name: coq-elpi - id: stepCheck - name: Checking presence of CI target category-theory + name: Checking presence of CI target autosubst run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.18\" --argstr job \"category-theory\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ - \ | grep \"built:\" | sed \"s/.*/built/\")\n" + \ bundle \"coq-8.18\" --argstr job \"autosubst\" \\\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 "coq-8.18" @@ -121,14 +185,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-ssreflect' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: equations' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" - --argstr job "equations" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" - --argstr job "category-theory" + --argstr job "autosubst" coq-elpi: needs: [] runs-on: ubuntu-latest @@ -170,8 +230,8 @@ jobs: name: Checking presence of CI target coq-elpi run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coq-8.18\" --argstr job \"coq-elpi\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" + 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 "coq-8.18" @@ -222,8 +282,8 @@ jobs: name: Checking presence of CI target coquelicot run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coq-8.18\" --argstr job \"coquelicot\" \\\n --dry-run 2>&1 >\ - \ /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ - \ | grep \"built:\" | sed \"s/.*/built/\")\n" + \ /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\"\ + \ | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" @@ -236,9 +296,9 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" --argstr job "coquelicot" - hierarchy-builder: + deriving: needs: - - coq-elpi + - mathcomp-ssreflect runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -275,28 +335,26 @@ jobs: extraPullNames: coq, coq-community, math-comp name: coq-elpi - id: stepCheck - name: Checking presence of CI target hierarchy-builder + name: Checking presence of CI target deriving run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.18\" --argstr job \"hierarchy-builder\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + \ bundle \"coq-8.18\" --argstr job \"deriving\" \\\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 "coq-8.18" --argstr job "coq" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq-elpi' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" - --argstr job "coq-elpi" + --argstr job "mathcomp-ssreflect" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" - --argstr job "hierarchy-builder" - interval: + --argstr job "deriving" + hierarchy-builder: needs: - - coquelicot - - mathcomp-ssreflect - - mathcomp-fingroup + - coq-elpi runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -333,39 +391,23 @@ jobs: extraPullNames: coq, coq-community, math-comp name: coq-elpi - id: stepCheck - name: Checking presence of CI target interval + name: Checking presence of CI target hierarchy-builder run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.18\" --argstr job \"interval\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" + \ bundle \"coq-8.18\" --argstr job \"hierarchy-builder\" \\\n --dry-run\ + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" --argstr job "coq" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: bignums' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" - --argstr job "bignums" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coquelicot' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" - --argstr job "coquelicot" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: flocq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" - --argstr job "flocq" - - 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 "coq-8.18" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-fingroup' + name: 'Building/fetching previous CI target: coq-elpi' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" - --argstr job "mathcomp-fingroup" + --argstr job "coq-elpi" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" - --argstr job "interval" + --argstr job "hierarchy-builder" mathcomp: needs: - mathcomp-ssreflect @@ -414,8 +456,8 @@ jobs: name: Checking presence of CI target mathcomp run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coq-8.18\" --argstr job \"mathcomp\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" + 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 "coq-8.18" @@ -496,8 +538,8 @@ jobs: name: Checking presence of CI target mathcomp-algebra run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coq-8.18\" --argstr job \"mathcomp-algebra\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ - \ | grep \"built:\" | sed \"s/.*/built/\")\n" + \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ + built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" @@ -563,8 +605,8 @@ jobs: name: Checking presence of CI target mathcomp-analysis run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coq-8.18\" --argstr job \"mathcomp-analysis\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" @@ -631,8 +673,8 @@ jobs: name: Checking presence of CI target mathcomp-bigenough run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coq-8.18\" --argstr job \"mathcomp-bigenough\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" @@ -692,8 +734,8 @@ jobs: name: Checking presence of CI target mathcomp-character run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coq-8.18\" --argstr job \"mathcomp-character\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" @@ -730,7 +772,6 @@ jobs: needs: - mathcomp-algebra - hierarchy-builder - - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -770,8 +811,8 @@ jobs: name: Checking presence of CI target mathcomp-classical run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coq-8.18\" --argstr job \"mathcomp-classical\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" @@ -784,10 +825,6 @@ jobs: name: 'Building/fetching previous CI target: hierarchy-builder' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" --argstr job "hierarchy-builder" - - 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 "coq-8.18" - --argstr job "hierarchy-builder" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" @@ -838,8 +875,8 @@ jobs: name: Checking presence of CI target mathcomp-field run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coq-8.18\" --argstr job \"mathcomp-field\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ - \ | grep \"built:\" | sed \"s/.*/built/\")\n" + \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ + built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" @@ -911,8 +948,8 @@ jobs: name: Checking presence of CI target mathcomp-fingroup run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coq-8.18\" --argstr job \"mathcomp-fingroup\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" @@ -974,8 +1011,8 @@ jobs: name: Checking presence of CI target mathcomp-solvable run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coq-8.18\" --argstr job \"mathcomp-solvable\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" @@ -1042,8 +1079,8 @@ jobs: name: Checking presence of CI target mathcomp-ssreflect run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coq-8.18\" --argstr job \"mathcomp-ssreflect\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" @@ -1104,8 +1141,8 @@ jobs: name: Checking presence of CI target odd-order run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coq-8.18\" --argstr job \"odd-order\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" + 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 "coq-8.18" @@ -1142,6 +1179,62 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" --argstr job "odd-order" + reglang: + needs: + - mathcomp-ssreflect + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target reglang + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.18\" --argstr job \"reglang\" \\\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 "coq-8.18" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "reglang" trakt: needs: - coq-elpi @@ -1184,8 +1277,8 @@ jobs: name: Checking presence of CI target trakt run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coq-8.18\" --argstr job \"trakt\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" + 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 "coq-8.18" From 82506fba577c4c22b65b78bf6751fbd21e76c405 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 16 Oct 2023 11:02:20 +0200 Subject: [PATCH 12/16] Update coq-nix-toolbox.nix --- .nix/coq-nix-toolbox.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index de2cac5a4..8fb619add 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"95c6764e932cd20d037ad13fead23f2540f0ac7c" +"cef6668e637efb2941cbda0ac0f0a435730fa3c1" From b62e61afb99a8bd36056e07bb8b21f6cc3ab326f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 16 Oct 2023 11:03:36 +0200 Subject: [PATCH 13/16] Create overlay MC-classical --- .nix/ coq-overlays/mathcomp-classical /default.nix | 2 ++ 1 file changed, 2 insertions(+) create mode 100644 .nix/ coq-overlays/mathcomp-classical /default.nix diff --git a/.nix/ coq-overlays/mathcomp-classical /default.nix b/.nix/ coq-overlays/mathcomp-classical /default.nix new file mode 100644 index 000000000..193265f29 --- /dev/null +++ b/.nix/ coq-overlays/mathcomp-classical /default.nix @@ -0,0 +1,2 @@ +{ mathcomp-analysis, version ? null }: +mathcomp-analysis.classical.override {inherit version;} From a67c6ba00d3ca5f7af2425fc5d9be4a34c6d0ff5 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 16 Oct 2023 13:42:38 +0200 Subject: [PATCH 14/16] Update .nix/config.nix --- .nix/config.nix | 1 + 1 file changed, 1 insertion(+) diff --git a/.nix/config.nix b/.nix/config.nix index d39bea2e4..86a920d7e 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -6,6 +6,7 @@ "coq-8.18".coqPackages = { hierarchy-builder.override.version = "master"; + coq.override.version = "8.18"; hierarchy-builder-shim.job = false; mathcomp.override.version = "master"; From cddb738c8f5d2094b8527d71bffc3ae84a19753f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 2 Nov 2023 12:57:18 +0100 Subject: [PATCH 15/16] fix nix --- .github/workflows/nix-action-coq-8.18.yml | 131 +++++++++++++++++++++- .nix/config.nix | 3 + .nix/coq-nix-toolbox.nix | 2 +- 3 files changed, 134 insertions(+), 2 deletions(-) diff --git a/.github/workflows/nix-action-coq-8.18.yml b/.github/workflows/nix-action-coq-8.18.yml index 2fbc8f05c..1a528864d 100644 --- a/.github/workflows/nix-action-coq-8.18.yml +++ b/.github/workflows/nix-action-coq-8.18.yml @@ -1,6 +1,7 @@ jobs: Verdi: needs: + - coq - mathcomp-ssreflect runs-on: ubuntu-latest steps: @@ -65,6 +66,7 @@ jobs: --argstr job "Verdi" addition-chains: needs: + - coq - mathcomp-ssreflect - mathcomp-algebra - mathcomp-fingroup @@ -135,6 +137,7 @@ jobs: --argstr job "addition-chains" autosubst: needs: + - coq - mathcomp-ssreflect runs-on: ubuntu-latest steps: @@ -189,10 +192,58 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" --argstr job "autosubst" - coq-elpi: + coq: needs: [] runs-on: ubuntu-latest steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - 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 \"coq-8.18\" --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 "coq-8.18" + --argstr job "coq" + coq-elpi: + needs: + - coq + runs-on: ubuntu-latest + steps: - name: Determine which commit to initially checkout run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ @@ -242,6 +293,7 @@ jobs: --argstr job "coq-elpi" coquelicot: needs: + - coq - mathcomp-ssreflect runs-on: ubuntu-latest steps: @@ -298,6 +350,7 @@ jobs: --argstr job "coquelicot" deriving: needs: + - coq - mathcomp-ssreflect runs-on: ubuntu-latest steps: @@ -354,6 +407,7 @@ jobs: --argstr job "deriving" hierarchy-builder: needs: + - coq - coq-elpi runs-on: ubuntu-latest steps: @@ -410,6 +464,7 @@ jobs: --argstr job "hierarchy-builder" mathcomp: needs: + - coq - mathcomp-ssreflect - mathcomp-fingroup - mathcomp-algebra @@ -496,6 +551,7 @@ jobs: --argstr job "mathcomp" mathcomp-algebra: needs: + - coq - mathcomp-ssreflect - mathcomp-fingroup - hierarchy-builder @@ -562,6 +618,7 @@ jobs: --argstr job "mathcomp-algebra" mathcomp-analysis: needs: + - coq - mathcomp-classical - mathcomp-field - mathcomp-bigenough @@ -633,6 +690,7 @@ jobs: --argstr job "mathcomp-analysis" mathcomp-bigenough: needs: + - coq - mathcomp-ssreflect runs-on: ubuntu-latest steps: @@ -689,6 +747,7 @@ jobs: --argstr job "mathcomp-bigenough" mathcomp-character: needs: + - coq - mathcomp-ssreflect - mathcomp-fingroup - mathcomp-algebra @@ -770,7 +829,9 @@ jobs: --argstr job "mathcomp-character" mathcomp-classical: needs: + - coq - mathcomp-algebra + - mathcomp-finmap - hierarchy-builder runs-on: ubuntu-latest steps: @@ -821,6 +882,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-algebra' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" --argstr job "mathcomp-algebra" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-finmap' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-finmap" - 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 "coq-8.18" @@ -831,6 +896,7 @@ jobs: --argstr job "mathcomp-classical" mathcomp-field: needs: + - coq - mathcomp-ssreflect - mathcomp-fingroup - mathcomp-algebra @@ -907,6 +973,7 @@ jobs: --argstr job "mathcomp-field" mathcomp-fingroup: needs: + - coq - mathcomp-ssreflect - hierarchy-builder runs-on: ubuntu-latest @@ -966,8 +1033,66 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" --argstr job "mathcomp-fingroup" + mathcomp-finmap: + needs: + - coq + - mathcomp-ssreflect + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target mathcomp-finmap + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.18\" --argstr job \"mathcomp-finmap\" \\\n --dry-run 2>&1\ + \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ + built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-finmap" mathcomp-solvable: needs: + - coq - mathcomp-ssreflect - mathcomp-fingroup - mathcomp-algebra @@ -1039,6 +1164,7 @@ jobs: --argstr job "mathcomp-solvable" mathcomp-ssreflect: needs: + - coq - hierarchy-builder runs-on: ubuntu-latest steps: @@ -1095,6 +1221,7 @@ jobs: --argstr job "mathcomp-ssreflect" odd-order: needs: + - coq - mathcomp-character - mathcomp-ssreflect - mathcomp-fingroup @@ -1181,6 +1308,7 @@ jobs: --argstr job "odd-order" reglang: needs: + - coq - mathcomp-ssreflect runs-on: ubuntu-latest steps: @@ -1237,6 +1365,7 @@ jobs: --argstr job "reglang" trakt: needs: + - coq - coq-elpi runs-on: ubuntu-latest steps: diff --git a/.nix/config.nix b/.nix/config.nix index 86a920d7e..b9488e1f0 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -18,6 +18,9 @@ mathcomp-analysis.override.version = "hierarchy-builder"; mathcomp-analysis.job = true; + mathcomp-finmap.override.version = "2.0.0"; + mathcomp-finmap.job = true; + mathcomp-classical.override.version = "hierarchy-builder"; mathcomp-classical.job = true; diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index 8fb619add..5b6bf1f08 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"cef6668e637efb2941cbda0ac0f0a435730fa3c1" +"e7a39f47847edcde691d7bf8f423e4806a1b660f" From 2812b724e7ac04a5346344be3976e9a5a482079e Mon Sep 17 00:00:00 2001 From: Davide Fissore Date: Thu, 9 Nov 2023 10:55:40 +0100 Subject: [PATCH 16/16] Locality can be charged to coq.elpi.add-predicate --- apps/tc/elpi/create_tc_predicate.elpi | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/apps/tc/elpi/create_tc_predicate.elpi b/apps/tc/elpi/create_tc_predicate.elpi index eb5b092ea..77ef64d7f 100644 --- a/apps/tc/elpi/create_tc_predicate.elpi +++ b/apps/tc/elpi/create_tc_predicate.elpi @@ -69,7 +69,7 @@ pred declare-class-in-coq i:gref. declare-class-in-coq ClassGR :- attr->modes CoqModes, if (CoqModes = []) true - (@global! => coq.hints.add-mode ClassGR "typeclass_instances" CoqModes), + (coq.hints.add-mode ClassGR "typeclass_instances" CoqModes), % CAVEAT: this triggers the observer coq.TC.declare-class ClassGR, attr->search-mode SearchMode,