From b0f3278c21c376d0acb166ddfb79d701e5fd2caa Mon Sep 17 00:00:00 2001 From: Anton Podkopaev Date: Wed, 28 Jun 2023 14:13:40 +0200 Subject: [PATCH] Nix and CI configuration --- .github/workflows/nix-action-default.yml | 284 ++++++++++++++++++++ .nix/config.nix | 106 ++++++++ .nix/coq-nix-toolbox.nix | 1 + .nix/coq-overlays/hahn/default.nix | 63 +++++ .nix/coq-overlays/imm/default.nix | 64 +++++ .nix/coq-overlays/promising-lib/default.nix | 63 +++++ .nix/coq-overlays/sflib/default.nix | 63 +++++ default.nix | 12 + 8 files changed, 656 insertions(+) create mode 100644 .github/workflows/nix-action-default.yml create mode 100644 .nix/config.nix create mode 100644 .nix/coq-nix-toolbox.nix create mode 100644 .nix/coq-overlays/hahn/default.nix create mode 100644 .nix/coq-overlays/imm/default.nix create mode 100644 .nix/coq-overlays/promising-lib/default.nix create mode 100644 .nix/coq-overlays/sflib/default.nix create mode 100644 default.nix diff --git a/.github/workflows/nix-action-default.yml b/.github/workflows/nix-action-default.yml new file mode 100644 index 0000000..fd6e4fe --- /dev/null +++ b/.github/workflows/nix-action-default.yml @@ -0,0 +1,284 @@ +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 weakmemory + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: weakmemory + - 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 \"default\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\")\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 "default" + --argstr job "coq" + hahn: + 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 weakmemory + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: weakmemory + - id: stepCheck + name: Checking presence of CI target hahn + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"default\" --argstr job \"hahn\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\")\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 "default" + --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 "default" + --argstr job "hahn" + imm: + needs: + - coq + - hahn + - promising-lib + 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 weakmemory + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: weakmemory + - id: stepCheck + name: Checking presence of CI target imm + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"default\" --argstr job \"imm\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\")\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 "default" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: hahn' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default" + --argstr job "hahn" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: promising-lib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default" + --argstr job "promising-lib" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default" + --argstr job "imm" + promising-lib: + needs: + - coq + - sflib + 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 weakmemory + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: weakmemory + - id: stepCheck + name: Checking presence of CI target promising-lib + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"default\" --argstr job \"promising-lib\" \\\n --dry-run 2>&1\ + \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\")\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 "default" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: sflib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default" + --argstr job "sflib" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default" + --argstr job "promising-lib" + sflib: + 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 weakmemory + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: weakmemory + - id: stepCheck + name: Checking presence of CI target sflib + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"default\" --argstr job \"sflib\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\")\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 "default" + --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 "default" + --argstr job "sflib" +name: Nix CI for bundle default +'on': + pull_request: + paths: + - .github/workflows/** + pull_request_target: + types: + - opened + - synchronize + - reopened + push: + branches: + - master diff --git a/.nix/config.nix b/.nix/config.nix new file mode 100644 index 0000000..9e0a2cb --- /dev/null +++ b/.nix/config.nix @@ -0,0 +1,106 @@ +{ + ## 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 = "imm"; + + ## 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 = "default"; + + ## write one `bundles.name` attribute set per + ## alternative configuration + ## When generating GitHub Action CI, one workflow file + ## will be created per bundle + bundles.default = { + + ## You can override Coq and other Coq coqPackages + ## through the following attribute + coqPackages.coq.override.version = "8.17"; + coqPackages.hahn.override.version = "anlun:master"; + coqPackages.sflib.override.version = "master"; + coqPackages.promising-lib.override.version = "weakmemory:master"; + + ## In some cases, light overrides are not available/enough + ## in which case you can use either + # coqPackages..overrideAttrs = o: ; + ## or a "long" overlay to put in `.nix/coq-overlays + ## you may use `nix-shell --run fetchOverlay ` + ## to automatically retrieve the one from nixpkgs + ## if it exists and is correctly named/located + + ## You can override Coq and other coqPackages + ## through the following attribute + ## If does not support light overrides, + ## you may use `overrideAttrs` or long overlays + ## located in `.nix/ocaml-overlays` + ## (there is no automation for this one) + # ocamlPackages..override.version = "x.xx"; + + ## You can also override packages from the nixpkgs toplevel + # .override.overrideAttrs = o: ; + ## Or put an overlay in `.nix/overlays` + + ## you may mark a package as a main CI job (one to take deps and + ## rev deps from) as follows + # coqPackages..main-job = true; + ## by default the current package and its shell attributes are main jobs + + ## you may mark a package as a CI job as follows + # coqPackages..job = "test"; + ## It can then built through + ## nix-build --argstr bundle "default" --arg job "test"; + ## in the absence of such a directive, the job "another-pkg" will + ## is still available, but will be automatically included in the CI + ## via the command genNixActions only if it is a dependency or a + ## reverse dependency of a job flagged as "main-job" (see above). + + ## Run on push on following branches (default [ "master" ]) + # push-branches = [ "master" "branch2" ]; + }; + + ## Cachix caches to use in CI + ## Below we list some standard ones + cachix.coq = {}; + cachix.math-comp = {}; + cachix.coq-community = {}; + + ## If you have write access to one of these caches you can + ## provide the auth token or signing key through a secret + ## variable on GitHub. Then, you should give the variable + ## name here. For instance, coq-community projects can use + ## the following line instead of the one above: + cachix.weakmemory.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 0000000..60b452b --- /dev/null +++ b/.nix/coq-nix-toolbox.nix @@ -0,0 +1 @@ +"f72eef6033e0abc9fa06f94fe718d8aa9c0d031a" diff --git a/.nix/coq-overlays/hahn/default.nix b/.nix/coq-overlays/hahn/default.nix new file mode 100644 index 0000000..2c9d02e --- /dev/null +++ b/.nix/coq-overlays/hahn/default.nix @@ -0,0 +1,63 @@ +## File initially generated by createOverlay +## and then supposedly modified manually. +## Some hints for manual modifications are in the file, +## but the full doc is on nixos / nix packages website: +## https://nixos.org/manual/nixpkgs/stable/#sec-language-coq + +{ lib, mkCoqDerivation, which, coq + ## declare extra dependencies here, to be used in propagateBuildInputs e.g. + # , mathcomp, coq-elpi + , version ? null }: + +with lib; mkCoqDerivation { + pname = "hahn"; + ## you can configure the domain, owner and repository, the default are: + # repo = "hahn"; + owner = "vafeiadis"; + # domain = "github.com"; + + inherit version; +## The `defaultVersion` attribute is important for nixpkgs but can be kept unchanged +## for local usage since it will be ignored locally if +## - this derivation corresponds to the main attribute, +## - or its version is overridden (by a branch, PR, url or path) in `.nix/config.nix`. + defaultVersion = with versions; switch coq.coq-version [ + ## Example of possible dependencies + # { case = range "8.13" "8.14"; out = "1.2.0"; } + ## other predicates are `isLe v`, `isLt v`, `isGe v`, `isGt v`, `isEq v` etc + ] null; + + ## Declare existing releases + ## leave sha256 empty at first and then copy paste + ## the resulting sha given by the error message + # release."1.1.1".sha256 = ""; + ## if the tag is not exactly the version number you can amend like this + # release."1.1.1".rev = "v1.1.1"; + ## if a consistent scheme gives the tag from the release number, you can do like this: + # releaseRev = v: "v${v}"; + + ## Add dependencies in here. In particular you can add + ## - arbitrary nix packages (you need to require them at the beginning of the file) + ## - Coq packages (require them at the beginning of the file) + ## - OCaml packages (use `coq.ocamlPackages.xxx`, no need to require them at the beginning of the file) + # propagatedBuildInputs = [ ]; ## e.g. `= [ mathcomp coq-elpi ]` + + ## Does the package contain OCaml code? + # mlPlugin = false; + + # installPhase = "make -f Makefile.coq install"; + extraInstallFlags = ["-f" "Makefile.coq"]; + + ## Give some meta data + ## This is needed for submitting the package to nixpkgs but not required for local use. + meta = { + ## Describe your package in one sentence + # description = ""; + ## Kindly ask one of these people if they want to be an official maintainer. + ## (You might also consider adding yourself to the list of maintainers) + # maintainers = with maintainers; [ cohencyril siraben vbgl Zimmi48 ]; + ## Pick a license from + ## https://github.com/NixOS/nixpkgs/blob/master/lib/licenses.nix + # license = licenses.mit; + }; +} diff --git a/.nix/coq-overlays/imm/default.nix b/.nix/coq-overlays/imm/default.nix new file mode 100644 index 0000000..90578d4 --- /dev/null +++ b/.nix/coq-overlays/imm/default.nix @@ -0,0 +1,64 @@ +## File initially generated by createOverlay +## and then supposedly modified manually. +## Some hints for manual modifications are in the file, +## but the full doc is on nixos / nix packages website: +## https://nixos.org/manual/nixpkgs/stable/#sec-language-coq + +{ lib, mkCoqDerivation, which, coq + ## declare extra dependencies here, to be used in propagateBuildInputs e.g. + , hahn, promising-lib + # , mathcomp, coq-elpi + , version ? null }: + +with lib; mkCoqDerivation { + pname = "imm"; + ## you can configure the domain, owner and repository, the default are: + # repo = "imm"; + owner = "weakmemory"; + # domain = "github.com"; + + inherit version; +## The `defaultVersion` attribute is important for nixpkgs but can be kept unchanged +## for local usage since it will be ignored locally if +## - this derivation corresponds to the main attribute, +## - or its version is overridden (by a branch, PR, url or path) in `.nix/config.nix`. + defaultVersion = with versions; switch coq.coq-version [ + ## Example of possible dependencies + # { case = range "8.13" "8.14"; out = "1.2.0"; } + ## other predicates are `isLe v`, `isLt v`, `isGe v`, `isGt v`, `isEq v` etc + ] null; + + ## Declare existing releases + ## leave sha256 empty at first and then copy paste + ## the resulting sha given by the error message + # release."1.1.1".sha256 = ""; + ## if the tag is not exactly the version number you can amend like this + # release."1.1.1".rev = "v1.1.1"; + ## if a consistent scheme gives the tag from the release number, you can do like this: + # releaseRev = v: "v${v}"; + + ## Add dependencies in here. In particular you can add + ## - arbitrary nix packages (you need to require them at the beginning of the file) + ## - Coq packages (require them at the beginning of the file) + ## - OCaml packages (use `coq.ocamlPackages.xxx`, no need to require them at the beginning of the file) + propagatedBuildInputs = [hahn promising-lib]; ## e.g. `= [ mathcomp coq-elpi ]` + + ## Does the package contain OCaml code? + # mlPlugin = false; + + dontConfigure = true; + installPhase = "make -f Makefile.coq install"; + + ## Give some meta data + ## This is needed for submitting the package to nixpkgs but not required for local use. + meta = { + ## Describe your package in one sentence + # description = ""; + ## Kindly ask one of these people if they want to be an official maintainer. + ## (You might also consider adding yourself to the list of maintainers) + # maintainers = with maintainers; [ cohencyril siraben vbgl Zimmi48 ]; + ## Pick a license from + ## https://github.com/NixOS/nixpkgs/blob/master/lib/licenses.nix + # license = licenses.mit; + }; +} diff --git a/.nix/coq-overlays/promising-lib/default.nix b/.nix/coq-overlays/promising-lib/default.nix new file mode 100644 index 0000000..546f4e2 --- /dev/null +++ b/.nix/coq-overlays/promising-lib/default.nix @@ -0,0 +1,63 @@ +## File initially generated by createOverlay +## and then supposedly modified manually. +## Some hints for manual modifications are in the file, +## but the full doc is on nixos / nix packages website: +## https://nixos.org/manual/nixpkgs/stable/#sec-language-coq + +{ lib, mkCoqDerivation, which, coq + ## declare extra dependencies here, to be used in propagateBuildInputs e.g. + , sflib# , mathcomp, coq-elpi + , version ? null }: + +with lib; mkCoqDerivation { + pname = "promising-lib"; + ## you can configure the domain, owner and repository, the default are: + # repo = "promising-lib"; + owner = "snu-sf"; + # domain = "github.com"; + + inherit version; +## The `defaultVersion` attribute is important for nixpkgs but can be kept unchanged +## for local usage since it will be ignored locally if +## - this derivation corresponds to the main attribute, +## - or its version is overridden (by a branch, PR, url or path) in `.nix/config.nix`. + defaultVersion = with versions; switch coq.coq-version [ + ## Example of possible dependencies + # { case = range "8.13" "8.14"; out = "1.2.0"; } + ## other predicates are `isLe v`, `isLt v`, `isGe v`, `isGt v`, `isEq v` etc + ] null; + + ## Declare existing releases + ## leave sha256 empty at first and then copy paste + ## the resulting sha given by the error message + # release."1.1.1".sha256 = ""; + ## if the tag is not exactly the version number you can amend like this + # release."1.1.1".rev = "v1.1.1"; + ## if a consistent scheme gives the tag from the release number, you can do like this: + # releaseRev = v: "v${v}"; + + ## Add dependencies in here. In particular you can add + ## - arbitrary nix packages (you need to require them at the beginning of the file) + ## - Coq packages (require them at the beginning of the file) + ## - OCaml packages (use `coq.ocamlPackages.xxx`, no need to require them at the beginning of the file) + propagatedBuildInputs = [sflib]; ## e.g. `= [ mathcomp coq-elpi ]` + + ## Does the package contain OCaml code? + # mlPlugin = false; + + # installPhase = "make -f Makefile.coq install"; + extraInstallFlags = ["-f" "Makefile.coq"]; + + ## Give some meta data + ## This is needed for submitting the package to nixpkgs but not required for local use. + meta = { + ## Describe your package in one sentence + # description = ""; + ## Kindly ask one of these people if they want to be an official maintainer. + ## (You might also consider adding yourself to the list of maintainers) + # maintainers = with maintainers; [ cohencyril siraben vbgl Zimmi48 ]; + ## Pick a license from + ## https://github.com/NixOS/nixpkgs/blob/master/lib/licenses.nix + # license = licenses.mit; + }; +} diff --git a/.nix/coq-overlays/sflib/default.nix b/.nix/coq-overlays/sflib/default.nix new file mode 100644 index 0000000..af2a384 --- /dev/null +++ b/.nix/coq-overlays/sflib/default.nix @@ -0,0 +1,63 @@ +## File initially generated by createOverlay +## and then supposedly modified manually. +## Some hints for manual modifications are in the file, +## but the full doc is on nixos / nix packages website: +## https://nixos.org/manual/nixpkgs/stable/#sec-language-coq + +{ lib, mkCoqDerivation, which, coq + ## declare extra dependencies here, to be used in propagateBuildInputs e.g. + # , mathcomp, coq-elpi + , version ? null }: + +with lib; mkCoqDerivation { + pname = "sflib"; + ## you can configure the domain, owner and repository, the default are: + # repo = "sflib"; + owner = "snu-sf"; + # domain = "github.com"; + + inherit version; +## The `defaultVersion` attribute is important for nixpkgs but can be kept unchanged +## for local usage since it will be ignored locally if +## - this derivation corresponds to the main attribute, +## - or its version is overridden (by a branch, PR, url or path) in `.nix/config.nix`. + defaultVersion = with versions; switch coq.coq-version [ + ## Example of possible dependencies + # { case = range "8.13" "8.14"; out = "1.2.0"; } + ## other predicates are `isLe v`, `isLt v`, `isGe v`, `isGt v`, `isEq v` etc + ] null; + + ## Declare existing releases + ## leave sha256 empty at first and then copy paste + ## the resulting sha given by the error message + # release."1.1.1".sha256 = ""; + ## if the tag is not exactly the version number you can amend like this + # release."1.1.1".rev = "v1.1.1"; + ## if a consistent scheme gives the tag from the release number, you can do like this: + # releaseRev = v: "v${v}"; + + ## Add dependencies in here. In particular you can add + ## - arbitrary nix packages (you need to require them at the beginning of the file) + ## - Coq packages (require them at the beginning of the file) + ## - OCaml packages (use `coq.ocamlPackages.xxx`, no need to require them at the beginning of the file) + # propagatedBuildInputs = [ ]; ## e.g. `= [ mathcomp coq-elpi ]` + + ## Does the package contain OCaml code? + # mlPlugin = false; + + # installPhase = "make -f Makefile.coq install"; + extraInstallFlags = ["-f" "Makefile.coq"]; + + ## Give some meta data + ## This is needed for submitting the package to nixpkgs but not required for local use. + meta = { + ## Describe your package in one sentence + # description = ""; + ## Kindly ask one of these people if they want to be an official maintainer. + ## (You might also consider adding yourself to the list of maintainers) + # maintainers = with maintainers; [ cohencyril siraben vbgl Zimmi48 ]; + ## Pick a license from + ## https://github.com/NixOS/nixpkgs/blob/master/lib/licenses.nix + # license = licenses.mit; + }; +} diff --git a/default.nix b/default.nix new file mode 100644 index 0000000..1a24d7a --- /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)