-
Notifications
You must be signed in to change notification settings - Fork 21
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #406 from math-comp/coq-elpi-2
separate synterp phase
- Loading branch information
Showing
17 changed files
with
470 additions
and
3,923 deletions.
There are no files selected for viewing
This file was deleted.
Oops, something went wrong.
This file was deleted.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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; | ||
| }; | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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" | ||
| ''; | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,73 @@ | ||
| /* Hierarchy Builder: algebraic hierarchies made easy | ||
| This software is released under the terms of the MIT license */ | ||
|
|
||
| % runs P in a context where Coq #[attributes] are parsed | ||
| pred with-attributes i:prop. | ||
| with-attributes P :- | ||
| attributes A, | ||
| coq.parse-attributes A [ | ||
| att "verbose" bool, | ||
| att "mathcomp" bool, | ||
| att "mathcomp.axiom" string, | ||
| att "short.type" string, | ||
| att "short.pack" string, | ||
| att "key" string, | ||
| att "arg_sort" bool, | ||
| att "log" bool, | ||
| att "log.raw" bool, | ||
| att "compress_coercions" bool, | ||
| att "export" bool, | ||
| att "skip" string, | ||
| att "local" bool, | ||
| att "fail" bool, | ||
| att "doc" string, | ||
| att "primitive" bool, | ||
| att "non_forgetful_inheritance" bool, | ||
| att "hnf" bool, | ||
| ] Opts, !, | ||
| Opts => (save-docstring, P). | ||
|
|
||
| pred if-verbose i:prop. | ||
| if-verbose P :- get-option "verbose" tt, !, P. | ||
| if-verbose _. | ||
|
|
||
| % header of if-verbose messages | ||
| pred header o:string. | ||
| header Msg :- Msg is "[" ^ {std.any->string {gettimeofday}} ^ "] HB: ". | ||
|
|
||
| % approximation, it should be logical path, not the file name | ||
| pred coq.env.current-library o:string. | ||
| coq.env.current-library L :- loc.fields {get-option "elpi.loc"} L _ _ _ _. | ||
| coq.env.current-library "dummy.v". | ||
|
|
||
| % this is only declared in hb.db, this declaration is only to avoid a warning | ||
| pred docstring o:loc, o:string. | ||
|
|
||
| pred save-docstring. | ||
| save-docstring :- | ||
| if (get-option "elpi.loc" Loc, get-option "elpi.phase" "interp", get-option "doc" Txt) | ||
| (coq.elpi.accumulate _ "hb.db" (clause _ _ (docstring Loc Txt))) | ||
| true. | ||
|
|
||
| pred compute-filter i:option string, o:list string. | ||
| compute-filter none []. | ||
| compute-filter (some S) MFilter :- % S is a component of the current modpath | ||
| coq.env.current-path P, | ||
| rex_split "\\." S L, | ||
| compute-filter.aux P L MFilter, !. | ||
| compute-filter (some S) MFilter :- | ||
| coq.locate-module S M, | ||
| coq.modpath->path M MFilter. | ||
| compute-filter.aux [S|_] [S] [S] :- !. | ||
| compute-filter.aux [S|XS] [S|SS] [S|YS] :- compute-filter.aux XS SS YS. | ||
| compute-filter.aux [X|XS] L [X|YS] :- compute-filter.aux XS L YS. | ||
|
|
||
| pred list-uniq i:list A, o:list A. | ||
| pred list-uniq.seen i:A. | ||
| list-uniq [] []. | ||
| list-uniq [X|XS] YS :- list-uniq.seen X, !, list-uniq XS YS. | ||
| list-uniq [X|XS] [X|YS] :- list-uniq.seen X => list-uniq XS YS. | ||
|
|
||
| pred record-decl->id i:indt-decl, o:id. | ||
| record-decl->id (parameter _ _ _ D) N :- pi p\ record-decl->id (D p) N. | ||
| record-decl->id (record N _ _ _) N. |
Oops, something went wrong.