coq: setup-hook for libraries
Adds a hook to automatically populate the $COQPATH variable. Coq libraries are expected to be installed in lib/coq/${coq-version}/user-contrib/
This commit is contained in:
parent
181139fe09
commit
fde68228d9
|
@ -54,7 +54,7 @@ stdenv.mkDerivation {
|
||||||
cp ide/*.cmi ide/ide.*a $out/lib/coq/ide/
|
cp ide/*.cmi ide/ide.*a $out/lib/coq/ide/
|
||||||
'' else "";
|
'' else "";
|
||||||
|
|
||||||
meta = {
|
meta = with stdenv.lib; {
|
||||||
description = "Coq proof assistant";
|
description = "Coq proof assistant";
|
||||||
longDescription = ''
|
longDescription = ''
|
||||||
Coq is a formal proof management system. It provides a formal language
|
Coq is a formal proof management system. It provides a formal language
|
||||||
|
@ -63,7 +63,7 @@ stdenv.mkDerivation {
|
||||||
machine-checked proofs.
|
machine-checked proofs.
|
||||||
'';
|
'';
|
||||||
homepage = "http://coq.inria.fr";
|
homepage = "http://coq.inria.fr";
|
||||||
license = "LGPL";
|
license = licenses.lgpl21;
|
||||||
maintainers = [ stdenv.lib.maintainers.roconnor ];
|
maintainers = with maintainers; [ roconnor vbgl ];
|
||||||
};
|
};
|
||||||
}
|
}
|
||||||
|
|
|
@ -1,19 +1,20 @@
|
||||||
# - coqide compilation can be disabled by setting lablgtk to null;
|
# - 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
|
let
|
||||||
version = "8.5pre-01feb42";
|
version = "8.5pre-01feb42";
|
||||||
|
coq-version = "8.5";
|
||||||
buildIde = lablgtk != null;
|
buildIde = lablgtk != null;
|
||||||
ideFlags = if buildIde then "-lablgtkdir ${lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt" else "";
|
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
|
in
|
||||||
|
|
||||||
stdenv.mkDerivation {
|
stdenv.mkDerivation {
|
||||||
name = "coq-${version}";
|
name = "coq-${version}";
|
||||||
|
|
||||||
|
inherit coq-version;
|
||||||
|
inherit ocaml camlp5;
|
||||||
|
|
||||||
src = fetchgit {
|
src = fetchgit {
|
||||||
url = git://scm.gforge.inria.fr/coq/coq.git;
|
url = git://scm.gforge.inria.fr/coq/coq.git;
|
||||||
rev = "01feb4206d26b41bfaab9bd45a7b2fc4db569baf";
|
rev = "01feb4206d26b41bfaab9bd45a7b2fc4db569baf";
|
||||||
|
@ -32,8 +33,17 @@ stdenv.mkDerivation {
|
||||||
substituteInPlace Makefile.build --replace "ifeq (\$(ARCH),Darwin)" "ifeq (\$(ARCH),Darwinx)"
|
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 = ''
|
preConfigure = ''
|
||||||
buildFlagsArray=(${idePath})
|
|
||||||
configureFlagsArray=(
|
configureFlagsArray=(
|
||||||
-opt
|
-opt
|
||||||
${ideFlags}
|
${ideFlags}
|
||||||
|
@ -44,7 +54,7 @@ stdenv.mkDerivation {
|
||||||
|
|
||||||
buildFlags = "revision coq coqide";
|
buildFlags = "revision coq coqide";
|
||||||
|
|
||||||
meta = {
|
meta = with stdenv.lib; {
|
||||||
description = "Coq proof assistant";
|
description = "Coq proof assistant";
|
||||||
longDescription = ''
|
longDescription = ''
|
||||||
Coq is a formal proof management system. It provides a formal language
|
Coq is a formal proof management system. It provides a formal language
|
||||||
|
@ -53,8 +63,8 @@ stdenv.mkDerivation {
|
||||||
machine-checked proofs.
|
machine-checked proofs.
|
||||||
'';
|
'';
|
||||||
homepage = "http://coq.inria.fr";
|
homepage = "http://coq.inria.fr";
|
||||||
license = "LGPL";
|
license = licenses.lgpl21;
|
||||||
maintainers = with stdenv.lib.maintainers; [ roconnor thoughtpolice ];
|
maintainers = with maintainers; [ roconnor thoughtpolice vbgl ];
|
||||||
platforms = stdenv.lib.platforms.unix;
|
platforms = platforms.unix;
|
||||||
};
|
};
|
||||||
}
|
}
|
||||||
|
|
|
@ -1,19 +1,20 @@
|
||||||
# - coqide compilation can be disabled by setting lablgtk to null;
|
# - 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";
|
version = "8.4pl4";
|
||||||
|
coq-version = "8.4";
|
||||||
buildIde = lablgtk != null;
|
buildIde = lablgtk != null;
|
||||||
ideFlags = if buildIde then "-lablgtkdir ${lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt" else "";
|
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
|
in
|
||||||
|
|
||||||
stdenv.mkDerivation {
|
stdenv.mkDerivation {
|
||||||
name = "coq-${version}";
|
name = "coq-${version}";
|
||||||
|
|
||||||
|
inherit coq-version;
|
||||||
|
inherit ocaml camlp5;
|
||||||
|
|
||||||
src = fetchurl {
|
src = fetchurl {
|
||||||
url = "http://coq.inria.fr/distrib/V${version}/files/coq-${version}.tar.gz";
|
url = "http://coq.inria.fr/distrib/V${version}/files/coq-${version}.tar.gz";
|
||||||
sha256 = "00bzf4kfbd0g279jrr8ynzvb9wqcly3wi577bkrxivhrg2msxhq6";
|
sha256 = "00bzf4kfbd0g279jrr8ynzvb9wqcly3wi577bkrxivhrg2msxhq6";
|
||||||
|
@ -31,7 +32,6 @@ stdenv.mkDerivation {
|
||||||
'';
|
'';
|
||||||
|
|
||||||
preConfigure = ''
|
preConfigure = ''
|
||||||
buildFlagsArray=(${idePath})
|
|
||||||
configureFlagsArray=(
|
configureFlagsArray=(
|
||||||
-opt
|
-opt
|
||||||
-camldir ${ocaml}/bin
|
-camldir ${ocaml}/bin
|
||||||
|
@ -44,7 +44,17 @@ stdenv.mkDerivation {
|
||||||
|
|
||||||
buildFlags = "revision coq coqide";
|
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";
|
description = "Formal proof management system";
|
||||||
longDescription = ''
|
longDescription = ''
|
||||||
Coq is a formal proof management system. It provides a formal language
|
Coq is a formal proof management system. It provides a formal language
|
||||||
|
@ -53,8 +63,8 @@ stdenv.mkDerivation {
|
||||||
machine-checked proofs.
|
machine-checked proofs.
|
||||||
'';
|
'';
|
||||||
homepage = "http://coq.inria.fr";
|
homepage = "http://coq.inria.fr";
|
||||||
license = "LGPL";
|
license = licenses.lgpl21;
|
||||||
maintainers = with stdenv.lib.maintainers; [ roconnor thoughtpolice ];
|
maintainers = with maintainers; [ roconnor thoughtpolice vbgl ];
|
||||||
platforms = stdenv.lib.platforms.unix;
|
platforms = platforms.unix;
|
||||||
};
|
};
|
||||||
}
|
}
|
||||||
|
|
Loading…
Reference in a new issue