Skip to content

Commit

Permalink
nix
Browse files Browse the repository at this point in the history
  • Loading branch information
gares committed Dec 5, 2023
1 parent bad63e3 commit e961027
Show file tree
Hide file tree
Showing 6 changed files with 199 additions and 3,751 deletions.
1,872 changes: 0 additions & 1,872 deletions .github/workflows/nix-action-coq-8.16.yml

This file was deleted.

1,872 changes: 0 additions & 1,872 deletions .github/workflows/nix-action-coq-8.17.yml

This file was deleted.

53 changes: 53 additions & 0 deletions .github/workflows/nix-action-coq-8.18.yml
Original file line number Diff line number Diff line change
Expand Up @@ -296,6 +296,58 @@ jobs:
name: Building/fetching current CI target
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
--argstr job "coq-bits"
coq-elpi:
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 coq-elpi
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
\ bundle \"coq-8.18\" --argstr job \"coq-elpi\" \\\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 "coq-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 "coq-8.18"
--argstr job "coq-elpi"
coqeal:
needs:
- coq
Expand Down Expand Up @@ -498,6 +550,7 @@ jobs:
hierarchy-builder:
needs:
- coq
- coq-elpi
runs-on: ubuntu-latest
steps:
- name: Determine which commit to initially checkout
Expand Down
15 changes: 8 additions & 7 deletions .nix/config.nix
Original file line number Diff line number Diff line change
Expand Up @@ -33,15 +33,16 @@
"coq-8.18".coqPackages = mcHBcommon // {
coq.override.version = "8.18";
interval.job = false;
coq-elpi.override.version = "fix-synterp";
};

"coq-8.17".coqPackages = mcHBcommon // {
coq.override.version = "8.17";
};

"coq-8.16".coqPackages = mcHBcommon // {
coq.override.version = "8.16";
};
# "coq-8.17".coqPackages = mcHBcommon // {
# coq.override.version = "8.17";
# };
#
# "coq-8.16".coqPackages = mcHBcommon // {
# coq.override.version = "8.16";
# };
};
cachix.coq = {};
cachix.coq-community = {};
Expand Down
73 changes: 73 additions & 0 deletions .nix/coq-overlays/coq-elpi/default.nix
Original file line number Diff line number Diff line change
@@ -0,0 +1,73 @@
{ lib, mkCoqDerivation, which, coq, version ? null }:

with builtins; with lib; let
elpi = coq.ocamlPackages.elpi.override (lib.switch coq.coq-version [
{ case = "8.11"; out = { version = "1.11.4"; };}
{ case = "8.12"; out = { version = "1.12.0"; };}
{ case = "8.13"; out = { version = "1.13.7"; };}
{ case = "8.14"; out = { version = "1.13.7"; };}
{ case = "8.15"; out = { version = "1.15.0"; };}
{ case = "8.16"; out = { version = "1.17.0"; };}
{ case = "8.17"; out = { version = "1.17.0"; };}
{ case = "8.18"; out = { version = "v1.18.1"; };}
] {} );
in mkCoqDerivation {
pname = "elpi";
repo = "coq-elpi";
owner = "LPCIC";
inherit version;
defaultVersion = lib.switch coq.coq-version [
{ case = "8.18"; out = "1.19.0"; }
{ case = "8.17"; out = "1.18.0"; }
{ case = "8.16"; out = "1.15.6"; }
{ case = "8.15"; out = "1.14.0"; }
{ case = "8.14"; out = "1.11.2"; }
{ case = "8.13"; out = "1.11.1"; }
{ case = "8.12"; out = "1.8.3_8.12"; }
{ case = "8.11"; out = "1.6.3_8.11"; }
] null;
release."1.19.0".sha256 = "sha256-kGoo61nJxeG/BqV+iQaV3iinwPStND+7+fYMxFkiKrQ=";
release."1.18.0".sha256 = "sha256-2fCOlhqi4YkiL5n8SYHuc3pLH+DArf9zuMH7IhpBc2Y=";
release."1.17.0".sha256 = "sha256-J8GatRKFU0ekNCG3V5dBI+FXypeHcLgC5QJYGYzFiEM=";
release."1.15.6".sha256 = "sha256-qc0q01tW8NVm83801HHOBHe/7H1/F2WGDbKO6nCXfno=";
release."1.15.1".sha256 = "sha256-NT2RlcIsFB9AvBhMxil4ZZIgx+KusMqDflj2HgQxsZg=";
release."1.14.0".sha256 = "sha256:1v2p5dlpviwzky2i14cj7gcgf8cr0j54bdm9fl5iz1ckx60j6nvp";
release."1.13.0".sha256 = "1j7s7dlnjbw222gnbrsjgmjck1yrx7h6hwm8zikcyxi0zys17w7n";
release."1.12.1".sha256 = "sha256-4mO6/co7NcIQSGIQJyoO8lNWXr6dqz+bIYPO/G0cPkY=";
release."1.11.2".sha256 = "0qk5cfh15y2zrja7267629dybd3irvxk1raz7z8qfir25a81ckd4";
release."1.11.1".sha256 = "10j076vc2hdcbm15m6s7b6xdzibgfcbzlkgjnlkr2vv9k13qf8kc";
release."1.10.1".sha256 = "1zsyx26dvj7pznfd2msl2w7zbw51q1nsdw0bdvdha6dga7ijf7xk";
release."1.9.7".sha256 = "0rvn12h9dpk9s4pxy32p8j0a1h7ib7kg98iv1cbrdg25y5vs85n1";
release."1.9.5".sha256 = "0gjdwmb6bvb5gh0a6ra48bz5fb3pr5kpxijb7a8mfydvar5i9qr6";
release."1.9.4".sha256 = "0nii7238mya74f9g6147qmpg6gv6ic9b54x5v85nb6q60d9jh0jq";
release."1.9.3".sha256 = "198irm800fx3n8n56vx1c6f626cizp1d7jfkrc6ba4iqhb62ma0z";
release."1.9.2".sha256 = "1rr2fr8vjkc0is7vh1461aidz2iwkigdkp6bqss4hhv0c3ijnn07";
release."1.8.3_8.12".sha256 = "15z2l4zy0qpw0ws7bvsmpmyv543aqghrfnl48nlwzn9q0v89p557";
release."1.8.3_8.12".version = "1.8.3";
release."1.8.2_8.12".sha256 = "1n6jwcdazvjgj8vsv2r9zgwpw5yqr5a1ndc2pwhmhqfl04b5dk4y";
release."1.8.2_8.12".version = "1.8.2";
release."1.8.1".sha256 = "1fbbdccdmr8g4wwpihzp4r2xacynjznf817lhijw6kqfav75zd0r";
release."1.8.0".sha256 = "13ywjg94zkbki22hx7s4gfm9rr87r4ghsgan23xyl3l9z8q0idd1";
release."1.7.0".sha256 = "1ws5cqr0xawv69prgygbl3q6dgglbaw0vc397h9flh90kxaqgyh8";
release."1.6.3_8.11".sha256 = "1j340cr2bv95clzzkkfmsjkklham1mj84cmiyprzwv20q89zr1hp";
release."1.6.3_8.11".version = "1.6.3";
release."1.6.2_8.11".sha256 = "06xrx0ljilwp63ik2sxxr7h617dgbch042xfcnfpy5x96br147rn";
release."1.6.2_8.11".version = "1.6.2";
release."1.6.1_8.11".sha256 = "0yyyh35i1nb3pg4hw7cak15kj4y6y9l84nwar9k1ifdsagh5zq53";
release."1.6.1_8.11".version = "1.6.1";
release."1.6.0_8.11".sha256 = "0ahxjnzmd7kl3gl38kyjqzkfgllncr2ybnw8bvgrc6iddgga7bpq";
release."1.6.0_8.11".version = "1.6.0";
release."1.6.0".sha256 = "0kf99i43mlf750fr7fric764mm495a53mg5kahnbp6zcjcxxrm0b";
releaseRev = v: "v${v}";

buildFlags = [ "OCAMLWARN=" ];

mlPlugin = true;
propagatedBuildInputs = [ coq.ocamlPackages.findlib elpi ];

meta = {
description = "Coq plugin embedding ELPI.";
maintainers = [ maintainers.cohencyril ];
license = licenses.lgpl21Plus;
};
}
65 changes: 65 additions & 0 deletions .nix/ocaml-overlays/elpi/default.nix
Original file line number Diff line number Diff line change
@@ -0,0 +1,65 @@
{ lib
, buildDunePackage, camlp5
, ocaml
, menhir, menhirLib
, atdgen
, stdlib-shims
, re, perl, ncurses
, ppxlib, ppx_deriving
, coqPackages
, version ? if lib.versionAtLeast ocaml.version "4.08" then "1.17.0"
else if lib.versionAtLeast ocaml.version "4.07" then "1.15.2" else "1.14.1"
}:

let p5 = camlp5; in
let camlp5 = p5.override { legacy = true; }; in

let fetched = coqPackages.metaFetch ({
release."1.17.0".sha256 = "sha256-DTxE8CvYl0et20pxueydI+WzraI6UPHMNvxyp2gU/+w=";
release."1.16.5".sha256 = "sha256-tKX5/cVPoBeHiUe+qn7c5FIRYCwY0AAukN7vSd/Nz9A=";
release."1.15.2".sha256 = "sha256-XgopNP83POFbMNyl2D+gY1rmqGg03o++Ngv3zJfCn2s=";
release."1.15.0".sha256 = "sha256:1ngdc41sgyzyz3i3lkzjhnj66gza5h912virkh077dyv17ysb6ar";
release."1.14.1".sha256 = "sha256-BZPVL8ymjrE9kVGyf6bpc+GA2spS5JBpkUtZi04nPis=";
release."1.13.7".sha256 = "10fnwz30bsvj7ii1vg4l1li5pd7n0qqmwj18snkdr5j9gk0apc1r";
release."1.13.5".sha256 = "02a6r23mximrdvs6kgv6rp0r2dgk7zynbs99nn7lphw2c4189kka";
release."1.13.1".sha256 = "12a9nbdvg9gybpw63lx3nw5wnxfznpraprb0wj3l68v1w43xq044";
release."1.13.0".sha256 = "0dmzy058m1mkndv90byjaik6lzzfk3aaac7v84mpmkv6my23bygr";
release."1.12.0".sha256 = "1agisdnaq9wrw3r73xz14yrq3wx742i6j8i5icjagqk0ypmly2is";
release."1.11.4".sha256 = "1m0jk9swcs3jcrw5yyw5343v8mgax238cjb03s8gc4wipw1fn9f5";
releaseRev = v: "v${v}";
location = { domain = "github.com"; owner = "LPCIC"; repo = "elpi"; };
}) version;
in
buildDunePackage rec {
pname = "elpi";
inherit (fetched) version src;

patches = lib.optional (version == "1.16.5")
./atd_2_10.patch;

minimalOCamlVersion = "4.04";
duneVersion = "3";

# atdgen is both a library and executable
nativeBuildInputs = [ perl ]
++ [ (if lib.versionAtLeast version "1.15" || version == "dev" then menhir else camlp5) ]
++ lib.optional (lib.versionAtLeast version "1.16" || version == "dev") atdgen;
buildInputs = [ ncurses ]
++ lib.optional (lib.versionAtLeast version "1.16" || version == "dev") atdgen;

propagatedBuildInputs = [ re stdlib-shims ]
++ [ menhirLib ]
++ [ ppxlib ppx_deriving ]
;

meta = with lib; {
description = "Embeddable λProlog Interpreter";
license = licenses.lgpl21Plus;
maintainers = [ maintainers.vbgl ];
homepage = "https://github.com/LPCIC/elpi";
};

postPatch = ''
substituteInPlace elpi_REPL.ml --replace "tput cols" "${ncurses}/bin/tput cols"
'';
}

0 comments on commit e961027

Please sign in to comment.