diff options
author | John Wiegley <johnw@newartisans.com> | 2017-11-12 09:34:06 -0800 |
---|---|---|
committer | John Wiegley <johnw@newartisans.com> | 2017-11-12 09:34:06 -0800 |
commit | bb038283c449c6ab37e32d9164a26602d23d2eee (patch) | |
tree | bb39f1c51d96b37cb9f96c0ee6753c5f5407167d /pkgs/development | |
parent | 7d6d4af1d1f05022d8c63c48e23227c238247b43 (diff) | |
download | nixlib-bb038283c449c6ab37e32d9164a26602d23d2eee.tar nixlib-bb038283c449c6ab37e32d9164a26602d23d2eee.tar.gz nixlib-bb038283c449c6ab37e32d9164a26602d23d2eee.tar.bz2 nixlib-bb038283c449c6ab37e32d9164a26602d23d2eee.tar.lz nixlib-bb038283c449c6ab37e32d9164a26602d23d2eee.tar.xz nixlib-bb038283c449c6ab37e32d9164a26602d23d2eee.tar.zst nixlib-bb038283c449c6ab37e32d9164a26602d23d2eee.zip |
coqPackages.metalib: New expression
Diffstat (limited to 'pkgs/development')
-rw-r--r-- | pkgs/development/coq-modules/metalib/default.nix | 53 |
1 files changed, 53 insertions, 0 deletions
diff --git a/pkgs/development/coq-modules/metalib/default.nix b/pkgs/development/coq-modules/metalib/default.nix new file mode 100644 index 000000000000..0304cb48b3b9 --- /dev/null +++ b/pkgs/development/coq-modules/metalib/default.nix @@ -0,0 +1,53 @@ +{ stdenv, fetchgit, coq, ocamlPackages, haskellPackages, which, ott +}: + +stdenv.mkDerivation rec { + name = "metalib-${coq.coq-version}-${version}"; + version = "20170713"; + + src = fetchgit { + url = https://github.com/plclub/metalib.git; + rev = "44e40aa082452dd333fc1ca2d2cc55311519bd52"; + sha256 = "1pra0nvx69q8d4bvpcvh9ngic1cy6z1chi03x56nisfqnc61b6y9"; + }; + + # The 'lngen' command-line utility is built from Haskell sources + lngen = with haskellPackages; mkDerivation { + pname = "lngen"; + version = "0.0.1"; + src = fetchgit { + url = https://github.com/plclub/lngen; + rev = "ea73ad315de33afd25f87ca738c71f358f1cd51c"; + sha256 = "1a0sj8n3lmsl1wlnqfy176k9lb9s8rl422bvg3ihl2i70ql8wisd"; + }; + isLibrary = true; + isExecutable = true; + libraryHaskellDepends = [ base containers mtl parsec syb ]; + executableHaskellDepends = [ base ]; + homepage = https://github.com/plclub/lngen; + description = "Tool for generating Locally Nameless definitions and proofs in Coq, working together with Ott"; + license = stdenv.lib.licenses.mit; + }; + + buildInputs = [ coq.ocaml coq.camlp5 which coq lngen ott ] + ++ (with ocamlPackages; [ findlib ]); + propagatedBuildInputs = [ coq ]; + + enableParallelBuilding = true; + + buildPhase = '' + (cd Metalib; make) + ''; + + installPhase = '' + (cd Metalib; make -f CoqSrc.mk DSTROOT=/ COQLIB=$out/lib/coq/${coq.coq-version}/ install) + ''; + + meta = with stdenv.lib; { + homepage = https://github.com/plclub/metalib; + license = licenses.mit; + maintainers = [ maintainers.jwiegley ]; + platforms = coq.meta.platforms; + }; + +} |