dev/nixpkgs
1
0
Fork 0
Code Issues Pull Requests Actions 2 Packages Projects Releases Wiki Activity

update coq to 8.3pl1

Browse Source 
update ssreflect to 1.3pl1

svn path=/nixpkgs/trunk/; revision=26692
This commit is contained in:
Russell O'Connor 2011-04-05 11:59:25 +00:00
parent 4551a76c2c
commit bec1a9c44f
2 changed files with 13 additions and 18 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
pkgs/applications/science/logic/coq/default.nix
View File

@ -4,7 +4,7 @@
{stdenv, fetchurl, ocaml, findlib, camlp5, lablgtk, ncurses}: {stdenv, fetchurl, ocaml, findlib, camlp5, lablgtk, ncurses}:
let let
version = "8.3"; version = "8.3pl1";
in in
stdenv.mkDerivation { stdenv.mkDerivation {
@ -12,7 +12,7 @@ stdenv.mkDerivation {
src = fetchurl { src = fetchurl {
url = "http://coq.inria.fr/V${version}/files/coq-${version}.tar.gz"; url = "http://coq.inria.fr/V${version}/files/coq-${version}.tar.gz";
sha256 = "02iy4rxz1n1kc85fb3vs4xpxqfxjw87y2gvmi39fxrj8742qx0dx"; sha256 = "0a791gsbf17y2wi0a376n78pxkhpl0lkzifhy5d3mx3lpn376j9s";
}; };
buildInputs = [ ocaml findlib camlp5 ncurses lablgtk ]; buildInputs = [ ocaml findlib camlp5 ncurses lablgtk ];
@ -29,7 +29,7 @@ stdenv.mkDerivation {
buildFlags = "world"; # Debug with "world VERBOSE=1"; buildFlags = "world"; # Debug with "world VERBOSE=1";
patches = [ ./configure.patch ./coq-8.3-make-3.82-compat.patch ]; patches = [ ./configure.patch ];
postPatch = '' postPatch = ''
UNAME=$(type -tp uname) UNAME=$(type -tp uname)
@ -41,6 +41,9 @@ stdenv.mkDerivation {
"\"-I\"; \"$(echo "${lablgtk}"/lib/ocaml/*/site-lib/lablgtk2)\"; \"-I\"; \"$(echo "${lablgtk}"/lib/ocaml/*/site-lib/stublibs)\"" "\"-I\"; \"$(echo "${lablgtk}"/lib/ocaml/*/site-lib/lablgtk2)\"; \"-I\"; \"$(echo "${lablgtk}"/lib/ocaml/*/site-lib/stublibs)\""
''; '';
# This post install step is needed to build ssrcoqide from the ssreflect package
# It could be made optional, but I see little harm in including it in the default
# distribution -- roconnor
postInstall = '' postInstall = ''
cp ide/*.cmi ide/ide.*a $out/lib/coq/ide/ cp ide/*.cmi ide/ide.*a $out/lib/coq/ide/
''; '';

22
pkgs/applications/science/logic/ssreflect/default.nix
View File

@ -1,13 +1,12 @@
# TODO: # TODO:
# - ssrcoqide does not build successfully (missing coqide libraries in the coq installation). # - coq needs to be invoked with the explicit path to the ssreflect theory
# - ssrcoq needs to be invoked with the explicit path to the ssreflect theory # e.g. coqide -R ~/.nix-profile/lib/coq/user-contrib/ ''
# e.g.. ssrcoq -I /nix/store/rp09dlb2y2hpddb0xa7fyrgjlzb284ar-ssreflect-1.2/lib/coq/user-contrib/theories/
{stdenv, fetchurl, ocaml, camlp5, coq}: {stdenv, fetchurl, ocaml, camlp5, coq}:
let let
pname = "ssreflect"; pname = "ssreflect";
version = "1.2"; version = "1.3pl1";
name = "${pname}-${version}"; name = "${pname}-${version}";
webpage = http://www.msr-inria.inria.fr/Projects/math-components; webpage = http://www.msr-inria.inria.fr/Projects/math-components;
in in
@ -16,18 +15,12 @@ stdenv.mkDerivation {
inherit name; inherit name;
src = fetchurl { src = fetchurl {
url = "${webpage}/${name}.tgz"; url = "${webpage}/${name}.tar.gz";
sha256 = "0800b085e6a0caec5093c6c02aacdd8dfd9cc282177e8586f14f9a9e15f64d0b"; sha256 = "0ykrhqb68aanl5d4dmn0vnx8m34gg0jsbdhwx2852rqi7r00b9ri";
}; };
buildInputs = [ ocaml camlp5 coq ]; buildInputs = [ ocaml camlp5 coq ];
preBuild = ''
coq_makefile -f Make -o Makefile
substituteInPlace Makefile \
--replace 'install -D $$i $(COQLIB)' 'install -D $$i '$out'/lib/coq'
'';
# this fails # this fails
/* /*
postBuild = '' postBuild = ''
@ -36,10 +29,9 @@ stdenv.mkDerivation {
''; '';
*/ */
postInstall = '' installPhase = ''
COQLIB=$out/lib/coq make -f Makefile.coq install -e
ensureDir $out/bin ensureDir $out/bin
#cp -a bin/ssrcoq bin/ssrcoqide $out/bin
cp -a bin/ssrcoq $out/bin
''; '';
meta = { meta = {