parent
39d8b61a25
commit
9402a56620
@ -0,0 +1,68 @@ |
||||
# - coqide compilation can be disabled by setting lablgtk to null; |
||||
|
||||
{stdenv, fetchurl, writeText, pkgconfig, ocaml, findlib, camlp5, ncurses, lablgtk ? null}: |
||||
|
||||
let |
||||
version = "8.5b2"; |
||||
coq-version = "8.5"; |
||||
buildIde = lablgtk != null; |
||||
ideFlags = if buildIde then "-lablgtkdir ${lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt" else ""; |
||||
in |
||||
|
||||
stdenv.mkDerivation { |
||||
name = "coq-${version}"; |
||||
|
||||
inherit coq-version; |
||||
inherit ocaml camlp5; |
||||
|
||||
src = fetchurl { |
||||
url = https://coq.inria.fr/distrib/V8.5beta2/files/coq-8.5beta2.tar.gz; |
||||
sha256 = "1z34ch56lld86srgsjdwdq3girz0k0wqmvyxsa7jwvvxn3qmmq2v"; |
||||
}; |
||||
|
||||
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 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 = '' |
||||
configureFlagsArray=( |
||||
-opt |
||||
${ideFlags} |
||||
) |
||||
''; |
||||
|
||||
prefixKey = "-prefix "; |
||||
|
||||
buildFlags = "revision coq coqide"; |
||||
|
||||
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; |
||||
}; |
||||
} |
@ -0,0 +1,26 @@ |
||||
{stdenv, fetchurl, coq, ssreflect}: |
||||
|
||||
stdenv.mkDerivation { |
||||
|
||||
name = "coq-mathcomp-1.5-8.5b2"; |
||||
|
||||
src = fetchurl { |
||||
url = http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.5.coq85beta2.tar.gz; |
||||
sha256 = "03bnq44ym43x8shi7whc02l0g5vy6rx8f1imjw478chlgwcxazqy"; |
||||
}; |
||||
|
||||
propagatedBuildInputs = [ coq ssreflect ]; |
||||
|
||||
enableParallelBuilding = true; |
||||
|
||||
installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/"; |
||||
|
||||
meta = with stdenv.lib; { |
||||
homepage = http://ssr.msr-inria.inria.fr/; |
||||
license = licenses.cecill-b; |
||||
maintainers = [ maintainers.vbgl maintainers.jwiegley ]; |
||||
platforms = coq.meta.platforms; |
||||
hydraPlatforms = []; |
||||
}; |
||||
|
||||
} |
@ -0,0 +1,42 @@ |
||||
{stdenv, fetchurl, coq}: |
||||
|
||||
assert coq.coq-version == "8.5"; |
||||
|
||||
stdenv.mkDerivation { |
||||
|
||||
name = "coq-ssreflect-1.5-8.5b2"; |
||||
|
||||
src = fetchurl { |
||||
url = http://ssr.msr-inria.inria.fr/FTP/ssreflect-1.5.coq85beta2.tar.gz; |
||||
sha256 = "084l9xd5vgb8jml0dkm66g8cil5rsf04w821pjhn2qk9mdbwaagf"; |
||||
}; |
||||
|
||||
buildInputs = [ coq.ocaml coq.camlp5 ]; |
||||
propagatedBuildInputs = [ coq ]; |
||||
|
||||
enableParallelBuilding = true; |
||||
|
||||
patches = [ ./threads.patch ]; |
||||
|
||||
postPatch = '' |
||||
# Permit building of the ssrcoq statically-bound executable |
||||
sed -i 's/^#-custom/-custom/' Make |
||||
sed -i 's/^#SSRCOQ/SSRCOQ/' Make |
||||
''; |
||||
|
||||
installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/"; |
||||
|
||||
postInstall = '' |
||||
mkdir -p $out/bin |
||||
cp -p bin/ssrcoq $out/bin |
||||
cp -p bin/ssrcoq.byte $out/bin |
||||
''; |
||||
|
||||
meta = with stdenv.lib; { |
||||
homepage = http://ssr.msr-inria.inria.fr/; |
||||
license = licenses.cecill-b; |
||||
maintainers = with maintainers; [ vbgl jwiegley ]; |
||||
platforms = coq.meta.platforms; |
||||
}; |
||||
|
||||
} |
@ -0,0 +1,16 @@ |
||||
--- a/Make 2015-04-20 13:37:06.000000000 +0200
|
||||
+++ b/Make 2015-04-25 11:32:53.885194600 +0200
|
||||
@@ -1,9 +1,9 @@
|
||||
### Uncomment for static linking
|
||||
##
|
||||
-#-custom "$(COQBIN)coqmktop -coqlib `$(COQBIN)coqtop -where` -opt -o bin/ssrcoq src/ssrmatching.cmx src/ssreflect.cmx" "src/ssrmatching.cmx src/ssreflect.cmx" bin/ssrcoq
|
||||
-#-custom "$(COQBIN)coqmktop -coqlib `$(COQBIN)coqtop -where` -o bin/ssrcoq.byte src/ssrmatching.cmo src/ssreflect.cmo" "src/ssrmatching.cmo src/ssreflect.cmo" bin/ssrcoq.byte
|
||||
-#-custom "$(SSRCOQ) $(COQFLAGS) -compile $*" "%.v $(SSRCOQ)" "%.vo"
|
||||
-#SSRCOQ = bin/ssrcoq
|
||||
+-custom "$(COQBIN)coqmktop -coqlib `$(COQBIN)coqtop -where` -opt -o bin/ssrcoq -I +threads src/ssrmatching.cmx src/ssreflect.cmx" "src/ssrmatching.cmx src/ssreflect.cmx" bin/ssrcoq
|
||||
+-custom "$(COQBIN)coqmktop -coqlib `$(COQBIN)coqtop -where` -o bin/ssrcoq.byte -I +threads src/ssrmatching.cmo src/ssreflect.cmo" "src/ssrmatching.cmo src/ssreflect.cmo" bin/ssrcoq.byte
|
||||
+-custom "$(SSRCOQ) $(COQFLAGS) -compile $*" "%.v $(SSRCOQ)" "%.vo"
|
||||
+SSRCOQ = bin/ssrcoq
|
||||
##
|
||||
|
||||
## What follows should be left untouched by the final user of ssreflect
|
Loading…
Reference in new issue