Lightweight Nix toolbox CI.

.travis.yml.mustache

@@ -49,13 +49,20 @@ language: shell
 {{# nix }}
 .nix: &NIX
   language: nix
+  nix: 2.3.7
   install:
   # for cachix we need travis to be a trusted nix user
   - echo "trusted-users = $USER" | sudo tee -a /etc/nix/nix.conf
   - sudo systemctl restart nix-daemon
-  script:
-  - nix-build --argstr coq-version-or-url "$COQ" --extra-substituters https://coq.cachix.org --trusted-public-keys "cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= coq.cachix.org-1:5QW/wwEnD+l2jvN6QRbRRsa4hBHG3QiQQ26cxu1F5tI="
-
+  - nix-env -iA nixpkgs.cachix
+{{# cachix }}
+  - cachix use {{ name }}
+{{/ cachix }}{{^ cachix }}  - cachix use coq
+  - cachix use coq-community
+  - cachix use math-comp
+{{/ cachix }}
+  script: >
+    nix-build https://coq.inria.fr/nix/toolbox --argstr job {{ shortname }} --arg override "{ $VERSIONS; {{ shortname }} = builtins.filterSource (path: _: baseNameOf path != \".git\") ./.; }"
 {{/ nix }}
 jobs:
   include:
@@ -64,10 +71,10 @@ jobs:
   # Test supported versions of Coq via Nix
 {{# tested_coq_nix_versions }}
   - env:
-    - COQ={{ version_or_url }}
+    - VERSIONS='coq = "{{ coq_version }}"{{# extra_dev_dependencies }}; {{ nix_name }} = {{ dev_version }}{{^ dev_version }}"master"{{/ dev_version }}{{/ extra_dev_dependencies }}'
     <<: *NIX
 {{/ tested_coq_nix_versions }}{{^ tested_coq_nix_versions }}  - env:
-    - COQ=https://github.com/coq/coq-on-cachix/tarball/master
+    - VERSIONS='coq = "master"'
     <<: *NIX
 {{/ tested_coq_nix_versions }}
 

generate.sh

@@ -104,15 +104,6 @@ for f in "$srcdir"/{,.}*.mustache; do
                 continue
             fi
             ;;
-        default.nix)
-            mustache='{{ nix }}'
-            bool=$(get_yaml meta.yml <<<"$mustache")
-            if [ -n "$bool" ] && [ "$bool" != false ]; then
-                : noop
-            else
-                continue
-            fi
-            ;;
     esac
     listed=false
     for specified_target in "$@"; do

nix-action.yml.mustache

@@ -19,25 +19,42 @@ jobs:
     runs-on: ubuntu-latest
     strategy:
       matrix:
-        version_or_url:
+        overrides:
 {{# tested_coq_nix_versions }}
-          - '{{ version_or_url }}'
-{{/ tested_coq_nix_versions }}{{^ tested_coq_nix_versions }}          - 'https://github.com/coq/coq-on-cachix/tarball/master'
+          - 'coq = "{{ coq_version }}"{{# extra_dev_dependencies }}; {{ nix_name }} = {{ dev_version }}{{^ dev_version }}"master"{{/ dev_version }}{{/ extra_dev_dependencies }}'
+{{/ tested_coq_nix_versions }}{{^ tested_coq_nix_versions }}          - 'coq = "master"'
 {{/ tested_coq_nix_versions }}
       fail-fast: false
     steps:
       - uses: cachix/install-nix-action@v12
         with:
           nix_path: nixpkgs=channel:nixpkgs-unstable
+{{# cachix }}
       - uses: cachix/cachix-action@v8
         with:
-          # Name of a cachix cache to pull/substitute
+          name: {{ name }}
+{{# push }}
+{{! Change delimiters to avoid the curly brackets on the following lines being parsed as mustache syntax. }}
+{{=<% %>=}}
+          authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
+<%/ push %>
+<%/ cachix %><%^ cachix %>      - uses: cachix/cachix-action@v8
+        with:
           name: coq
+      - uses: cachix/cachix-action@v8
+        with:
+          name: coq-community
+<%# community %>
+          authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
+<%/ community %>
+      - uses: cachix/cachix-action@v8
+        with:
+          name: math-comp
+<%/ cachix %>
       - uses: actions/checkout@v2
-{{# submodule }}
+<%# submodule %>
       - name: Checkout submodules
         uses: textbook/[email protected]
-{{/ submodule }}
-{{! Change delimiters to avoid the next line being parsed as mustache syntax. }}
-{{=<% %>=}}
-      - run: nix-build --argstr coq-version-or-url "${{ matrix.version_or_url }}"
+<%/ submodule %>
+      - run: >
+          nix-build https://coq.inria.fr/nix/toolbox --argstr job <% shortname %> --arg override '{ ${{ matrix.overrides }}; <% shortname %> = builtins.filterSource (path: _: baseNameOf path != ".git") ./.; }'

ref.yml

@@ -18,7 +18,6 @@ fields:
         - coq.opam
         - extracted.opam
         - config.yml
-        - default.nix
         - dune
         - dune-project
   - branch:
@@ -64,7 +63,14 @@ fields:
   - nix:
       type: bool
       description: >
-        Set to true to generate a default.nix file and to test it.
+        Set to true to generate Nix-based CI configuration. For now,
+        this is only supported if either:
+        - the project is already available in nixpkgs under shortname
+          (same casing) and the build instructions and dependencies
+          have not changed;
+        - or, the project has no extra dependencies and builds with
+          the standard mechanism (coq_makefile with a _CoqProject
+          file).
       used:
         - README.md
         - .travis.yml
@@ -222,10 +228,6 @@ fields:
             required: true
             used:
               - coq.opam
-  - plugin:
-      type: bool
-      used:
-        - default.nix
   - dependencies:
       type: list
       item_fields:
@@ -242,16 +244,6 @@ fields:
             used:
               - coq.opam
               - extracted.opam
-        - nix:
-            required: true
-            description: >
-              The list of Coq packages in nixpkgs can be seen here:
-              https://github.com/NixOS/nixpkgs/blob/nixpkgs-unstable/pkgs/top-level/coq-packages.nix
-              Casing matters and might differ from the opam name.  The
-              leading coq- is present only if it is really an integral
-              part of the package name.
-            used:
-              - default.nix
   - categories:
       required: false
       fields:
@@ -396,22 +388,35 @@ fields:
       type: list
       description: If empty, the master branch of Coq will be tested.
       item_fields:
-        - version_or_url:
+        - coq_version:
             required: true
             description: >
-              This can be a version number of a version packaged in
-              nixpkgs (example: 8.5, 8.11).  Cf. the coqPackages_8_XX
-              attributes defined at the end of this file:
-              https://github.com/NixOS/nixpkgs/blob/nixpkgs-unstable/pkgs/top-level/coq-packages.nix
-              (Quote the version number, otherwise '8.10' becomes '8.1'.)
-
-              Or this can be a URL, to test your project with a
-              version of Coq under development.  Typically this is
-              https://github.com/coq/coq-on-cachix/tarball/master but
-              'master' may be replaced by any valid reference like one
-              of the branches available at
-              https://github.com/coq/coq-on-cachix/branches or a valid
-              commit hash.
+              See https://nixos.org/manual/nixpkgs/unstable/#sec-language-coq
+              for the supported syntax.
+        - extra_dev_dependencies:
+            type: list
+            description: >
+              To be used if a development version of an extra
+              dependency is needed. In particular, this is required
+              for all dependencies when testing a branch of Coq
+              (instead of a released version).
+            item_fields:
+              - nix_name:
+                  required: true
+                  description: >
+                    Nix package name for the dependency (casing
+                    matters). See a list of available packages at
+                    https://search.nixos.org/packages?channel=unstable&query=coqPackages
+                    Put mathcomp when depending on one or several
+                    mathcomp-* package(s).
+              - dev_version:
+                  required: false
+                  default: master
+                  description: >
+                    Which version to use (generally the branch name or
+                    the PR hash). See
+                    https://nixos.org/manual/nixpkgs/unstable/#sec-language-coq
+                    for the supported syntax.
       used:
         - .travis.yml
         - nix-action.yml
@@ -454,8 +459,32 @@ fields:
         generate a daily schedule starting at a random night-time
         minute.
       examples:
-        - '5 4 * * *' #daily at 4:05
-        - '5 4 * * 0' #at 04:05 on Sunday
+        - '5 4 * * *'  # daily at 4:05
+        - '5 4 * * 0'  # at 04:05 on Sunday
       used:
         - docker-action.yml
         - nix-action.yml
+  - cachix:
+      type: list
+      required: false
+      description: >
+        List of Cachix caches to install (to fetch from and optionally
+        to push to). By default, the coq, coq-community and math-comp
+        caches are installed and, if community is set to true, pushing
+        to the coq-community cache is activated.
+      item_fields:
+        - name:
+            required: true
+            description: Name of a public Cachix cache.
+            used:
+              - .travis.yml
+              - nix-action.yml
+        - push:
+            type: bool
+            description: >
+              To activate pushing to the Cachix cache.  This is only
+              supported in GitHub Actions (for now) and requires
+              having set the secret variable CACHIX_AUTH_TOKEN at the
+              repository or organization level.
+            used:
+              - nix-action.yml