add algebra-tactics to ci

.github/workflows/users.yml

@@ -34,6 +34,7 @@ jobs:
         - run: opam pin --ignore-constraints-on elpi add coq-elpi https://github.com/LPCIC/coq-elpi.git#fix-elpi-3.0
         - run: opam pin --ignore-constraints-on elpi add rocq-stdlib https://github.com/rocq-prover/stdlib.git#master
         - run: opam pin --ignore-constraints-on elpi add rocq-hierarchy-builder https://github.com/gares/hierarchy-builder.git#elpi-3.0
+        - run: opam pin --ignore-constraints-on elpi add rocq-hierarchy-builder https://github.com/math-comp/algebra-tactics.git#master
         - run: opam pin --ignore-constraints-on elpi add rocq-mathcomp-boot https://github.com/math-comp/math-comp.git#master
         - run: opam pin --ignore-constraints-on elpi add rocq-mathcomp-order https://github.com/math-comp/math-comp.git#master
         - run: opam pin --ignore-constraints-on elpi add rocq-mathcomp-fingroup https://github.com/math-comp/math-comp.git#master

.nix/config.nix

@@ -0,0 +1,115 @@
+{
+  ## DO NOT CHANGE THIS
+  format = "1.0.0";
+  ## unless you made an automated or manual update
+  ## to another supported format.
+
+  ## The attribute to build from the local sources,
+  ## either using nixpkgs data or the overlays located in `.nix/rocq-overlaygis`
+  ## and `.nix/coq-overlays`
+  ## Will determine the default main-job of the bundles defined below
+  attribute = "coq-elpi";
+
+  ## The attribute for coq compat shim, default to attribute
+  ## set this when you need both to differ
+  ## (for instance "rocq-elpi" and "coq-elpi")
+  # coq-attribute = "elpi";
+
+  ## If you want to select a different attribute (to build from the local sources as well)
+  ## when calling `nix-shell` and `nix-build` without the `--argstr job` argument
+  # shell-attribute = "{{nix_name}}";
+
+  ## Maybe the shortname of the library is different from
+  ## the name of the nixpkgs attribute, if so, set it here:
+  # pname = "{{shortname}}";
+
+  ## Lists the dependencies, phrased in terms of nix attributes.
+  ## No need to list Coq, it is already included.
+  ## These dependencies will systematically be added to the currently
+  ## known dependencies, if any more than Coq.
+  ## /!\ Remove this field as soon as the package is available on nixpkgs.
+  ## /!\ Manual overlays in `.nix/rocq-overlays` or `.nix/coq-overlays`
+  ##     should be preferred then.
+  # buildInputs = [ ];
+
+  ## Indicate the relative location of your _CoqProject
+  ## If not specified, it defaults to "_CoqProject"
+  # coqproject = "_CoqProject";
+
+  ## select an entry to build in the following `bundles` set
+  ## defaults to "default"
+  default-bundle = "default";
+
+  ## write one `bundles.name` attribute set per
+  ## alternative configuration
+  ## When generating GitHub Action CI, one workflow file
+  ## will be created per bundle
+  bundles.default = {
+    ## You can override Rocq and other Rocq rocqPackages
+    ## through the following attribute
+    # rocqPackages.rocq-core.override.version = "9.0";
+
+    ## You can override Coq and other Coq coqPackages
+    ## through the following attribute
+    # coqPackages.coq.override.version = "8.11";
+
+    ## In some cases, light overrides are not available/enough
+    ## in which case you can use either
+    # rocqPackages.<rocq-pkg>.overrideAttrs = o: <overrides>;
+    # coqPackages.<coq-pkg>.overrideAttrs = o: <overrides>;
+    ## or a "long" overlay to put in `.nix/rocq-overlays` or `.nix/coq-overlays`
+    ## you may use `nix-shell --run fetchOverlay <coq-pkg>`
+    ## to automatically retrieve the one from nixpkgs
+    ## if it exists and is correctly named/located
+
+    ## You can override Coq and other coqPackages
+    ## through the following attribute
+    ## If <ocaml-pkg> does not support light overrides,
+    ## you may use `overrideAttrs` or long overlays
+    ## located in `.nix/ocaml-overlays`
+    ## (there is no automation for this one)
+    ocamlPackages.elpi.override.version = "#mcat-ci";
+
+    ## You can also override packages from the nixpkgs toplevel
+    # <nix-pkg>.override.overrideAttrs = o: <overrides>;
+    ## Or put an overlay in `.nix/overlays`
+
+    ## you may mark a package as a main CI job (one to take deps and
+    ## rev deps from) as follows
+    # coqPackages.<main-pkg>.main-job = true;
+    ## by default the current package and its shell attributes are main jobs
+
+    ## you may mark a package as a CI job as follows
+    #  rocqPackages.<another-pkg>.job = "test";
+    #  coqPackages.<another-pkg>.job = "test";
+    ## It can then built through
+    ## nix-build --argstr bundle "default" --arg job "test";
+    ## in the absence of such a directive, the job "another-pkg" will
+    ## is still available, but will be automatically included in the CI
+    ## via the command genNixActions only if it is a dependency or a
+    ## reverse dependency of a job flagged as "main-job" (see above).
+
+    ## Run on push on following branches (default [ "master" ])
+    # push-branches = [ "master" "branch2" ];
+  };
+
+  ## Cachix caches to use in CI
+  ## Below we list some standard ones
+  cachix.coq = {};
+  cachix.math-comp = {};
+  cachix.coq-community = {};
+
+  ## If you have write access to one of these caches you can
+  ## provide the auth token or signing key through a secret
+  ## variable on GitHub. Then, you should give the variable
+  ## name here. For instance, coq-community projects can use
+  ## the following line instead of the one above:
+  # cachix.coq-community.authToken = "CACHIX_AUTH_TOKEN";
+
+  ## Or if you have a signing key for a given Cachix cache:
+  # cachix.my-cache.signingKey = "CACHIX_SIGNING_KEY"
+
+  ## Note that here, CACHIX_AUTH_TOKEN and CACHIX_SIGNING_KEY
+  ## are the names of secret variables. They are set in
+  ## GitHub's web interface.
+}

.nix/coq-nix-toolbox.nix

@@ -0,0 +1 @@
+"61a1c4da3df5ff208a9d735e64e4039c5066b31c"

Makefile

@@ -25,6 +25,10 @@ help:
 	@echo '  menhir-complete-errormsgs run when updating the grammar'
 	@echo '  menhir-strip-errormsgs remove comments from error message file'
 	@echo
+	@echo 'CI maintenance targets:'
+	@echo
+	@echo '  nix'
+	@echo
 
 INSTALL=_build/install/default
 BUILD=_build/default
@@ -141,3 +145,7 @@ menhir-strip-errormsgs:
 	sed -e "/^##/d" -i.bak src/parser/error_messages.txt
 
 .PHONY: tests help install build clean gh-pages
+
+nix:
+	nix-shell --arg do-nothing true --run "updateNixToolBox && genNixActions"
+.PHONY: nix

default.nix

@@ -0,0 +1,12 @@
+{ config ? {}, withEmacs ? false, print-env ? false, do-nothing ? false,
+  update-nixpkgs ? false, ci-matrix ? false,
+  override ? {}, coq-override ? {}, ocaml-override ? {}, global-override ? {},
+  bundle ? null, job ? null, inNixShell ? null, src ? ./.,
+}@args:
+let auto = fetchGit {
+  url = "https://github.com/coq-community/coq-nix-toolbox.git";
+  ref = "master";
+  rev = import .nix/coq-nix-toolbox.nix;
+};
+in
+import auto ({inherit src;} // args)