diff options
-rw-r--r-- | pkgs/applications/science/logic/coq/8.5.nix | 68 | ||||
-rw-r--r-- | pkgs/development/coq-modules/mathcomp/1.5.nix | 26 | ||||
-rw-r--r-- | pkgs/development/coq-modules/ssreflect/1.5.nix | 42 | ||||
-rw-r--r-- | pkgs/development/coq-modules/ssreflect/threads.patch | 16 | ||||
-rw-r--r-- | pkgs/top-level/all-packages.nix | 19 |
5 files changed, 171 insertions, 0 deletions
diff --git a/pkgs/applications/science/logic/coq/8.5.nix b/pkgs/applications/science/logic/coq/8.5.nix new file mode 100644 index 000000000000..87b476249f44 --- /dev/null +++ b/pkgs/applications/science/logic/coq/8.5.nix @@ -0,0 +1,68 @@ +# - coqide compilation can be disabled by setting lablgtk to null; + +{stdenv, fetchurl, writeText, pkgconfig, ocaml, findlib, camlp5, ncurses, lablgtk ? null}: + +let + version = "8.5b2"; + coq-version = "8.5"; + buildIde = lablgtk != null; + ideFlags = if buildIde then "-lablgtkdir ${lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt" else ""; +in + +stdenv.mkDerivation { + name = "coq-${version}"; + + inherit coq-version; + inherit ocaml camlp5; + + src = fetchurl { + url = https://coq.inria.fr/distrib/V8.5beta2/files/coq-8.5beta2.tar.gz; + sha256 = "1z34ch56lld86srgsjdwdq3girz0k0wqmvyxsa7jwvvxn3qmmq2v"; + }; + + buildInputs = [ pkgconfig ocaml findlib camlp5 ncurses lablgtk ]; + + postPatch = '' + UNAME=$(type -tp uname) + RM=$(type -tp rm) + substituteInPlace configure --replace "/bin/uname" "$UNAME" + substituteInPlace tools/beautify-archive --replace "/bin/rm" "$RM" + substituteInPlace Makefile.build --replace "ifeq (\$(ARCH),Darwin)" "ifeq (\$(ARCH),Darwinx)" + ''; + + setupHook = writeText "setupHook.sh" '' + addCoqPath () { + if test -d "''$1/lib/coq/${coq-version}/user-contrib"; then + export COQPATH="''${COQPATH}''${COQPATH:+:}''$1/lib/coq/${coq-version}/user-contrib/" + fi + } + + envHooks=(''${envHooks[@]} addCoqPath) + ''; + + preConfigure = '' + configureFlagsArray=( + -opt + ${ideFlags} + ) + ''; + + prefixKey = "-prefix "; + + buildFlags = "revision coq coqide"; + + meta = with stdenv.lib; { + 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 = licenses.lgpl21; + branch = coq-version; + maintainers = with maintainers; [ roconnor thoughtpolice vbgl ]; + platforms = platforms.unix; + }; +} diff --git a/pkgs/development/coq-modules/mathcomp/1.5.nix b/pkgs/development/coq-modules/mathcomp/1.5.nix new file mode 100644 index 000000000000..c984bab49171 --- /dev/null +++ b/pkgs/development/coq-modules/mathcomp/1.5.nix @@ -0,0 +1,26 @@ +{stdenv, fetchurl, coq, ssreflect}: + +stdenv.mkDerivation { + + name = "coq-mathcomp-1.5-8.5b2"; + + src = fetchurl { + url = http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.5.coq85beta2.tar.gz; + sha256 = "03bnq44ym43x8shi7whc02l0g5vy6rx8f1imjw478chlgwcxazqy"; + }; + + propagatedBuildInputs = [ coq ssreflect ]; + + enableParallelBuilding = true; + + installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/"; + + meta = with stdenv.lib; { + homepage = http://ssr.msr-inria.inria.fr/; + license = licenses.cecill-b; + maintainers = [ maintainers.vbgl maintainers.jwiegley ]; + platforms = coq.meta.platforms; + hydraPlatforms = []; + }; + +} diff --git a/pkgs/development/coq-modules/ssreflect/1.5.nix b/pkgs/development/coq-modules/ssreflect/1.5.nix new file mode 100644 index 000000000000..7c16b43ba8cb --- /dev/null +++ b/pkgs/development/coq-modules/ssreflect/1.5.nix @@ -0,0 +1,42 @@ +{stdenv, fetchurl, coq}: + +assert coq.coq-version == "8.5"; + +stdenv.mkDerivation { + + name = "coq-ssreflect-1.5-8.5b2"; + + src = fetchurl { + url = http://ssr.msr-inria.inria.fr/FTP/ssreflect-1.5.coq85beta2.tar.gz; + sha256 = "084l9xd5vgb8jml0dkm66g8cil5rsf04w821pjhn2qk9mdbwaagf"; + }; + + buildInputs = [ coq.ocaml coq.camlp5 ]; + propagatedBuildInputs = [ coq ]; + + enableParallelBuilding = true; + + patches = [ ./threads.patch ]; + + postPatch = '' + # Permit building of the ssrcoq statically-bound executable + sed -i 's/^#-custom/-custom/' Make + sed -i 's/^#SSRCOQ/SSRCOQ/' Make + ''; + + installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/"; + + postInstall = '' + mkdir -p $out/bin + cp -p bin/ssrcoq $out/bin + cp -p bin/ssrcoq.byte $out/bin + ''; + + meta = with stdenv.lib; { + homepage = http://ssr.msr-inria.inria.fr/; + license = licenses.cecill-b; + maintainers = with maintainers; [ vbgl jwiegley ]; + platforms = coq.meta.platforms; + }; + +} diff --git a/pkgs/development/coq-modules/ssreflect/threads.patch b/pkgs/development/coq-modules/ssreflect/threads.patch new file mode 100644 index 000000000000..d60a645f6ee8 --- /dev/null +++ b/pkgs/development/coq-modules/ssreflect/threads.patch @@ -0,0 +1,16 @@ +--- a/Make 2015-04-20 13:37:06.000000000 +0200 ++++ b/Make 2015-04-25 11:32:53.885194600 +0200 +@@ -1,9 +1,9 @@ + ### 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 ++-custom "$(COQBIN)coqmktop -coqlib `$(COQBIN)coqtop -where` -opt -o bin/ssrcoq -I +threads 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 -I +threads 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 diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index bdf86837e35b..75c7dc9789c3 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -13523,6 +13523,11 @@ let camlp5 = ocamlPackages.camlp5_transitional; }; + coq_8_5 = callPackage ../applications/science/logic/coq/8.5.nix { + inherit (ocamlPackages) findlib lablgtk; + camlp5 = ocamlPackages.camlp5_transitional; + }; + coq_8_3 = callPackage ../applications/science/logic/coq/8.3.nix { inherit (ocamlPackages_3_12_1) ocaml findlib; camlp5 = ocamlPackages_3_12_1.camlp5_transitional; @@ -13569,7 +13574,21 @@ let }; + mkCoqPackages_8_5 = self: let callPackage = newScope self; in rec { + + mathcomp = callPackage ../development/coq-modules/mathcomp/1.5.nix { + coq = coq_8_5; + ssreflect = ssreflect; + }; + + ssreflect = callPackage ../development/coq-modules/ssreflect/1.5.nix { + coq = coq_8_5; + }; + + }; + coqPackages = recurseIntoAttrs (mkCoqPackages_8_4 coqPackages); + coqPackages_8_5 = recurseIntoAttrs (mkCoqPackages_8_5 coqPackages); cvc3 = callPackage ../applications/science/logic/cvc3 {}; cvc4 = callPackage ../applications/science/logic/cvc4 {}; |