diff options
author | Russell O'Connor <roconnor@theorem.ca> | 2012-05-16 22:04:02 +0000 |
---|---|---|
committer | Russell O'Connor <roconnor@theorem.ca> | 2012-05-16 22:04:02 +0000 |
commit | cfc8538326100117fca6cec3df4bb7f8e22ef182 (patch) | |
tree | 1567d5c68b7712f4d0c9186520a728dde6e51f10 /pkgs/applications/science/logic | |
parent | 503576d27708c1196bed931d78de8ab848aa4246 (diff) | |
download | nixlib-cfc8538326100117fca6cec3df4bb7f8e22ef182.tar nixlib-cfc8538326100117fca6cec3df4bb7f8e22ef182.tar.gz nixlib-cfc8538326100117fca6cec3df4bb7f8e22ef182.tar.bz2 nixlib-cfc8538326100117fca6cec3df4bb7f8e22ef182.tar.lz nixlib-cfc8538326100117fca6cec3df4bb7f8e22ef182.tar.xz nixlib-cfc8538326100117fca6cec3df4bb7f8e22ef182.tar.zst nixlib-cfc8538326100117fca6cec3df4bb7f8e22ef182.zip |
Updating coq and ssreflect to patch level 4.
svn path=/nixpkgs/trunk/; revision=34146
Diffstat (limited to 'pkgs/applications/science/logic')
-rw-r--r-- | pkgs/applications/science/logic/coq/default.nix | 5 | ||||
-rw-r--r-- | pkgs/applications/science/logic/ssreflect/default.nix | 22 | ||||
-rw-r--r-- | pkgs/applications/science/logic/ssreflect/static.patch | 33 |
3 files changed, 51 insertions, 9 deletions
diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix index 3fef10b44fb2..cfd769fa6a2c 100644 --- a/pkgs/applications/science/logic/coq/default.nix +++ b/pkgs/applications/science/logic/coq/default.nix @@ -4,7 +4,7 @@ {stdenv, fetchurl, ocaml, findlib, camlp5, lablgtk, ncurses}: let - version = "8.3pl3"; + version = "8.3pl4"; in stdenv.mkDerivation { @@ -12,7 +12,7 @@ stdenv.mkDerivation { src = fetchurl { url = "http://coq.inria.fr/V${version}/files/coq-${version}.tar.gz"; - sha256 = "0ivrafwr4p8pklb9wfq3zyai19xdk05xr3q16xqk4q9pfad9w9dg"; + sha256 = "17d3lmchmqir1rawnr52g78srg4wkd7clzpzfsivxc4y1zp6rwkr"; }; buildInputs = [ ocaml findlib camlp5 ncurses lablgtk ]; @@ -58,5 +58,6 @@ stdenv.mkDerivation { ''; homepage = "http://coq.inria.fr"; license = "LGPL"; + maintainers = [ stdenv.lib.maintainers.roconnor ]; }; } diff --git a/pkgs/applications/science/logic/ssreflect/default.nix b/pkgs/applications/science/logic/ssreflect/default.nix index 8443974a0a0a..c554b5dcea1c 100644 --- a/pkgs/applications/science/logic/ssreflect/default.nix +++ b/pkgs/applications/science/logic/ssreflect/default.nix @@ -2,11 +2,11 @@ # - coq needs to be invoked with the explicit path to the ssreflect theory # e.g. coqide -R ~/.nix-profile/lib/coq/user-contrib/ '' -{stdenv, fetchurl, ocaml, camlp5, coq}: +{stdenv, fetchurl, ocaml, camlp5, coq, makeWrapper}: let pname = "ssreflect"; - version = "1.3pl1"; + version = "1.3pl4"; name = "${pname}-${version}"; webpage = http://www.msr-inria.inria.fr/Projects/math-components; in @@ -16,22 +16,29 @@ stdenv.mkDerivation { src = fetchurl { url = "${webpage}/${name}.tar.gz"; - sha256 = "0ykrhqb68aanl5d4dmn0vnx8m34gg0jsbdhwx2852rqi7r00b9ri"; + sha256 = "1ha3iiqq79pgll5ra9z0xdi3d3dr3wb9f5vsm4amy884l5anva02"; }; - buildInputs = [ ocaml camlp5 coq ]; + buildInputs = [ ocaml camlp5 coq makeWrapper ]; + + patches = [ ./static.patch ]; - # this fails - /* postBuild = '' cd src coqmktop -ide -opt ssreflect.cmx -o ../bin/ssrcoqide + cd .. ''; - */ installPhase = '' COQLIB=$out/lib/coq make -f Makefile.coq install -e mkdir -p $out/bin + cp bin/* $out/bin + for i in $out/bin/*; do + wrapProgram "$i" \ + --add-flags "-R" \ + --add-flags "$out/lib/coq/user-contrib/Ssreflect" \ + --add-flags "Ssreflect" + done ''; meta = { @@ -43,5 +50,6 @@ stdenv.mkDerivation { ''; homepage = webpage; license = "CeCILL B FREE SOFTWARE LICENSE or CeCILL FREE SOFTWARE LICENSE"; + maintainers = [ stdenv.lib.maintainers.roconnor ]; }; } diff --git a/pkgs/applications/science/logic/ssreflect/static.patch b/pkgs/applications/science/logic/ssreflect/static.patch new file mode 100644 index 000000000000..edb8a6111f7e --- /dev/null +++ b/pkgs/applications/science/logic/ssreflect/static.patch @@ -0,0 +1,33 @@ +--- ssreflect1.3pl4/Make (revision 3823) ++++ ssreflect1.3pl4/Make (working copy) +@@ -1,18 +1,18 @@ + ## Uncomment for static linking + ## <static> +-# +-#-custom "$(COQBIN)coqmktop -opt -o bin/ssrcoq src/ssreflect.cmx" "src/ssreflect.cmx" bin/ssrcoq +-#-custom "$(COQBIN)coqmktop -o bin/ssrcoq.byte src/ssreflect.cmo" "src/ssreflect.cmo bin/ssrcoq" bin/ssrcoq.byte +-#-custom "$(SSRCOQ) $(COQFLAGS) -compile $*" "%.v $(SSRCOQ)" "%.vo" +-#SSRCOQ = bin/ssrcoq +-# ++ ++-custom "$(COQBIN)coqmktop -opt -o bin/ssrcoq src/ssreflect.cmx" "src/ssreflect.cmx" bin/ssrcoq ++-custom "$(COQBIN)coqmktop -o bin/ssrcoq.byte src/ssreflect.cmo" "src/ssreflect.cmo bin/ssrcoq" bin/ssrcoq.byte ++-custom "$(SSRCOQ) $(COQFLAGS) -compile $*" "%.v $(SSRCOQ)" "%.vo" ++SSRCOQ = bin/ssrcoq ++ + ## </static> + + ## Uncomment for dynamic linking + ## <dynamic> +- +--I src +- ++# ++#-I src ++# + ## </dynamic> + + ## What follows should be left untouched by the final user of ssreflect +Common subdirectories: old/src and new/src +Common subdirectories: old/test and new/test +Common subdirectories: old/theories and new/theories |