Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

coq_HEAD: Update to the latest commit #21822

Merged
merged 3 commits into from
Apr 30, 2017
Merged

coq_HEAD: Update to the latest commit #21822

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
975d040
coq_HEAD: Update to the latest commit
rht Jan 12, 2017
7264efb
Fold in specific ocaml version choice into let
rht Jan 15, 2017
bbd1c3d
coq_HEAD: Update once more
rht Feb 6, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
21 changes: 12 additions & 9 deletions pkgs/applications/science/logic/coq/HEAD.nix
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,31 +1,34 @@
# - 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 = "8.6pre-0c999f02";
version = "2017-02-03";
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;
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@vbgl I overrode the definition here so that there is no need to put an extra prefix ocamlPackages_4_02 in buildInputs. Plus, the version-specific statement is localized to only within the let clause. WDYT?

findlib = ocamlPackages_4_02.findlib;
lablgtk = ocamlPackages_4_02.lablgtk;
camlp5 = ocamlPackages_4_02.camlp5_transitional;
in

stdenv.mkDerivation {
name = "coq-${version}";
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;
rev = "ad768e435a736ca51ac79a575967b388b34918c7";
sha256 = "05s7sk1l3mvdjag3idnhkpj707y4bv56da7kpffw862f2qgfr77j";
rev = "078598d029792a3d9a54fae9b9ac189b75bc3b06";
sha256 = "0sflrpp6x0ada0bjh67q1x65g88d179n3cawpwkp1pm4kw76g8x7";
};

buildInputs = [ pkgconfig ocaml findlib camlp5 ncurses lablgtk ];
Expand Down
5 changes: 1 addition & 4 deletions pkgs/top-level/all-packages.nix
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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) ocaml findlib lablgtk;
camlp5 = ocamlPackages.camlp5_transitional;
};
coq_HEAD = callPackage ../applications/science/logic/coq/HEAD.nix {};
coq = coq_8_6;

mkCoqPackages_8_4 = self: let callPackage = newScope self; in {
Expand Down