diff options
author | John Wiegley <johnw@newartisans.com> | 2015-01-09 14:07:02 -0600 |
---|---|---|
committer | John Wiegley <johnw@newartisans.com> | 2015-01-09 14:07:39 -0600 |
commit | 2aec1b0f31f35e7ce416b56ff2405f5fe05acf52 (patch) | |
tree | 1f6c49acec7b6d49b916c39b0dbf72396dc8e3cd /pkgs/development/coq-modules | |
parent | d2566a190e1e0526e458bff0d5e19e699dee1a4f (diff) | |
download | nixlib-2aec1b0f31f35e7ce416b56ff2405f5fe05acf52.tar nixlib-2aec1b0f31f35e7ce416b56ff2405f5fe05acf52.tar.gz nixlib-2aec1b0f31f35e7ce416b56ff2405f5fe05acf52.tar.bz2 nixlib-2aec1b0f31f35e7ce416b56ff2405f5fe05acf52.tar.lz nixlib-2aec1b0f31f35e7ce416b56ff2405f5fe05acf52.tar.xz nixlib-2aec1b0f31f35e7ce416b56ff2405f5fe05acf52.tar.zst nixlib-2aec1b0f31f35e7ce416b56ff2405f5fe05acf52.zip |
coqPackages.fiat: new expression
Diffstat (limited to 'pkgs/development/coq-modules')
-rw-r--r-- | pkgs/development/coq-modules/fiat/default.nix | 41 |
1 files changed, 41 insertions, 0 deletions
diff --git a/pkgs/development/coq-modules/fiat/default.nix b/pkgs/development/coq-modules/fiat/default.nix new file mode 100644 index 000000000000..4eca588b205c --- /dev/null +++ b/pkgs/development/coq-modules/fiat/default.nix @@ -0,0 +1,41 @@ +{stdenv, fetchurl, coq}: + +stdenv.mkDerivation rec { + + name = "coq-fiat-${coq.coq-version}-${version}"; + version = "20141031"; + + src = fetchurl { + url = "http://plv.csail.mit.edu/fiat/releases/fiat-${version}.tar.gz"; + sha256 = "0c5jrcgbpdj0gfzg2q4naqw7frf0xxs1f451fnic6airvpaj0d55"; + }; + + buildInputs = [ coq.ocaml coq.camlp5 ]; + propagatedBuildInputs = [ coq ]; + + enableParallelBuilding = true; + + unpackPhase = '' + mkdir fiat + cd fiat + tar xvzf ${src} + ''; + + buildPhase = "make sources"; + + installPhase = '' + COQLIB=$out/lib/coq/${coq.coq-version}/ + mkdir -p $COQLIB/user-contrib/Fiat + cp -pR src $COQLIB/user-contrib/Fiat + ''; + + installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/"; + + meta = with stdenv.lib; { + homepage = http://plv.csail.mit.edu/fiat/; + description = "Fiat is a library for the Coq proof assistant for synthesizing efficient correct-by-construction programs from declarative specifications"; + maintainers = with maintainers; [ jwiegley ]; + platforms = coq.meta.platforms; + }; + +} |