From df43dcbc862075dbcea7538bf356c36a527d1845 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Thu, 10 Dec 2020 17:30:12 +0100 Subject: [PATCH 01/33] update meta.yml --- .gitattributes | 2 + .github/workflows/coq-action.yml | 30 ---- .github/workflows/docker-action.yml | 3 +- .github/workflows/nix-action.yml | 109 ++++++++++++ .github/workflows/nix.yml | 18 -- .nix/config.nix | 22 +++ .../mathcomp-analysis/default.nix | 31 ++++ .nix/coq-overlays/multinomials/default.nix | 34 ++++ .nix/nixpkgs.nix | 4 + README.md | 4 + config.nix | 6 - default.nix | 160 ++---------------- index.md | 54 ++++++ meta.yml | 10 ++ package.nix | 37 +++- 15 files changed, 320 insertions(+), 204 deletions(-) delete mode 100644 .github/workflows/coq-action.yml create mode 100644 .github/workflows/nix-action.yml delete mode 100644 .github/workflows/nix.yml create mode 100644 .nix/config.nix create mode 100644 .nix/coq-overlays/mathcomp-analysis/default.nix create mode 100644 .nix/coq-overlays/multinomials/default.nix create mode 100644 .nix/nixpkgs.nix delete mode 100644 config.nix create mode 100644 index.md diff --git a/.gitattributes b/.gitattributes index 035f68b71..ef19d53db 100644 --- a/.gitattributes +++ b/.gitattributes @@ -1 +1,3 @@ +.git* export-ignore +.nix export-ignore CHANGELOG_UNRELEASED.md merge=union \ No newline at end of file diff --git a/.github/workflows/coq-action.yml b/.github/workflows/coq-action.yml deleted file mode 100644 index e57449e75..000000000 --- a/.github/workflows/coq-action.yml +++ /dev/null @@ -1,30 +0,0 @@ -name: CI - -on: - push: - branches: - - master - pull_request: - branches: - - '**' - -jobs: - build: - # the OS must be GNU/Linux to be able to use the docker-coq-action - runs-on: ubuntu-latest - strategy: - matrix: - image: - - 'mathcomp/mathcomp:1.12.0-coq-8.11' - - 'mathcomp/mathcomp:1.12.0-coq-8.12' - fail-fast: false - steps: - - uses: actions/checkout@v2 - - uses: coq-community/docker-coq-action@v1 - with: - opam_file: 'coq-mathcomp-analysis.opam' - custom_image: ${{ matrix.image }} - -# See also: -# https://github.com/coq-community/docker-coq-action#readme -# https://github.com/erikmd/docker-coq-github-action-demo diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index b06387ed1..2d1dbfdd7 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -20,9 +20,10 @@ jobs: - 'mathcomp/mathcomp:1.12.0-coq-8.11' - 'mathcomp/mathcomp:1.12.0-coq-8.12' - 'mathcomp/mathcomp:1.12.0-coq-8.13' + - 'mathcomp/mathcomp:1.12.0-coq-dev' - 'mathcomp/mathcomp-dev:coq-8.11' - 'mathcomp/mathcomp-dev:coq-8.12' - - 'mathcomp/mathcomp-dev:coq-8.13' + - 'mathcomp/mathcomp-dev:coq-dev' fail-fast: false steps: - uses: actions/checkout@v2 diff --git a/.github/workflows/nix-action.yml b/.github/workflows/nix-action.yml new file mode 100644 index 000000000..6221da917 --- /dev/null +++ b/.github/workflows/nix-action.yml @@ -0,0 +1,109 @@ +# This file was generated from `meta.yml`, please do not edit manually. +# Follow the instructions on https://github.com/coq-community/templates to regenerate. +name: Nix CI + +on: + push: + branches: + - master + pull_request: + branches: + - '**' + +jobs: + dependencies: + runs-on: ubuntu-latest + outputs: + matrix: ${{ steps.set-matrix.outputs.matrix }} + steps: + - name: Cachix install + uses: cachix/install-nix-action@v12 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq + uses: cachix/cachix-action@v8 + with: + # Name of a cachix cache to pull/substitute + name: coq + - name: Cachix setup math-comp + uses: cachix/cachix-action@v8 + with: + # Name of a cachix cache to pull/substitute + name: math-comp + authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}' + - name: Git checkout + uses: actions/checkout@v2 + with: + fetch-depth: 0 + - name: Building/fetching dependencies + run: nix-build --argstr ci-step dependencies + - name: Setup build matrix + id: set-matrix + run: | + matrix=$(nix-shell --arg do-nothing true --run nixInputs) + echo ::set-output name=matrix::{\"input\":$(echo $matrix)}\" + + main: + runs-on: ubuntu-latest + needs: + - dependencies + strategy: + matrix: ${{fromJson(needs.dependencies.outputs.matrix)}} + steps: + - name: Cachix install + uses: cachix/install-nix-action@v12 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq + uses: cachix/cachix-action@v8 + with: + # Name of a cachix cache to pull/substitute + name: coq + - name: Cachix setup math-comp + uses: cachix/cachix-action@v8 + with: + # Name of a cachix cache to pull/substitute + name: math-comp + authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}' + - name: Git checkout + uses: actions/checkout@v2 + with: + fetch-depth: 0 + - name: Building/fetching dependencies + run: nix-build --argstr ci "${{ matrix.input }}" --argstr ci-step dependencies + - name: Building/fetching current project + run: nix-build --argstr ci "${{ matrix.input }}" --argstr ci-step main + + all: + runs-on: ubuntu-latest + needs: + - dependencies + - main + strategy: + matrix: ${{fromJson(needs.dependencies.outputs.matrix)}} + steps: + - name: Cachix install + uses: cachix/install-nix-action@v12 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq + uses: cachix/cachix-action@v8 + with: + # Name of a cachix cache to pull/substitute + name: coq + - name: Cachix setup math-comp + uses: cachix/cachix-action@v8 + with: + # Name of a cachix cache to pull/substitute + name: math-comp + authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}' + - name: Git checkout + uses: actions/checkout@v2 + with: + fetch-depth: 0 + - name: Building/fetching dependencies + run: nix-build --argstr ci "${{ matrix.input }}" --argstr ci-step dependencies + - name: Building/fetching current project + run: nix-build --argstr ci "${{ matrix.input }}" --argstr ci-step main + - name: Building/fetching current CI target + run: nix-build --argstr ci "${{ matrix.input }}" --argstr ci-step all diff --git a/.github/workflows/nix.yml b/.github/workflows/nix.yml deleted file mode 100644 index fa42fead9..000000000 --- a/.github/workflows/nix.yml +++ /dev/null @@ -1,18 +0,0 @@ -name: Cachix -on: - push: -jobs: - cachix: - name: Cachix branch - runs-on: ubuntu-latest - steps: - - uses: cachix/install-nix-action@v12 - - uses: cachix/cachix-action@v8 - with: - # Name of a cachix cache to push and pull/substitute - name: math-comp - # Authentication token for Cachix, needed only for private cache access - authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}' - - uses: actions/checkout@v2 - - run: nix-build - # - run: export CACHIX_SIGNING_KEY=${{ secrets.CACHIX_SIGNING_KEY }} cachix push math-comp result diff --git a/.nix/config.nix b/.nix/config.nix new file mode 100644 index 000000000..9d6b60d03 --- /dev/null +++ b/.nix/config.nix @@ -0,0 +1,22 @@ +{ + format = "1.0.0"; + coq-attribute = "mathcomp-analysis"; + pname = "analysis"; + namespace = "mathcomp.analysis"; + realpath = "theories"; + select = "coq-8.13"; + inputs."coq-8.13".coqPackages = { + coq.override.version = "8.13"; + mathcomp.override.version = "1.12.0"; + mathcomp-real-closed.override.version = "1.1"; + mathcomp-finmap.override.version = "1.5"; + hierarchy-builder.override.version = "1.0.0"; + coq-elpi.override.version = "1.8.1"; }; + inputs."coq-8.12".coqPackages = { + coq.override.version = "8.12"; + mathcomp.override.version = "1.12.0"; }; + inputs."coq-8.11+multinomials".coqPackages = { + coq.override.version = "8.11"; + mathcomp.override.version = "1.11.0"; + multinomials.ci.step = "all"; }; +} diff --git a/.nix/coq-overlays/mathcomp-analysis/default.nix b/.nix/coq-overlays/mathcomp-analysis/default.nix new file mode 100644 index 000000000..a3170a899 --- /dev/null +++ b/.nix/coq-overlays/mathcomp-analysis/default.nix @@ -0,0 +1,31 @@ +{ coq, mkCoqDerivation, mathcomp, mathcomp-finmap, + mathcomp-bigenough, mathcomp-real-closed, + hierarchy-builder, + stdenv, lib, fetchFromGitHub, version ? null }: + +with lib; mkCoqDerivation { + + prefix-list = [ "coq" "mathcomp" ]; + pname = "analysis"; + owner = "math-comp"; + + release."0.3.1".sha256 = "1iad288yvrjv8ahl9v18vfblgqb1l5z6ax644w49w9hwxs93f2k8"; + release."0.2.3".sha256 = "0p9mr8g1qma6h10qf7014dv98ln90dfkwn76ynagpww7qap8s966"; + + inherit version; + default-version = with versions; switch [ coq.version mathcomp.version ] [ + { cases = [ (range "8.10" "8.12~") "1.11.0" ]; out = "0.3.1"; } + { cases = [ (range "8.9" "8.12~") "1.10.0" ]; out = "0.3.0"; } + { cases = [ (range "8.8" "8.11~") (range "1.8.0" "1.11~") ]; + out = "0.2.3"; } + ] null; + + propagatedBuildInputs = + [ mathcomp.ssreflect mathcomp.field hierarchy-builder + mathcomp-finmap mathcomp-bigenough mathcomp-real-closed ]; + + meta = { + description = "Analysis library compatible with Mathematical Components"; + license = licenses.cecill-c; + }; +} diff --git a/.nix/coq-overlays/multinomials/default.nix b/.nix/coq-overlays/multinomials/default.nix new file mode 100644 index 000000000..11c71da39 --- /dev/null +++ b/.nix/coq-overlays/multinomials/default.nix @@ -0,0 +1,34 @@ +{ coq, mkCoqDerivation, mathcomp, mathcomp-finmap, mathcomp-bigenough, + lib, version ? null }: +with lib; mkCoqDerivation { + + namePrefix = [ "coq" "mathcomp" ]; + pname = "multinomials"; + owner = "math-comp"; + inherit version; + defaultVersion = with versions; switch [ coq.version mathcomp.version ] [ + { cases = [ (range "8.7" "8.13") "1.11.0" ]; out = "1.5.2"; } + { cases = [ (range "8.7" "8.11") (range "1.8" "1.10") ]; out = "1.5.0"; } + { cases = [ (range "8.7" "8.10") (range "1.8" "1.10") ]; out = "1.4"; } + { cases = [ "8.6" (range "1.6" "1.7") ]; out = "1.1"; } + ] null; + release = { + "1.5.2".sha256 = "15aspf3jfykp1xgsxf8knqkxv8aav2p39c2fyirw7pwsfbsv2c4s"; + "1.5.1".sha256 = "13nlfm2wqripaq671gakz5mn4r0xwm0646araxv0nh455p9ndjs3"; + "1.5.0".sha256 = "064rvc0x5g7y1a0nip6ic91vzmq52alf6in2bc2dmss6dmzv90hw"; + "1.5.0".rev = "1.5"; + "1.4".sha256 = "0vnkirs8iqsv8s59yx1fvg1nkwnzydl42z3scya1xp1b48qkgn0p"; + "1.3".sha256 = "0l3vi5n094nx3qmy66hsv867fnqm196r8v605kpk24gl0aa57wh4"; + "1.2".sha256 = "1mh1w339dslgv4f810xr1b8v2w7rpx6fgk9pz96q0fyq49fw2xcq"; + "1.1".sha256 = "1q8alsm89wkc0lhcvxlyn0pd8rbl2nnxg81zyrabpz610qqjqc3s"; + "1.0".sha256 = "1qmbxp1h81cy3imh627pznmng0kvv37k4hrwi2faa101s6bcx55m"; + }; + + propagatedBuildInputs = + [ mathcomp.ssreflect mathcomp.algebra mathcomp-finmap mathcomp-bigenough ]; + + meta = { + description = "A Coq/SSReflect Library for Monoidal Rings and Multinomials"; + license = licenses.cecill-c; + }; +} diff --git a/.nix/nixpkgs.nix b/.nix/nixpkgs.nix new file mode 100644 index 000000000..f9ce973b3 --- /dev/null +++ b/.nix/nixpkgs.nix @@ -0,0 +1,4 @@ +fetchTarball { + url = https://github.com/NixOS/nixpkgs/archive/66e66b9d481386f4c7a6b998f32ce794af0182ae.tar.gz; + sha256 = "1zw3ib0705n7nskv9a2ipj1z0ys4wn2j8frnzhf1gx1yrgyjm8sn"; + } diff --git a/README.md b/README.md index cc08603c0..a1233288d 100644 --- a/README.md +++ b/README.md @@ -5,10 +5,14 @@ Follow the instructions on https://github.com/coq-community/templates to regener # Analysis library compatible with Mathematical Components [![Docker CI][docker-action-shield]][docker-action-link] +[![Nix CI][nix-action-shield]][nix-action-link] [![Chat][chat-shield]][chat-link] [docker-action-shield]: https://github.com/math-comp/analysis/workflows/Docker%20CI/badge.svg?branch=master [docker-action-link]: https://github.com/math-comp/analysis/actions?query=workflow:"Docker%20CI" + +[nix-action-shield]: https://github.com/math-comp/analysis/workflows/Nix%20CI/badge.svg?branch=master +[nix-action-link]: https://github.com/math-comp/analysis/actions?query=workflow:"Nix%20CI" [chat-shield]: https://img.shields.io/badge/zulip-join_chat-brightgreen.svg [chat-link]: https://coq.zulipchat.com/login/#narrow/stream/237666-math-comp-analysis diff --git a/config.nix b/config.nix deleted file mode 100644 index 1daa16d79..000000000 --- a/config.nix +++ /dev/null @@ -1,6 +0,0 @@ -{ - coq = "8.11"; - mathcomp = "mathcomp-1.12.0"; - mathcomp-real-closed = "1.1.2"; - mathcomp-finmap = "1.5.1"; -} diff --git a/default.nix b/default.nix index 1f6bda078..0ece3cd7b 100644 --- a/default.nix +++ b/default.nix @@ -1,149 +1,13 @@ -{ - nixpkgs ? (if builtins.pathExists ./nixpkgs.nix then import ./nixpkgs.nix - else fetchTarball https://github.com/NixOS/nixpkgs-channels/archive/502845c3e31ef3de0e424f3fcb09217df2ce6df6.tar.gz), - config ? (if builtins.pathExists ./config.nix then import ./config.nix else {}), - withEmacs ? false, - print-env ? false, - do-nothing ? false, - package ? (if builtins.pathExists ./package.nix then import ./package.nix else "mathcomp-fast"), - src ? (if builtins.pathExists ./package.nix then ./. else false) -}: -with builtins; -let - cfg-fun = if isFunction config then config else (pkgs: config); - pkg-src = if src == false then {} - else { ${if package == "mathcomp.single" then "mathcomp" else package} = src; }; - pkgs = if isAttrs nixpkgs then nixpkgs else import nixpkgs { - overlays = [ (pkgs: super-pkgs: with pkgs.lib; - let coqPackages = with pkgs; { - "8.7" = coqPackages_8_7; - "8.8" = coqPackages_8_8; - "8.9" = coqPackages_8_9; - "8.10" = coqPackages_8_10; - "8.11" = coqPackages_8_11; - "8.12" = coqPackages_8_12; - "default" = coqPackages_8_11; - }.${(cfg-fun pkgs).coq or "default"}.overrideScope' - (coqPackages: super-coqPackages: - let - all-pkgs = pkgs // { inherit coqPackages; }; - cfg = pkg-src // { - mathcomp-fast = { - src = ./.; - propagatedBuildInputs = with coqPackages; ([ mathcomp ] ++ mathcomp-extra-fast); - }; - mathcomp-full = { - src = ./.; - propagatedBuildInputs = with coqPackages; ([ mathcomp ] ++ mathcomp-extra-all); - }; - } // (cfg-fun all-pkgs); - in { - mathcomp-extra-config = - let mec = super-coqPackages.mathcomp-extra-config; in - lib.recursiveUpdate mec { - initial = { - # fixing mathcomp analysis to depend on real-closed - mathcomp-analysis = {version, coqPackages} @ args: - let mca = mec.initial.mathcomp-analysis args; in - mca // ( - if elem version [ "master" "cauchy_etoile" "holomorphy" ] - then { - propagatedBuildInputs = mca.propagatedBuildInputs ++ - [ coqPackages.mathcomp-real-closed coqPackages.hierarchy-builder ]; - } else { - propagatedBuildInputs = mca.propagatedBuildInputs ++ - (with coqPackages; [ coq-elpi hierarchy-builder ]); - }); - }; - for-coq-and-mc.${coqPackages.coq.coq-version}.${coqPackages.mathcomp.version} = - (super-coqPackages.mathcomp-extra-config.${coqPackages.coq.coq-version}.${coqPackages.mathcomp.version} or {}) // - (removeAttrs cfg [ "mathcomp" "coq" "mathcomp-fast" "mathcomp-full" ]); - }; - mathcomp = if cfg?mathcomp then coqPackages.mathcomp_ cfg.mathcomp else super-coqPackages.mathcomp; - } // mapAttrs - (package: version: coqPackages.mathcomp-extra package version) - (removeAttrs cfg ["mathcomp" "coq"]) - ); in { - coqPackages = coqPackages.filterPackages coqPackages.coq coqPackages; - coq = coqPackages.coq; - mc-clean = src: { - version = baseNameOf src; - src = cleanSourceWith { - src = cleanSource src; - filter = path: type: let baseName = baseNameOf (toString path); in ! ( - hasSuffix ".aux" baseName || - hasSuffix ".d" baseName || - hasSuffix ".vo" baseName || - hasSuffix ".glob" baseName || - elem baseName ["Makefile.coq" "Makefile.coq.conf" ".mailmap" ".git"] - ); - }; - }; - })]; - }; +# This file was generated from `meta.yml`, please do not edit manually. +# Follow the instructions on https://github.com/coq-community/templates to regenerate. +{ config ? {}, withEmacs ? false, print-env ? false, do-nothing ? false, + update-nixpkgs ? false, ci-matrix ? false, ci-step ? null, + override ? {}, ocaml-override ? {}, global-override ? {}, + ci ? (!isNull ci-step), inNixShell ? null +}@args: +let src = fetchGit { + url = "https://github.com/coq-community/nix-toolbox.git"; + ref = "master"; +}; in +(import "${src}/auto-config.nix" ./. args).nix-auto - mathcompnix = ./.; - - shellHook = '' - nixEnv () { - echo "Here is your work environement" - echo "buildInputs:" - for x in $buildInputs; do printf " "; echo $x | cut -d "-" -f "2-"; done - echo "propagatedBuildInputs:" - for x in $propagatedBuildInputs; do printf " "; echo $x | cut -d "-" -f "2-"; done - echo "you can pass option --arg config '{coq = \"x.y\"; math-comp = \"x.y.z\";}' to nix-shell to change coq and/or math-comp versions" - } - - printEnv () { - for x in $buildInputs; do echo $x; done - for x in $propagatedBuildInputs; do echo $x; done - } - - cachixEnv () { - echo "Pushing environement to cachix" - printEnv | cachix push math-comp - } - - nixDefault () { - cat $mathcompnix/default.nix - } > default.nix - - updateNixPkgs (){ - HASH=$(git ls-remote https://github.com/NixOS/nixpkgs-channels refs/heads/nixpkgs-unstable | cut -f1); - URL=https://github.com/NixOS/nixpkgs-channels/archive/$HASH.tar.gz - SHA256=$(nix-prefetch-url --unpack $URL) - echo "fetchTarball { - url = $URL; - sha256 = \"$SHA256\"; - }" > nixpkgs.nix - } - updateNixPkgsMaster (){ - HASH=$(git ls-remote https://github.com/NixOS/nixpkgs refs/heads/master | cut -f1); - URL=https://github.com/NixOS/nixpkgs/archive/$HASH.tar.gz - SHA256=$(nix-prefetch-url --unpack $URL) - echo "fetchTarball { - url = $URL; - sha256 = \"$SHA256\"; - }" > nixpkgs.nix - } - '' - + pkgs.lib.optionalString print-env "nixEnv"; - - emacs = with pkgs; emacsWithPackages - (epkgs: with epkgs.melpaStablePackages; [proof-general]); - - pkg = with pkgs; - if package == "mathcomp.single" then coqPackages.mathcomp.single - else coqPackages.${package} or (coqPackages.current-mathcomp-extra package); -in -if pkgs.lib.trivial.inNixShell then pkg.overrideAttrs (old: { - inherit shellHook mathcompnix; - - buildInputs = if do-nothing then [] - else (old.buildInputs ++ - (if pkgs.lib.trivial.inNixShell then pkgs.lib.optional withEmacs pkgs.emacs - else [])); - - propagatedBuildInputs = if do-nothing then [] else old.propagatedBuildInputs; - -}) else pkg diff --git a/index.md b/index.md new file mode 100644 index 000000000..95b589783 --- /dev/null +++ b/index.md @@ -0,0 +1,54 @@ +--- +# This file was generated from `meta.yml`, please do not edit manually. +# Follow the instructions on https://github.com/coq-community/templates to regenerate. +title: Analysis library compatible with Mathematical Components +lang: en +header-includes: + - | + + + + + +--- + +
+View the project on GitHub +
+ +## About + +Welcome to the Analysis library compatible with Mathematical Components project website! + +This repository contains an experimental library for real analysis for +the Coq proof-assistant and using the Mathematical Components library. + +This is an open source project, licensed under the CeCILL-C. + +## Get the code + +The current stable release of Analysis library compatible with Mathematical Components can be [downloaded from GitHub](https://github.com/math-comp/analysis/releases). + +## Documentation + + +Related publications, if any, are listed below. + +- [Formalization Techniques for Asymptotic Reasoning in Classical Analysis](https://jfr.unibo.it/article/view/8124) doi:[10.6092/issn.1972-5787/8124](https://doi.org/10.6092/issn.1972-5787/8124) +- [Competing inheritance paths in dependent type theory---a case study in functional analysis](https://hal.inria.fr/hal-02463336) doi:[10.1007/978-3-030-51054-1_1](https://doi.org/10.1007/978-3-030-51054-1_1) +- [Formalisation Tools for Classical Analysis](http://www-sop.inria.fr/members/Damien.Rouhling/data/phd/thesis.pdf) + +## Help and contact + +- Report issues on [GitHub](https://github.com/math-comp/analysis/issues) + +## Authors and contributors + +- Reynald Affeldt +- Cyril Cohen +- Marie Kerjean +- Assia Mahboubi +- Damien Rouhling +- Kazuhiko Sakaguchi +- Pierre-Yves Strub + diff --git a/meta.yml b/meta.yml index 2e286e9ac..223840c49 100644 --- a/meta.yml +++ b/meta.yml @@ -2,10 +2,20 @@ fullname: Analysis library compatible with Mathematical Components shortname: analysis organization: math-comp opam_name: coq-mathcomp-analysis +nix_name: mathcomp-analysis community: false action: true coqdoc: false +nix: true +cachix: +- name: coq +- name: math-comp + token: CACHIX_AUTH_TOKEN + +nix-ci: +- name: all + synopsis: >- An analysis library for mathematical components description: |- diff --git a/package.nix b/package.nix index e8e708431..f5b0de146 100644 --- a/package.nix +++ b/package.nix @@ -1 +1,36 @@ -"mathcomp-analysis" +# This file was generated from `meta.yml`, please do not edit manually. +# Follow the instructions on https://github.com/coq-community/templates to +# regenerate. +{ + config-file ? ./.nix/config.nix, + config ? {}, + withEmacs ? false, + print-env ? false, + do-nothing ? false, + update-nixpkgs ? false, + ci ? false, +}@args: +let do-nothing = (args.do-nothing or false) || update-nixpkgs; in +with builtins; +let result = (import ./.nix/auto-config.nix {inherit config config-file;}); in +with result; +with selected-instance.pkgs.coqPackages.lib; +if trivial.inNixShell then + with selected-instance; this-pkg.overrideAttrs (old: { + inherit json_input; + shellHook = result.shellHook + + optionalString print-env "nixEnv" + + optionalString update-nixpkgs "updateNixPkgs"; + currentdir = "./."; + coq_version = pkgs.coqPackages.coq.coq-version; + inherit (result.config) nixpkgs logpath realpath; + + buildInputs = optionals (!do-nothing) + (old.buildInputs or [] ++ optional withEmacs pkgs.emacs); + + propagatedBuildInputs = optionals (!do-nothing) + (old.propagatedBuildInputs or []); + }) +else + if ci then map (b: b.ci-coqpkgs) instances + else selected-instance.this-pkg From 5b6a57b1ab65963c7e150a29956bfa67d1c99959 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Thu, 11 Mar 2021 04:11:02 +0100 Subject: [PATCH 02/33] update nix-config --- .nix/config.nix | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/.nix/config.nix b/.nix/config.nix index 9d6b60d03..a7818c724 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -5,18 +5,18 @@ namespace = "mathcomp.analysis"; realpath = "theories"; select = "coq-8.13"; - inputs."coq-8.13".coqPackages = { + medleys."coq-8.13".coqPackages = { coq.override.version = "8.13"; mathcomp.override.version = "1.12.0"; mathcomp-real-closed.override.version = "1.1"; mathcomp-finmap.override.version = "1.5"; hierarchy-builder.override.version = "1.0.0"; coq-elpi.override.version = "1.8.1"; }; - inputs."coq-8.12".coqPackages = { + medleys."coq-8.12".coqPackages = { coq.override.version = "8.12"; mathcomp.override.version = "1.12.0"; }; - inputs."coq-8.11+multinomials".coqPackages = { + medleys."coq-8.11+multinomials".coqPackages = { coq.override.version = "8.11"; mathcomp.override.version = "1.11.0"; - multinomials.ci.step = "all"; }; + multinomials.ci.job = "all"; }; } From 85c3efed49dcc7fd27c41f680c8839b99f4d7d75 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Thu, 11 Mar 2021 04:11:30 +0100 Subject: [PATCH 03/33] correct defult.nix --- default.nix | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/default.nix b/default.nix index 0ece3cd7b..9a0d78ee8 100644 --- a/default.nix +++ b/default.nix @@ -5,9 +5,10 @@ override ? {}, ocaml-override ? {}, global-override ? {}, ci ? (!isNull ci-step), inNixShell ? null }@args: -let src = fetchGit { +let auto = fetchGit { url = "https://github.com/coq-community/nix-toolbox.git"; ref = "master"; + rev = "4755bb40df95c6f7451d14ecb343606b5b83c115"; }; in -(import "${src}/auto-config.nix" ./. args).nix-auto +(import auto ({src = ./.;} // args)).nix-auto From 2d2c1d19c27609f2fca0e6ceb17dcee03ac97d91 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Thu, 11 Mar 2021 04:43:37 +0100 Subject: [PATCH 04/33] temp --- default.nix | 12 +++++------- meta.yml | 3 +++ 2 files changed, 8 insertions(+), 7 deletions(-) diff --git a/default.nix b/default.nix index 9a0d78ee8..574b9fe16 100644 --- a/default.nix +++ b/default.nix @@ -1,14 +1,12 @@ # This file was generated from `meta.yml`, please do not edit manually. # Follow the instructions on https://github.com/coq-community/templates to regenerate. { config ? {}, withEmacs ? false, print-env ? false, do-nothing ? false, - update-nixpkgs ? false, ci-matrix ? false, ci-step ? null, + update-nixpkgs ? false, ci-matrix ? false, ci-step ? null, override ? {}, ocaml-override ? {}, global-override ? {}, - ci ? (!isNull ci-step), inNixShell ? null + ci ? (!isNull ci-step), inNixShell ? null }@args: -let auto = fetchGit { - url = "https://github.com/coq-community/nix-toolbox.git"; - ref = "master"; - rev = "4755bb40df95c6f7451d14ecb343606b5b83c115"; -}; in +let + auto = ~/git/coq-nix-toolbox/master; +in (import auto ({src = ./.;} // args)).nix-auto diff --git a/meta.yml b/meta.yml index 223840c49..0662a7304 100644 --- a/meta.yml +++ b/meta.yml @@ -13,6 +13,9 @@ cachix: - name: math-comp token: CACHIX_AUTH_TOKEN +nix-auto-config: + src: ~/git/coq-nix-toolbox/master + nix-ci: - name: all From b50c773a54adcb7571468108df6015bd8ddc8cdc Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Thu, 11 Mar 2021 04:44:19 +0100 Subject: [PATCH 05/33] generated fallback --- .nix/fallback-config.nix | 69 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 69 insertions(+) create mode 100644 .nix/fallback-config.nix diff --git a/.nix/fallback-config.nix b/.nix/fallback-config.nix new file mode 100644 index 000000000..e35034c8b --- /dev/null +++ b/.nix/fallback-config.nix @@ -0,0 +1,69 @@ +# This file was generated from `meta.yml`, please do not edit manually. +# Follow the instructions on https://github.com/coq-community/templates to regenerate. + +# HOWEVER, we encourage you to copy paste it to `config.nix` +# in the same subdirectory .nix and extend it as needed. + +{ + ## DO NOT CHANGE THIS + format = "1.0.0"; + ## unless you made an automated or manual update + ## to another supported format. + + ## The attribute to build, either from nixpkgs + ## of from the overlays located in `.nix/coq-overlays` + coq-attribute = "mathcomp-analysis"; + + ## If you want to select a different attribute + ## to serve as a basis for nix-shell edit this + # coq-shell-attribute = "mathcomp-analysis"; + + ## Maybe the shortname of the library is different from + ## the name of the nixpkgs attribute, if so, set it here: + pname = "analysis"; + + ## Write here the Coq `-R ` mapping + ## Multiple mappings are not suppported yet. + ## In the future we may read the designated `_CoqProject` instead + # namespace = ""; + # realpath = ""; + + ## select an entry to build in the following `medleys` set + # select = "default"; + + ## write one `medleys.name` attribute set per + ## alternative configuration, the can be used to + ## compute several ci jobs as well + # medleys.default = { + + ## You can override Coq and other Coq coqPackages + ## throught 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 + # coqPackages..overrideAttrs = o: ; + ## or a "long" overlay to put in `.nix/coq-overlays + ## you may use `nix-shell --run fetchOverlay ` + ## to automatically retrieve the one from nixpkgs + ## if it exists and is correctly named/located + + ## You can override Coq and other Coq coqPackages + ## throught the following attribute + ## If does not support lights overload, + ## you may use `overrideAttrs` or long overlays + ## located in `.nix/ocaml-overlays` + ## (there is no automation for this one) + # ocamlPackages..override.version = "x.xx"; + + ## You can also override packages from the nixpkgs toplevel + # .override.overrideAttrs = o: ; + ## Or put an overlay in `.nix/overlays` + + ## you may mark a package as a CI job as follows + # coqPackages..ci.job = "test"; + ## It can then be built throught + ## nix-build --argstr ci "default" --arg ci-job "test"; + + # } +}; \ No newline at end of file From 01b1b7dba1ac9f0c1683fe03698030fc9d0c225d Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Thu, 11 Mar 2021 06:07:39 +0100 Subject: [PATCH 06/33] tests --- .github/workflows/nix-action.yml | 12 ++++++------ .nix/config.nix | 6 +++--- .nix/fallback-config.nix | 15 +++++++-------- default.nix | 12 +++++++----- meta.yml | 8 ++++---- 5 files changed, 27 insertions(+), 26 deletions(-) diff --git a/.github/workflows/nix-action.yml b/.github/workflows/nix-action.yml index 6221da917..580e173de 100644 --- a/.github/workflows/nix-action.yml +++ b/.github/workflows/nix-action.yml @@ -36,7 +36,7 @@ jobs: with: fetch-depth: 0 - name: Building/fetching dependencies - run: nix-build --argstr ci-step dependencies + run: nix-build --argstr ci-job dependencies - name: Setup build matrix id: set-matrix run: | @@ -70,9 +70,9 @@ jobs: with: fetch-depth: 0 - name: Building/fetching dependencies - run: nix-build --argstr ci "${{ matrix.input }}" --argstr ci-step dependencies + run: nix-build --argstr ci "${{ matrix.input }}" --argstr ci-job dependencies - name: Building/fetching current project - run: nix-build --argstr ci "${{ matrix.input }}" --argstr ci-step main + run: nix-build --argstr ci "${{ matrix.input }}" --argstr ci-job main all: runs-on: ubuntu-latest @@ -102,8 +102,8 @@ jobs: with: fetch-depth: 0 - name: Building/fetching dependencies - run: nix-build --argstr ci "${{ matrix.input }}" --argstr ci-step dependencies + run: nix-build --argstr ci "${{ matrix.input }}" --argstr ci-job dependencies - name: Building/fetching current project - run: nix-build --argstr ci "${{ matrix.input }}" --argstr ci-step main + run: nix-build --argstr ci "${{ matrix.input }}" --argstr ci-job main - name: Building/fetching current CI target - run: nix-build --argstr ci "${{ matrix.input }}" --argstr ci-step all + run: nix-build --argstr ci "${{ matrix.input }}" --argstr ci-job all diff --git a/.nix/config.nix b/.nix/config.nix index a7818c724..c4795b438 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -5,17 +5,17 @@ namespace = "mathcomp.analysis"; realpath = "theories"; select = "coq-8.13"; - medleys."coq-8.13".coqPackages = { + tasks."coq-8.13".coqPackages = { coq.override.version = "8.13"; mathcomp.override.version = "1.12.0"; mathcomp-real-closed.override.version = "1.1"; mathcomp-finmap.override.version = "1.5"; hierarchy-builder.override.version = "1.0.0"; coq-elpi.override.version = "1.8.1"; }; - medleys."coq-8.12".coqPackages = { + tasks."coq-8.12".coqPackages = { coq.override.version = "8.12"; mathcomp.override.version = "1.12.0"; }; - medleys."coq-8.11+multinomials".coqPackages = { + tasks."coq-8.11+multinomials".coqPackages = { coq.override.version = "8.11"; mathcomp.override.version = "1.11.0"; multinomials.ci.job = "all"; }; diff --git a/.nix/fallback-config.nix b/.nix/fallback-config.nix index e35034c8b..a003a50f9 100644 --- a/.nix/fallback-config.nix +++ b/.nix/fallback-config.nix @@ -22,24 +22,23 @@ ## the name of the nixpkgs attribute, if so, set it here: pname = "analysis"; - ## Write here the Coq `-R ` mapping - ## Multiple mappings are not suppported yet. - ## In the future we may read the designated `_CoqProject` instead - # namespace = ""; - # realpath = ""; + ## Indicate the relative location of your _CoqProject + ## If not specified, it defaults to "_CoqProject" + # coqproject = "_CoqProject"; ## select an entry to build in the following `medleys` set + ## defaults to "default" # select = "default"; ## write one `medleys.name` attribute set per ## alternative configuration, the can be used to ## compute several ci jobs as well # medleys.default = { - + ## You can override Coq and other Coq coqPackages ## throught 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 # coqPackages..overrideAttrs = o: ; @@ -66,4 +65,4 @@ ## nix-build --argstr ci "default" --arg ci-job "test"; # } -}; \ No newline at end of file +} \ No newline at end of file diff --git a/default.nix b/default.nix index 574b9fe16..b20154f5d 100644 --- a/default.nix +++ b/default.nix @@ -1,12 +1,14 @@ # This file was generated from `meta.yml`, please do not edit manually. # Follow the instructions on https://github.com/coq-community/templates to regenerate. { config ? {}, withEmacs ? false, print-env ? false, do-nothing ? false, - update-nixpkgs ? false, ci-matrix ? false, ci-step ? null, + update-nixpkgs ? false, ci-matrix ? false, ci-step ? null, override ? {}, ocaml-override ? {}, global-override ? {}, - ci ? (!isNull ci-step), inNixShell ? null + ci ? (!isNull ci-step), inNixShell ? null }@args: -let - auto = ~/git/coq-nix-toolbox/master; -in +let auto = fetchGit { + url = "https://github.com/coq-community/coq-nix-toolbox.git"; + ref = "master"; + rev = "12dbd4a2f02f2cac2f75337ac6b848e4e037f4de"; +}; in (import auto ({src = ./.;} // args)).nix-auto diff --git a/meta.yml b/meta.yml index 0662a7304..fe505f69e 100644 --- a/meta.yml +++ b/meta.yml @@ -12,13 +12,13 @@ cachix: - name: coq - name: math-comp token: CACHIX_AUTH_TOKEN - -nix-auto-config: - src: ~/git/coq-nix-toolbox/master - + nix-ci: - name: all +nix-dependencies: +- coquelicot + synopsis: >- An analysis library for mathematical components description: |- From 33a68a6fe389e7d8239b29928affe9435db69a82 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Thu, 11 Mar 2021 06:17:30 +0100 Subject: [PATCH 07/33] fixup --- .nix/fallback-config.nix | 21 +++++++++++++++------ meta.yml | 3 --- 2 files changed, 15 insertions(+), 9 deletions(-) diff --git a/.nix/fallback-config.nix b/.nix/fallback-config.nix index a003a50f9..50e006fb0 100644 --- a/.nix/fallback-config.nix +++ b/.nix/fallback-config.nix @@ -1,8 +1,9 @@ # This file was generated from `meta.yml`, please do not edit manually. # Follow the instructions on https://github.com/coq-community/templates to regenerate. -# HOWEVER, we encourage you to copy paste it to `config.nix` +# *However*, you may copy paste it to `config.nix` # in the same subdirectory .nix and extend it as needed. +# Note that this would completely deactivate this file. { ## DO NOT CHANGE THIS @@ -22,18 +23,26 @@ ## the name of the nixpkgs attribute, if so, set it here: pname = "analysis"; + ## 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 packaged is available on nixpkgs. + ## /!\ Manual overlays in `.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 `medleys` set + ## select an entry to build in the following `tasks` set ## defaults to "default" - # select = "default"; + select = "default"; - ## write one `medleys.name` attribute set per + ## write one `tasks.name` attribute set per ## alternative configuration, the can be used to ## compute several ci jobs as well - # medleys.default = { + tasks.default = { ## You can override Coq and other Coq coqPackages ## throught the following attribute @@ -64,5 +73,5 @@ ## It can then be built throught ## nix-build --argstr ci "default" --arg ci-job "test"; - # } + }; } \ No newline at end of file diff --git a/meta.yml b/meta.yml index fe505f69e..6ac54756f 100644 --- a/meta.yml +++ b/meta.yml @@ -16,9 +16,6 @@ cachix: nix-ci: - name: all -nix-dependencies: -- coquelicot - synopsis: >- An analysis library for mathematical components description: |- From c5c0a35232629f1adff091e99bf84f4ae42d1622 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Thu, 11 Mar 2021 22:15:20 +0100 Subject: [PATCH 08/33] up --- .github/workflows/nix-action.yml | 14 +++++++------- .nix/fallback-config.nix | 8 ++++---- default.nix | 2 +- 3 files changed, 12 insertions(+), 12 deletions(-) diff --git a/.github/workflows/nix-action.yml b/.github/workflows/nix-action.yml index 580e173de..2ddc7d4f7 100644 --- a/.github/workflows/nix-action.yml +++ b/.github/workflows/nix-action.yml @@ -40,8 +40,8 @@ jobs: - name: Setup build matrix id: set-matrix run: | - matrix=$(nix-shell --arg do-nothing true --run nixInputs) - echo ::set-output name=matrix::{\"input\":$(echo $matrix)}\" + matrix=$(nix-shell --arg do-nothing true --run nixTasks) + echo ::set-output name=matrix::{\"task\":$(echo $matrix)}\" main: runs-on: ubuntu-latest @@ -70,9 +70,9 @@ jobs: with: fetch-depth: 0 - name: Building/fetching dependencies - run: nix-build --argstr ci "${{ matrix.input }}" --argstr ci-job dependencies + run: nix-build --argstr ci "${{ matrix.task }}" --argstr ci-job dependencies - name: Building/fetching current project - run: nix-build --argstr ci "${{ matrix.input }}" --argstr ci-job main + run: nix-build --argstr ci "${{ matrix.task }}" --argstr ci-job main all: runs-on: ubuntu-latest @@ -102,8 +102,8 @@ jobs: with: fetch-depth: 0 - name: Building/fetching dependencies - run: nix-build --argstr ci "${{ matrix.input }}" --argstr ci-job dependencies + run: nix-build --argstr ci "${{ matrix.task }}" --argstr ci-job dependencies - name: Building/fetching current project - run: nix-build --argstr ci "${{ matrix.input }}" --argstr ci-job main + run: nix-build --argstr ci "${{ matrix.task }}" --argstr ci-job main - name: Building/fetching current CI target - run: nix-build --argstr ci "${{ matrix.input }}" --argstr ci-job all + run: nix-build --argstr ci "${{ matrix.task }}" --argstr ci-job all diff --git a/.nix/fallback-config.nix b/.nix/fallback-config.nix index 50e006fb0..7dc8709d3 100644 --- a/.nix/fallback-config.nix +++ b/.nix/fallback-config.nix @@ -27,7 +27,7 @@ ## 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 packaged is available on nixpkgs. + ## /!\ Remove this field as soon as the package is available on nixpkgs. ## /!\ Manual overlays in `.nix/coq-overlays` should be preferred then. #buildInputs = [ ]; @@ -45,7 +45,7 @@ tasks.default = { ## You can override Coq and other Coq coqPackages - ## throught the following attribute + ## through the following attribute # coqPackages.coq.override.version = "8.11"; ## In some cases, light overrides are not available/enough @@ -58,7 +58,7 @@ ## You can override Coq and other Coq coqPackages ## throught the following attribute - ## If does not support lights overload, + ## If does not support lights overrides, ## you may use `overrideAttrs` or long overlays ## located in `.nix/ocaml-overlays` ## (there is no automation for this one) @@ -74,4 +74,4 @@ ## nix-build --argstr ci "default" --arg ci-job "test"; }; -} \ No newline at end of file +} diff --git a/default.nix b/default.nix index b20154f5d..aa93ab58b 100644 --- a/default.nix +++ b/default.nix @@ -8,7 +8,7 @@ let auto = fetchGit { url = "https://github.com/coq-community/coq-nix-toolbox.git"; ref = "master"; - rev = "12dbd4a2f02f2cac2f75337ac6b848e4e037f4de"; + rev = import ./nix/.coq-nix-toolbox.nix; }; in (import auto ({src = ./.;} // args)).nix-auto From 2ee37ba7c26289ae08b3bb3196164c1f5be9f749 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Fri, 12 Mar 2021 00:59:25 +0100 Subject: [PATCH 09/33] up --- .nix/config.nix | 2 +- default.nix | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/.nix/config.nix b/.nix/config.nix index c4795b438..4f9cddb49 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -17,6 +17,6 @@ mathcomp.override.version = "1.12.0"; }; tasks."coq-8.11+multinomials".coqPackages = { coq.override.version = "8.11"; - mathcomp.override.version = "1.11.0"; + mathcomp.override.version = "1.12.0"; multinomials.ci.job = "all"; }; } diff --git a/default.nix b/default.nix index aa93ab58b..8d82490eb 100644 --- a/default.nix +++ b/default.nix @@ -8,7 +8,7 @@ let auto = fetchGit { url = "https://github.com/coq-community/coq-nix-toolbox.git"; ref = "master"; - rev = import ./nix/.coq-nix-toolbox.nix; + rev = import ./.nix/coq-nix-toolbox.nix; }; in (import auto ({src = ./.;} // args)).nix-auto From 57f3503afff78af7112040ef93bea4e17b4388b4 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Fri, 12 Mar 2021 08:39:57 +0100 Subject: [PATCH 10/33] appropriate nix config --- .nix/config.nix | 26 +++++++++++++++----------- 1 file changed, 15 insertions(+), 11 deletions(-) diff --git a/.nix/config.nix b/.nix/config.nix index 4f9cddb49..31bc292e5 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -4,19 +4,23 @@ pname = "analysis"; namespace = "mathcomp.analysis"; realpath = "theories"; - select = "coq-8.13"; - tasks."coq-8.13".coqPackages = { + select = "mc-1.12-coq-8.13"; + tasks."mc-1.12-coq-8.13".coqPackages = { coq.override.version = "8.13"; - mathcomp.override.version = "1.12.0"; - mathcomp-real-closed.override.version = "1.1"; - mathcomp-finmap.override.version = "1.5"; - hierarchy-builder.override.version = "1.0.0"; - coq-elpi.override.version = "1.8.1"; }; - tasks."coq-8.12".coqPackages = { + mathcomp.override.version = "1.12.0"; }; + tasks."mc-1.12-coq-8.12".coqPackages = { coq.override.version = "8.12"; mathcomp.override.version = "1.12.0"; }; - tasks."coq-8.11+multinomials".coqPackages = { + tasks."mc-1.12-coq-8.11".coqPackages = { + coq.override.version = "8.11"; + mathcomp.override.version = "1.12.0";}; + tasks."mc-master-coq-8.13".coqPackages = { + coq.override.version = "8.13"; + mathcomp.override.version = "master"; }; + tasks."mc-master-coq-8.12".coqPackages = { + coq.override.version = "8.12"; + mathcomp.override.version = "master"; }; + tasks."mc-master-coq-8.11".coqPackages = { coq.override.version = "8.11"; - mathcomp.override.version = "1.12.0"; - multinomials.ci.job = "all"; }; + mathcomp.override.version = "master";}; } From 50194352784d71c779f514b316564f581ae34592 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Fri, 12 Mar 2021 08:40:42 +0100 Subject: [PATCH 11/33] fixup --- meta.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/meta.yml b/meta.yml index 6ac54756f..02e16e297 100644 --- a/meta.yml +++ b/meta.yml @@ -13,8 +13,8 @@ cachix: - name: math-comp token: CACHIX_AUTH_TOKEN -nix-ci: -- name: all +# nix-ci: +# - name: all synopsis: >- An analysis library for mathematical components From 0bda7c0252d4ecd35d388048c0beacc05bc347f5 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Fri, 12 Mar 2021 08:41:52 +0100 Subject: [PATCH 12/33] up --- .github/workflows/nix-action.yml | 33 -------------------------------- 1 file changed, 33 deletions(-) diff --git a/.github/workflows/nix-action.yml b/.github/workflows/nix-action.yml index 2ddc7d4f7..f999142c9 100644 --- a/.github/workflows/nix-action.yml +++ b/.github/workflows/nix-action.yml @@ -74,36 +74,3 @@ jobs: - name: Building/fetching current project run: nix-build --argstr ci "${{ matrix.task }}" --argstr ci-job main - all: - runs-on: ubuntu-latest - needs: - - dependencies - - main - strategy: - matrix: ${{fromJson(needs.dependencies.outputs.matrix)}} - steps: - - name: Cachix install - uses: cachix/install-nix-action@v12 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq - uses: cachix/cachix-action@v8 - with: - # Name of a cachix cache to pull/substitute - name: coq - - name: Cachix setup math-comp - uses: cachix/cachix-action@v8 - with: - # Name of a cachix cache to pull/substitute - name: math-comp - authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}' - - name: Git checkout - uses: actions/checkout@v2 - with: - fetch-depth: 0 - - name: Building/fetching dependencies - run: nix-build --argstr ci "${{ matrix.task }}" --argstr ci-job dependencies - - name: Building/fetching current project - run: nix-build --argstr ci "${{ matrix.task }}" --argstr ci-job main - - name: Building/fetching current CI target - run: nix-build --argstr ci "${{ matrix.task }}" --argstr ci-job all From 146e3506c9cb15a6dac9a8520fff663e1ea545c1 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Fri, 12 Mar 2021 14:54:10 +0100 Subject: [PATCH 13/33] fixes --- .github/workflows/nix-action.yml | 43 ++++++++++++++++++++++++++------ default.nix | 4 +-- meta.yml | 6 +++-- 3 files changed, 42 insertions(+), 11 deletions(-) diff --git a/.github/workflows/nix-action.yml b/.github/workflows/nix-action.yml index f999142c9..9ba86365f 100644 --- a/.github/workflows/nix-action.yml +++ b/.github/workflows/nix-action.yml @@ -11,7 +11,7 @@ on: - '**' jobs: - dependencies: + setup: runs-on: ubuntu-latest outputs: matrix: ${{ steps.set-matrix.outputs.matrix }} @@ -35,8 +35,6 @@ jobs: uses: actions/checkout@v2 with: fetch-depth: 0 - - name: Building/fetching dependencies - run: nix-build --argstr ci-job dependencies - name: Setup build matrix id: set-matrix run: | @@ -46,7 +44,8 @@ jobs: main: runs-on: ubuntu-latest needs: - - dependencies + - setup + - dependencies strategy: matrix: ${{fromJson(needs.dependencies.outputs.matrix)}} steps: @@ -70,7 +69,37 @@ jobs: with: fetch-depth: 0 - name: Building/fetching dependencies - run: nix-build --argstr ci "${{ matrix.task }}" --argstr ci-job dependencies - - name: Building/fetching current project - run: nix-build --argstr ci "${{ matrix.task }}" --argstr ci-job main + run: nix-build --no-out-link --argstr ci "${{ matrix.task }}" --argstr ci-job dependencies + - name: Building/fetching current CI target + run: nix-build --no-out-link --argstr ci "${{ matrix.task }}" --argstr ci-job main + dependencies: + runs-on: ubuntu-latest + needs: + - setup + strategy: + matrix: ${{fromJson(needs.dependencies.outputs.matrix)}} + steps: + - name: Cachix install + uses: cachix/install-nix-action@v12 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq + uses: cachix/cachix-action@v8 + with: + # Name of a cachix cache to pull/substitute + name: coq + - name: Cachix setup math-comp + uses: cachix/cachix-action@v8 + with: + # Name of a cachix cache to pull/substitute + name: math-comp + authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}' + - name: Git checkout + uses: actions/checkout@v2 + with: + fetch-depth: 0 + - name: Building/fetching dependencies + run: nix-build --no-out-link --argstr ci "${{ matrix.task }}" --argstr ci-job dependencies + - name: Building/fetching current CI target + run: nix-build --no-out-link --argstr ci "${{ matrix.task }}" --argstr ci-job dependencies diff --git a/default.nix b/default.nix index 8d82490eb..de65fe52c 100644 --- a/default.nix +++ b/default.nix @@ -1,9 +1,9 @@ # This file was generated from `meta.yml`, please do not edit manually. # Follow the instructions on https://github.com/coq-community/templates to regenerate. { config ? {}, withEmacs ? false, print-env ? false, do-nothing ? false, - update-nixpkgs ? false, ci-matrix ? false, ci-step ? null, + update-nixpkgs ? false, ci-matrix ? false, ci-job ? null, override ? {}, ocaml-override ? {}, global-override ? {}, - ci ? (!isNull ci-step), inNixShell ? null + ci ? (!isNull ci-job), inNixShell ? null }@args: let auto = fetchGit { url = "https://github.com/coq-community/coq-nix-toolbox.git"; diff --git a/meta.yml b/meta.yml index 02e16e297..466777571 100644 --- a/meta.yml +++ b/meta.yml @@ -13,8 +13,10 @@ cachix: - name: math-comp token: CACHIX_AUTH_TOKEN -# nix-ci: -# - name: all +nix-ci: +- job: main + needs: [ dependencies ] +- job: dependencies synopsis: >- An analysis library for mathematical components From 57cc63df27c8e3c46c767f3a39c996f2ea8fbd0c Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Sun, 14 Mar 2021 14:58:15 +0100 Subject: [PATCH 14/33] up --- .github/workflows/nix-action.yml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/.github/workflows/nix-action.yml b/.github/workflows/nix-action.yml index 9ba86365f..76f9e5411 100644 --- a/.github/workflows/nix-action.yml +++ b/.github/workflows/nix-action.yml @@ -44,10 +44,10 @@ jobs: main: runs-on: ubuntu-latest needs: - - setup - - dependencies + - setup + - dependencies strategy: - matrix: ${{fromJson(needs.dependencies.outputs.matrix)}} + matrix: ${{fromJson(needs.setup.outputs.matrix)}} steps: - name: Cachix install uses: cachix/install-nix-action@v12 @@ -76,9 +76,9 @@ jobs: dependencies: runs-on: ubuntu-latest needs: - - setup + - setup strategy: - matrix: ${{fromJson(needs.dependencies.outputs.matrix)}} + matrix: ${{fromJson(needs.setup.outputs.matrix)}} steps: - name: Cachix install uses: cachix/install-nix-action@v12 From e0767cad707cc653276c08e91fd0e81357ab62b7 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Sun, 14 Mar 2021 14:58:47 +0100 Subject: [PATCH 15/33] Revert "appropriate nix config" This reverts commit 77044bb66f088092d31ab558d4e91d63ba990677. --- .nix/config.nix | 26 +++++++++++--------------- 1 file changed, 11 insertions(+), 15 deletions(-) diff --git a/.nix/config.nix b/.nix/config.nix index 31bc292e5..4f9cddb49 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -4,23 +4,19 @@ pname = "analysis"; namespace = "mathcomp.analysis"; realpath = "theories"; - select = "mc-1.12-coq-8.13"; - tasks."mc-1.12-coq-8.13".coqPackages = { + select = "coq-8.13"; + tasks."coq-8.13".coqPackages = { coq.override.version = "8.13"; - mathcomp.override.version = "1.12.0"; }; - tasks."mc-1.12-coq-8.12".coqPackages = { + mathcomp.override.version = "1.12.0"; + mathcomp-real-closed.override.version = "1.1"; + mathcomp-finmap.override.version = "1.5"; + hierarchy-builder.override.version = "1.0.0"; + coq-elpi.override.version = "1.8.1"; }; + tasks."coq-8.12".coqPackages = { coq.override.version = "8.12"; mathcomp.override.version = "1.12.0"; }; - tasks."mc-1.12-coq-8.11".coqPackages = { - coq.override.version = "8.11"; - mathcomp.override.version = "1.12.0";}; - tasks."mc-master-coq-8.13".coqPackages = { - coq.override.version = "8.13"; - mathcomp.override.version = "master"; }; - tasks."mc-master-coq-8.12".coqPackages = { - coq.override.version = "8.12"; - mathcomp.override.version = "master"; }; - tasks."mc-master-coq-8.11".coqPackages = { + tasks."coq-8.11+multinomials".coqPackages = { coq.override.version = "8.11"; - mathcomp.override.version = "master";}; + mathcomp.override.version = "1.12.0"; + multinomials.ci.job = "all"; }; } From 3003d6efd8f2256c2e85929ffd874700bc3ba37a Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Sun, 14 Mar 2021 16:06:14 +0100 Subject: [PATCH 16/33] More is generated from meta --- .github/workflows/nix-action.yml | 40 ++++++++++++-- .nix/config.nix | 22 -------- .nix/coq-overlays/multinomials/default.nix | 34 ------------ .nix/fallback-config.nix | 63 +++++++++------------- .nix/nixpkgs.nix | 4 +- coq-nix-toolbox.nix | 1 + meta.yml | 38 ++++++++++++- 7 files changed, 98 insertions(+), 104 deletions(-) delete mode 100644 .nix/config.nix delete mode 100644 .nix/coq-overlays/multinomials/default.nix create mode 100644 coq-nix-toolbox.nix diff --git a/.github/workflows/nix-action.yml b/.github/workflows/nix-action.yml index 76f9e5411..5f66726ef 100644 --- a/.github/workflows/nix-action.yml +++ b/.github/workflows/nix-action.yml @@ -41,6 +41,35 @@ jobs: matrix=$(nix-shell --arg do-nothing true --run nixTasks) echo ::set-output name=matrix::{\"task\":$(echo $matrix)}\" + dependencies: + runs-on: ubuntu-latest + needs: + - setup + strategy: + matrix: ${{fromJson(needs.setup.outputs.matrix)}} + steps: + - name: Cachix install + uses: cachix/install-nix-action@v12 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq + uses: cachix/cachix-action@v8 + with: + # Name of a cachix cache to pull/substitute + name: coq + - name: Cachix setup math-comp + uses: cachix/cachix-action@v8 + with: + # Name of a cachix cache to pull/substitute + name: math-comp + authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}' + - name: Git checkout + uses: actions/checkout@v2 + with: + fetch-depth: 0 + - name: Building/fetching current CI target + run: nix-build --no-out-link --argstr ci "${{ matrix.task }}" --argstr ci-job dependencies + main: runs-on: ubuntu-latest needs: @@ -68,15 +97,16 @@ jobs: uses: actions/checkout@v2 with: fetch-depth: 0 - - name: Building/fetching dependencies + - name: Building/fetching previous target dependencies run: nix-build --no-out-link --argstr ci "${{ matrix.task }}" --argstr ci-job dependencies - name: Building/fetching current CI target run: nix-build --no-out-link --argstr ci "${{ matrix.task }}" --argstr ci-job main - dependencies: + all: runs-on: ubuntu-latest needs: - setup + - main strategy: matrix: ${{fromJson(needs.setup.outputs.matrix)}} steps: @@ -99,7 +129,7 @@ jobs: uses: actions/checkout@v2 with: fetch-depth: 0 - - name: Building/fetching dependencies - run: nix-build --no-out-link --argstr ci "${{ matrix.task }}" --argstr ci-job dependencies + - name: Building/fetching previous target main + run: nix-build --no-out-link --argstr ci "${{ matrix.task }}" --argstr ci-job main - name: Building/fetching current CI target - run: nix-build --no-out-link --argstr ci "${{ matrix.task }}" --argstr ci-job dependencies + run: nix-build --no-out-link --argstr ci "${{ matrix.task }}" --argstr ci-job all diff --git a/.nix/config.nix b/.nix/config.nix deleted file mode 100644 index 4f9cddb49..000000000 --- a/.nix/config.nix +++ /dev/null @@ -1,22 +0,0 @@ -{ - format = "1.0.0"; - coq-attribute = "mathcomp-analysis"; - pname = "analysis"; - namespace = "mathcomp.analysis"; - realpath = "theories"; - select = "coq-8.13"; - tasks."coq-8.13".coqPackages = { - coq.override.version = "8.13"; - mathcomp.override.version = "1.12.0"; - mathcomp-real-closed.override.version = "1.1"; - mathcomp-finmap.override.version = "1.5"; - hierarchy-builder.override.version = "1.0.0"; - coq-elpi.override.version = "1.8.1"; }; - tasks."coq-8.12".coqPackages = { - coq.override.version = "8.12"; - mathcomp.override.version = "1.12.0"; }; - tasks."coq-8.11+multinomials".coqPackages = { - coq.override.version = "8.11"; - mathcomp.override.version = "1.12.0"; - multinomials.ci.job = "all"; }; -} diff --git a/.nix/coq-overlays/multinomials/default.nix b/.nix/coq-overlays/multinomials/default.nix deleted file mode 100644 index 11c71da39..000000000 --- a/.nix/coq-overlays/multinomials/default.nix +++ /dev/null @@ -1,34 +0,0 @@ -{ coq, mkCoqDerivation, mathcomp, mathcomp-finmap, mathcomp-bigenough, - lib, version ? null }: -with lib; mkCoqDerivation { - - namePrefix = [ "coq" "mathcomp" ]; - pname = "multinomials"; - owner = "math-comp"; - inherit version; - defaultVersion = with versions; switch [ coq.version mathcomp.version ] [ - { cases = [ (range "8.7" "8.13") "1.11.0" ]; out = "1.5.2"; } - { cases = [ (range "8.7" "8.11") (range "1.8" "1.10") ]; out = "1.5.0"; } - { cases = [ (range "8.7" "8.10") (range "1.8" "1.10") ]; out = "1.4"; } - { cases = [ "8.6" (range "1.6" "1.7") ]; out = "1.1"; } - ] null; - release = { - "1.5.2".sha256 = "15aspf3jfykp1xgsxf8knqkxv8aav2p39c2fyirw7pwsfbsv2c4s"; - "1.5.1".sha256 = "13nlfm2wqripaq671gakz5mn4r0xwm0646araxv0nh455p9ndjs3"; - "1.5.0".sha256 = "064rvc0x5g7y1a0nip6ic91vzmq52alf6in2bc2dmss6dmzv90hw"; - "1.5.0".rev = "1.5"; - "1.4".sha256 = "0vnkirs8iqsv8s59yx1fvg1nkwnzydl42z3scya1xp1b48qkgn0p"; - "1.3".sha256 = "0l3vi5n094nx3qmy66hsv867fnqm196r8v605kpk24gl0aa57wh4"; - "1.2".sha256 = "1mh1w339dslgv4f810xr1b8v2w7rpx6fgk9pz96q0fyq49fw2xcq"; - "1.1".sha256 = "1q8alsm89wkc0lhcvxlyn0pd8rbl2nnxg81zyrabpz610qqjqc3s"; - "1.0".sha256 = "1qmbxp1h81cy3imh627pznmng0kvv37k4hrwi2faa101s6bcx55m"; - }; - - propagatedBuildInputs = - [ mathcomp.ssreflect mathcomp.algebra mathcomp-finmap mathcomp-bigenough ]; - - meta = { - description = "A Coq/SSReflect Library for Monoidal Rings and Multinomials"; - license = licenses.cecill-c; - }; -} diff --git a/.nix/fallback-config.nix b/.nix/fallback-config.nix index 7dc8709d3..e80032324 100644 --- a/.nix/fallback-config.nix +++ b/.nix/fallback-config.nix @@ -6,7 +6,7 @@ # Note that this would completely deactivate this file. { - ## DO NOT CHANGE THIS + ## DO NOT CHANGE THE format format = "1.0.0"; ## unless you made an automated or manual update ## to another supported format. @@ -33,45 +33,30 @@ ## Indicate the relative location of your _CoqProject ## If not specified, it defaults to "_CoqProject" - # coqproject = "_CoqProject"; + coqproject = "_CoqProject"; - ## select an entry to build in the following `tasks` set + ## Select a task to build by default in the following `tasks` set + ## It will be used when typing nix-shell or nix-build without argument ## defaults to "default" - select = "default"; - - ## write one `tasks.name` attribute set per - ## alternative configuration, the can be used to - ## compute several ci jobs as well - tasks.default = { - - ## 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 - # coqPackages..overrideAttrs = o: ; - ## or a "long" overlay to put in `.nix/coq-overlays - ## you may use `nix-shell --run fetchOverlay ` - ## to automatically retrieve the one from nixpkgs - ## if it exists and is correctly named/located - - ## You can override Coq and other Coq coqPackages - ## throught the following attribute - ## If does not support lights overrides, - ## you may use `overrideAttrs` or long overlays - ## located in `.nix/ocaml-overlays` - ## (there is no automation for this one) - # ocamlPackages..override.version = "x.xx"; - - ## You can also override packages from the nixpkgs toplevel - # .override.overrideAttrs = o: ; - ## Or put an overlay in `.nix/overlays` - - ## you may mark a package as a CI job as follows - # coqPackages..ci.job = "test"; - ## It can then be built throught - ## nix-build --argstr ci "default" --arg ci-job "test"; - + select = "coq-8.13"; + tasks."coq-8.13" = {}; + + tasks."coq-8.13" = { + coqPackages."coq".override.version = "8.13"; + coqPackages."mathcomp".override.version = "1.12.0"; + coqPackages."real-closed".override.version = "1.1"; + coqPackages."finmap".override.version = "1.5"; + coqPackages."hierarchy-builder".override.version = "1.0.0"; + coqPackages."coq-elpi".override.version = "1.8.1"; + }; + tasks."coq-8.12" = { + coqPackages."coq".override.version = "8.11"; + coqPackages."mathcomp".override.version = "1.12.0"; + }; + tasks."coq-8.11+multinomials" = { + coqPackages."coq".override.version = "8.11"; + coqPackages."mathcomp".override.version = "1.12.0"; + coqPackages."multinomials".override.version = "1.5.4"; + coqPackages."multinomials".ci.job = "all"; }; } diff --git a/.nix/nixpkgs.nix b/.nix/nixpkgs.nix index f9ce973b3..197902d24 100644 --- a/.nix/nixpkgs.nix +++ b/.nix/nixpkgs.nix @@ -1,4 +1,4 @@ fetchTarball { - url = https://github.com/NixOS/nixpkgs/archive/66e66b9d481386f4c7a6b998f32ce794af0182ae.tar.gz; - sha256 = "1zw3ib0705n7nskv9a2ipj1z0ys4wn2j8frnzhf1gx1yrgyjm8sn"; + url = https://github.com/NixOS/nixpkgs/archive/0e1a8cc3ec6fd5844d30a24d99e44ad4a6971235.tar.gz; + sha256 = "1gsvr0h0rmc0vx0x9vabrcfdndl5kcd617i5wxy5r35nr68rbvaj"; } diff --git a/coq-nix-toolbox.nix b/coq-nix-toolbox.nix new file mode 100644 index 000000000..ba2d94364 --- /dev/null +++ b/coq-nix-toolbox.nix @@ -0,0 +1 @@ +"e54b920493f0494ede95b5f7d083cc8b20b1f5a6" diff --git a/meta.yml b/meta.yml index 466777571..7f2e48198 100644 --- a/meta.yml +++ b/meta.yml @@ -13,10 +13,44 @@ cachix: - name: math-comp token: CACHIX_AUTH_TOKEN -nix-ci: +nix-jobs: +- job: dependencies - job: main needs: [ dependencies ] -- job: dependencies +- job: all + needs: [ main ] + +nix-default-task: coq-8.13 +nix-tasks: +- task: coq-8.13 + packages: + - name: coq + version: 8.13 + - name: mathcomp + version: 1.12.0 + - name: real-closed + version: 1.1 + - name: finmap + version: 1.5 + - name: hierarchy-builder + version: 1.0.0 + - name: coq-elpi + version: 1.8.1 +- task: coq-8.12 + packages: + - name: coq + version: 8.11 + - name: mathcomp + version: 1.12.0 +- task: coq-8.11+multinomials + packages: + - name: coq + version: 8.11 + - name: mathcomp + version: 1.12.0 + - name: multinomials + ci-job: all + version: 1.5.4 synopsis: >- An analysis library for mathematical components From 1f371421359f699538bf774d7afbb9bf6150ac5b Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Sun, 14 Mar 2021 17:01:52 +0100 Subject: [PATCH 17/33] better way of pinning the toolbox --- default.nix | 16 +++++++++------- meta.yml | 4 ++++ 2 files changed, 13 insertions(+), 7 deletions(-) diff --git a/default.nix b/default.nix index de65fe52c..8b6e44add 100644 --- a/default.nix +++ b/default.nix @@ -1,14 +1,16 @@ # This file was generated from `meta.yml`, please do not edit manually. # Follow the instructions on https://github.com/coq-community/templates to regenerate. { config ? {}, withEmacs ? false, print-env ? false, do-nothing ? false, - update-nixpkgs ? false, ci-matrix ? false, ci-job ? null, + update-nixpkgs ? false, ci-matrix ? false, ci-job ? null, override ? {}, ocaml-override ? {}, global-override ? {}, - ci ? (!isNull ci-job), inNixShell ? null + ci ? (!isNull ci-job), inNixShell ? null }@args: -let auto = fetchGit { - url = "https://github.com/coq-community/coq-nix-toolbox.git"; - ref = "master"; - rev = import ./.nix/coq-nix-toolbox.nix; -}; in +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 ({src = ./.;} // args)).nix-auto diff --git a/meta.yml b/meta.yml index 7f2e48198..0be04b153 100644 --- a/meta.yml +++ b/meta.yml @@ -8,6 +8,10 @@ action: true coqdoc: false nix: true +nix_name: mathcomp-analysis +nix-default: + ref: master + cachix: - name: coq - name: math-comp From c0b43a0a5b048cf39f9f7f4c80eb53c9ff5e0dad Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Sun, 14 Mar 2021 17:06:47 +0100 Subject: [PATCH 18/33] missing file --- .nix/coq-nix-toolbox.nix | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 .nix/coq-nix-toolbox.nix diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix new file mode 100644 index 000000000..7614da775 --- /dev/null +++ b/.nix/coq-nix-toolbox.nix @@ -0,0 +1,5 @@ +# This file was generated from meta.yml, please do not edit manually. +# Follow the instructions on https://github.com/coq-community/templates to regenerate. +# However, this rev was not handled by mustache, but by a special eval command +# because you picked the option nix-default: ... in meta.yml +"de89ff16c149b7a7aec3cfe9d379641ee1aca229" From 671fd0c0fa4bf5b9a3c405661a1245cf7450c457 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Sun, 14 Mar 2021 17:18:45 +0100 Subject: [PATCH 19/33] inlining tasks -> no setup --- .github/workflows/nix-action.yml | 59 ++++++++++++++------------------ meta.yml | 15 ++++---- 2 files changed, 34 insertions(+), 40 deletions(-) diff --git a/.github/workflows/nix-action.yml b/.github/workflows/nix-action.yml index 5f66726ef..287f0e013 100644 --- a/.github/workflows/nix-action.yml +++ b/.github/workflows/nix-action.yml @@ -13,40 +13,20 @@ on: jobs: setup: runs-on: ubuntu-latest - outputs: - matrix: ${{ steps.set-matrix.outputs.matrix }} steps: - - name: Cachix install - uses: cachix/install-nix-action@v12 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq - uses: cachix/cachix-action@v8 - with: - # Name of a cachix cache to pull/substitute - name: coq - - name: Cachix setup math-comp - uses: cachix/cachix-action@v8 - with: - # Name of a cachix cache to pull/substitute - name: math-comp - authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}' - - name: Git checkout - uses: actions/checkout@v2 - with: - fetch-depth: 0 - - name: Setup build matrix - id: set-matrix - run: | - matrix=$(nix-shell --arg do-nothing true --run nixTasks) - echo ::set-output name=matrix::{\"task\":$(echo $matrix)}\" + - name: Do nothing + run: echo "No setup, using meta.yml tasks" dependencies: runs-on: ubuntu-latest needs: - - setup + - setup strategy: - matrix: ${{fromJson(needs.setup.outputs.matrix)}} + matrix: + task: + - coq-8.13 + - coq-8.12 + - coq-8.11+multinomials steps: - name: Cachix install uses: cachix/install-nix-action@v12 @@ -73,10 +53,14 @@ jobs: main: runs-on: ubuntu-latest needs: - - setup - - dependencies + - setup + - dependencies strategy: - matrix: ${{fromJson(needs.setup.outputs.matrix)}} + matrix: + task: + - coq-8.13 + - coq-8.12 + - coq-8.11+multinomials steps: - name: Cachix install uses: cachix/install-nix-action@v12 @@ -105,10 +89,15 @@ jobs: all: runs-on: ubuntu-latest needs: - - setup - - main + - setup + - dependencies + - main strategy: - matrix: ${{fromJson(needs.setup.outputs.matrix)}} + matrix: + task: + - coq-8.13 + - coq-8.12 + - coq-8.11+multinomials steps: - name: Cachix install uses: cachix/install-nix-action@v12 @@ -129,6 +118,8 @@ jobs: uses: actions/checkout@v2 with: fetch-depth: 0 + - name: Building/fetching previous target dependencies + run: nix-build --no-out-link --argstr ci "${{ matrix.task }}" --argstr ci-job dependencies - name: Building/fetching previous target main run: nix-build --no-out-link --argstr ci "${{ matrix.task }}" --argstr ci-job main - name: Building/fetching current CI target diff --git a/meta.yml b/meta.yml index 0be04b153..62dce71b9 100644 --- a/meta.yml +++ b/meta.yml @@ -16,13 +16,16 @@ cachix: - name: coq - name: math-comp token: CACHIX_AUTH_TOKEN - + nix-jobs: - job: dependencies - job: main - needs: [ dependencies ] + needs: + - dependencies - job: all - needs: [ main ] + needs: + - dependencies + - main nix-default-task: coq-8.13 nix-tasks: @@ -153,7 +156,7 @@ keywords: publications: - pub_url: https://jfr.unibo.it/article/view/8124 pub_title: Formalization Techniques for Asymptotic Reasoning in Classical Analysis - pub_doi: 10.6092/issn.1972-5787/8124 + pub_doi: 10.6092/issn.1972-5787/8124 - pub_url: https://hal.inria.fr/hal-02463336 pub_title: Competing inheritance paths in dependent type theory---a case study in functional analysis pub_doi: 10.1007/978-3-030-51054-1_1 @@ -162,7 +165,7 @@ publications: documentation: |- ## Disclaimer - + This library is still at an experimental stage. Contents may change, definitions and theorems may be renamed, and inference mechanisms may be replaced at any major version bump. Use at your @@ -174,7 +177,7 @@ documentation: |- Changes are documented in [CHANGELOG.md](CHANGELOG.md) and [CHANGELOG_UNRELEASED.md](CHANGELOG_UNRELEASED.md). - + Overview presentation: [Classical Analysis with Coq](https://perso.crans.org/cohen/CoqWS2018.pdf) (2018) Other work using MathComp-Analysis: [A Formal Classical Proof of Hahn-Banach in Coq](https://lipn.univ-paris13.fr/~kerjean/slides/slidesTYPES19.pdf) (2019) From 7d73e6bcc783e1837142c360f5ed9047186485c3 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Sun, 14 Mar 2021 18:27:46 +0100 Subject: [PATCH 20/33] fix --- .nix/fallback-config.nix | 2 +- meta.yml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/.nix/fallback-config.nix b/.nix/fallback-config.nix index e80032324..3e10a0df9 100644 --- a/.nix/fallback-config.nix +++ b/.nix/fallback-config.nix @@ -47,7 +47,7 @@ coqPackages."real-closed".override.version = "1.1"; coqPackages."finmap".override.version = "1.5"; coqPackages."hierarchy-builder".override.version = "1.0.0"; - coqPackages."coq-elpi".override.version = "1.8.1"; + coqPackages."coq-elpi".override.version = "1.9.3"; }; tasks."coq-8.12" = { coqPackages."coq".override.version = "8.11"; diff --git a/meta.yml b/meta.yml index 62dce71b9..804bcc5d3 100644 --- a/meta.yml +++ b/meta.yml @@ -42,7 +42,7 @@ nix-tasks: - name: hierarchy-builder version: 1.0.0 - name: coq-elpi - version: 1.8.1 + version: 1.9.3 - task: coq-8.12 packages: - name: coq From 35d81388c0fc669a1cb61b1cf595c55649b63c6f Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Tue, 16 Mar 2021 23:15:33 +0100 Subject: [PATCH 21/33] up --- .github/workflows/nix-action.yml | 12 ++++++------ .nix/coq-nix-toolbox.nix | 2 +- default.nix | 8 ++++---- meta.yml | 2 +- 4 files changed, 12 insertions(+), 12 deletions(-) diff --git a/.github/workflows/nix-action.yml b/.github/workflows/nix-action.yml index 287f0e013..3c335bd8a 100644 --- a/.github/workflows/nix-action.yml +++ b/.github/workflows/nix-action.yml @@ -48,7 +48,7 @@ jobs: with: fetch-depth: 0 - name: Building/fetching current CI target - run: nix-build --no-out-link --argstr ci "${{ matrix.task }}" --argstr ci-job dependencies + run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job dependencies main: runs-on: ubuntu-latest @@ -82,9 +82,9 @@ jobs: with: fetch-depth: 0 - name: Building/fetching previous target dependencies - run: nix-build --no-out-link --argstr ci "${{ matrix.task }}" --argstr ci-job dependencies + run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job dependencies - name: Building/fetching current CI target - run: nix-build --no-out-link --argstr ci "${{ matrix.task }}" --argstr ci-job main + run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job main all: runs-on: ubuntu-latest @@ -119,8 +119,8 @@ jobs: with: fetch-depth: 0 - name: Building/fetching previous target dependencies - run: nix-build --no-out-link --argstr ci "${{ matrix.task }}" --argstr ci-job dependencies + run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job dependencies - name: Building/fetching previous target main - run: nix-build --no-out-link --argstr ci "${{ matrix.task }}" --argstr ci-job main + run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job main - name: Building/fetching current CI target - run: nix-build --no-out-link --argstr ci "${{ matrix.task }}" --argstr ci-job all + run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job all diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index 7614da775..1a5da2dca 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -2,4 +2,4 @@ # Follow the instructions on https://github.com/coq-community/templates to regenerate. # However, this rev was not handled by mustache, but by a special eval command # because you picked the option nix-default: ... in meta.yml -"de89ff16c149b7a7aec3cfe9d379641ee1aca229" +"d3227ad13ad0a1a1b971e8a51a8cdd3ade69c821" diff --git a/default.nix b/default.nix index 8b6e44add..3757629cc 100644 --- a/default.nix +++ b/default.nix @@ -1,16 +1,16 @@ # This file was generated from `meta.yml`, please do not edit manually. # Follow the instructions on https://github.com/coq-community/templates to regenerate. { config ? {}, withEmacs ? false, print-env ? false, do-nothing ? false, - update-nixpkgs ? false, ci-matrix ? false, ci-job ? null, + update-nixpkgs ? false, ci-matrix ? false, override ? {}, ocaml-override ? {}, global-override ? {}, - ci ? (!isNull ci-job), inNixShell ? null + task ? null, job ? null, inNixShell ? null, src ? ./., }@args: let auto = fetchGit { url = "https://github.com/coq-community/coq-nix-toolbox.git"; - ref = "master"; + ref = "renaming-ci"; rev = import ./.nix/coq-nix-toolbox.nix; }; in -(import auto ({src = ./.;} // args)).nix-auto +(import auto ({inherit src;} // args)).nix-auto diff --git a/meta.yml b/meta.yml index 804bcc5d3..1d229a92b 100644 --- a/meta.yml +++ b/meta.yml @@ -10,7 +10,7 @@ coqdoc: false nix: true nix_name: mathcomp-analysis nix-default: - ref: master + ref: renaming-ci cachix: - name: coq From cc4e0e8a7f8c826a4e0d0aaa85a430ffffb16a7e Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 17 Mar 2021 01:00:03 +0100 Subject: [PATCH 22/33] up --- .github/workflows/nix-action.yml | 28 ++++++++++++++-------------- .nix/coq-nix-toolbox.nix | 2 +- .nix/fallback-config.nix | 4 ++-- default.nix | 2 +- meta.yml | 12 ++++++------ 5 files changed, 24 insertions(+), 24 deletions(-) diff --git a/.github/workflows/nix-action.yml b/.github/workflows/nix-action.yml index 3c335bd8a..fdecc05fa 100644 --- a/.github/workflows/nix-action.yml +++ b/.github/workflows/nix-action.yml @@ -17,7 +17,7 @@ jobs: - name: Do nothing run: echo "No setup, using meta.yml tasks" - dependencies: + !: runs-on: ubuntu-latest needs: - setup @@ -48,13 +48,13 @@ jobs: with: fetch-depth: 0 - name: Building/fetching current CI target - run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job dependencies + run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "!" main: runs-on: ubuntu-latest needs: - setup - - dependencies + - ! strategy: matrix: task: @@ -81,17 +81,17 @@ jobs: uses: actions/checkout@v2 with: fetch-depth: 0 - - name: Building/fetching previous target dependencies - run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job dependencies + - name: Building/fetching previous target ! + run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "!" - name: Building/fetching current CI target - run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job main + run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "main" - all: + **: runs-on: ubuntu-latest needs: - setup - - dependencies - - main + - ! + - mathcomp-analysis strategy: matrix: task: @@ -118,9 +118,9 @@ jobs: uses: actions/checkout@v2 with: fetch-depth: 0 - - name: Building/fetching previous target dependencies - run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job dependencies - - name: Building/fetching previous target main - run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job main + - name: Building/fetching previous target ! + run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "!" + - name: Building/fetching previous target mathcomp-analysis + run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "mathcomp-analysis" - name: Building/fetching current CI target - run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job all + run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "**" diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index 1a5da2dca..c541b14f3 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -2,4 +2,4 @@ # Follow the instructions on https://github.com/coq-community/templates to regenerate. # However, this rev was not handled by mustache, but by a special eval command # because you picked the option nix-default: ... in meta.yml -"d3227ad13ad0a1a1b971e8a51a8cdd3ade69c821" +"65ab38c883efbbb93e733dfde6184e283923264f" diff --git a/.nix/fallback-config.nix b/.nix/fallback-config.nix index 3e10a0df9..8d1179ebd 100644 --- a/.nix/fallback-config.nix +++ b/.nix/fallback-config.nix @@ -13,11 +13,11 @@ ## The attribute to build, either from nixpkgs ## of from the overlays located in `.nix/coq-overlays` - coq-attribute = "mathcomp-analysis"; + attribute = "mathcomp-analysis"; ## If you want to select a different attribute ## to serve as a basis for nix-shell edit this - # coq-shell-attribute = "mathcomp-analysis"; + # shell-attribute = "mathcomp-analysis"; ## Maybe the shortname of the library is different from ## the name of the nixpkgs attribute, if so, set it here: diff --git a/default.nix b/default.nix index 3757629cc..34b759e12 100644 --- a/default.nix +++ b/default.nix @@ -8,7 +8,7 @@ let auto = fetchGit { url = "https://github.com/coq-community/coq-nix-toolbox.git"; - ref = "renaming-ci"; + ref = "simpler-ci-jobs"; rev = import ./.nix/coq-nix-toolbox.nix; }; in diff --git a/meta.yml b/meta.yml index 1d229a92b..060896ebf 100644 --- a/meta.yml +++ b/meta.yml @@ -10,7 +10,7 @@ coqdoc: false nix: true nix_name: mathcomp-analysis nix-default: - ref: renaming-ci + ref: simpler-ci-jobs cachix: - name: coq @@ -18,14 +18,14 @@ cachix: token: CACHIX_AUTH_TOKEN nix-jobs: -- job: dependencies +- job: "!" - job: main needs: - - dependencies -- job: all + - "!" +- job: "**" needs: - - dependencies - - main + - "!" + - mathcomp-analysis nix-default-task: coq-8.13 nix-tasks: From 450617b356c6ef9d9cd2e50f1e908272f97696bf Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 17 Mar 2021 01:06:31 +0100 Subject: [PATCH 23/33] up --- .github/workflows/nix-action.yml | 41 ++++++++++++++++---------------- meta.yml | 7 +++--- 2 files changed, 25 insertions(+), 23 deletions(-) diff --git a/.github/workflows/nix-action.yml b/.github/workflows/nix-action.yml index fdecc05fa..200723ec0 100644 --- a/.github/workflows/nix-action.yml +++ b/.github/workflows/nix-action.yml @@ -17,16 +17,17 @@ jobs: - name: Do nothing run: echo "No setup, using meta.yml tasks" - !: + "!": + name: dependencies runs-on: ubuntu-latest needs: - setup strategy: matrix: task: - - coq-8.13 - - coq-8.12 - - coq-8.11+multinomials + - "coq-8.13" + - "coq-8.12" + - "coq-8.11+multinomials" steps: - name: Cachix install uses: cachix/install-nix-action@v12 @@ -50,17 +51,17 @@ jobs: - name: Building/fetching current CI target run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "!" - main: + "mathcomp-analysis": runs-on: ubuntu-latest needs: - setup - - ! + - "dependencies" strategy: matrix: task: - - coq-8.13 - - coq-8.12 - - coq-8.11+multinomials + - "coq-8.13" + - "coq-8.12" + - "coq-8.11+multinomials" steps: - name: Cachix install uses: cachix/install-nix-action@v12 @@ -81,23 +82,23 @@ jobs: uses: actions/checkout@v2 with: fetch-depth: 0 - - name: Building/fetching previous target ! - run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "!" + - name: Building/fetching previous target dependencies + run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "dependencies" - name: Building/fetching current CI target - run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "main" + run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "mathcomp-analysis" - **: + "**": runs-on: ubuntu-latest needs: - setup - - ! - - mathcomp-analysis + - "dependencies" + - "mathcomp-analysis" strategy: matrix: task: - - coq-8.13 - - coq-8.12 - - coq-8.11+multinomials + - "coq-8.13" + - "coq-8.12" + - "coq-8.11+multinomials" steps: - name: Cachix install uses: cachix/install-nix-action@v12 @@ -118,8 +119,8 @@ jobs: uses: actions/checkout@v2 with: fetch-depth: 0 - - name: Building/fetching previous target ! - run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "!" + - name: Building/fetching previous target dependencies + run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "dependencies" - name: Building/fetching previous target mathcomp-analysis run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "mathcomp-analysis" - name: Building/fetching current CI target diff --git a/meta.yml b/meta.yml index 060896ebf..01b417bde 100644 --- a/meta.yml +++ b/meta.yml @@ -19,12 +19,13 @@ cachix: nix-jobs: - job: "!" -- job: main + name: dependencies +- job: mathcomp-analysis needs: - - "!" + - dependencies - job: "**" needs: - - "!" + - dependencies - mathcomp-analysis nix-default-task: coq-8.13 From 3c5d41d06b2596dc864bce40eab0f2918a5a9f13 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 17 Mar 2021 01:20:10 +0100 Subject: [PATCH 24/33] up --- .github/workflows/nix-action.yml | 21 ++++++++++----------- .nix/coq-nix-toolbox.nix | 2 +- .nix/fallback-config.nix | 1 - meta.yml | 10 ++++------ 4 files changed, 15 insertions(+), 19 deletions(-) diff --git a/.github/workflows/nix-action.yml b/.github/workflows/nix-action.yml index 200723ec0..5884427c8 100644 --- a/.github/workflows/nix-action.yml +++ b/.github/workflows/nix-action.yml @@ -17,8 +17,7 @@ jobs: - name: Do nothing run: echo "No setup, using meta.yml tasks" - "!": - name: dependencies + "_deps": runs-on: ubuntu-latest needs: - setup @@ -49,13 +48,13 @@ jobs: with: fetch-depth: 0 - name: Building/fetching current CI target - run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "!" + run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "_deps" "mathcomp-analysis": runs-on: ubuntu-latest needs: - setup - - "dependencies" + - "_deps" strategy: matrix: task: @@ -82,16 +81,16 @@ jobs: uses: actions/checkout@v2 with: fetch-depth: 0 - - name: Building/fetching previous target dependencies - run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "dependencies" + - name: Building/fetching previous target _deps + run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "_deps" - name: Building/fetching current CI target run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "mathcomp-analysis" - "**": + "_inTask": runs-on: ubuntu-latest needs: - setup - - "dependencies" + - "_deps" - "mathcomp-analysis" strategy: matrix: @@ -119,9 +118,9 @@ jobs: uses: actions/checkout@v2 with: fetch-depth: 0 - - name: Building/fetching previous target dependencies - run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "dependencies" + - name: Building/fetching previous target _deps + run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "_deps" - name: Building/fetching previous target mathcomp-analysis run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "mathcomp-analysis" - name: Building/fetching current CI target - run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "**" + run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "_inTask" diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index c541b14f3..96502cc40 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -2,4 +2,4 @@ # Follow the instructions on https://github.com/coq-community/templates to regenerate. # However, this rev was not handled by mustache, but by a special eval command # because you picked the option nix-default: ... in meta.yml -"65ab38c883efbbb93e733dfde6184e283923264f" +"74619bd76a14e81017c46148473012ae87c8fa87" diff --git a/.nix/fallback-config.nix b/.nix/fallback-config.nix index 8d1179ebd..e7c2c7f90 100644 --- a/.nix/fallback-config.nix +++ b/.nix/fallback-config.nix @@ -57,6 +57,5 @@ coqPackages."coq".override.version = "8.11"; coqPackages."mathcomp".override.version = "1.12.0"; coqPackages."multinomials".override.version = "1.5.4"; - coqPackages."multinomials".ci.job = "all"; }; } diff --git a/meta.yml b/meta.yml index 01b417bde..a769493aa 100644 --- a/meta.yml +++ b/meta.yml @@ -18,14 +18,13 @@ cachix: token: CACHIX_AUTH_TOKEN nix-jobs: -- job: "!" - name: dependencies +- job: _deps - job: mathcomp-analysis needs: - - dependencies -- job: "**" + - _deps +- job: _inTask needs: - - dependencies + - _deps - mathcomp-analysis nix-default-task: coq-8.13 @@ -57,7 +56,6 @@ nix-tasks: - name: mathcomp version: 1.12.0 - name: multinomials - ci-job: all version: 1.5.4 synopsis: >- From 751623d53e563e3223115aa501442d230e91e371 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 17 Mar 2021 01:32:20 +0100 Subject: [PATCH 25/33] fixup --- .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 96502cc40..a17196e18 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -2,4 +2,4 @@ # Follow the instructions on https://github.com/coq-community/templates to regenerate. # However, this rev was not handled by mustache, but by a special eval command # because you picked the option nix-default: ... in meta.yml -"74619bd76a14e81017c46148473012ae87c8fa87" +"fdebf68e207b6182b7ef35111338ae4d33fa5295" From 2fb41ce489b5a8cc5e8df847b04668ab0a46cba1 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 17 Mar 2021 01:43:47 +0100 Subject: [PATCH 26/33] up --- .nix/coq-nix-toolbox.nix | 2 +- .nix/fallback-config.nix | 2 +- meta.yml | 6 +----- 3 files changed, 3 insertions(+), 7 deletions(-) diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index a17196e18..0c315151c 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -2,4 +2,4 @@ # Follow the instructions on https://github.com/coq-community/templates to regenerate. # However, this rev was not handled by mustache, but by a special eval command # because you picked the option nix-default: ... in meta.yml -"fdebf68e207b6182b7ef35111338ae4d33fa5295" +"d9c97834a0671db81a35984e7e08d2dbdd26c360" diff --git a/.nix/fallback-config.nix b/.nix/fallback-config.nix index e7c2c7f90..2c3b5ae99 100644 --- a/.nix/fallback-config.nix +++ b/.nix/fallback-config.nix @@ -50,7 +50,7 @@ coqPackages."coq-elpi".override.version = "1.9.3"; }; tasks."coq-8.12" = { - coqPackages."coq".override.version = "8.11"; + coqPackages."coq".override.version = "8.12"; coqPackages."mathcomp".override.version = "1.12.0"; }; tasks."coq-8.11+multinomials" = { diff --git a/meta.yml b/meta.yml index a769493aa..3d6cf6b22 100644 --- a/meta.yml +++ b/meta.yml @@ -8,15 +8,12 @@ action: true coqdoc: false nix: true -nix_name: mathcomp-analysis nix-default: ref: simpler-ci-jobs - cachix: - name: coq - name: math-comp token: CACHIX_AUTH_TOKEN - nix-jobs: - job: _deps - job: mathcomp-analysis @@ -26,7 +23,6 @@ nix-jobs: needs: - _deps - mathcomp-analysis - nix-default-task: coq-8.13 nix-tasks: - task: coq-8.13 @@ -46,7 +42,7 @@ nix-tasks: - task: coq-8.12 packages: - name: coq - version: 8.11 + version: 8.12 - name: mathcomp version: 1.12.0 - task: coq-8.11+multinomials From 8a380ff8a450d01b249dd1909d6abdf8f54a8609 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 17 Mar 2021 02:02:02 +0100 Subject: [PATCH 27/33] up --- .github/workflows/nix-action.yml | 4 ++-- .nix/coq-nix-toolbox.nix | 2 +- .nix/fallback-config.nix | 4 ++-- meta.yml | 6 +++--- 4 files changed, 8 insertions(+), 8 deletions(-) diff --git a/.github/workflows/nix-action.yml b/.github/workflows/nix-action.yml index 5884427c8..bdfb96e09 100644 --- a/.github/workflows/nix-action.yml +++ b/.github/workflows/nix-action.yml @@ -86,7 +86,7 @@ jobs: - name: Building/fetching current CI target run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "mathcomp-analysis" - "_inTask": + "_allJobs": runs-on: ubuntu-latest needs: - setup @@ -123,4 +123,4 @@ jobs: - name: Building/fetching previous target mathcomp-analysis run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "mathcomp-analysis" - name: Building/fetching current CI target - run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "_inTask" + run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "_allJobs" diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index 0c315151c..00d98904f 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -2,4 +2,4 @@ # Follow the instructions on https://github.com/coq-community/templates to regenerate. # However, this rev was not handled by mustache, but by a special eval command # because you picked the option nix-default: ... in meta.yml -"d9c97834a0671db81a35984e7e08d2dbdd26c360" +"da2ea25c53aeac9935c5b1f64074d860c13477b3" diff --git a/.nix/fallback-config.nix b/.nix/fallback-config.nix index 2c3b5ae99..eaca48dc9 100644 --- a/.nix/fallback-config.nix +++ b/.nix/fallback-config.nix @@ -44,8 +44,8 @@ tasks."coq-8.13" = { coqPackages."coq".override.version = "8.13"; coqPackages."mathcomp".override.version = "1.12.0"; - coqPackages."real-closed".override.version = "1.1"; - coqPackages."finmap".override.version = "1.5"; + coqPackages."mathcomp-real-closed".override.version = "1.1"; + coqPackages."mathcomp-finmap".override.version = "1.5"; coqPackages."hierarchy-builder".override.version = "1.0.0"; coqPackages."coq-elpi".override.version = "1.9.3"; }; diff --git a/meta.yml b/meta.yml index 3d6cf6b22..ed54d080c 100644 --- a/meta.yml +++ b/meta.yml @@ -19,7 +19,7 @@ nix-jobs: - job: mathcomp-analysis needs: - _deps -- job: _inTask +- job: _allJobs needs: - _deps - mathcomp-analysis @@ -31,9 +31,9 @@ nix-tasks: version: 8.13 - name: mathcomp version: 1.12.0 - - name: real-closed + - name: mathcomp-real-closed version: 1.1 - - name: finmap + - name: mathcomp-finmap version: 1.5 - name: hierarchy-builder version: 1.0.0 From 021977c5393be3283b2eda1c43cffc10a037c685 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 17 Mar 2021 02:08:59 +0100 Subject: [PATCH 28/33] + tgt multinomials+ exclusion --- .github/workflows/nix-action.yml | 36 ++++++++++++++++++++++++++++++++ .nix/fallback-config.nix | 1 + meta.yml | 7 +++++++ 3 files changed, 44 insertions(+) diff --git a/.github/workflows/nix-action.yml b/.github/workflows/nix-action.yml index bdfb96e09..7a1c9cb00 100644 --- a/.github/workflows/nix-action.yml +++ b/.github/workflows/nix-action.yml @@ -86,6 +86,42 @@ jobs: - name: Building/fetching current CI target run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "mathcomp-analysis" + "multinomials": + runs-on: ubuntu-latest + needs: + - setup + - "_deps" + strategy: + matrix: + task: + - "coq-8.13" + - "coq-8.12" + - "coq-8.11+multinomials" + steps: + - name: Cachix install + uses: cachix/install-nix-action@v12 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq + uses: cachix/cachix-action@v8 + with: + # Name of a cachix cache to pull/substitute + name: coq + - name: Cachix setup math-comp + uses: cachix/cachix-action@v8 + with: + # Name of a cachix cache to pull/substitute + name: math-comp + authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}' + - name: Git checkout + uses: actions/checkout@v2 + with: + fetch-depth: 0 + - name: Building/fetching previous target _deps + run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "_deps" + - name: Building/fetching current CI target + run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "multinomials" + "_allJobs": runs-on: ubuntu-latest needs: diff --git a/.nix/fallback-config.nix b/.nix/fallback-config.nix index eaca48dc9..e3fb69ddd 100644 --- a/.nix/fallback-config.nix +++ b/.nix/fallback-config.nix @@ -44,6 +44,7 @@ tasks."coq-8.13" = { coqPackages."coq".override.version = "8.13"; coqPackages."mathcomp".override.version = "1.12.0"; + coqPackages."mathcomp".job = "_excluded"; coqPackages."mathcomp-real-closed".override.version = "1.1"; coqPackages."mathcomp-finmap".override.version = "1.5"; coqPackages."hierarchy-builder".override.version = "1.0.0"; diff --git a/meta.yml b/meta.yml index ed54d080c..2fed7ade1 100644 --- a/meta.yml +++ b/meta.yml @@ -10,19 +10,25 @@ coqdoc: false nix: true nix-default: ref: simpler-ci-jobs + cachix: - name: coq - name: math-comp token: CACHIX_AUTH_TOKEN + nix-jobs: - job: _deps - job: mathcomp-analysis needs: - _deps +- job: multinomials + needs: + - _deps - job: _allJobs needs: - _deps - mathcomp-analysis + nix-default-task: coq-8.13 nix-tasks: - task: coq-8.13 @@ -31,6 +37,7 @@ nix-tasks: version: 8.13 - name: mathcomp version: 1.12.0 + job: _excluded - name: mathcomp-real-closed version: 1.1 - name: mathcomp-finmap From b47f965b0e15e9c8393aee88f504cd1867c40c9f Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 17 Mar 2021 02:29:23 +0100 Subject: [PATCH 29/33] exclusions --- .nix/fallback-config.nix | 10 ++++++++++ meta.yml | 10 ++++++++++ 2 files changed, 20 insertions(+) diff --git a/.nix/fallback-config.nix b/.nix/fallback-config.nix index e3fb69ddd..ced8e0e35 100644 --- a/.nix/fallback-config.nix +++ b/.nix/fallback-config.nix @@ -43,20 +43,30 @@ tasks."coq-8.13" = { coqPackages."coq".override.version = "8.13"; + coqPackages."coq".job = "_excluded"; coqPackages."mathcomp".override.version = "1.12.0"; coqPackages."mathcomp".job = "_excluded"; coqPackages."mathcomp-real-closed".override.version = "1.1"; + coqPackages."mathcomp-real-closed".job = "_excluded"; coqPackages."mathcomp-finmap".override.version = "1.5"; + coqPackages."mathcomp-finmap".job = "_excluded"; coqPackages."hierarchy-builder".override.version = "1.0.0"; + coqPackages."hierarchy-builder".job = "_excluded"; coqPackages."coq-elpi".override.version = "1.9.3"; + coqPackages."coq-elpi".job = "_excluded"; }; tasks."coq-8.12" = { coqPackages."coq".override.version = "8.12"; + coqPackages."coq".job = "_excluded"; coqPackages."mathcomp".override.version = "1.12.0"; + coqPackages."mathcomp".job = "_excluded"; }; tasks."coq-8.11+multinomials" = { coqPackages."coq".override.version = "8.11"; + coqPackages."coq".job = "_excluded"; coqPackages."mathcomp".override.version = "1.12.0"; + coqPackages."mathcomp".job = "_excluded"; coqPackages."multinomials".override.version = "1.5.4"; + coqPackages."multinomials".job = "_excluded"; }; } diff --git a/meta.yml b/meta.yml index 2fed7ade1..02f08db91 100644 --- a/meta.yml +++ b/meta.yml @@ -35,30 +35,40 @@ nix-tasks: packages: - name: coq version: 8.13 + job: _excluded - name: mathcomp version: 1.12.0 job: _excluded - name: mathcomp-real-closed version: 1.1 + job: _excluded - name: mathcomp-finmap version: 1.5 + job: _excluded - name: hierarchy-builder version: 1.0.0 + job: _excluded - name: coq-elpi version: 1.9.3 + job: _excluded - task: coq-8.12 packages: - name: coq version: 8.12 + job: _excluded - name: mathcomp + job: _excluded version: 1.12.0 - task: coq-8.11+multinomials packages: - name: coq + job: _excluded version: 8.11 - name: mathcomp + job: _excluded version: 1.12.0 - name: multinomials + job: _excluded version: 1.5.4 synopsis: >- From d77a222c163ee8515d44cc59a2fa330bd87f00ae Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 17 Mar 2021 02:29:27 +0100 Subject: [PATCH 30/33] Revert "exclusions" This reverts commit eed1c566cdc5e798d5873196fa95e8382eb81d26. --- .nix/fallback-config.nix | 10 ---------- meta.yml | 10 ---------- 2 files changed, 20 deletions(-) diff --git a/.nix/fallback-config.nix b/.nix/fallback-config.nix index ced8e0e35..e3fb69ddd 100644 --- a/.nix/fallback-config.nix +++ b/.nix/fallback-config.nix @@ -43,30 +43,20 @@ tasks."coq-8.13" = { coqPackages."coq".override.version = "8.13"; - coqPackages."coq".job = "_excluded"; coqPackages."mathcomp".override.version = "1.12.0"; coqPackages."mathcomp".job = "_excluded"; coqPackages."mathcomp-real-closed".override.version = "1.1"; - coqPackages."mathcomp-real-closed".job = "_excluded"; coqPackages."mathcomp-finmap".override.version = "1.5"; - coqPackages."mathcomp-finmap".job = "_excluded"; coqPackages."hierarchy-builder".override.version = "1.0.0"; - coqPackages."hierarchy-builder".job = "_excluded"; coqPackages."coq-elpi".override.version = "1.9.3"; - coqPackages."coq-elpi".job = "_excluded"; }; tasks."coq-8.12" = { coqPackages."coq".override.version = "8.12"; - coqPackages."coq".job = "_excluded"; coqPackages."mathcomp".override.version = "1.12.0"; - coqPackages."mathcomp".job = "_excluded"; }; tasks."coq-8.11+multinomials" = { coqPackages."coq".override.version = "8.11"; - coqPackages."coq".job = "_excluded"; coqPackages."mathcomp".override.version = "1.12.0"; - coqPackages."mathcomp".job = "_excluded"; coqPackages."multinomials".override.version = "1.5.4"; - coqPackages."multinomials".job = "_excluded"; }; } diff --git a/meta.yml b/meta.yml index 02f08db91..2fed7ade1 100644 --- a/meta.yml +++ b/meta.yml @@ -35,40 +35,30 @@ nix-tasks: packages: - name: coq version: 8.13 - job: _excluded - name: mathcomp version: 1.12.0 job: _excluded - name: mathcomp-real-closed version: 1.1 - job: _excluded - name: mathcomp-finmap version: 1.5 - job: _excluded - name: hierarchy-builder version: 1.0.0 - job: _excluded - name: coq-elpi version: 1.9.3 - job: _excluded - task: coq-8.12 packages: - name: coq version: 8.12 - job: _excluded - name: mathcomp - job: _excluded version: 1.12.0 - task: coq-8.11+multinomials packages: - name: coq - job: _excluded version: 8.11 - name: mathcomp - job: _excluded version: 1.12.0 - name: multinomials - job: _excluded version: 1.5.4 synopsis: >- From fe53d7b91b63113f7c117631a10a137718fcc398 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 17 Mar 2021 03:05:16 +0100 Subject: [PATCH 31/33] up --- .github/workflows/nix-action.yml | 3 +++ .nix/coq-nix-toolbox.nix | 2 +- meta.yml | 1 + 3 files changed, 5 insertions(+), 1 deletion(-) diff --git a/.github/workflows/nix-action.yml b/.github/workflows/nix-action.yml index 7a1c9cb00..0d7a0843f 100644 --- a/.github/workflows/nix-action.yml +++ b/.github/workflows/nix-action.yml @@ -127,6 +127,7 @@ jobs: needs: - setup - "_deps" + - "multinomials" - "mathcomp-analysis" strategy: matrix: @@ -156,6 +157,8 @@ jobs: fetch-depth: 0 - name: Building/fetching previous target _deps run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "_deps" + - name: Building/fetching previous target multinomials + run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "multinomials" - name: Building/fetching previous target mathcomp-analysis run: nix-build --no-out-link --argstr task "${{ matrix.task }}" --argstr job "mathcomp-analysis" - name: Building/fetching current CI target diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index 00d98904f..b42153574 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -2,4 +2,4 @@ # Follow the instructions on https://github.com/coq-community/templates to regenerate. # However, this rev was not handled by mustache, but by a special eval command # because you picked the option nix-default: ... in meta.yml -"da2ea25c53aeac9935c5b1f64074d860c13477b3" +"868f7ed993f83f82388189257301f34e832933e0" diff --git a/meta.yml b/meta.yml index 2fed7ade1..992485693 100644 --- a/meta.yml +++ b/meta.yml @@ -27,6 +27,7 @@ nix-jobs: - job: _allJobs needs: - _deps + - multinomials - mathcomp-analysis nix-default-task: coq-8.13 From b24f58228891ebfb46f6485bfb3ff86475a617a5 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 17 Mar 2021 03:35:34 +0100 Subject: [PATCH 32/33] update --- .github/workflows/docker-action.yml | 3 +-- .nix/fallback-config.nix | 2 +- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 2d1dbfdd7..b06387ed1 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -20,10 +20,9 @@ jobs: - 'mathcomp/mathcomp:1.12.0-coq-8.11' - 'mathcomp/mathcomp:1.12.0-coq-8.12' - 'mathcomp/mathcomp:1.12.0-coq-8.13' - - 'mathcomp/mathcomp:1.12.0-coq-dev' - 'mathcomp/mathcomp-dev:coq-8.11' - 'mathcomp/mathcomp-dev:coq-8.12' - - 'mathcomp/mathcomp-dev:coq-dev' + - 'mathcomp/mathcomp-dev:coq-8.13' fail-fast: false steps: - uses: actions/checkout@v2 diff --git a/.nix/fallback-config.nix b/.nix/fallback-config.nix index e3fb69ddd..e10c47339 100644 --- a/.nix/fallback-config.nix +++ b/.nix/fallback-config.nix @@ -38,7 +38,7 @@ ## Select a task to build by default in the following `tasks` set ## It will be used when typing nix-shell or nix-build without argument ## defaults to "default" - select = "coq-8.13"; + default-task = "coq-8.13"; tasks."coq-8.13" = {}; tasks."coq-8.13" = { From 17c47cf99aa15548eb3edf247d37eb8b1bc1dd3f Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 17 Mar 2021 03:35:34 +0100 Subject: [PATCH 33/33] update --- .nix/coq-nix-toolbox.nix | 2 +- default.nix | 2 +- meta.yml | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index b42153574..632ecf6e3 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -2,4 +2,4 @@ # Follow the instructions on https://github.com/coq-community/templates to regenerate. # However, this rev was not handled by mustache, but by a special eval command # because you picked the option nix-default: ... in meta.yml -"868f7ed993f83f82388189257301f34e832933e0" +"0ea896bc753c0770331911381d78b2fcdfa48c66" diff --git a/default.nix b/default.nix index 34b759e12..446181f1a 100644 --- a/default.nix +++ b/default.nix @@ -8,7 +8,7 @@ let auto = fetchGit { url = "https://github.com/coq-community/coq-nix-toolbox.git"; - ref = "simpler-ci-jobs"; + ref = "simplify_allJobs"; rev = import ./.nix/coq-nix-toolbox.nix; }; in diff --git a/meta.yml b/meta.yml index 992485693..e317c36ec 100644 --- a/meta.yml +++ b/meta.yml @@ -9,7 +9,7 @@ coqdoc: false nix: true nix-default: - ref: simpler-ci-jobs + ref: simplify_allJobs cachix: - name: coq