From 1162f7cf8629bd72b794a93b168c1d2936cf2778 Mon Sep 17 00:00:00 2001 From: Sebastian Ertel Date: Wed, 13 Mar 2024 14:37:10 +0100 Subject: [PATCH 01/33] Switching to the existing nix tooling. --- flake.nix | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/flake.nix b/flake.nix index cf4bfc64..1d8d68ba 100644 --- a/flake.nix +++ b/flake.nix @@ -9,19 +9,21 @@ let extructures' = coqPackages.extructures.override { version = "0.4.0"; }; in - stdenv.mkDerivation { + coqPackages.mkCoqDerivation { pname = "ssprove"; + owner = "SSProve"; version = "0.0.1"; - src = ./.; - nativeBuildInputs = [ which coq.ocamlPackages.findlib ] ++ - (with coqPackages; [ + propagatedBuildInputs = (with coqPackages; [ equations mathcomp-analysis mathcomp-ssreflect deriving ]) ++ [extructures']; - buildInputs = [ coq ]; + meta = { + description = "A foundational framework for modular cryptographic proofs in Coq "; + license = licenses.mit; + }; }; in { inherit mkDrv; } // flake-utils.lib.eachDefaultSystem (system: From 649c250204307a6f70c73dcf6682ec86a1c6eb4f Mon Sep 17 00:00:00 2001 From: Sebastian Ertel Date: Wed, 13 Mar 2024 14:49:08 +0100 Subject: [PATCH 02/33] lib is not available yet. --- flake.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/flake.nix b/flake.nix index 1d8d68ba..88079eca 100644 --- a/flake.nix +++ b/flake.nix @@ -22,7 +22,7 @@ ++ [extructures']; meta = { description = "A foundational framework for modular cryptographic proofs in Coq "; - license = licenses.mit; + # license = licenses.mit; TODO load lib }; }; in { inherit mkDrv; } // From dfbc7c0190aa97b8f7c90a0dbb52de5e09307cf1 Mon Sep 17 00:00:00 2001 From: Sebastian Ertel Date: Wed, 13 Mar 2024 16:36:42 +0100 Subject: [PATCH 03/33] coqPackages already contains the proper coq version. --- flake.nix | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/flake.nix b/flake.nix index 88079eca..de148b53 100644 --- a/flake.nix +++ b/flake.nix @@ -5,7 +5,7 @@ }; outputs = { self, nixpkgs, flake-utils }: let - mkDrv = { stdenv, which, coqPackages, coq } : + mkDrv = { stdenv, which, coqPackages } : let extructures' = coqPackages.extructures.override { version = "0.4.0"; }; in @@ -13,16 +13,15 @@ pname = "ssprove"; owner = "SSProve"; version = "0.0.1"; - propagatedBuildInputs = (with coqPackages; [ - equations + propagatedBuildInputs = + (with coqPackages; [equations mathcomp-analysis mathcomp-ssreflect - deriving - ]) - ++ [extructures']; + deriving]) + ++ [extructures']; meta = { description = "A foundational framework for modular cryptographic proofs in Coq "; - # license = licenses.mit; TODO load lib + license = coqPackages.lib.licenses.mit; }; }; in { inherit mkDrv; } // @@ -35,7 +34,6 @@ let args = { inherit (pkgs) stdenv which; - coq = pkgs.coq_8_18; coqPackages = pkgs.coqPackages_8_18.overrideScope (self: super: { mathcomp = super.mathcomp.override { version = "2.1.0"; }; From ac206660c99514a10d5f6e306fcfc0c53b21f717 Mon Sep 17 00:00:00 2001 From: Sebastian Ertel Date: Wed, 13 Mar 2024 18:12:33 +0100 Subject: [PATCH 04/33] for flakes the src of the library must be flake input. --- flake.nix | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/flake.nix b/flake.nix index de148b53..0e99c5e8 100644 --- a/flake.nix +++ b/flake.nix @@ -8,8 +8,7 @@ mkDrv = { stdenv, which, coqPackages } : let extructures' = coqPackages.extructures.override { version = "0.4.0"; }; - in - coqPackages.mkCoqDerivation { + d = coqPackages.mkCoqDerivation { pname = "ssprove"; owner = "SSProve"; version = "0.0.1"; @@ -19,11 +18,15 @@ mathcomp-ssreflect deriving]) ++ [extructures']; - meta = { + meta = { description = "A foundational framework for modular cryptographic proofs in Coq "; license = coqPackages.lib.licenses.mit; + }; }; - }; + in + # getting this the flake-style means the code is already there + d.overrideAttrs (oldAttrs: { src = "./."; }) + ; in { inherit mkDrv; } // flake-utils.lib.eachDefaultSystem (system: let From 204f6e932427e91d81322554b45c2404f9e7408f Mon Sep 17 00:00:00 2001 From: Sebastian Ertel Date: Wed, 13 Mar 2024 21:01:27 +0100 Subject: [PATCH 05/33] the unpackPhase needs to be skipped too --- flake.nix | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/flake.nix b/flake.nix index 0e99c5e8..d7058bf8 100644 --- a/flake.nix +++ b/flake.nix @@ -25,8 +25,10 @@ }; in # getting this the flake-style means the code is already there - d.overrideAttrs (oldAttrs: { src = "./."; }) - ; + d.overrideAttrs (oldAttrs: { + src = "./."; + unpackPhase = "true"; + }); in { inherit mkDrv; } // flake-utils.lib.eachDefaultSystem (system: let From 2916ecf121a2b4901b657970c92cb1bd43ffaac7 Mon Sep 17 00:00:00 2001 From: Sebastian Ertel Date: Thu, 14 Mar 2024 21:47:18 +0100 Subject: [PATCH 06/33] need to set the native build inputs for the shell to work. --- flake.lock | 12 ++++++------ flake.nix | 8 +++++++- 2 files changed, 13 insertions(+), 7 deletions(-) diff --git a/flake.lock b/flake.lock index 49c856c9..5bca994c 100644 --- a/flake.lock +++ b/flake.lock @@ -5,11 +5,11 @@ "systems": "systems" }, "locked": { - "lastModified": 1705309234, - "narHash": "sha256-uNRRNRKmJyCRC/8y1RqBkqWBLM034y4qN7EprSdmgyA=", + "lastModified": 1710146030, + "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=", "owner": "numtide", "repo": "flake-utils", - "rev": "1ef2e671c3b0c19053962c07dbda38332dcebf26", + "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a", "type": "github" }, "original": { @@ -20,11 +20,11 @@ }, "nixpkgs": { "locked": { - "lastModified": 1707824078, - "narHash": "sha256-Au3wLi2d06bU7TDvahP2jIEeKwmjAxKHqi8l2uiBkGA=", + "lastModified": 1710410081, + "narHash": "sha256-5n3OrpL8V+isTDMwlGNjDwA/57R/HH0X7NIsvFFWUUs=", "owner": "nixos", "repo": "nixpkgs", - "rev": "99d7b32e4cfdaf763d9335b4d9ecf4415cbdc405", + "rev": "1a399f214e41e079f0edba674a415816286d1fbd", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index d7058bf8..7dd6cbeb 100644 --- a/flake.nix +++ b/flake.nix @@ -12,13 +12,19 @@ pname = "ssprove"; owner = "SSProve"; version = "0.0.1"; + nativeBuildInputs = + (with coqPackages; [equations + mathcomp-analysis + mathcomp-ssreflect + deriving]) + ++ [extructures']; propagatedBuildInputs = (with coqPackages; [equations mathcomp-analysis mathcomp-ssreflect deriving]) ++ [extructures']; - meta = { + meta = { description = "A foundational framework for modular cryptographic proofs in Coq "; license = coqPackages.lib.licenses.mit; }; From f4da62d357360632981a04d49f3f584750138bbb Mon Sep 17 00:00:00 2001 From: Sebastian Ertel Date: Fri, 15 Mar 2024 10:33:52 +0100 Subject: [PATCH 07/33] Indeed I do not need the nativeBuildInputs. That was a bug in the flake script. --- flake.nix | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/flake.nix b/flake.nix index 7dd6cbeb..da2bc050 100644 --- a/flake.nix +++ b/flake.nix @@ -12,12 +12,6 @@ pname = "ssprove"; owner = "SSProve"; version = "0.0.1"; - nativeBuildInputs = - (with coqPackages; [equations - mathcomp-analysis - mathcomp-ssreflect - deriving]) - ++ [extructures']; propagatedBuildInputs = (with coqPackages; [equations mathcomp-analysis @@ -57,7 +51,7 @@ packages = (with pkgs; [ coq gnumake ]) ++ - (with ssprove'; nativeBuildInputs); + (with ssprove'; propagatedBuildInputs); }; }); } From 51c3f2bc8683827983d70d84b2a3c83358eb25bf Mon Sep 17 00:00:00 2001 From: Sebastian Ertel Date: Fri, 15 Mar 2024 15:59:52 +0100 Subject: [PATCH 08/33] still testing --- flake.nix | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/flake.nix b/flake.nix index da2bc050..04f8c7e6 100644 --- a/flake.nix +++ b/flake.nix @@ -26,8 +26,8 @@ in # getting this the flake-style means the code is already there d.overrideAttrs (oldAttrs: { - src = "./."; - unpackPhase = "true"; +# src = "./."; +# unpackPhase = "true"; }); in { inherit mkDrv; } // flake-utils.lib.eachDefaultSystem (system: From cbfa5f597a619290fdccb2831458e1ea2aa4cf84 Mon Sep 17 00:00:00 2001 From: Sebastian Ertel Date: Fri, 15 Mar 2024 16:05:17 +0100 Subject: [PATCH 09/33] src --- flake.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/flake.nix b/flake.nix index 04f8c7e6..00832b35 100644 --- a/flake.nix +++ b/flake.nix @@ -26,7 +26,7 @@ in # getting this the flake-style means the code is already there d.overrideAttrs (oldAttrs: { -# src = "./."; + src = "./."; # unpackPhase = "true"; }); in { inherit mkDrv; } // From 97012d9e47cddda857cb6ff291d1365c8fa3274e Mon Sep 17 00:00:00 2001 From: Sebastian Ertel Date: Mon, 18 Mar 2024 14:18:32 +0100 Subject: [PATCH 10/33] no unpacking --- flake.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/flake.nix b/flake.nix index 00832b35..5f936018 100644 --- a/flake.nix +++ b/flake.nix @@ -27,7 +27,7 @@ # getting this the flake-style means the code is already there d.overrideAttrs (oldAttrs: { src = "./."; -# unpackPhase = "true"; + unpackPhase = ''true''; }); in { inherit mkDrv; } // flake-utils.lib.eachDefaultSystem (system: From 8daeca2e29d84dc26460ae71233612ef98f0227d Mon Sep 17 00:00:00 2001 From: Sebastian Ertel Date: Mon, 18 Mar 2024 20:59:43 +0100 Subject: [PATCH 11/33] adding Coq itself to the propagated build inputs to hopefully enable the setup hook of Coq for SSProve. --- flake.nix | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/flake.nix b/flake.nix index 5f936018..2c9348c3 100644 --- a/flake.nix +++ b/flake.nix @@ -5,7 +5,7 @@ }; outputs = { self, nixpkgs, flake-utils }: let - mkDrv = { stdenv, which, coqPackages } : + mkDrv = { stdenv, which, coqPackages, coq } : let extructures' = coqPackages.extructures.override { version = "0.4.0"; }; d = coqPackages.mkCoqDerivation { @@ -13,6 +13,8 @@ owner = "SSProve"; version = "0.0.1"; propagatedBuildInputs = + [ coq ] + ++ (with coqPackages; [equations mathcomp-analysis mathcomp-ssreflect @@ -44,12 +46,13 @@ mathcomp = super.mathcomp.override { version = "2.1.0"; }; mathcomp-analysis = super.mathcomp-analysis.override { version = "1.0.0"; }; }); + coq = pkgs.coq_8_18; }; ssprove' = mkDrv args; in pkgs.mkShell { packages = - (with pkgs; [ coq gnumake ]) + (with pkgs; [ gnumake ]) ++ (with ssprove'; propagatedBuildInputs); }; From 0c86617c3d7c8cdf0cf1a10d6d79d67511579f8a Mon Sep 17 00:00:00 2001 From: Sebastian Ertel Date: Tue, 19 Mar 2024 21:10:07 +0100 Subject: [PATCH 12/33] adding the stdenv version for testing and debugging --- flake.nix | 20 +++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) diff --git a/flake.nix b/flake.nix index 2c9348c3..f2929661 100644 --- a/flake.nix +++ b/flake.nix @@ -31,7 +31,25 @@ src = "./."; unpackPhase = ''true''; }); - in { inherit mkDrv; } // + mkDrvFromStdenv = { stdenv, which, coqPackages, coq } : + let + extructures' = coqPackages.extructures.override { version = "0.4.0"; }; + in + stdenv.mkDerivation { + pname = "ssprove"; + version = "0.0.1"; + src = ./.; + buildInputs = [ which coq.ocamlPackages.findlib coq ] ++ + (with coqPackages; [ + equations + mathcomp-analysis + mathcomp-ssreflect + deriving + ]) + ++ [extructures']; + propagatedBuildInputs = [ coq ]; + }; + in { inherit mkDrv mkDrvFromStdenv; } // flake-utils.lib.eachDefaultSystem (system: let pkgs = nixpkgs.legacyPackages.${system}; From 86dd4429a7080c3dc92d9f84b310d1af2f91c3e7 Mon Sep 17 00:00:00 2001 From: Sebastian Ertel Date: Wed, 20 Mar 2024 10:43:34 +0100 Subject: [PATCH 13/33] no quotes --- flake.nix | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/flake.nix b/flake.nix index f2929661..4abff9c7 100644 --- a/flake.nix +++ b/flake.nix @@ -28,8 +28,8 @@ in # getting this the flake-style means the code is already there d.overrideAttrs (oldAttrs: { - src = "./."; - unpackPhase = ''true''; + src = ./.; + #unpackPhase = ''true''; }); mkDrvFromStdenv = { stdenv, which, coqPackages, coq } : let From 51b7d413f394a16d3e3eb7a27bd864525a5592e1 Mon Sep 17 00:00:00 2001 From: Sebastian Ertel Date: Wed, 20 Mar 2024 16:22:26 +0100 Subject: [PATCH 14/33] the quotes around the path were the problem. now everything is working. cleanup. --- flake.nix | 23 ++--------------------- 1 file changed, 2 insertions(+), 21 deletions(-) diff --git a/flake.nix b/flake.nix index 4abff9c7..22e44776 100644 --- a/flake.nix +++ b/flake.nix @@ -29,27 +29,8 @@ # getting this the flake-style means the code is already there d.overrideAttrs (oldAttrs: { src = ./.; - #unpackPhase = ''true''; - }); - mkDrvFromStdenv = { stdenv, which, coqPackages, coq } : - let - extructures' = coqPackages.extructures.override { version = "0.4.0"; }; - in - stdenv.mkDerivation { - pname = "ssprove"; - version = "0.0.1"; - src = ./.; - buildInputs = [ which coq.ocamlPackages.findlib coq ] ++ - (with coqPackages; [ - equations - mathcomp-analysis - mathcomp-ssreflect - deriving - ]) - ++ [extructures']; - propagatedBuildInputs = [ coq ]; - }; - in { inherit mkDrv mkDrvFromStdenv; } // + }); + in { inherit mkDrv; } // flake-utils.lib.eachDefaultSystem (system: let pkgs = nixpkgs.legacyPackages.${system}; From 8a0d34ffa5650c87de5ffe3a4980180551c31ea8 Mon Sep 17 00:00:00 2001 From: Sebastian Ertel Date: Fri, 12 Apr 2024 14:23:50 +0200 Subject: [PATCH 15/33] CI setup --- .github/workflows/nix-action-8.17.yml | 188 +++++++++++++++++++++++++ .github/workflows/nix-action-8.18.yml | 192 ++++++++++++++++++++++++++ .github/workflows/nix-action-8.19.yml | 192 ++++++++++++++++++++++++++ .nix/config.nix | 75 ++++++++++ .nix/coq-nix-toolbox.nix | 1 + default.nix | 12 ++ 6 files changed, 660 insertions(+) create mode 100644 .github/workflows/nix-action-8.17.yml create mode 100644 .github/workflows/nix-action-8.18.yml create mode 100644 .github/workflows/nix-action-8.19.yml create mode 100644 .nix/config.nix create mode 100644 .nix/coq-nix-toolbox.nix create mode 100644 default.nix diff --git a/.github/workflows/nix-action-8.17.yml b/.github/workflows/nix-action-8.17.yml new file mode 100644 index 00000000..2506a386 --- /dev/null +++ b/.github/workflows/nix-action-8.17.yml @@ -0,0 +1,188 @@ +jobs: + coq: + needs: [] + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq + uses: cachix/cachix-action@v12 + with: + extraPullNames: coq-community, math-comp + name: coq + - id: stepCheck + name: Checking presence of CI target coq + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"8.17\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ + s/.*/built/\") >> $GITHUB_OUTPUT\n" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr + job "coq" + mathcomp: + needs: + - coq + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq + uses: cachix/cachix-action@v12 + with: + extraPullNames: coq-community, math-comp + name: coq + - id: stepCheck + name: Checking presence of CI target mathcomp + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"8.17\" --argstr job \"mathcomp\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ + s/.*/built/\") >> $GITHUB_OUTPUT\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr + job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr + job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-fingroup' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr + job "mathcomp-fingroup" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr + job "mathcomp-algebra" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-solvable' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr + job "mathcomp-solvable" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-field' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr + job "mathcomp-field" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-character' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr + job "mathcomp-character" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr + job "mathcomp" + ssprove: + needs: + - coq + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq + uses: cachix/cachix-action@v12 + with: + extraPullNames: coq-community, math-comp + name: coq + - id: stepCheck + name: Checking presence of CI target ssprove + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"8.17\" --argstr job \"ssprove\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ + s/.*/built/\") >> $GITHUB_OUTPUT\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr + job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr + job "ssprove" +name: Nix CI for bundle 8.17 +'on': + pull_request: + paths: + - .github/workflows/nix-action-8.17.yml + pull_request_target: + paths-ignore: + - .github/workflows/nix-action-8.17.yml + types: + - opened + - synchronize + - reopened + push: + branches: + - master diff --git a/.github/workflows/nix-action-8.18.yml b/.github/workflows/nix-action-8.18.yml new file mode 100644 index 00000000..e690c4d0 --- /dev/null +++ b/.github/workflows/nix-action-8.18.yml @@ -0,0 +1,192 @@ +jobs: + coq: + needs: [] + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq + uses: cachix/cachix-action@v12 + with: + extraPullNames: coq-community, math-comp + name: coq + - id: stepCheck + name: Checking presence of CI target coq + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"8.18\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ + s/.*/built/\") >> $GITHUB_OUTPUT\n" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "coq" + mathcomp: + needs: + - coq + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq + uses: cachix/cachix-action@v12 + with: + extraPullNames: coq-community, math-comp + name: coq + - id: stepCheck + name: Checking presence of CI target mathcomp + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"8.18\" --argstr job \"mathcomp\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ + s/.*/built/\") >> $GITHUB_OUTPUT\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-fingroup' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "mathcomp-fingroup" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "mathcomp-algebra" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-solvable' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "mathcomp-solvable" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-field' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "mathcomp-field" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-character' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "mathcomp-character" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "hierarchy-builder" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "mathcomp" + ssprove: + needs: + - coq + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq + uses: cachix/cachix-action@v12 + with: + extraPullNames: coq-community, math-comp + name: coq + - id: stepCheck + name: Checking presence of CI target ssprove + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"8.18\" --argstr job \"ssprove\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ + s/.*/built/\") >> $GITHUB_OUTPUT\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "ssprove" +name: Nix CI for bundle 8.18 +'on': + pull_request: + paths: + - .github/workflows/nix-action-8.18.yml + pull_request_target: + paths-ignore: + - .github/workflows/nix-action-8.18.yml + types: + - opened + - synchronize + - reopened + push: + branches: + - master diff --git a/.github/workflows/nix-action-8.19.yml b/.github/workflows/nix-action-8.19.yml new file mode 100644 index 00000000..3fd7e162 --- /dev/null +++ b/.github/workflows/nix-action-8.19.yml @@ -0,0 +1,192 @@ +jobs: + coq: + needs: [] + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq + uses: cachix/cachix-action@v12 + with: + extraPullNames: coq-community, math-comp + name: coq + - id: stepCheck + name: Checking presence of CI target coq + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"8.19\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ + s/.*/built/\") >> $GITHUB_OUTPUT\n" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "coq" + mathcomp: + needs: + - coq + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq + uses: cachix/cachix-action@v12 + with: + extraPullNames: coq-community, math-comp + name: coq + - id: stepCheck + name: Checking presence of CI target mathcomp + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"8.19\" --argstr job \"mathcomp\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ + s/.*/built/\") >> $GITHUB_OUTPUT\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-fingroup' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-fingroup" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-algebra" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-solvable' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-solvable" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-field' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-field" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-character' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-character" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "hierarchy-builder" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp" + ssprove: + needs: + - coq + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq + uses: cachix/cachix-action@v12 + with: + extraPullNames: coq-community, math-comp + name: coq + - id: stepCheck + name: Checking presence of CI target ssprove + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"8.19\" --argstr job \"ssprove\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ + s/.*/built/\") >> $GITHUB_OUTPUT\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "ssprove" +name: Nix CI for bundle 8.19 +'on': + pull_request: + paths: + - .github/workflows/nix-action-8.19.yml + pull_request_target: + paths-ignore: + - .github/workflows/nix-action-8.19.yml + types: + - opened + - synchronize + - reopened + push: + branches: + - master diff --git a/.nix/config.nix b/.nix/config.nix new file mode 100644 index 00000000..d0b985c8 --- /dev/null +++ b/.nix/config.nix @@ -0,0 +1,75 @@ +{ + ## DO NOT CHANGE THIS + format = "1.0.0"; + ## unless you made an automated or manual update + ## to another supported format. + + ## The attribute to build from the local sources, + ## either using nixpkgs data or the overlays located in `.nix/coq-overlays` + ## Will determine the default main-job of the bundles defined below + attribute = "ssprove"; + + ## If you want to select a different attribute (to build from the local sources as well) + ## when calling `nix-shell` and `nix-build` without the `--argstr job` argument + # shell-attribute = "{{nix_name}}"; + + ## Maybe the shortname of the library is different from + ## the name of the nixpkgs attribute, if so, set it here: + # pname = "{{shortname}}"; + + ## Lists the dependencies, phrased in terms of nix attributes. + ## No need to list Coq, it is already included. + ## These dependencies will systematically be added to the currently + ## known dependencies, if any more than Coq. + ## /!\ Remove this field as soon as the package is available on nixpkgs. + ## /!\ Manual overlays in `.nix/coq-overlays` should be preferred then. + # buildInputs = [ ]; + + ## Indicate the relative location of your _CoqProject + ## If not specified, it defaults to "_CoqProject" + # coqproject = "_CoqProject"; + + ## select an entry to build in the following `bundles` set + ## defaults to "default" + default-bundle = "8.19"; + + ## write one `bundles.name` attribute set per + ## alternative configuration + ## When generating GitHub Action CI, one workflow file + ## will be created per bundle + bundles."8.17".coqPackages = { + coq.override.version = "8.17"; + mathcomp.override.version = "1.17.0"; + mathcomp-analysis.override.version = "0.6.0"; + }; + bundles."8.18".coqPackages = { + coq.override.version = "8.18"; + mathcomp.override.version = "2.1.0"; + mathcomp-analysis.override.version = "1.0.0"; + }; + bundles."8.19".coqPackages = { + coq.override.version = "8.19"; + mathcomp.override.version = "2.2.0"; + mathcomp-analysis.override.version = "1.0.0"; + }; + + ## Cachix caches to use in CI + ## Below we list some standard ones + cachix.coq = {}; + cachix.math-comp = {}; + cachix.coq-community = {}; + + ## If you have write access to one of these caches you can + ## provide the auth token or signing key through a secret + ## variable on GitHub. Then, you should give the variable + ## name here. For instance, coq-community projects can use + ## the following line instead of the one above: + # cachix.coq-community.authToken = "CACHIX_AUTH_TOKEN"; + + ## Or if you have a signing key for a given Cachix cache: + # cachix.my-cache.signingKey = "CACHIX_SIGNING_KEY" + + ## Note that here, CACHIX_AUTH_TOKEN and CACHIX_SIGNING_KEY + ## are the names of secret variables. They are set in + ## GitHub's web interface. +} diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix new file mode 100644 index 00000000..c3398402 --- /dev/null +++ b/.nix/coq-nix-toolbox.nix @@ -0,0 +1 @@ +"544d3d77a4a0f4fef30ad7825d2a8d2255abb0e3" diff --git a/default.nix b/default.nix new file mode 100644 index 00000000..1a24d7a1 --- /dev/null +++ b/default.nix @@ -0,0 +1,12 @@ +{ config ? {}, withEmacs ? false, print-env ? false, do-nothing ? false, + update-nixpkgs ? false, ci-matrix ? false, + override ? {}, ocaml-override ? {}, global-override ? {}, + bundle ? null, job ? null, inNixShell ? null, src ? ./., +}@args: +let auto = fetchGit { + url = "https://github.com/coq-community/coq-nix-toolbox.git"; + ref = "master"; + rev = import .nix/coq-nix-toolbox.nix; +}; +in +import auto ({inherit src;} // args) From 584532c2be973b2011f1a0098c2bab95564b3a99 Mon Sep 17 00:00:00 2001 From: Sebastian Ertel Date: Fri, 12 Apr 2024 14:35:15 +0200 Subject: [PATCH 16/33] make the CI jobs manually executable. --- .github/workflows/nix-action-8.17.yml | 3 +++ .github/workflows/nix-action-8.18.yml | 3 +++ .github/workflows/nix-action-8.19.yml | 3 +++ 3 files changed, 9 insertions(+) diff --git a/.github/workflows/nix-action-8.17.yml b/.github/workflows/nix-action-8.17.yml index 2506a386..c7391788 100644 --- a/.github/workflows/nix-action-8.17.yml +++ b/.github/workflows/nix-action-8.17.yml @@ -1,3 +1,6 @@ +on: + workflow_dispatch: + jobs: coq: needs: [] diff --git a/.github/workflows/nix-action-8.18.yml b/.github/workflows/nix-action-8.18.yml index e690c4d0..3a572b64 100644 --- a/.github/workflows/nix-action-8.18.yml +++ b/.github/workflows/nix-action-8.18.yml @@ -1,3 +1,6 @@ +on: + workflow_dispatch: + jobs: coq: needs: [] diff --git a/.github/workflows/nix-action-8.19.yml b/.github/workflows/nix-action-8.19.yml index 3fd7e162..daf6a25e 100644 --- a/.github/workflows/nix-action-8.19.yml +++ b/.github/workflows/nix-action-8.19.yml @@ -1,3 +1,6 @@ +on: + workflow_dispatch: + jobs: coq: needs: [] From 71124b31f194afed01c5aac7c8381e6b24af4c37 Mon Sep 17 00:00:00 2001 From: Sebastian Ertel Date: Fri, 12 Apr 2024 14:38:26 +0200 Subject: [PATCH 17/33] fix. --- .github/workflows/nix-action-8.17.yml | 4 +--- .github/workflows/nix-action-8.18.yml | 4 +--- .github/workflows/nix-action-8.19.yml | 1 + 3 files changed, 3 insertions(+), 6 deletions(-) diff --git a/.github/workflows/nix-action-8.17.yml b/.github/workflows/nix-action-8.17.yml index c7391788..e466ee69 100644 --- a/.github/workflows/nix-action-8.17.yml +++ b/.github/workflows/nix-action-8.17.yml @@ -1,6 +1,3 @@ -on: - workflow_dispatch: - jobs: coq: needs: [] @@ -189,3 +186,4 @@ name: Nix CI for bundle 8.17 push: branches: - master + workflow_dispatch: diff --git a/.github/workflows/nix-action-8.18.yml b/.github/workflows/nix-action-8.18.yml index 3a572b64..b77d7b32 100644 --- a/.github/workflows/nix-action-8.18.yml +++ b/.github/workflows/nix-action-8.18.yml @@ -1,6 +1,3 @@ -on: - workflow_dispatch: - jobs: coq: needs: [] @@ -193,3 +190,4 @@ name: Nix CI for bundle 8.18 push: branches: - master + workflow_dispatch: diff --git a/.github/workflows/nix-action-8.19.yml b/.github/workflows/nix-action-8.19.yml index daf6a25e..7a4bfce9 100644 --- a/.github/workflows/nix-action-8.19.yml +++ b/.github/workflows/nix-action-8.19.yml @@ -193,3 +193,4 @@ name: Nix CI for bundle 8.19 push: branches: - master + workflow_dispatch: From 3ac61c8942b2530b16b3864dacfebcefeb3a8904 Mon Sep 17 00:00:00 2001 From: Sebastian Ertel Date: Fri, 12 Apr 2024 14:40:23 +0200 Subject: [PATCH 18/33] forgotten fix. --- .github/workflows/nix-action-8.19.yml | 3 --- 1 file changed, 3 deletions(-) diff --git a/.github/workflows/nix-action-8.19.yml b/.github/workflows/nix-action-8.19.yml index 7a4bfce9..de4fcdaf 100644 --- a/.github/workflows/nix-action-8.19.yml +++ b/.github/workflows/nix-action-8.19.yml @@ -1,6 +1,3 @@ -on: - workflow_dispatch: - jobs: coq: needs: [] From 98bcf59c3c2e9b7e8e322e74796c10fe28e78f36 Mon Sep 17 00:00:00 2001 From: Sebastian Ertel Date: Fri, 3 May 2024 16:03:29 +0200 Subject: [PATCH 19/33] jobs generated against the SSProve package in nixpkgs --- .github/workflows/nix-action-8.17.yml | 189 -------------------------- .github/workflows/nix-action-8.18.yml | 69 +++++++++- .github/workflows/nix-action-8.19.yml | 69 +++++++++- .nix/config.nix | 16 ++- flake.nix | 93 ++++++------- 5 files changed, 188 insertions(+), 248 deletions(-) delete mode 100644 .github/workflows/nix-action-8.17.yml diff --git a/.github/workflows/nix-action-8.17.yml b/.github/workflows/nix-action-8.17.yml deleted file mode 100644 index e466ee69..00000000 --- a/.github/workflows/nix-action-8.17.yml +++ /dev/null @@ -1,189 +0,0 @@ -jobs: - coq: - needs: [] - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ - \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ - \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ - \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ - \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq - uses: cachix/cachix-action@v12 - with: - extraPullNames: coq-community, math-comp - name: coq - - id: stepCheck - name: Checking presence of CI target coq - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.17\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ - s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr - job "coq" - mathcomp: - needs: - - coq - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ - \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ - \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ - \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ - \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq - uses: cachix/cachix-action@v12 - with: - extraPullNames: coq-community, math-comp - name: coq - - id: stepCheck - name: Checking presence of CI target mathcomp - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.17\" --argstr job \"mathcomp\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ - s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr - job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr - job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr - job "mathcomp-fingroup" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr - job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-solvable' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr - job "mathcomp-solvable" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr - job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-character' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr - job "mathcomp-character" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr - job "mathcomp" - ssprove: - needs: - - coq - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ - \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ - \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ - \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ - \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq - uses: cachix/cachix-action@v12 - with: - extraPullNames: coq-community, math-comp - name: coq - - id: stepCheck - name: Checking presence of CI target ssprove - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.17\" --argstr job \"ssprove\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ - s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr - job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr - job "ssprove" -name: Nix CI for bundle 8.17 -'on': - pull_request: - paths: - - .github/workflows/nix-action-8.17.yml - pull_request_target: - paths-ignore: - - .github/workflows/nix-action-8.17.yml - types: - - opened - - synchronize - - reopened - push: - branches: - - master - workflow_dispatch: diff --git a/.github/workflows/nix-action-8.18.yml b/.github/workflows/nix-action-8.18.yml index b77d7b32..b92e2688 100644 --- a/.github/workflows/nix-action-8.18.yml +++ b/.github/workflows/nix-action-8.18.yml @@ -124,6 +124,73 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr job "mathcomp" + mathcomp-analysis: + needs: + - coq + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq + uses: cachix/cachix-action@v12 + with: + extraPullNames: coq-community, math-comp + name: coq + - id: stepCheck + name: Checking presence of CI target mathcomp-analysis + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"8.18\" --argstr job \"mathcomp-analysis\" \\\n --dry-run 2>&1\ + \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ + built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-classical' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "mathcomp-classical" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-field' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "mathcomp-field" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-bigenough' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "mathcomp-bigenough" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "hierarchy-builder" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "mathcomp-analysis" ssprove: needs: - coq @@ -190,4 +257,4 @@ name: Nix CI for bundle 8.18 push: branches: - master - workflow_dispatch: + workflow_dispatch: diff --git a/.github/workflows/nix-action-8.19.yml b/.github/workflows/nix-action-8.19.yml index de4fcdaf..292e6115 100644 --- a/.github/workflows/nix-action-8.19.yml +++ b/.github/workflows/nix-action-8.19.yml @@ -124,6 +124,73 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr job "mathcomp" + mathcomp-analysis: + needs: + - coq + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq + uses: cachix/cachix-action@v12 + with: + extraPullNames: coq-community, math-comp + name: coq + - id: stepCheck + name: Checking presence of CI target mathcomp-analysis + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"8.19\" --argstr job \"mathcomp-analysis\" \\\n --dry-run 2>&1\ + \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ + built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-classical' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-classical" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-field' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-field" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-bigenough' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-bigenough" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "hierarchy-builder" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-analysis" ssprove: needs: - coq @@ -190,4 +257,4 @@ name: Nix CI for bundle 8.19 push: branches: - master - workflow_dispatch: + workflow_dispatch: diff --git a/.nix/config.nix b/.nix/config.nix index d0b985c8..195296dd 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -37,11 +37,17 @@ ## alternative configuration ## When generating GitHub Action CI, one workflow file ## will be created per bundle - bundles."8.17".coqPackages = { - coq.override.version = "8.17"; - mathcomp.override.version = "1.17.0"; - mathcomp-analysis.override.version = "0.6.0"; - }; + + ## It is not possible as of yet to the coq-nix-toolbox to use a + ## certain version. All jobs only run against the latest version. + ## To do this check as a CI job you either need to manually edit + ## the generated workflow or create branch off of version 0.1.0 + ## and add it there. + # bundles."8.17".coqPackages = { + # coq.override.version = "8.17"; + # mathcomp.override.version = "1.17.0"; + # mathcomp-analysis.override.version = "0.6.0"; + # }; bundles."8.18".coqPackages = { coq.override.version = "8.18"; mathcomp.override.version = "2.1.0"; diff --git a/flake.nix b/flake.nix index 22e44776..0cbb102c 100644 --- a/flake.nix +++ b/flake.nix @@ -1,59 +1,48 @@ { inputs = { - nixpkgs.url = github:nixos/nixpkgs; + nixpkgs.url = github:nixos/nixpkgs/release-23.11; flake-utils.url = github:numtide/flake-utils; }; outputs = { self, nixpkgs, flake-utils }: let - mkDrv = { stdenv, which, coqPackages, coq } : - let - extructures' = coqPackages.extructures.override { version = "0.4.0"; }; - d = coqPackages.mkCoqDerivation { - pname = "ssprove"; - owner = "SSProve"; - version = "0.0.1"; - propagatedBuildInputs = - [ coq ] - ++ - (with coqPackages; [equations - mathcomp-analysis - mathcomp-ssreflect - deriving]) - ++ [extructures']; - meta = { - description = "A foundational framework for modular cryptographic proofs in Coq "; - license = coqPackages.lib.licenses.mit; - }; - }; - in - # getting this the flake-style means the code is already there - d.overrideAttrs (oldAttrs: { - src = ./.; - }); - in { inherit mkDrv; } // - flake-utils.lib.eachDefaultSystem (system: - let - pkgs = nixpkgs.legacyPackages.${system}; - in - rec { - devShell = - let - args = { - inherit (pkgs) stdenv which; - coqPackages = pkgs.coqPackages_8_18.overrideScope - (self: super: { - mathcomp = super.mathcomp.override { version = "2.1.0"; }; - mathcomp-analysis = super.mathcomp-analysis.override { version = "1.0.0"; }; - }); - coq = pkgs.coq_8_18; - }; - ssprove' = mkDrv args; - in - pkgs.mkShell { - packages = - (with pkgs; [ gnumake ]) - ++ - (with ssprove'; propagatedBuildInputs); - }; - }); + ssprovePkg = { lib, mkCoqDerivation, coq + , equations, extructures, deriving + , mathcomp-analysis, mathcomp-ssreflect }: + mkCoqDerivation { + pname = "ssprove"; + owner = "SSProve"; + version = "0.2.0"; + src = ./.; + propagatedBuildInputs = [ + coq + equations + mathcomp-analysis + mathcomp-ssreflect + deriving + extructures + ]; + meta = { + description = "A foundational framework for modular cryptographic proofs in Coq "; + license = lib.licenses.mit; + }; + }; + in { + overlays.default = final: prev: { + coqPackages_8_18 = prev.coqPackages_8_18.overrideScope (self: super: { + extructures = super.extructures.override { version = "0.4.0"; }; + mathcomp = super.mathcomp.override { version = "2.1.0"; }; + mathcomp-analysis = super.mathcomp-analysis.override { version = "1.0.0"; }; + ssprove = self.callPackage ssprovePkg {}; + }); + }; + } // flake-utils.lib.eachDefaultSystem (system: + let + pkgs = import nixpkgs { + inherit system; + overlays = [ self.overlays.default ]; + }; + in { + packages.default = pkgs.coqPackages_8_18.ssprove; + devShells.default = self.packages.${system}.default; + }); } From bdc751ac5fec54472ccba2956304ebdecccce124 Mon Sep 17 00:00:00 2001 From: Sebastian Ertel Date: Fri, 3 May 2024 16:29:00 +0200 Subject: [PATCH 20/33] enable workflows for main and manual execution. --- .github/workflows/nix-action-8.18.yml | 4 ++-- .github/workflows/nix-action-8.19.yml | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/.github/workflows/nix-action-8.18.yml b/.github/workflows/nix-action-8.18.yml index b92e2688..6933e1a0 100644 --- a/.github/workflows/nix-action-8.18.yml +++ b/.github/workflows/nix-action-8.18.yml @@ -256,5 +256,5 @@ name: Nix CI for bundle 8.18 - reopened push: branches: - - master - workflow_dispatch: + - main + workflow_dispatch: diff --git a/.github/workflows/nix-action-8.19.yml b/.github/workflows/nix-action-8.19.yml index 292e6115..70ee9a09 100644 --- a/.github/workflows/nix-action-8.19.yml +++ b/.github/workflows/nix-action-8.19.yml @@ -256,5 +256,5 @@ name: Nix CI for bundle 8.19 - reopened push: branches: - - master - workflow_dispatch: + - main + workflow_dispatch: From 0e57e1ca4d90dc819c9159d9f27e6b80ca937098 Mon Sep 17 00:00:00 2001 From: Sebastian Ertel Date: Fri, 3 May 2024 21:25:53 +0200 Subject: [PATCH 21/33] use mathcomp-ssreflect as in the CI and run against master because it already has the SSProve package. --- .github/workflows/nix-action-8.18.yml | 60 ++++++++------------------- .github/workflows/nix-action-8.19.yml | 60 ++++++++------------------- .nix/config.nix | 4 +- 3 files changed, 38 insertions(+), 86 deletions(-) diff --git a/.github/workflows/nix-action-8.18.yml b/.github/workflows/nix-action-8.18.yml index 6933e1a0..2a955f0e 100644 --- a/.github/workflows/nix-action-8.18.yml +++ b/.github/workflows/nix-action-8.18.yml @@ -29,7 +29,7 @@ jobs: - name: Cachix install uses: cachix/install-nix-action@v20 with: - nix_path: nixpkgs=channel:nixpkgs-unstable + nix_path: nixpkgs=channel:master - name: Cachix setup coq uses: cachix/cachix-action@v12 with: @@ -45,7 +45,7 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr job "coq" - mathcomp: + mathcomp-analysis: needs: - coq runs-on: ubuntu-latest @@ -76,46 +76,34 @@ jobs: - name: Cachix install uses: cachix/install-nix-action@v20 with: - nix_path: nixpkgs=channel:nixpkgs-unstable + nix_path: nixpkgs=channel:master - name: Cachix setup coq uses: cachix/cachix-action@v12 with: extraPullNames: coq-community, math-comp name: coq - id: stepCheck - name: Checking presence of CI target mathcomp + name: Checking presence of CI target mathcomp-analysis run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.18\" --argstr job \"mathcomp\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ - s/.*/built/\") >> $GITHUB_OUTPUT\n" + \ bundle \"8.18\" --argstr job \"mathcomp-analysis\" \\\n --dry-run 2>&1\ + \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ + built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr job "coq" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr - job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr - job "mathcomp-fingroup" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr - job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-solvable' + name: 'Building/fetching previous CI target: mathcomp-classical' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr - job "mathcomp-solvable" + job "mathcomp-classical" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-field' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr job "mathcomp-field" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-character' + name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr - job "mathcomp-character" + job "mathcomp-bigenough" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: hierarchy-builder' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr @@ -123,8 +111,8 @@ jobs: - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr - job "mathcomp" - mathcomp-analysis: + job "mathcomp-analysis" + mathcomp-ssreflect: needs: - coq runs-on: ubuntu-latest @@ -155,34 +143,22 @@ jobs: - name: Cachix install uses: cachix/install-nix-action@v20 with: - nix_path: nixpkgs=channel:nixpkgs-unstable + nix_path: nixpkgs=channel:master - name: Cachix setup coq uses: cachix/cachix-action@v12 with: extraPullNames: coq-community, math-comp name: coq - id: stepCheck - name: Checking presence of CI target mathcomp-analysis + name: Checking presence of CI target mathcomp-ssreflect run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.18\" --argstr job \"mathcomp-analysis\" \\\n --dry-run 2>&1\ + \ bundle \"8.18\" --argstr job \"mathcomp-ssreflect\" \\\n --dry-run 2>&1\ \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-classical' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr - job "mathcomp-classical" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr - job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr - job "mathcomp-bigenough" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: hierarchy-builder' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr @@ -190,7 +166,7 @@ jobs: - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr - job "mathcomp-analysis" + job "mathcomp-ssreflect" ssprove: needs: - coq @@ -222,7 +198,7 @@ jobs: - name: Cachix install uses: cachix/install-nix-action@v20 with: - nix_path: nixpkgs=channel:nixpkgs-unstable + nix_path: nixpkgs=channel:master - name: Cachix setup coq uses: cachix/cachix-action@v12 with: diff --git a/.github/workflows/nix-action-8.19.yml b/.github/workflows/nix-action-8.19.yml index 70ee9a09..c9b8fab0 100644 --- a/.github/workflows/nix-action-8.19.yml +++ b/.github/workflows/nix-action-8.19.yml @@ -29,7 +29,7 @@ jobs: - name: Cachix install uses: cachix/install-nix-action@v20 with: - nix_path: nixpkgs=channel:nixpkgs-unstable + nix_path: nixpkgs=channel:master - name: Cachix setup coq uses: cachix/cachix-action@v12 with: @@ -45,7 +45,7 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr job "coq" - mathcomp: + mathcomp-analysis: needs: - coq runs-on: ubuntu-latest @@ -76,46 +76,34 @@ jobs: - name: Cachix install uses: cachix/install-nix-action@v20 with: - nix_path: nixpkgs=channel:nixpkgs-unstable + nix_path: nixpkgs=channel:master - name: Cachix setup coq uses: cachix/cachix-action@v12 with: extraPullNames: coq-community, math-comp name: coq - id: stepCheck - name: Checking presence of CI target mathcomp + name: Checking presence of CI target mathcomp-analysis run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.19\" --argstr job \"mathcomp\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ - s/.*/built/\") >> $GITHUB_OUTPUT\n" + \ bundle \"8.19\" --argstr job \"mathcomp-analysis\" \\\n --dry-run 2>&1\ + \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ + built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr job "coq" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr - job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr - job "mathcomp-fingroup" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr - job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-solvable' + name: 'Building/fetching previous CI target: mathcomp-classical' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr - job "mathcomp-solvable" + job "mathcomp-classical" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-field' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr job "mathcomp-field" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-character' + name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr - job "mathcomp-character" + job "mathcomp-bigenough" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: hierarchy-builder' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr @@ -123,8 +111,8 @@ jobs: - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr - job "mathcomp" - mathcomp-analysis: + job "mathcomp-analysis" + mathcomp-ssreflect: needs: - coq runs-on: ubuntu-latest @@ -155,34 +143,22 @@ jobs: - name: Cachix install uses: cachix/install-nix-action@v20 with: - nix_path: nixpkgs=channel:nixpkgs-unstable + nix_path: nixpkgs=channel:master - name: Cachix setup coq uses: cachix/cachix-action@v12 with: extraPullNames: coq-community, math-comp name: coq - id: stepCheck - name: Checking presence of CI target mathcomp-analysis + name: Checking presence of CI target mathcomp-ssreflect run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.19\" --argstr job \"mathcomp-analysis\" \\\n --dry-run 2>&1\ + \ bundle \"8.19\" --argstr job \"mathcomp-ssreflect\" \\\n --dry-run 2>&1\ \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-classical' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr - job "mathcomp-classical" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr - job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr - job "mathcomp-bigenough" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: hierarchy-builder' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr @@ -190,7 +166,7 @@ jobs: - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr - job "mathcomp-analysis" + job "mathcomp-ssreflect" ssprove: needs: - coq @@ -222,7 +198,7 @@ jobs: - name: Cachix install uses: cachix/install-nix-action@v20 with: - nix_path: nixpkgs=channel:nixpkgs-unstable + nix_path: nixpkgs=channel:master - name: Cachix setup coq uses: cachix/cachix-action@v12 with: diff --git a/.nix/config.nix b/.nix/config.nix index 195296dd..3f15996c 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -50,12 +50,12 @@ # }; bundles."8.18".coqPackages = { coq.override.version = "8.18"; - mathcomp.override.version = "2.1.0"; + mathcomp-ssreflect.override.version = "2.1.0"; mathcomp-analysis.override.version = "1.0.0"; }; bundles."8.19".coqPackages = { coq.override.version = "8.19"; - mathcomp.override.version = "2.2.0"; + mathcomp-ssreflect.override.version = "2.2.0"; mathcomp-analysis.override.version = "1.0.0"; }; From 6b4cee7657e641b60822cb0731037bcfa70d71d9 Mon Sep 17 00:00:00 2001 From: Sebastian Ertel Date: Fri, 3 May 2024 21:39:16 +0200 Subject: [PATCH 22/33] for some reason using ssreflect does not work. --- .github/workflows/nix-action-8.18.yml | 52 +++++++++++++++++++-------- .github/workflows/nix-action-8.19.yml | 52 +++++++++++++++++++-------- .nix/config.nix | 4 +-- 3 files changed, 78 insertions(+), 30 deletions(-) diff --git a/.github/workflows/nix-action-8.18.yml b/.github/workflows/nix-action-8.18.yml index 2a955f0e..f2306dbc 100644 --- a/.github/workflows/nix-action-8.18.yml +++ b/.github/workflows/nix-action-8.18.yml @@ -45,7 +45,7 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr job "coq" - mathcomp-analysis: + mathcomp: needs: - coq runs-on: ubuntu-latest @@ -83,27 +83,39 @@ jobs: extraPullNames: coq-community, math-comp name: coq - id: stepCheck - name: Checking presence of CI target mathcomp-analysis + name: Checking presence of CI target mathcomp run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.18\" --argstr job \"mathcomp-analysis\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ - built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" + \ bundle \"8.18\" --argstr job \"mathcomp\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ + s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr job "coq" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-classical' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr - job "mathcomp-classical" + job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-fingroup' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "mathcomp-fingroup" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "mathcomp-algebra" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-solvable' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "mathcomp-solvable" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-field' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr job "mathcomp-field" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-bigenough' + name: 'Building/fetching previous CI target: mathcomp-character' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr - job "mathcomp-bigenough" + job "mathcomp-character" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: hierarchy-builder' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr @@ -111,8 +123,8 @@ jobs: - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr - job "mathcomp-analysis" - mathcomp-ssreflect: + job "mathcomp" + mathcomp-analysis: needs: - coq runs-on: ubuntu-latest @@ -150,15 +162,27 @@ jobs: extraPullNames: coq-community, math-comp name: coq - id: stepCheck - name: Checking presence of CI target mathcomp-ssreflect + name: Checking presence of CI target mathcomp-analysis run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.18\" --argstr job \"mathcomp-ssreflect\" \\\n --dry-run 2>&1\ + \ bundle \"8.18\" --argstr job \"mathcomp-analysis\" \\\n --dry-run 2>&1\ \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-classical' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "mathcomp-classical" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-field' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "mathcomp-field" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-bigenough' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "mathcomp-bigenough" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: hierarchy-builder' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr @@ -166,7 +190,7 @@ jobs: - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr - job "mathcomp-ssreflect" + job "mathcomp-analysis" ssprove: needs: - coq diff --git a/.github/workflows/nix-action-8.19.yml b/.github/workflows/nix-action-8.19.yml index c9b8fab0..11936739 100644 --- a/.github/workflows/nix-action-8.19.yml +++ b/.github/workflows/nix-action-8.19.yml @@ -45,7 +45,7 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr job "coq" - mathcomp-analysis: + mathcomp: needs: - coq runs-on: ubuntu-latest @@ -83,27 +83,39 @@ jobs: extraPullNames: coq-community, math-comp name: coq - id: stepCheck - name: Checking presence of CI target mathcomp-analysis + name: Checking presence of CI target mathcomp run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.19\" --argstr job \"mathcomp-analysis\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ - built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" + \ bundle \"8.19\" --argstr job \"mathcomp\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ + s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr job "coq" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-classical' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr - job "mathcomp-classical" + job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-fingroup' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-fingroup" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-algebra" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-solvable' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-solvable" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-field' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr job "mathcomp-field" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-bigenough' + name: 'Building/fetching previous CI target: mathcomp-character' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr - job "mathcomp-bigenough" + job "mathcomp-character" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: hierarchy-builder' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr @@ -111,8 +123,8 @@ jobs: - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr - job "mathcomp-analysis" - mathcomp-ssreflect: + job "mathcomp" + mathcomp-analysis: needs: - coq runs-on: ubuntu-latest @@ -150,15 +162,27 @@ jobs: extraPullNames: coq-community, math-comp name: coq - id: stepCheck - name: Checking presence of CI target mathcomp-ssreflect + name: Checking presence of CI target mathcomp-analysis run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.19\" --argstr job \"mathcomp-ssreflect\" \\\n --dry-run 2>&1\ + \ bundle \"8.19\" --argstr job \"mathcomp-analysis\" \\\n --dry-run 2>&1\ \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-classical' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-classical" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-field' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-field" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-bigenough' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-bigenough" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: hierarchy-builder' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr @@ -166,7 +190,7 @@ jobs: - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr - job "mathcomp-ssreflect" + job "mathcomp-analysis" ssprove: needs: - coq diff --git a/.nix/config.nix b/.nix/config.nix index 3f15996c..195296dd 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -50,12 +50,12 @@ # }; bundles."8.18".coqPackages = { coq.override.version = "8.18"; - mathcomp-ssreflect.override.version = "2.1.0"; + mathcomp.override.version = "2.1.0"; mathcomp-analysis.override.version = "1.0.0"; }; bundles."8.19".coqPackages = { coq.override.version = "8.19"; - mathcomp-ssreflect.override.version = "2.2.0"; + mathcomp.override.version = "2.2.0"; mathcomp-analysis.override.version = "1.0.0"; }; From 1882afa81a8f3379f302b49c65cfd98d122487ab Mon Sep 17 00:00:00 2001 From: Sebastian Ertel Date: Fri, 3 May 2024 21:53:23 +0200 Subject: [PATCH 23/33] forcing the job to load the most recent state of nixpkgs --- .nix/nixpkgs.nix | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 .nix/nixpkgs.nix diff --git a/.nix/nixpkgs.nix b/.nix/nixpkgs.nix new file mode 100644 index 00000000..08ba21a1 --- /dev/null +++ b/.nix/nixpkgs.nix @@ -0,0 +1,4 @@ +fetchTarball { + url = https://github.com/NixOS/nixpkgs/archive/d121ce778b2609ae9e749a711295ffca013a82c4.tar.gz; + sha256 = "d121ce778b2609ae9e749a711295ffca013a82c4"; + } \ No newline at end of file From ed79bb2ec94378fe3cce606b3a09ca67ddbb192a Mon Sep 17 00:00:00 2001 From: Sebastian Ertel Date: Fri, 3 May 2024 22:11:56 +0200 Subject: [PATCH 24/33] after updating nixpkgs. --- .github/workflows/nix-action-8.18.yml | 29 +++++++++++++++++++++++---- .github/workflows/nix-action-8.19.yml | 29 +++++++++++++++++++++++---- .nix/nixpkgs.nix | 6 +++--- 3 files changed, 53 insertions(+), 11 deletions(-) diff --git a/.github/workflows/nix-action-8.18.yml b/.github/workflows/nix-action-8.18.yml index f2306dbc..7857c760 100644 --- a/.github/workflows/nix-action-8.18.yml +++ b/.github/workflows/nix-action-8.18.yml @@ -29,7 +29,7 @@ jobs: - name: Cachix install uses: cachix/install-nix-action@v20 with: - nix_path: nixpkgs=channel:master + nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup coq uses: cachix/cachix-action@v12 with: @@ -76,7 +76,7 @@ jobs: - name: Cachix install uses: cachix/install-nix-action@v20 with: - nix_path: nixpkgs=channel:master + nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup coq uses: cachix/cachix-action@v12 with: @@ -155,7 +155,7 @@ jobs: - name: Cachix install uses: cachix/install-nix-action@v20 with: - nix_path: nixpkgs=channel:master + nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup coq uses: cachix/cachix-action@v12 with: @@ -194,6 +194,7 @@ jobs: ssprove: needs: - coq + - mathcomp-analysis runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -222,7 +223,7 @@ jobs: - name: Cachix install uses: cachix/install-nix-action@v20 with: - nix_path: nixpkgs=channel:master + nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup coq uses: cachix/cachix-action@v12 with: @@ -238,6 +239,26 @@ jobs: name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: equations' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "equations" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-analysis' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "mathcomp-analysis" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: extructures' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "extructures" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: deriving' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "deriving" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr diff --git a/.github/workflows/nix-action-8.19.yml b/.github/workflows/nix-action-8.19.yml index 11936739..36cebd71 100644 --- a/.github/workflows/nix-action-8.19.yml +++ b/.github/workflows/nix-action-8.19.yml @@ -29,7 +29,7 @@ jobs: - name: Cachix install uses: cachix/install-nix-action@v20 with: - nix_path: nixpkgs=channel:master + nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup coq uses: cachix/cachix-action@v12 with: @@ -76,7 +76,7 @@ jobs: - name: Cachix install uses: cachix/install-nix-action@v20 with: - nix_path: nixpkgs=channel:master + nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup coq uses: cachix/cachix-action@v12 with: @@ -155,7 +155,7 @@ jobs: - name: Cachix install uses: cachix/install-nix-action@v20 with: - nix_path: nixpkgs=channel:master + nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup coq uses: cachix/cachix-action@v12 with: @@ -194,6 +194,7 @@ jobs: ssprove: needs: - coq + - mathcomp-analysis runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -222,7 +223,7 @@ jobs: - name: Cachix install uses: cachix/install-nix-action@v20 with: - nix_path: nixpkgs=channel:master + nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup coq uses: cachix/cachix-action@v12 with: @@ -238,6 +239,26 @@ jobs: name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: equations' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "equations" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-analysis' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-analysis" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: extructures' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "extructures" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: deriving' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "deriving" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr diff --git a/.nix/nixpkgs.nix b/.nix/nixpkgs.nix index 08ba21a1..551bfce5 100644 --- a/.nix/nixpkgs.nix +++ b/.nix/nixpkgs.nix @@ -1,4 +1,4 @@ fetchTarball { - url = https://github.com/NixOS/nixpkgs/archive/d121ce778b2609ae9e749a711295ffca013a82c4.tar.gz; - sha256 = "d121ce778b2609ae9e749a711295ffca013a82c4"; - } \ No newline at end of file + url = https://github.com/NixOS/nixpkgs/archive/045a097bde2100af7301e50632a02d0425031042.tar.gz; + sha256 = "1gw6xkyzhc08q93dkb6p2s0c8b7vhj9nq5amwn5146ag38cp0j3l"; + } From b9ff63cfbdb1b564bac1b20a8eacef1cf9ae400a Mon Sep 17 00:00:00 2001 From: Sebastian Ertel Date: Sat, 4 May 2024 22:22:11 +0200 Subject: [PATCH 25/33] flake build --- .github/workflows/flake-build.yml | 27 +++++++++++++++++++ .../workflows/{build.yml => opam-build.yml} | 2 +- 2 files changed, 28 insertions(+), 1 deletion(-) create mode 100644 .github/workflows/flake-build.yml rename .github/workflows/{build.yml => opam-build.yml} (98%) diff --git a/.github/workflows/flake-build.yml b/.github/workflows/flake-build.yml new file mode 100644 index 00000000..12051774 --- /dev/null +++ b/.github/workflows/flake-build.yml @@ -0,0 +1,27 @@ +name: Flake build + +# Controls when the action will run. +on: + # Triggers the workflow on push or pull request events but only for the main branch + push: + branches: [ main ] + pull_request: + branches: [ main ] + + # Allows you to run this workflow manually from the Actions tab + workflow_dispatch: + +jobs: + # This workflow contains a single job called "build" + build: + # The type of runner that the job will run on + runs-on: ubuntu-latest + + # Steps represent a sequence of tasks that will be executed as part of the job + steps: + - uses: actions/checkout@v4 + - uses: cachix/install-nix-action@v25 + with: + github_access_token: ${{ secrets.GITHUB_TOKEN }} + - run: nix build + - run: nix flake check diff --git a/.github/workflows/build.yml b/.github/workflows/opam-build.yml similarity index 98% rename from .github/workflows/build.yml rename to .github/workflows/opam-build.yml index 46141271..46ca966a 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/opam-build.yml @@ -1,6 +1,6 @@ # This is a basic workflow to help you get started with Actions -name: Test build +name: Opam build # Controls when the action will run. on: From c253bf7d6d1701dce17a3c22cdfb62bf429112cd Mon Sep 17 00:00:00 2001 From: Sebastian Ertel Date: Mon, 6 May 2024 14:10:13 +0200 Subject: [PATCH 26/33] fixing flake --- flake.lock | 6 +++--- flake.nix | 12 +++++------- 2 files changed, 8 insertions(+), 10 deletions(-) diff --git a/flake.lock b/flake.lock index 5bca994c..9cb1f818 100644 --- a/flake.lock +++ b/flake.lock @@ -20,11 +20,11 @@ }, "nixpkgs": { "locked": { - "lastModified": 1710410081, - "narHash": "sha256-5n3OrpL8V+isTDMwlGNjDwA/57R/HH0X7NIsvFFWUUs=", + "lastModified": 1714981191, + "narHash": "sha256-REcrlvQ9iDorYv7s1E4NXkR8xqyk1UqY/Wy334/42ac=", "owner": "nixos", "repo": "nixpkgs", - "rev": "1a399f214e41e079f0edba674a415816286d1fbd", + "rev": "6d418318193fe8922d8aa404cc7fcd5c2a7edb63", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index 0cbb102c..45557e40 100644 --- a/flake.nix +++ b/flake.nix @@ -1,6 +1,6 @@ { inputs = { - nixpkgs.url = github:nixos/nixpkgs/release-23.11; + nixpkgs.url = github:nixos/nixpkgs; flake-utils.url = github:numtide/flake-utils; }; outputs = { self, nixpkgs, flake-utils }: @@ -28,11 +28,9 @@ }; in { overlays.default = final: prev: { - coqPackages_8_18 = prev.coqPackages_8_18.overrideScope (self: super: { - extructures = super.extructures.override { version = "0.4.0"; }; - mathcomp = super.mathcomp.override { version = "2.1.0"; }; - mathcomp-analysis = super.mathcomp-analysis.override { version = "1.0.0"; }; - ssprove = self.callPackage ssprovePkg {}; + coqPackages_8_19 = prev.coqPackages_8_19.overrideScope (self: super: { + mathcomp-ssreflect = super.mathcomp-ssreflect.override { version = "2.2.0"; }; + ssprove = self.callPackage ssprovePkg {}; }); }; } // flake-utils.lib.eachDefaultSystem (system: @@ -42,7 +40,7 @@ overlays = [ self.overlays.default ]; }; in { - packages.default = pkgs.coqPackages_8_18.ssprove; + packages.default = pkgs.coqPackages_8_19.ssprove; devShells.default = self.packages.${system}.default; }); } From 48e24b3319dbd39251888b578b0dbdda5862e5bd Mon Sep 17 00:00:00 2001 From: Sebastian Ertel Date: Mon, 6 May 2024 14:18:46 +0200 Subject: [PATCH 27/33] no cache --- .github/workflows/flake-build.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/flake-build.yml b/.github/workflows/flake-build.yml index 12051774..7a4c902d 100644 --- a/.github/workflows/flake-build.yml +++ b/.github/workflows/flake-build.yml @@ -20,8 +20,8 @@ jobs: # Steps represent a sequence of tasks that will be executed as part of the job steps: - uses: actions/checkout@v4 - - uses: cachix/install-nix-action@v25 - with: - github_access_token: ${{ secrets.GITHUB_TOKEN }} +# - uses: cachix/install-nix-action@v25 +# with: +# github_access_token: ${{ secrets.GITHUB_TOKEN }} - run: nix build - run: nix flake check From fb11d220585b8d027890df87b21af8a67bbe7c02 Mon Sep 17 00:00:00 2001 From: Sebastian Ertel Date: Wed, 8 May 2024 14:07:43 +0200 Subject: [PATCH 28/33] minor --- .github/workflows/flake-build.yml | 6 +++--- flake.lock | 7 ++++--- flake.nix | 3 +-- 3 files changed, 8 insertions(+), 8 deletions(-) diff --git a/.github/workflows/flake-build.yml b/.github/workflows/flake-build.yml index 7a4c902d..12051774 100644 --- a/.github/workflows/flake-build.yml +++ b/.github/workflows/flake-build.yml @@ -20,8 +20,8 @@ jobs: # Steps represent a sequence of tasks that will be executed as part of the job steps: - uses: actions/checkout@v4 -# - uses: cachix/install-nix-action@v25 -# with: -# github_access_token: ${{ secrets.GITHUB_TOKEN }} + - uses: cachix/install-nix-action@v25 + with: + github_access_token: ${{ secrets.GITHUB_TOKEN }} - run: nix build - run: nix flake check diff --git a/flake.lock b/flake.lock index 9cb1f818..7a694349 100644 --- a/flake.lock +++ b/flake.lock @@ -20,16 +20,17 @@ }, "nixpkgs": { "locked": { - "lastModified": 1714981191, - "narHash": "sha256-REcrlvQ9iDorYv7s1E4NXkR8xqyk1UqY/Wy334/42ac=", + "lastModified": 1714997724, + "narHash": "sha256-zEGJP3VwxsWOQ2RtpF0VskZv5NVxkxGz+vfiIbCQPho=", "owner": "nixos", "repo": "nixpkgs", - "rev": "6d418318193fe8922d8aa404cc7fcd5c2a7edb63", + "rev": "1e9759cb3731963f7007cce49dfa6ff1f412ea0c", "type": "github" }, "original": { "owner": "nixos", "repo": "nixpkgs", + "rev": "1e9759cb3731963f7007cce49dfa6ff1f412ea0c", "type": "github" } }, diff --git a/flake.nix b/flake.nix index 45557e40..7ab50fbb 100644 --- a/flake.nix +++ b/flake.nix @@ -1,6 +1,6 @@ { inputs = { - nixpkgs.url = github:nixos/nixpkgs; + nixpkgs.url = github:nixos/nixpkgs/1e9759cb3731963f7007cce49dfa6ff1f412ea0c; flake-utils.url = github:numtide/flake-utils; }; outputs = { self, nixpkgs, flake-utils }: @@ -14,7 +14,6 @@ version = "0.2.0"; src = ./.; propagatedBuildInputs = [ - coq equations mathcomp-analysis mathcomp-ssreflect From e53690fa45f0e08cd27d12c15adab8b3b24c314b Mon Sep 17 00:00:00 2001 From: Sebastian Ertel Date: Fri, 31 May 2024 08:49:25 +0200 Subject: [PATCH 29/33] discovered and fixed inconsistencies in loading mathcomp dependencies. --- flake.lock | 7 +++---- flake.nix | 10 +++++++--- 2 files changed, 10 insertions(+), 7 deletions(-) diff --git a/flake.lock b/flake.lock index 7a694349..0f791735 100644 --- a/flake.lock +++ b/flake.lock @@ -20,17 +20,16 @@ }, "nixpkgs": { "locked": { - "lastModified": 1714997724, - "narHash": "sha256-zEGJP3VwxsWOQ2RtpF0VskZv5NVxkxGz+vfiIbCQPho=", + "lastModified": 1717096212, + "narHash": "sha256-1Tti/eg2jTKYiVonCCjy+DnJspZ5q+tw9+C/bV9y0mg=", "owner": "nixos", "repo": "nixpkgs", - "rev": "1e9759cb3731963f7007cce49dfa6ff1f412ea0c", + "rev": "afd3a57b83977a2e0fe8c4685ca2016a12103d03", "type": "github" }, "original": { "owner": "nixos", "repo": "nixpkgs", - "rev": "1e9759cb3731963f7007cce49dfa6ff1f412ea0c", "type": "github" } }, diff --git a/flake.nix b/flake.nix index 7ab50fbb..3098a73e 100644 --- a/flake.nix +++ b/flake.nix @@ -1,6 +1,6 @@ { inputs = { - nixpkgs.url = github:nixos/nixpkgs/1e9759cb3731963f7007cce49dfa6ff1f412ea0c; + nixpkgs.url = github:nixos/nixpkgs; flake-utils.url = github:numtide/flake-utils; }; outputs = { self, nixpkgs, flake-utils }: @@ -28,8 +28,12 @@ in { overlays.default = final: prev: { coqPackages_8_19 = prev.coqPackages_8_19.overrideScope (self: super: { - mathcomp-ssreflect = super.mathcomp-ssreflect.override { version = "2.2.0"; }; - ssprove = self.callPackage ssprovePkg {}; + # mathcomp-ssreflect inherits this version + # setting it to mathcomp-ssreflect does not work. + # see my question on Zulip: + # https://coq.zulipchat.com/#narrow/stream/290990-Nix-toolbox-devs-.26-users/topic/Loading.20inconsistency.20in.20mathcomp.20dependencies + mathcomp = super.mathcomp.override { version = "2.2.0"; }; + ssprove = self.callPackage ssprovePkg {}; }); }; } // flake-utils.lib.eachDefaultSystem (system: From d52ae4c6bfe160adba2e44879c97244fa90b68a6 Mon Sep 17 00:00:00 2001 From: Sebastian Ertel Date: Fri, 31 May 2024 10:48:08 +0200 Subject: [PATCH 30/33] documentation of Nix --- .nix/flake.nix.template_latest | 22 ++++++++++++++ .nix/flake.nix.template_versioned | 30 +++++++++++++++++++ README.md | 48 ++++++++++++++++++++++--------- 3 files changed, 86 insertions(+), 14 deletions(-) create mode 100644 .nix/flake.nix.template_latest create mode 100644 .nix/flake.nix.template_versioned diff --git a/.nix/flake.nix.template_latest b/.nix/flake.nix.template_latest new file mode 100644 index 00000000..73098e95 --- /dev/null +++ b/.nix/flake.nix.template_latest @@ -0,0 +1,22 @@ +{ + inputs = { + nixpkgs.url = github:nixos/nixpkgs; + flake-utils.url = github:numtide/flake-utils; + + ssprove.url = github:ssprove/ssprove/nix; + ssprove.inputs.nixpkgs.follows = "nixpkgs"; + ssprove.inputs.flake-utils.follows = "flake-utils"; + }; + outputs = { self, nixpkgs, flake-utils + , ssprove }: + flake-utils.lib.eachDefaultSystem (system: + let + pkgs = nixpkgs.legacyPackages.${system}; + in { + devShell = pkgs.mkShell { + packages = [ssprove]; + shellHook = '' alias ll="ls -lasi" ''; + }; + } + ); +} diff --git a/.nix/flake.nix.template_versioned b/.nix/flake.nix.template_versioned new file mode 100644 index 00000000..c1e7135a --- /dev/null +++ b/.nix/flake.nix.template_versioned @@ -0,0 +1,30 @@ +{ + inputs = { + nixpkgs.url = github:nixos/nixpkgs; + flake-utils.url = github:numtide/flake-utils; + + ## We have start using Nix flakes only after version 0.2.0. + ## Hence, loading versions flake-style works best after + ## version 0.2.0. + # ssprove.url = github:ssprove/ssprove/nix; + # ssprove.inputs.nixpkgs.follows = "nixpkgs"; + # ssprove.inputs.flake-utils.follows = "flake-utils"; + }; + outputs = { self, nixpkgs, flake-utils + #, ssprove + }: + flake-utils.lib.eachDefaultSystem (system: + let + pkgs = nixpkgs.legacyPackages.${system}; + coqPackages = pkgs.coqPackages_8_17.overrideScope + (self: super:{ + ssprove = super.ssprove.override { version = "0.1.0"; }; + }); + in { + devShell = pkgs.mkShell { + packages = (with coqPackages; [ssprove]); + shellHook = '' alias ll="ls -lasi" ''; + }; + } + ); +} diff --git a/README.md b/README.md index 6e4374b9..79937836 100644 --- a/README.md +++ b/README.md @@ -33,17 +33,25 @@ A documentation is available in [DOC.md]. ## Installation +There are two installation options: +- via `opam` +- via `nix` + #### Prerequisites -- OCaml `>=4.05.0 & <5` -- Coq `>=8.16.0 & <8.18.0` -- Equations `1.3` -- Mathcomp `>=1.15.0` -- Mathcomp analysis `>=0.5.3` -- Coq Extructures `0.3.1` -- Coq Deriving `0.1` +- OCaml +- Coq +- Equations +- Mathcomp +- Mathcomp analysis +- Coq Extructures +- Coq Deriving + + +### OPAM-based installation + -You can get them all from the `opam` package manager for OCaml: +You can get all dependencies from the `opam` package manager for OCaml: ```sh opam repo add coq-released https://coq.inria.fr/opam/released opam update @@ -53,6 +61,18 @@ opam install ./ssprove.opam To build the dependency graph, you can optionally install `graphviz`. On macOS, `gsed` is additionally required for this. +### Nix-based installation + +`ssprove` is available on `nixpkgs`, e.g., `coqPackages_8*19.ssprove`. +The following flake-based templates for your new SSProve project are available: +- [SSProve latest](.nix/flake.nix.template_latest) -- provides a project setup +with the latest SSProve development readily installed. +- [SSProve versioned](.nix/flake.nix.template_versioned) -- provides +a Nix flake that loads a dedicated version (that you may change). + + +## Build instructions + #### Running verification Run `make` from this directory to verify all the Coq files. @@ -63,12 +83,12 @@ Run `make graph` to build a graph of dependencies between sources. ## Directory organisation -| Directory | Description | -|-----------------------|------------------------------------------------------| -| [theories] | Root of all the Coq files | -| [theories/Mon] | External development coming from "Dijkstra Monads For All" | -| [theories/Relational] | External development coming from "The Next 700 Relational Program Logics"| -| [theories/Crypt] | This paper | +| Directory | Description | +|-----------------------|---------------------------------------------------------------------------| +| [theories] | Root of all the Coq files | +| [theories/Mon] | External development coming from "Dijkstra Monads For All" | +| [theories/Relational] | External development coming from "The Next 700 Relational Program Logics" | +| [theories/Crypt] | This paper | Unless specified with a full path, all files considered in this README can safely be assumed to be in [theories/Crypt]. From 4a59d11349dbb8f886625dd184e01c2c3dbb1e49 Mon Sep 17 00:00:00 2001 From: Sebastian Ertel Date: Tue, 4 Jun 2024 10:27:50 +0200 Subject: [PATCH 31/33] adding a comment on the use of Equations. --- DOC.md | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/DOC.md b/DOC.md index 30829a04..c3000d04 100644 --- a/DOC.md +++ b/DOC.md @@ -437,6 +437,9 @@ but where the set of locations is internalised. `package` then, `{package p₀ ∘ p₁ }` is a valid expression, and will be complete if the interfaces match. +**Note:** When using `Equations`, please `Set Equations Transparent` such +that code simplification in proofs via `ssprove_code_simpl` resolves properly. + ## High-level SSP proofs To reason at the high-level of state-separating proofs, we have two main @@ -1196,4 +1199,4 @@ develop something more general. 🚧 [extructures]: https://github.com/arthuraa/extructures -[open an issue]: https://github.com/SSProve/ssprove/issues \ No newline at end of file +[open an issue]: https://github.com/SSProve/ssprove/issues From 9066771c19f3bc328a152e519e363f82a7edc408 Mon Sep 17 00:00:00 2001 From: Sebastian Ertel Date: Wed, 12 Jun 2024 18:30:38 +0200 Subject: [PATCH 32/33] Typo fix in README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 79937836..3e0ea246 100644 --- a/README.md +++ b/README.md @@ -63,7 +63,7 @@ On macOS, `gsed` is additionally required for this. ### Nix-based installation -`ssprove` is available on `nixpkgs`, e.g., `coqPackages_8*19.ssprove`. +`ssprove` is available on `nixpkgs`, e.g., `coqPackages_8_19.ssprove`. The following flake-based templates for your new SSProve project are available: - [SSProve latest](.nix/flake.nix.template_latest) -- provides a project setup with the latest SSProve development readily installed. From 7a717b51a716a6e28e67eda8b649cfb1398edeeb Mon Sep 17 00:00:00 2001 From: Sebastian Ertel Date: Mon, 12 Aug 2024 13:31:56 +0200 Subject: [PATCH 33/33] Quick start guide on project setup via Nix --- README.md | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/README.md b/README.md index 3e0ea246..9e9261ba 100644 --- a/README.md +++ b/README.md @@ -70,6 +70,23 @@ with the latest SSProve development readily installed. - [SSProve versioned](.nix/flake.nix.template_versioned) -- provides a Nix flake that loads a dedicated version (that you may change). +#### Quick start guide + +##### Nix installation +This is performed only once. +1. [Install Nix](https://nix.dev/install-nix.html) with `curl -L https://nixos.org/nix/install | sh -s -- --daemon` +2. Enable [flake support](https://nixos.wiki/wiki/Flakes) with `mkdir -p ~/.config/nix && echo -e "experimental-features = nix-command flakes" >> ~/.config/nix/nix.conf` +All set. + +##### Project setup +1. Create a new project folder and `cd` into it. +2. Copy one of the above templates into it (removing the `.template*` suffix). +3. And finally run `nix develop` which throws you into a shell where SSProve is already installed. (`From Crypt Require Import ...`) + +You may need to initialize the project as a Git repository and add the `flake.nix` to it. +The generated `flake.lock` pins the versions and hence also needs to be added to this new project repo. + +In the `flake.nix`, you can add [more Coq packages from the Nix repository](https://github.com/NixOS/nixpkgs/blob/a194f9d0654e368fb900830a19396f9d7792647a/pkgs/top-level/coq-packages.nix#L20). ## Build instructions