diff options
author | Marco Maggesi <maggesi@math.unifi.it> | 2009-11-02 11:44:27 +0000 |
---|---|---|
committer | Marco Maggesi <maggesi@math.unifi.it> | 2009-11-02 11:44:27 +0000 |
commit | a0207b3dc7ff3583df37f2bb8bab939390f964c7 (patch) | |
tree | 73d3a5c3f60ca547200cbd98064ad97b7bb973f9 /pkgs/applications/science/logic/coq | |
parent | c4533b8d2487cdb501fa28649b84affb6d659105 (diff) |
Updated Coq to version 8.2pl1
svn path=/nixpkgs/trunk/; revision=18069
Diffstat (limited to 'pkgs/applications/science/logic/coq')
-rw-r--r-- | pkgs/applications/science/logic/coq/configure.patch.gz | bin | 0 -> 438 bytes | |||
-rw-r--r-- | pkgs/applications/science/logic/coq/default.nix | 65 |
2 files changed, 54 insertions, 11 deletions
diff --git a/pkgs/applications/science/logic/coq/configure.patch.gz b/pkgs/applications/science/logic/coq/configure.patch.gz new file mode 100644 index 0000000000000..85ecfda6dae16 --- /dev/null +++ b/pkgs/applications/science/logic/coq/configure.patch.gz Binary files differdiff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix index 475c68f7b9cf0..19827022072d6 100644 --- a/pkgs/applications/science/logic/coq/default.nix +++ b/pkgs/applications/science/logic/coq/default.nix @@ -1,23 +1,66 @@ -{stdenv, fetchurl, ocaml, ncurses}: +# TODO: +# - coqide compilation should be optional or (better) separate; +# - coqide libraries are not installed; -stdenv.mkDerivation (rec { +{stdenv, fetchurl, ocaml, camlp5, lablgtk, ncurses}: + +let + + pname = "coq"; + version = "8.2pl1"; + name = "${pname}-${version}"; + +in + +stdenv.mkDerivation { + inherit name; - name = "coq-8.1pl3"; src = fetchurl { - url = "http://coq.inria.fr/V8.1pl3/files/coq-8.1pl3.tar.gz"; - sha256 = "7f8f45594adff2625312c5ecb144cb00d39c99201dac309c9286b34d01a36bb6"; + url = "http://coq.inria.fr/V${version}/files/${name}.tar.gz"; + sha256 = "7c15acfd369111e51d937cce632d22fc77a6718a5ac9f2dd2dcbdfab4256ae0c"; }; - buildInputs = [ocaml ncurses]; + buildInputs = [ ocaml camlp5 ncurses lablgtk ]; prefixKey = "-prefix "; - patchPhase = '' + + configureFlags = + "-camldir ${ocaml}/bin " + + "-camlp5dir ${camlp5}/lib/ocaml/camlp5 " + + "-lablgtkdir ${lablgtk}/lib/ocaml/lablgtk2 " + + "-opt -coqide opt"; + + buildFlags = "world"; # Debug with "world VERBOSE=1"; + + patches = [ ./configure.patch.gz ]; + + postPatch = '' + BASH=$(type -tp bash) UNAME=$(type -tp uname) MV=$(type -tp mv) - RM=$(type -tp cp) - substituteInPlace ./configure --replace "/bin/uname" "$UNAME" - substituteInPlace Makefile --replace "/bin/mv" "$MV" \ + RM=$(type -tp rm) + substituteInPlace configure --replace "/bin/bash" "$BASH" \ + --replace "/bin/uname" "$UNAME" + substituteInPlace Makefile --replace "/bin/bash" "$BASH" \ + --replace "/bin/mv" "$MV" \ --replace "/bin/rm" "$RM" + substituteInPlace Makefile.stage1 --replace "/bin/bash" "$BASH" + substituteInPlace install.sh --replace "/bin/bash" "$BASH" + substituteInPlace dev/v8-syntax/check-grammar --replace "/bin/bash" "$BASH" + substituteInPlace scripts/coqmktop.ml --replace \ + "\"-I\"; \"+lablgtk2\"" \ + "\"-I\"; \"${lablgtk}/lib/ocaml/lablgtk2\"; \"-I\"; \"${lablgtk}/lib/ocaml/stublibs\"" ''; -}) + meta = { + description = "Coq proof assistant"; + longDescription = '' + Coq is a formal proof management system. It provides a formal language + to write mathematical definitions, executable algorithms and theorems + together with an environment for semi-interactive development of + machine-checked proofs. + ''; + homepage = "http://coq.inria.fr"; + license = "LGPL"; + }; +} |