From 34c0a31bd30492841db26cf44c0003418a6f774e Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Mon, 15 Jan 2024 17:07:24 +0100 Subject: [PATCH] Add Coq 8.19 --- .github/workflows/docker-action.yml | 1 + .github/workflows/nix-action-8.19.yml | 172 +++++++++++++++++++++++++ .nix/config.nix | 4 +- .nix/coq-overlays/mathcomp/default.nix | 139 ++++++++++++++++++++ coq-mathcomp-classical.opam | 2 +- 5 files changed, 316 insertions(+), 2 deletions(-) create mode 100644 .github/workflows/nix-action-8.19.yml create mode 100644 .nix/coq-overlays/mathcomp/default.nix diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 4b0c9b7a0b..2275c619e2 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -19,6 +19,7 @@ jobs: - 'mathcomp/mathcomp:1.17.0-coq-8.16' - 'mathcomp/mathcomp:1.17.0-coq-8.17' - 'mathcomp/mathcomp:1.18.0-coq-8.18' + - 'mathcomp/mathcomp:1.19.0-coq-8.19' fail-fast: false steps: - uses: actions/checkout@v2 diff --git a/.github/workflows/nix-action-8.19.yml b/.github/workflows/nix-action-8.19.yml new file mode 100644 index 0000000000..fb4d121501 --- /dev/null +++ b/.github/workflows/nix-action-8.19.yml @@ -0,0 +1,172 @@ +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 math-comp + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - 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-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 math-comp + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - 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 current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-analysis" + mathcomp-analysis-single: + 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 math-comp + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target mathcomp-analysis-single + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"8.19\" --argstr job \"mathcomp-analysis-single\" \\\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 current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-analysis-single" +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 + - hierarchy-builder diff --git a/.nix/config.nix b/.nix/config.nix index 45cbfaf149..49d742f0a1 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -31,7 +31,7 @@ ## select an entry to build in the following `bundles` set ## defaults to "default" - default-bundle = "8.15"; + default-bundle = "8.18"; ## write one `bundles.name` attribute set per ## alternative configuration @@ -44,6 +44,8 @@ bundles."8.17".coqPackages.coq.override.version = "8.17"; bundles."8.18".push-branches = [ "master" "hierarchy-builder" ]; bundles."8.18".coqPackages.coq.override.version = "8.18"; + bundles."8.19".push-branches = [ "master" "hierarchy-builder" ]; + bundles."8.19".coqPackages.coq.override.version = "8.19"; bundles."master".push-branches = [ "master" "hierarchy-builder" ]; bundles."master".coqPackages = { diff --git a/.nix/coq-overlays/mathcomp/default.nix b/.nix/coq-overlays/mathcomp/default.nix new file mode 100644 index 0000000000..43bee68e7b --- /dev/null +++ b/.nix/coq-overlays/mathcomp/default.nix @@ -0,0 +1,139 @@ +############################################################################ +# This file mainly provides the `mathcomp` derivation, which is # +# essentially a meta-package containing all core mathcomp libraries # +# (ssreflect fingroup algebra solvable field character). They can be # +# accessed individually through the passthrough attributes of mathcomp # +# bearing the same names (mathcomp.ssreflect, etc). # +############################################################################ +# Compiling a custom version of mathcomp using `mathcomp.override`. # +# This is the replacement for the former `mathcomp_ config` function. # +# See the documentation at doc/languages-frameworks/coq.section.md. # +############################################################################ + +{ lib, ncurses, graphviz, lua, fetchzip, + mkCoqDerivation, recurseIntoAttrs, withDoc ? false, single ? false, + coqPackages, coq, hierarchy-builder, version ? null }@args: +with builtins // lib; +let + repo = "math-comp"; + owner = "math-comp"; + withDoc = single && (args.withDoc or false); + defaultVersion = with versions; lib.switch coq.coq-version [ + { case = range "8.17" "8.18"; out = "1.18.0"; } + { case = range "8.15" "8.18"; out = "1.17.0"; } + { case = range "8.16" "8.18"; out = "2.1.0"; } + { case = range "8.16" "8.18"; out = "2.0.0"; } + { case = range "8.13" "8.18"; out = "1.16.0"; } + { case = range "8.14" "8.16"; out = "1.15.0"; } + { case = range "8.11" "8.15"; out = "1.14.0"; } + { case = range "8.11" "8.15"; out = "1.13.0"; } + { case = range "8.10" "8.13"; out = "1.12.0"; } + { case = range "8.7" "8.12"; out = "1.11.0"; } + { case = range "8.7" "8.11"; out = "1.10.0"; } + { case = range "8.7" "8.11"; out = "1.9.0"; } + { case = range "8.7" "8.9"; out = "1.8.0"; } + { case = range "8.6" "8.9"; out = "1.7.0"; } + { case = range "8.5" "8.7"; out = "1.6.4"; } + ] null; + release = { + "2.1.0".sha256 = "sha256-XDLx0BIkVRkSJ4sGCIE51j3rtkSGemNTs/cdVmTvxqo="; + "2.0.0".sha256 = "sha256-dpOmrHYUXBBS9kmmz7puzufxlbNpIZofpcTvJFLG5DI="; + "1.18.0".sha256 = "sha256-mJJ/zvM2WtmBZU3U4oid/zCMvDXei/93v5hwyyqwiiY="; + "1.17.0".sha256 = "sha256-bUfoSTMiW/GzC1jKFay6DRqGzKPuLOSUsO6/wPSFwNg="; + "1.16.0".sha256 = "sha256-gXTKhRgSGeRBUnwdDezMsMKbOvxdffT+kViZ9e1gEz0="; + "1.15.0".sha256 = "1bp0jxl35ms54s0mdqky15w9af03f3i0n06qk12k4gw1xzvwqv21"; + "1.14.0".sha256 = "07yamlp1c0g5nahkd2gpfhammcca74ga2s6qr7a3wm6y6j5pivk9"; + "1.13.0".sha256 = "0j4cz2y1r1aw79snkcf1pmicgzf8swbaf9ippz0vg99a572zqzri"; + "1.12.0".sha256 = "1ccfny1vwgmdl91kz5xlmhq4wz078xm4z5wpd0jy5rn890dx03wp"; + "1.11.0".sha256 = "06a71d196wd5k4wg7khwqb7j7ifr7garhwkd54s86i0j7d6nhl3c"; + "1.10.0".sha256 = "1b9m6pwxxyivw7rgx82gn5kmgv2mfv3h3y0mmjcjfypi8ydkrlbv"; + "1.9.0".sha256 = "0lid9zaazdi3d38l8042lczb02pw5m9wq0yysiilx891hgq2p81r"; + "1.8.0".sha256 = "07l40is389ih8bi525gpqs3qp4yb2kl11r9c8ynk1ifpjzpnabwp"; + "1.7.0".sha256 = "0wnhj9nqpx2bw6n1l4i8jgrw3pjajvckvj3lr4vzjb3my2lbxdd1"; + "1.6.4".sha256 = "09ww48qbjsvpjmy1g9yhm0rrkq800ffq21p6fjkbwd34qvd82raz"; + "1.6.1".sha256 = "1ilw6vm4dlsdv9cd7kmf0vfrh2kkzr45wrqr8m37miy0byzr4p9i"; + }; + releaseRev = v: "mathcomp-${v}"; + + # list of core mathcomp packages sorted by dependency order + packages = [ "ssreflect" "fingroup" "algebra" "solvable" "field" "character" "all" ]; + + mathcomp_ = package: let + mathcomp-deps = lib.optionals (package != "single") (map mathcomp_ (head (splitList (lib.pred.equal package) packages))); + pkgpath = if package == "single" then "mathcomp" else "mathcomp/${package}"; + pname = if package == "single" then "mathcomp" else "mathcomp-${package}"; + pkgallMake = '' + echo "all.v" > Make + echo "-I ." >> Make + echo "-R . mathcomp.all" >> Make + ''; + derivation = mkCoqDerivation ({ + inherit version pname defaultVersion release releaseRev repo owner; + + mlPlugin = versions.isLe "8.6" coq.coq-version; + nativeBuildInputs = optionals withDoc [ graphviz lua ]; + buildInputs = [ ncurses ]; + propagatedBuildInputs = mathcomp-deps; + + buildFlags = optional withDoc "doc"; + + preBuild = '' + if [[ -f etc/utils/ssrcoqdep ]] + then patchShebangs etc/utils/ssrcoqdep + fi + if [[ -f etc/buildlibgraph ]] + then patchShebangs etc/buildlibgraph + fi + '' + '' + cd ${pkgpath} + '' + optionalString (package == "all") pkgallMake; + + meta = { + homepage = "https://math-comp.github.io/"; + license = licenses.cecill-b; + maintainers = with maintainers; [ vbgl jwiegley cohencyril ]; + }; + } // optionalAttrs (package != "single") + { passthru = genAttrs packages mathcomp_; } + // optionalAttrs withDoc { + htmldoc_template = + fetchzip { + url = "https://github.com/math-comp/math-comp.github.io/archive/doc-1.12.0.zip"; + sha256 = "0y1352ha2yy6k2dl375sb1r68r1qi9dyyy7dyzj5lp9hxhhq69x8"; + }; + postBuild = '' + cp -rf _build_doc/* . + rm -r _build_doc + ''; + postInstall = + let tgt = "$out/share/coq/${coq.coq-version}/"; in + optionalString withDoc '' + mkdir -p ${tgt} + cp -r htmldoc ${tgt} + cp -r $htmldoc_template/htmldoc_template/* ${tgt}/htmldoc/ + ''; + buildTargets = "doc"; + extraInstallFlags = [ "-f Makefile.coq" ]; + }); + patched-derivation1 = derivation.overrideAttrs (o: + optionalAttrs (o.pname != null && o.pname == "mathcomp-all" && + o.version != null && o.version != "dev" && versions.isLt "1.7" o.version) + { preBuild = ""; buildPhase = ""; installPhase = "echo doing nothing"; } + ); + patched-derivation2 = patched-derivation1.overrideAttrs (o: + optionalAttrs (versions.isLe "8.7" coq.coq-version || + (o.version != "dev" && versions.isLe "1.7" o.version)) + { + installFlags = o.installFlags ++ [ "-f Makefile.coq" ]; + } + ); + patched-derivation = patched-derivation2.overrideAttrs (o: + optionalAttrs (o.version != null + && (o.version == "dev" || versions.isGe "2.0.0" o.version)) + { + propagatedBuildInputs = o.propagatedBuildInputs ++ [ hierarchy-builder ]; + } + ); + in patched-derivation; +in +mathcomp_ (if single then "single" else "all") diff --git a/coq-mathcomp-classical.opam b/coq-mathcomp-classical.opam index 98e33e80cd..1f2b1c898e 100644 --- a/coq-mathcomp-classical.opam +++ b/coq-mathcomp-classical.opam @@ -18,7 +18,7 @@ the Coq proof-assistant and using the Mathematical Components library.""" build: [make "-C" "classical" "-j%{jobs}%"] install: [make "-C" "classical" "install"] depends: [ - "coq" { (>= "8.15" & < "8.19~") | (= "dev") } + "coq" { (>= "8.15" & < "8.20~") | (= "dev") } "coq-mathcomp-ssreflect" { (>= "1.17.0" & < "1.20~") | (= "dev") } "coq-mathcomp-fingroup" "coq-mathcomp-algebra"