Skip to content

Commit

Permalink
library-undecidability rev dep
Browse files Browse the repository at this point in the history
  • Loading branch information
4ever2 committed Oct 14, 2024
1 parent 02cc21a commit f7966ec
Show file tree
Hide file tree
Showing 3 changed files with 93 additions and 33 deletions.
64 changes: 32 additions & 32 deletions .github/workflows/nix-action-coq-8.19.yml
Original file line number Diff line number Diff line change
@@ -1,8 +1,6 @@
jobs:
ElmExtraction:
needs:
- coq
- metacoq
coq:
needs: []
runs-on: ubuntu-latest
steps:
- name: Determine which commit to initially checkout
Expand All @@ -29,7 +27,7 @@ jobs:
fetch-depth: 0
ref: ${{ env.tested_commit }}
- name: Cachix install
uses: cachix/install-nix-action@v30
uses: cachix/install-nix-action@v27
with:
nix_path: nixpkgs=channel:nixpkgs-unstable
- name: Cachix setup coq
Expand All @@ -38,25 +36,18 @@ jobs:
extraPullNames: coq-community
name: coq
- id: stepCheck
name: Checking presence of CI target ElmExtraction
name: Checking presence of CI target coq
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
\ bundle \"coq-8.19\" --argstr job \"ElmExtraction\" \\\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 "coq-8.19"
--argstr job "coq"
- if: steps.stepCheck.outputs.status == 'built'
name: 'Building/fetching previous CI target: metacoq'
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19"
--argstr job "metacoq"
\ bundle \"coq-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 "coq-8.19"
--argstr job "ElmExtraction"
coq:
needs: []
--argstr job "coq"
equations:
needs:
- coq
runs-on: ubuntu-latest
steps:
- name: Determine which commit to initially checkout
Expand All @@ -83,7 +74,7 @@ jobs:
fetch-depth: 0
ref: ${{ env.tested_commit }}
- name: Cachix install
uses: cachix/install-nix-action@v30
uses: cachix/install-nix-action@v27
with:
nix_path: nixpkgs=channel:nixpkgs-unstable
- name: Cachix setup coq
Expand All @@ -92,18 +83,23 @@ jobs:
extraPullNames: coq-community
name: coq
- id: stepCheck
name: Checking presence of CI target coq
name: Checking presence of CI target equations
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
\ bundle \"coq-8.19\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\
\ bundle \"coq-8.19\" --argstr job \"equations\" \\\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
name: 'Building/fetching previous CI target: coq'
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19"
--argstr job "coq"
equations:
- if: steps.stepCheck.outputs.status == 'built'
name: Building/fetching current CI target
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19"
--argstr job "equations"
library-undecidability:
needs:
- coq
- metacoq
runs-on: ubuntu-latest
steps:
- name: Determine which commit to initially checkout
Expand All @@ -130,7 +126,7 @@ jobs:
fetch-depth: 0
ref: ${{ env.tested_commit }}
- name: Cachix install
uses: cachix/install-nix-action@v30
uses: cachix/install-nix-action@v27
with:
nix_path: nixpkgs=channel:nixpkgs-unstable
- name: Cachix setup coq
Expand All @@ -139,19 +135,23 @@ jobs:
extraPullNames: coq-community
name: coq
- id: stepCheck
name: Checking presence of CI target equations
name: Checking presence of CI target library-undecidability
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
\ bundle \"coq-8.19\" --argstr job \"equations\" \\\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 \"coq-8.19\" --argstr job \"library-undecidability\" \\\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 "coq-8.19"
--argstr job "coq"
- if: steps.stepCheck.outputs.status == 'built'
name: 'Building/fetching previous CI target: metacoq'
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19"
--argstr job "metacoq"
- if: steps.stepCheck.outputs.status == 'built'
name: Building/fetching current CI target
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19"
--argstr job "equations"
--argstr job "library-undecidability"
metacoq:
needs:
- coq
Expand Down Expand Up @@ -182,7 +182,7 @@ jobs:
fetch-depth: 0
ref: ${{ env.tested_commit }}
- name: Cachix install
uses: cachix/install-nix-action@v30
uses: cachix/install-nix-action@v27
with:
nix_path: nixpkgs=channel:nixpkgs-unstable
- name: Cachix setup coq
Expand Down
3 changes: 2 additions & 1 deletion .nix/config.nix
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,8 @@
push-branches = ["coq-8.19"];

# Reverse dependencies
coqPackages.ElmExtraction.override.version = "master";
# coqPackages.ElmExtraction.override.version = "master";
coqPackages.library-undecidability.override.version = "coq-8.19";
};

## Cachix caches to use in CI
Expand Down
59 changes: 59 additions & 0 deletions .nix/coq-overlays/library-undecidability/default.nix
Original file line number Diff line number Diff line change
@@ -0,0 +1,59 @@
## 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.
, metacoq
, version ? null }:

with lib; mkCoqDerivation {
pname = "library-undecidability";
repo = "coq-library-undecidability";
owner = "uds-psl";
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 = [ metacoq ];

## Does the package contain OCaml code?
# mlPlugin = false;

## 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;
};
}

0 comments on commit f7966ec

Please sign in to comment.