diff options
author | Vincent Laporte <Vincent.Laporte@gmail.com> | 2014-09-28 13:51:33 +0100 |
---|---|---|
committer | Vincent Laporte <Vincent.Laporte@gmail.com> | 2014-09-28 14:03:15 +0100 |
commit | f3b8d82ce683d38d11f29a6b82de11fc6259d3a0 (patch) | |
tree | 363ae8cd26a67a86ac6423871cd6a0afca0934eb | |
parent | c30c5f7cf3759ca37a845de8a2ed280aaac238f0 (diff) | |
download | nixlib-f3b8d82ce683d38d11f29a6b82de11fc6259d3a0.tar nixlib-f3b8d82ce683d38d11f29a6b82de11fc6259d3a0.tar.gz nixlib-f3b8d82ce683d38d11f29a6b82de11fc6259d3a0.tar.bz2 nixlib-f3b8d82ce683d38d11f29a6b82de11fc6259d3a0.tar.lz nixlib-f3b8d82ce683d38d11f29a6b82de11fc6259d3a0.tar.xz nixlib-f3b8d82ce683d38d11f29a6b82de11fc6259d3a0.tar.zst nixlib-f3b8d82ce683d38d11f29a6b82de11fc6259d3a0.zip |
Removes duplicate ssreflect
-rw-r--r-- | pkgs/applications/science/logic/ssreflect/default.nix | 50 | ||||
-rw-r--r-- | pkgs/applications/science/logic/ssreflect/static.patch | 21 | ||||
-rw-r--r-- | pkgs/top-level/all-packages.nix | 4 |
3 files changed, 0 insertions, 75 deletions
diff --git a/pkgs/applications/science/logic/ssreflect/default.nix b/pkgs/applications/science/logic/ssreflect/default.nix deleted file mode 100644 index a784e5fe1b6e..000000000000 --- a/pkgs/applications/science/logic/ssreflect/default.nix +++ /dev/null @@ -1,50 +0,0 @@ -# TODO: -# - 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, makeWrapper}: - -let - pname = "ssreflect"; - version = "1.5"; - name = "${pname}-${version}"; - webpage = http://www.msr-inria.inria.fr/Projects/math-components; -in - -stdenv.mkDerivation { - inherit name; - - src = fetchurl { - url = "http://ssr.msr-inria.inria.fr/FTP/${name}.tar.gz"; - sha256 = "0hm1ha7sxqfqhc7iwhx6zdz3nki4rj5nfd3ab24hmz8v7mlpinds"; - }; - - buildInputs = [ ocaml camlp5 coq makeWrapper ]; - - patches = [ ./static.patch ]; - - 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 - makeWrapper "${coq}/bin/coqide" "$out/bin/ssrcoqide" --add-flags "-coqtop" --add-flags "$out/bin/ssrcoq" - ''; - - meta = { - description = "Small Scale Reflection extension for Coq"; - longDescription = '' - Small Scale Reflection (ssreflect) is an extension of the Coq Theorem - Prover which enable a formal proof methodology based on the pervasive - use of computation with symbolic representation - ''; - 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 deleted file mode 100644 index 2211d8802582..000000000000 --- a/pkgs/applications/science/logic/ssreflect/static.patch +++ /dev/null @@ -1,21 +0,0 @@ ---- ssreflect1.4-coq8.4/Make (revision 3823) -+++ ssreflect1.4-coq8.4/Make (working copy) -@@ -1,10 +1,10 @@ --### Uncomment for static linking --## --#-custom "$(COQBIN)coqmktop -coqlib `$(COQBIN)coqtop -where` -opt -o bin/ssrcoq src/ssrmatching.cmx src/ssreflect.cmx" "src/ssrmatching.cmx src/ssreflect.cmx" bin/ssrcoq --#-custom "$(COQBIN)coqmktop -coqlib `$(COQBIN)coqtop -where` -o bin/ssrcoq.byte src/ssrmatching.cmo src/ssreflect.cmo" "src/ssrmatching.cmo src/ssreflect.cmo" bin/ssrcoq.byte --#-custom "$(SSRCOQ) $(COQFLAGS) -compile $*" "%.v $(SSRCOQ)" "%.vo" --#SSRCOQ = bin/ssrcoq --## -+## Uncomment for static linking -+# -+-custom "$(COQBIN)coqmktop -coqlib `$(COQBIN)coqtop -where` -opt -o bin/ssrcoq src/ssrmatching.cmx src/ssreflect.cmx" "src/ssrmatching.cmx src/ssreflect.cmx" bin/ssrcoq -+-custom "$(COQBIN)coqmktop -coqlib `$(COQBIN)coqtop -where` -o bin/ssrcoq.byte src/ssrmatching.cmo src/ssreflect.cmo" "src/ssrmatching.cmo src/ssreflect.cmo" bin/ssrcoq.byte -+-custom "$(SSRCOQ) $(COQFLAGS) -compile $*" "%.v $(SSRCOQ)" "%.vo" -+SSRCOQ = bin/ssrcoq -+# - - ## What follows should be left untouched by the final user of ssreflect - -R theories Ssreflect - diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index 17ca09f8635c..a1bb92e26bf4 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -11519,10 +11519,6 @@ let spass = callPackage ../applications/science/logic/spass {}; - ssreflect = callPackage ../applications/science/logic/ssreflect { - camlp5 = ocamlPackages.camlp5_transitional; - }; - tptp = callPackage ../applications/science/logic/tptp {}; twelf = callPackage ../applications/science/logic/twelf { |