Skip to content

Commit f62e5cb

Browse files
garesgares
committed
nix
1 parent b4e8cbc commit f62e5cb

File tree

6 files changed

+199
-3751
lines changed

6 files changed

+199
-3751
lines changed

‎.github/workflows/nix-action-coq-8.16.yml‎

Lines changed: 0 additions & 1872 deletions
This file was deleted.

‎.github/workflows/nix-action-coq-8.17.yml‎

Lines changed: 0 additions & 1872 deletions
This file was deleted.

‎.github/workflows/nix-action-coq-8.18.yml‎

Lines changed: 53 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -296,6 +296,58 @@ jobs:
296296
name: Building/fetching current CI target
297297
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
298298
--argstr job "coq-bits"
299+
coq-elpi:
300+
needs:
301+
- coq
302+
runs-on: ubuntu-latest
303+
steps:
304+
- name: Determine which commit to initially checkout
305+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\
306+
\ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\
307+
\ }}\" >> $GITHUB_ENV\nfi\n"
308+
- name: Git checkout
309+
uses: actions/checkout@v3
310+
with:
311+
fetch-depth: 0
312+
ref: ${{ env.target_commit }}
313+
- name: Determine which commit to test
314+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\
315+
\ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\
316+
\ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
317+
\ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\
318+
\ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\
319+
\ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\
320+
\ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\
321+
\ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n"
322+
- name: Git checkout
323+
uses: actions/checkout@v3
324+
with:
325+
fetch-depth: 0
326+
ref: ${{ env.tested_commit }}
327+
- name: Cachix install
328+
uses: cachix/install-nix-action@v20
329+
with:
330+
nix_path: nixpkgs=channel:nixpkgs-unstable
331+
- name: Cachix setup math-comp
332+
uses: cachix/cachix-action@v12
333+
with:
334+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
335+
extraPullNames: coq, coq-community
336+
name: math-comp
337+
- id: stepCheck
338+
name: Checking presence of CI target coq-elpi
339+
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
340+
\ bundle \"coq-8.18\" --argstr job \"coq-elpi\" \\\n --dry-run 2>&1 > /dev/null)\n\
341+
echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\
342+
s/.*/built/\") >> $GITHUB_OUTPUT\n"
343+
- if: steps.stepCheck.outputs.status == 'built'
344+
name: 'Building/fetching previous CI target: coq'
345+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
346+
--argstr job "coq"
347+
- if: steps.stepCheck.outputs.status == 'built'
348+
name: Building/fetching current CI target
349+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
350+
--argstr job "coq-elpi"
299351
coqeal:
300352
needs:
301353
- coq
@@ -498,6 +550,7 @@ jobs:
498550
hierarchy-builder:
499551
needs:
500552
- coq
553+
- coq-elpi
501554
runs-on: ubuntu-latest
502555
steps:
503556
- name: Determine which commit to initially checkout

‎.nix/config.nix‎

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -33,15 +33,16 @@
3333
"coq-8.18".coqPackages = mcHBcommon // {
3434
coq.override.version = "8.18";
3535
interval.job = false;
36+
coq-elpi.override.version = "fix-synterp";
3637
};
3738

38-
"coq-8.17".coqPackages = mcHBcommon // {
39-
coq.override.version = "8.17";
40-
};
41-
42-
"coq-8.16".coqPackages = mcHBcommon // {
43-
coq.override.version = "8.16";
44-
};
39+
# "coq-8.17".coqPackages = mcHBcommon // {
40+
# coq.override.version = "8.17";
41+
# };
42+
#
43+
# "coq-8.16".coqPackages = mcHBcommon // {
44+
# coq.override.version = "8.16";
45+
# };
4546
};
4647
cachix.coq = {};
4748
cachix.coq-community = {};

‎.nix/coq-overlays/coq-elpi/default.nix‎

Lines changed: 73 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,73 @@
1+
{ lib, mkCoqDerivation, which, coq, version ? null }:
2+
3+
with builtins; with lib; let
4+
elpi = coq.ocamlPackages.elpi.override (lib.switch coq.coq-version [
5+
{ case = "8.11"; out = { version = "1.11.4"; };}
6+
{ case = "8.12"; out = { version = "1.12.0"; };}
7+
{ case = "8.13"; out = { version = "1.13.7"; };}
8+
{ case = "8.14"; out = { version = "1.13.7"; };}
9+
{ case = "8.15"; out = { version = "1.15.0"; };}
10+
{ case = "8.16"; out = { version = "1.17.0"; };}
11+
{ case = "8.17"; out = { version = "1.17.0"; };}
12+
{ case = "8.18"; out = { version = "v1.18.1"; };}
13+
] {} );
14+
in mkCoqDerivation {
15+
pname = "elpi";
16+
repo = "coq-elpi";
17+
owner = "LPCIC";
18+
inherit version;
19+
defaultVersion = lib.switch coq.coq-version [
20+
{ case = "8.18"; out = "1.19.0"; }
21+
{ case = "8.17"; out = "1.18.0"; }
22+
{ case = "8.16"; out = "1.15.6"; }
23+
{ case = "8.15"; out = "1.14.0"; }
24+
{ case = "8.14"; out = "1.11.2"; }
25+
{ case = "8.13"; out = "1.11.1"; }
26+
{ case = "8.12"; out = "1.8.3_8.12"; }
27+
{ case = "8.11"; out = "1.6.3_8.11"; }
28+
] null;
29+
release."1.19.0".sha256 = "sha256-kGoo61nJxeG/BqV+iQaV3iinwPStND+7+fYMxFkiKrQ=";
30+
release."1.18.0".sha256 = "sha256-2fCOlhqi4YkiL5n8SYHuc3pLH+DArf9zuMH7IhpBc2Y=";
31+
release."1.17.0".sha256 = "sha256-J8GatRKFU0ekNCG3V5dBI+FXypeHcLgC5QJYGYzFiEM=";
32+
release."1.15.6".sha256 = "sha256-qc0q01tW8NVm83801HHOBHe/7H1/F2WGDbKO6nCXfno=";
33+
release."1.15.1".sha256 = "sha256-NT2RlcIsFB9AvBhMxil4ZZIgx+KusMqDflj2HgQxsZg=";
34+
release."1.14.0".sha256 = "sha256:1v2p5dlpviwzky2i14cj7gcgf8cr0j54bdm9fl5iz1ckx60j6nvp";
35+
release."1.13.0".sha256 = "1j7s7dlnjbw222gnbrsjgmjck1yrx7h6hwm8zikcyxi0zys17w7n";
36+
release."1.12.1".sha256 = "sha256-4mO6/co7NcIQSGIQJyoO8lNWXr6dqz+bIYPO/G0cPkY=";
37+
release."1.11.2".sha256 = "0qk5cfh15y2zrja7267629dybd3irvxk1raz7z8qfir25a81ckd4";
38+
release."1.11.1".sha256 = "10j076vc2hdcbm15m6s7b6xdzibgfcbzlkgjnlkr2vv9k13qf8kc";
39+
release."1.10.1".sha256 = "1zsyx26dvj7pznfd2msl2w7zbw51q1nsdw0bdvdha6dga7ijf7xk";
40+
release."1.9.7".sha256 = "0rvn12h9dpk9s4pxy32p8j0a1h7ib7kg98iv1cbrdg25y5vs85n1";
41+
release."1.9.5".sha256 = "0gjdwmb6bvb5gh0a6ra48bz5fb3pr5kpxijb7a8mfydvar5i9qr6";
42+
release."1.9.4".sha256 = "0nii7238mya74f9g6147qmpg6gv6ic9b54x5v85nb6q60d9jh0jq";
43+
release."1.9.3".sha256 = "198irm800fx3n8n56vx1c6f626cizp1d7jfkrc6ba4iqhb62ma0z";
44+
release."1.9.2".sha256 = "1rr2fr8vjkc0is7vh1461aidz2iwkigdkp6bqss4hhv0c3ijnn07";
45+
release."1.8.3_8.12".sha256 = "15z2l4zy0qpw0ws7bvsmpmyv543aqghrfnl48nlwzn9q0v89p557";
46+
release."1.8.3_8.12".version = "1.8.3";
47+
release."1.8.2_8.12".sha256 = "1n6jwcdazvjgj8vsv2r9zgwpw5yqr5a1ndc2pwhmhqfl04b5dk4y";
48+
release."1.8.2_8.12".version = "1.8.2";
49+
release."1.8.1".sha256 = "1fbbdccdmr8g4wwpihzp4r2xacynjznf817lhijw6kqfav75zd0r";
50+
release."1.8.0".sha256 = "13ywjg94zkbki22hx7s4gfm9rr87r4ghsgan23xyl3l9z8q0idd1";
51+
release."1.7.0".sha256 = "1ws5cqr0xawv69prgygbl3q6dgglbaw0vc397h9flh90kxaqgyh8";
52+
release."1.6.3_8.11".sha256 = "1j340cr2bv95clzzkkfmsjkklham1mj84cmiyprzwv20q89zr1hp";
53+
release."1.6.3_8.11".version = "1.6.3";
54+
release."1.6.2_8.11".sha256 = "06xrx0ljilwp63ik2sxxr7h617dgbch042xfcnfpy5x96br147rn";
55+
release."1.6.2_8.11".version = "1.6.2";
56+
release."1.6.1_8.11".sha256 = "0yyyh35i1nb3pg4hw7cak15kj4y6y9l84nwar9k1ifdsagh5zq53";
57+
release."1.6.1_8.11".version = "1.6.1";
58+
release."1.6.0_8.11".sha256 = "0ahxjnzmd7kl3gl38kyjqzkfgllncr2ybnw8bvgrc6iddgga7bpq";
59+
release."1.6.0_8.11".version = "1.6.0";
60+
release."1.6.0".sha256 = "0kf99i43mlf750fr7fric764mm495a53mg5kahnbp6zcjcxxrm0b";
61+
releaseRev = v: "v${v}";
62+
63+
buildFlags = [ "OCAMLWARN=" ];
64+
65+
mlPlugin = true;
66+
propagatedBuildInputs = [ coq.ocamlPackages.findlib elpi ];
67+
68+
meta = {
69+
description = "Coq plugin embedding ELPI.";
70+
maintainers = [ maintainers.cohencyril ];
71+
license = licenses.lgpl21Plus;
72+
};
73+
}

‎.nix/ocaml-overlays/elpi/default.nix‎

Lines changed: 65 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,65 @@
1+
{ lib
2+
, buildDunePackage, camlp5
3+
, ocaml
4+
, menhir, menhirLib
5+
, atdgen
6+
, stdlib-shims
7+
, re, perl, ncurses
8+
, ppxlib, ppx_deriving
9+
, coqPackages
10+
, version ? if lib.versionAtLeast ocaml.version "4.08" then "1.17.0"
11+
else if lib.versionAtLeast ocaml.version "4.07" then "1.15.2" else "1.14.1"
12+
}:
13+
14+
let p5 = camlp5; in
15+
let camlp5 = p5.override { legacy = true; }; in
16+
17+
let fetched = coqPackages.metaFetch ({
18+
release."1.17.0".sha256 = "sha256-DTxE8CvYl0et20pxueydI+WzraI6UPHMNvxyp2gU/+w=";
19+
release."1.16.5".sha256 = "sha256-tKX5/cVPoBeHiUe+qn7c5FIRYCwY0AAukN7vSd/Nz9A=";
20+
release."1.15.2".sha256 = "sha256-XgopNP83POFbMNyl2D+gY1rmqGg03o++Ngv3zJfCn2s=";
21+
release."1.15.0".sha256 = "sha256:1ngdc41sgyzyz3i3lkzjhnj66gza5h912virkh077dyv17ysb6ar";
22+
release."1.14.1".sha256 = "sha256-BZPVL8ymjrE9kVGyf6bpc+GA2spS5JBpkUtZi04nPis=";
23+
release."1.13.7".sha256 = "10fnwz30bsvj7ii1vg4l1li5pd7n0qqmwj18snkdr5j9gk0apc1r";
24+
release."1.13.5".sha256 = "02a6r23mximrdvs6kgv6rp0r2dgk7zynbs99nn7lphw2c4189kka";
25+
release."1.13.1".sha256 = "12a9nbdvg9gybpw63lx3nw5wnxfznpraprb0wj3l68v1w43xq044";
26+
release."1.13.0".sha256 = "0dmzy058m1mkndv90byjaik6lzzfk3aaac7v84mpmkv6my23bygr";
27+
release."1.12.0".sha256 = "1agisdnaq9wrw3r73xz14yrq3wx742i6j8i5icjagqk0ypmly2is";
28+
release."1.11.4".sha256 = "1m0jk9swcs3jcrw5yyw5343v8mgax238cjb03s8gc4wipw1fn9f5";
29+
releaseRev = v: "v${v}";
30+
location = { domain = "github.com"; owner = "LPCIC"; repo = "elpi"; };
31+
}) version;
32+
in
33+
buildDunePackage rec {
34+
pname = "elpi";
35+
inherit (fetched) version src;
36+
37+
patches = lib.optional (version == "1.16.5")
38+
./atd_2_10.patch;
39+
40+
minimalOCamlVersion = "4.04";
41+
duneVersion = "3";
42+
43+
# atdgen is both a library and executable
44+
nativeBuildInputs = [ perl ]
45+
++ [ (if lib.versionAtLeast version "1.15" || version == "dev" then menhir else camlp5) ]
46+
++ lib.optional (lib.versionAtLeast version "1.16" || version == "dev") atdgen;
47+
buildInputs = [ ncurses ]
48+
++ lib.optional (lib.versionAtLeast version "1.16" || version == "dev") atdgen;
49+
50+
propagatedBuildInputs = [ re stdlib-shims ]
51+
++ [ menhirLib ]
52+
++ [ ppxlib ppx_deriving ]
53+
;
54+
55+
meta = with lib; {
56+
description = "Embeddable λProlog Interpreter";
57+
license = licenses.lgpl21Plus;
58+
maintainers = [ maintainers.vbgl ];
59+
homepage = "https://github.com/LPCIC/elpi";
60+
};
61+
62+
postPatch = ''
63+
substituteInPlace elpi_REPL.ml --replace "tput cols" "${ncurses}/bin/tput cols"
64+
'';
65+
}

0 commit comments

Comments
 (0)