Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
coq_8_6: new package, based on Coq 8.6rc1
- Loading branch information
Showing
2 changed files
with
115 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,89 @@ | ||
# - coqide compilation can be disabled by setting lablgtk to null; | ||
# - 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 | ||
, pl ? "1" | ||
}: | ||
|
||
let | ||
version = "8.6rc${pl}"; | ||
sha256 = { | ||
"1" = "0wral36h39q7g2sa2z8jvjc8ggqmqsjrbs0k299n0nykmmrq1pr8"; | ||
}."${pl}"; | ||
coq-version = "8.6"; | ||
buildIde = lablgtk != null; | ||
ideFlags = if buildIde then "-lablgtkdir ${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 ""; | ||
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"; | ||
inherit sha256; | ||
}; | ||
|
||
buildInputs = [ pkgconfig ocaml findlib camlp5 ncurses lablgtk ]; | ||
|
||
postPatch = '' | ||
UNAME=$(type -tp uname) | ||
RM=$(type -tp rm) | ||
substituteInPlace configure --replace "/bin/uname" "$UNAME" | ||
substituteInPlace tools/beautify-archive --replace "/bin/rm" "$RM" | ||
substituteInPlace configure.ml --replace '"md5 -q"' '"md5sum"' | ||
${csdpPatch} | ||
''; | ||
|
||
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 = '' | ||
configureFlagsArray=( | ||
-opt | ||
${ideFlags} | ||
) | ||
''; | ||
|
||
prefixKey = "-prefix "; | ||
|
||
buildFlags = "revision coq coqide bin/votour"; | ||
|
||
postInstall = '' | ||
cp bin/votour $out/bin/ | ||
''; | ||
|
||
meta = with stdenv.lib; { | ||
description = "Coq proof assistant"; | ||
longDescription = '' | ||
Coq is a formal proof management system. It provides a formal language | ||
to write mathematical definitions, executable algorithms and theorems | ||
together with an environment for semi-interactive development of | ||
machine-checked proofs. | ||
''; | ||
homepage = "http://coq.inria.fr"; | ||
license = licenses.lgpl21; | ||
branch = coq-version; | ||
maintainers = with maintainers; [ roconnor thoughtpolice vbgl ]; | ||
platforms = platforms.unix; | ||
}; | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters