diff --git a/pkgs/applications/science/logic/coq/8.3.nix b/pkgs/applications/science/logic/coq/8.3.nix index f23622de8a0..8664b822cca 100644 --- a/pkgs/applications/science/logic/coq/8.3.nix +++ b/pkgs/applications/science/logic/coq/8.3.nix @@ -54,7 +54,7 @@ stdenv.mkDerivation { cp ide/*.cmi ide/ide.*a $out/lib/coq/ide/ '' else ""; - meta = { + meta = with stdenv.lib; { description = "Coq proof assistant"; longDescription = '' Coq is a formal proof management system. It provides a formal language @@ -63,7 +63,7 @@ stdenv.mkDerivation { machine-checked proofs. ''; homepage = "http://coq.inria.fr"; - license = "LGPL"; - maintainers = [ stdenv.lib.maintainers.roconnor ]; + license = licenses.lgpl21; + maintainers = with maintainers; [ roconnor vbgl ]; }; } diff --git a/pkgs/applications/science/logic/coq/HEAD.nix b/pkgs/applications/science/logic/coq/HEAD.nix index c76e563ff5f..4081465fbd2 100644 --- a/pkgs/applications/science/logic/coq/HEAD.nix +++ b/pkgs/applications/science/logic/coq/HEAD.nix @@ -1,19 +1,20 @@ # - coqide compilation can be disabled by setting lablgtk to null; -{stdenv, fetchgit, pkgconfig, ocaml, findlib, camlp5, ncurses, lablgtk ? null}: +{stdenv, fetchgit, writeText, pkgconfig, ocaml, findlib, camlp5, ncurses, lablgtk ? null}: let version = "8.5pre-01feb42"; + coq-version = "8.5"; buildIde = lablgtk != null; ideFlags = if buildIde then "-lablgtkdir ${lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt" else ""; - idePath = if buildIde then '' - CAML_LD_LIBRARY_PATH=${lablgtk}/lib/ocaml/3.12.1/site-lib/stublibs - '' else ""; in stdenv.mkDerivation { name = "coq-${version}"; + inherit coq-version; + inherit ocaml camlp5; + src = fetchgit { url = git://scm.gforge.inria.fr/coq/coq.git; rev = "01feb4206d26b41bfaab9bd45a7b2fc4db569baf"; @@ -32,8 +33,17 @@ stdenv.mkDerivation { 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 = '' - buildFlagsArray=(${idePath}) configureFlagsArray=( -opt ${ideFlags} @@ -44,7 +54,7 @@ stdenv.mkDerivation { buildFlags = "revision coq coqide"; - meta = { + meta = with stdenv.lib; { description = "Coq proof assistant"; longDescription = '' Coq is a formal proof management system. It provides a formal language @@ -53,8 +63,8 @@ stdenv.mkDerivation { machine-checked proofs. ''; homepage = "http://coq.inria.fr"; - license = "LGPL"; - maintainers = with stdenv.lib.maintainers; [ roconnor thoughtpolice ]; - platforms = stdenv.lib.platforms.unix; + license = licenses.lgpl21; + maintainers = with maintainers; [ roconnor thoughtpolice vbgl ]; + platforms = platforms.unix; }; } diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix index da77a4c5a9a..f0f62bfb353 100644 --- a/pkgs/applications/science/logic/coq/default.nix +++ b/pkgs/applications/science/logic/coq/default.nix @@ -1,19 +1,20 @@ # - coqide compilation can be disabled by setting lablgtk to null; -{stdenv, fetchurl, pkgconfig, ocaml, findlib, camlp5, ncurses, lablgtk ? null}: +{stdenv, fetchurl, pkgconfig, writeText, ocaml, findlib, camlp5, ncurses, lablgtk ? null}: -let +let version = "8.4pl4"; + coq-version = "8.4"; buildIde = lablgtk != null; ideFlags = if buildIde then "-lablgtkdir ${lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt" else ""; - idePath = if buildIde then '' - CAML_LD_LIBRARY_PATH=${lablgtk}/lib/ocaml/3.12.1/site-lib/stublibs - '' else ""; in stdenv.mkDerivation { name = "coq-${version}"; + inherit coq-version; + inherit ocaml camlp5; + src = fetchurl { url = "http://coq.inria.fr/distrib/V${version}/files/coq-${version}.tar.gz"; sha256 = "00bzf4kfbd0g279jrr8ynzvb9wqcly3wi577bkrxivhrg2msxhq6"; @@ -31,7 +32,6 @@ stdenv.mkDerivation { ''; preConfigure = '' - buildFlagsArray=(${idePath}) configureFlagsArray=( -opt -camldir ${ocaml}/bin @@ -44,7 +44,17 @@ stdenv.mkDerivation { buildFlags = "revision coq coqide"; - meta = { + 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) + ''; + + meta = with stdenv.lib; { description = "Formal proof management system"; longDescription = '' Coq is a formal proof management system. It provides a formal language @@ -53,8 +63,8 @@ stdenv.mkDerivation { machine-checked proofs. ''; homepage = "http://coq.inria.fr"; - license = "LGPL"; - maintainers = with stdenv.lib.maintainers; [ roconnor thoughtpolice ]; - platforms = stdenv.lib.platforms.unix; + license = licenses.lgpl21; + maintainers = with maintainers; [ roconnor thoughtpolice vbgl ]; + platforms = platforms.unix; }; }