From 975d040f07eff23289e7698cb4bf02461c3fdd19 Mon Sep 17 00:00:00 2001 From: rht Date: Thu, 12 Jan 2017 04:31:36 +0400 Subject: [PATCH 1/3] coq_HEAD: Update to the latest commit --- pkgs/applications/science/logic/coq/HEAD.nix | 8 ++++---- pkgs/top-level/all-packages.nix | 4 ++-- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/pkgs/applications/science/logic/coq/HEAD.nix b/pkgs/applications/science/logic/coq/HEAD.nix index f6837397e21..e02170793ea 100644 --- a/pkgs/applications/science/logic/coq/HEAD.nix +++ b/pkgs/applications/science/logic/coq/HEAD.nix @@ -6,7 +6,7 @@ {stdenv, fetchgit, writeText, pkgconfig, ocaml, findlib, camlp5, ncurses, lablgtk ? null, csdp ? null}: let - version = "8.6pre-0c999f02"; + version = "2017-01-22"; coq-version = "8.6"; buildIde = lablgtk != null; ideFlags = if buildIde then "-lablgtkdir ${lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt" else ""; @@ -17,15 +17,15 @@ let in stdenv.mkDerivation { - name = "coq-${version}"; + name = "coq-unstable-${version}"; inherit coq-version; inherit ocaml camlp5; src = fetchgit { url = git://scm.gforge.inria.fr/coq/coq.git; - rev = "ad768e435a736ca51ac79a575967b388b34918c7"; - sha256 = "05s7sk1l3mvdjag3idnhkpj707y4bv56da7kpffw862f2qgfr77j"; + rev = "d6bcc6ebe4f65d0555414851f7e4fb6fa1fb22a4"; + sha256 = "1k5wkwlis836iwy1s8hfjw9gwdk8vp405hp09s6d44ijb2ihr356"; }; buildInputs = [ pkgconfig ocaml findlib camlp5 ncurses lablgtk ]; diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index 5fe47cdf560..f8d0ac7ce67 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -17222,8 +17222,8 @@ with pkgs; }; coq_8_6 = callPackage ../applications/science/logic/coq {}; coq_HEAD = callPackage ../applications/science/logic/coq/HEAD.nix { - inherit (ocamlPackages) ocaml findlib lablgtk; - camlp5 = ocamlPackages.camlp5_transitional; + inherit (ocamlPackages_4_02) ocaml findlib lablgtk; + camlp5 = ocamlPackages_4_02.camlp5_transitional; }; coq = coq_8_6; From 7264efb5cb387ada5e739ec35d4b48db1904705b Mon Sep 17 00:00:00 2001 From: rht Date: Sun, 15 Jan 2017 18:21:57 +0400 Subject: [PATCH 2/3] Fold in specific ocaml version choice into let --- pkgs/applications/science/logic/coq/HEAD.nix | 13 ++++++++----- pkgs/top-level/all-packages.nix | 5 +---- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/pkgs/applications/science/logic/coq/HEAD.nix b/pkgs/applications/science/logic/coq/HEAD.nix index e02170793ea..79893c38997 100644 --- a/pkgs/applications/science/logic/coq/HEAD.nix +++ b/pkgs/applications/science/logic/coq/HEAD.nix @@ -1,26 +1,29 @@ -# - coqide compilation can be disabled by setting lablgtk to null; +# - coqide compilation can be disabled by setting buildIde to false; # - 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. -{stdenv, fetchgit, writeText, pkgconfig, ocaml, findlib, camlp5, ncurses, lablgtk ? null, csdp ? null}: +{stdenv, fetchgit, writeText, pkgconfig, ocamlPackages_4_02, ncurses, buildIde ? true, csdp ? null}: let version = "2017-01-22"; coq-version = "8.6"; - buildIde = lablgtk != null; - ideFlags = if buildIde then "-lablgtkdir ${lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt" else ""; + ideFlags = if buildIde then "-lablgtkdir ${ocamlPackages_4_02.lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt" else ""; csdpPatch = if csdp != null then '' substituteInPlace plugins/micromega/sos.ml --replace "; csdp" "; ${csdp}/bin/csdp" substituteInPlace plugins/micromega/coq_micromega.ml --replace "System.is_in_system_path \"csdp\"" "true" '' else ""; + ocaml = ocamlPackages_4_02.ocaml; + findlib = ocamlPackages_4_02.findlib; + lablgtk = ocamlPackages_4_02.lablgtk; + camlp5 = ocamlPackages_4_02.camlp5_transitional; in stdenv.mkDerivation { name = "coq-unstable-${version}"; inherit coq-version; - inherit ocaml camlp5; + inherit ocaml camlp5 findlib; src = fetchgit { url = git://scm.gforge.inria.fr/coq/coq.git; diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index f8d0ac7ce67..75c817782f5 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -17221,10 +17221,7 @@ with pkgs; version = "8.5pl3"; }; coq_8_6 = callPackage ../applications/science/logic/coq {}; - coq_HEAD = callPackage ../applications/science/logic/coq/HEAD.nix { - inherit (ocamlPackages_4_02) ocaml findlib lablgtk; - camlp5 = ocamlPackages_4_02.camlp5_transitional; - }; + coq_HEAD = callPackage ../applications/science/logic/coq/HEAD.nix {}; coq = coq_8_6; mkCoqPackages_8_4 = self: let callPackage = newScope self; in { From bbd1c3d58a8652f3712348c4683c7c02738994d6 Mon Sep 17 00:00:00 2001 From: rht Date: Mon, 6 Feb 2017 16:27:13 +0400 Subject: [PATCH 3/3] coq_HEAD: Update once more --- pkgs/applications/science/logic/coq/HEAD.nix | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/pkgs/applications/science/logic/coq/HEAD.nix b/pkgs/applications/science/logic/coq/HEAD.nix index 79893c38997..8d3fb19b263 100644 --- a/pkgs/applications/science/logic/coq/HEAD.nix +++ b/pkgs/applications/science/logic/coq/HEAD.nix @@ -6,7 +6,7 @@ {stdenv, fetchgit, writeText, pkgconfig, ocamlPackages_4_02, ncurses, buildIde ? true, csdp ? null}: let - version = "2017-01-22"; + version = "2017-02-03"; coq-version = "8.6"; ideFlags = if buildIde then "-lablgtkdir ${ocamlPackages_4_02.lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt" else ""; csdpPatch = if csdp != null then '' @@ -27,8 +27,8 @@ stdenv.mkDerivation { src = fetchgit { url = git://scm.gforge.inria.fr/coq/coq.git; - rev = "d6bcc6ebe4f65d0555414851f7e4fb6fa1fb22a4"; - sha256 = "1k5wkwlis836iwy1s8hfjw9gwdk8vp405hp09s6d44ijb2ihr356"; + rev = "078598d029792a3d9a54fae9b9ac189b75bc3b06"; + sha256 = "0sflrpp6x0ada0bjh67q1x65g88d179n3cawpwkp1pm4kw76g8x7"; }; buildInputs = [ pkgconfig ocaml findlib camlp5 ncurses lablgtk ];