From da68cc24f087176c576cb7ff0e05faeb4ea7672f Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Thu, 27 Oct 2016 20:58:52 +0200 Subject: [PATCH 1/5] coq: 8.5pl2 -> 8.5pl3 --- pkgs/applications/science/logic/coq/8.5.nix | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/pkgs/applications/science/logic/coq/8.5.nix b/pkgs/applications/science/logic/coq/8.5.nix index eb74891f511c..91266553c938 100644 --- a/pkgs/applications/science/logic/coq/8.5.nix +++ b/pkgs/applications/science/logic/coq/8.5.nix @@ -6,7 +6,7 @@ {stdenv, fetchurl, writeText, pkgconfig, ocaml, findlib, camlp5, ncurses, lablgtk ? null, csdp ? null}: let - version = "8.5pl2"; + version = "8.5pl3"; coq-version = "8.5"; buildIde = lablgtk != null; ideFlags = if buildIde then "-lablgtkdir ${lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt" else ""; @@ -24,7 +24,7 @@ stdenv.mkDerivation { src = fetchurl { url = "http://coq.inria.fr/distrib/V${version}/files/coq-${version}.tar.gz"; - sha256 = "0wyywia0darak2zmc5v0ra9rn0b9whwdfiahralm8v5za499s8w3"; + sha256 = "0fyk2a4fpifibq8y8jhx1891k55qnsnlygglch64sva0bph94nrh"; }; buildInputs = [ pkgconfig ocaml findlib camlp5 ncurses lablgtk ]; @@ -34,7 +34,7 @@ stdenv.mkDerivation { RM=$(type -tp rm) substituteInPlace configure --replace "/bin/uname" "$UNAME" substituteInPlace tools/beautify-archive --replace "/bin/rm" "$RM" - substituteInPlace configure.ml --replace "if arch = \"Darwin\" || arch = \"FreeBSD\" then \"md5" "if arch = \"Darwinx\" then \"md5" + substituteInPlace configure.ml --replace '"md5 -q"' '"md5sum"' ${csdpPatch} ''; From b840da02cd91a67010826a9f375a02d71eaa7254 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Thu, 27 Oct 2016 21:09:59 +0200 Subject: [PATCH 2/5] coq: build and install the votour utility --- pkgs/applications/science/logic/coq/8.5.nix | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/pkgs/applications/science/logic/coq/8.5.nix b/pkgs/applications/science/logic/coq/8.5.nix index 91266553c938..9512e27080f3 100644 --- a/pkgs/applications/science/logic/coq/8.5.nix +++ b/pkgs/applications/science/logic/coq/8.5.nix @@ -57,7 +57,11 @@ stdenv.mkDerivation { prefixKey = "-prefix "; - buildFlags = "revision coq coqide"; + buildFlags = "revision coq coqide bin/votour"; + + postInstall = '' + cp bin/votour $out/bin/ + ''; meta = with stdenv.lib; { description = "Coq proof assistant"; From 7c53518663658db36218fa8f5566442d3f71da99 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Mon, 31 Oct 2016 19:10:30 +0100 Subject: [PATCH 3/5] compcert: patch to build with Coq-8.5pl3 --- pkgs/development/compilers/compcert/default.nix | 1 + 1 file changed, 1 insertion(+) diff --git a/pkgs/development/compilers/compcert/default.nix b/pkgs/development/compilers/compcert/default.nix index fb95372a96f7..f5554ee0ce39 100644 --- a/pkgs/development/compilers/compcert/default.nix +++ b/pkgs/development/compilers/compcert/default.nix @@ -19,6 +19,7 @@ stdenv.mkDerivation rec { enableParallelBuilding = true; configurePhase = '' + substituteInPlace ./configure --replace pl2 pl3 substituteInPlace ./configure --replace '{toolprefix}gcc' '{toolprefix}cc' ./configure -prefix $out -toolprefix ${tools}/bin/ '' + (if stdenv.isDarwin then "ia32-macosx" else "ia32-linux"); From 5f49eeb935112e69f8992083ca173728a90cbf8c Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Mon, 31 Oct 2016 19:10:39 +0100 Subject: [PATCH 4/5] coq: move out of ocamlPackages --- pkgs/top-level/all-packages.nix | 22 ++++++++++++++++++---- pkgs/top-level/ocaml-packages.nix | 20 +------------------- 2 files changed, 19 insertions(+), 23 deletions(-) diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index 4e0efdfe5a5f..3ac37ea39691 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -16470,13 +16470,27 @@ in aspino = callPackage ../applications/science/logic/aspino {}; - inherit (ocaml-ng.ocamlPackages_4_01_0) coq; + coq = callPackage ../applications/science/logic/coq { + inherit (ocamlPackages_4_01_0) ocaml findlib lablgtk; + camlp5 = ocamlPackages_4_01_0.camlp5_transitional; + }; - inherit (ocamlPackages) coq_HEAD; + coq_HEAD = callPackage ../applications/science/logic/coq/HEAD.nix { + inherit (ocamlPackages) ocaml findlib lablgtk; + camlp5 = ocamlPackages.camlp5_transitional; + }; - inherit (ocamlPackages) coq_8_5; + coq_8_5 = callPackage ../applications/science/logic/coq/8.5.nix { + inherit (ocamlPackages) ocaml findlib lablgtk; + camlp5 = ocamlPackages.camlp5_transitional; + }; - inherit (ocaml-ng.ocamlPackages_3_12_1) coq_8_3; + coq_8_3 = callPackage ../applications/science/logic/coq/8.3.nix { + make = pkgs.gnumake3; + inherit (ocamlPackages_3_12_1) ocaml findlib; + camlp5 = ocamlPackages_3_12_1.camlp5_transitional; + lablgtk = ocamlPackages_3_12_1.lablgtk_2_14; + }; mkCoqPackages_8_4 = self: let callPackage = newScope self; in { diff --git a/pkgs/top-level/ocaml-packages.nix b/pkgs/top-level/ocaml-packages.nix index 58e9512e31c6..d4ca17f6dbd8 100644 --- a/pkgs/top-level/ocaml-packages.nix +++ b/pkgs/top-level/ocaml-packages.nix @@ -612,7 +612,7 @@ let then { tools = pkgs.pkgsi686Linux.stdenv.cc; } else {} ) // { - coq = coq_8_5; + coq = pkgs.coq_8_5; }); haxe = callPackage ../development/compilers/haxe { }; @@ -654,24 +654,6 @@ let enableX11 = config.unison.enableX11 or true; }; - coq = callPackage ../applications/science/logic/coq { - camlp5 = camlp5_transitional; - }; - - coq_HEAD = callPackage ../applications/science/logic/coq/HEAD.nix { - camlp5 = camlp5_transitional; - }; - - coq_8_5 = callPackage ../applications/science/logic/coq/8.5.nix { - camlp5 = camlp5_transitional; - }; - - coq_8_3 = callPackage ../applications/science/logic/coq/8.3.nix { - make = pkgs.gnumake3; - camlp5 = camlp5_transitional; - lablgtk = lablgtk_2_14; - }; - hol_light = callPackage ../applications/science/logic/hol_light { camlp5 = camlp5_strict; }; From b028b5f4ef03d6c3dae4cdda898c1996348c4e18 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Wed, 2 Nov 2016 19:39:22 +0100 Subject: [PATCH 5/5] coq-8.5: ease the selection of an older (patch level) version --- pkgs/applications/science/logic/coq/8.5.nix | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) diff --git a/pkgs/applications/science/logic/coq/8.5.nix b/pkgs/applications/science/logic/coq/8.5.nix index 9512e27080f3..aae2101f50e9 100644 --- a/pkgs/applications/science/logic/coq/8.5.nix +++ b/pkgs/applications/science/logic/coq/8.5.nix @@ -2,11 +2,22 @@ # - The csdp program used for the Micromega tactic is statically referenced. # However, coq can build without csdp by setting it to null. # In this case some Micromega tactics will search the user's path for the csdp program and will fail if it is not found. +# - The patch-level version can be specified through the `pl` argument to +# the derivation; it defaults to the greatest. -{stdenv, fetchurl, writeText, pkgconfig, ocaml, findlib, camlp5, ncurses, lablgtk ? null, csdp ? null}: +{ stdenv, fetchurl, writeText, pkgconfig +, ocaml, findlib, camlp5, ncurses +, lablgtk ? null, csdp ? null +, pl ? "3" +}: let - version = "8.5pl3"; + version = "8.5pl${pl}"; + sha256 = { + "1" = "1w2xvm6w16khfn63bp95s25hnkn2ny3w0yqg3lq63gp11aqpbyjb"; + "2" = "0wyywia0darak2zmc5v0ra9rn0b9whwdfiahralm8v5za499s8w3"; + "3" = "0fyk2a4fpifibq8y8jhx1891k55qnsnlygglch64sva0bph94nrh"; + }."${pl}"; coq-version = "8.5"; buildIde = lablgtk != null; ideFlags = if buildIde then "-lablgtkdir ${lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt" else ""; @@ -24,7 +35,7 @@ stdenv.mkDerivation { src = fetchurl { url = "http://coq.inria.fr/distrib/V${version}/files/coq-${version}.tar.gz"; - sha256 = "0fyk2a4fpifibq8y8jhx1891k55qnsnlygglch64sva0bph94nrh"; + inherit sha256; }; buildInputs = [ pkgconfig ocaml findlib camlp5 ncurses lablgtk ];