jolheiser/nixpkgs
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Merge pull request #4305 from vbgl/coq-containers

Browse Source 
Working with Coq
This commit is contained in:
Mateusz Kowalczyk 2014-09-30 15:04:30 +01:00
commit ce4ae2aa1e
13 changed files with 193 additions and 100 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

36
doc/language-support.xml
View File

@ -377,6 +377,42 @@ fileSystem = buildLuaPackage {
</section>
<section xml:id="ssec-language-coq"><title>Coq</title>
<para>
Coq libraries should be installed in
<literal>$(out)/lib/coq/${coq.coq-version}/user-contrib/</literal>.
Such directories are automatically added to the
<literal>$COQPATH</literal> environment variable by the hook defined
in the Coq derivation.
</para>
<para>
Some libraries require OCaml and sometimes also Camlp5. The exact
versions that were used to build Coq are saved in the
<literal>coq.ocaml</literal> and <literal>coq.camlp5</literal>
attributes.
</para>
<para>
Here is a simple package example. It is a pure Coq library, thus it
only depends on Coq. Its <literal>makefile</literal> has been
generated using <literal>coq_makefile</literal> so we only have to
set the <literal>$COQLIB</literal> variable at install time.
</para>
<programlisting>
{stdenv, fetchurl, coq}:
stdenv.mkDerivation {
src = fetchurl {
url = http://coq.inria.fr/pylons/contribs/files/Karatsuba/v8.4/Karatsuba.tar.gz;
sha256 = "0ymfpv4v49k4fm63nq6gcl1hbnnxrvjjp7yzc4973n49b853c5b1";
};
name = "coq-karatsuba";
buildInputs = [ coq ];
installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
}
</programlisting>
</section>
<!--
<section><title>Haskell</title>

5
lib/licenses.nix
View File

@ -82,6 +82,11 @@ rec {
fullName = "Common Development and Distribution License 1.0";
};
cecill-b = spdx {
shortName = "CECILL-B";
fullName = "CeCILL-B Free Software License Agreement";
};
cecill-c = spdx {
shortName = "CECILL-C";
fullName = "CeCILL-C Free Software License Agreement";

11
pkgs/applications/editors/emacs-modes/proofgeneral/4.3pre.nix
View File

@ -1,4 +1,4 @@
{ stdenv, fetchurl, emacs, texinfo, texLive, perl, which, automake }:
{ stdenv, fetchurl, emacs, texinfo, texLive, perl, which, automake, enableDoc ? false }:
stdenv.mkDerivation (rec {
name = "ProofGeneral-4.3pre131011";
@ -10,7 +10,7 @@ stdenv.mkDerivation (rec {
sourceRoot = name;
buildInputs = [ emacs texinfo texLive perl which ];
buildInputs = [ emacs texinfo perl which ] ++ stdenv.lib.optional enableDoc texLive;
prePatch =
'' sed -i "Makefile" \
@ -25,15 +25,20 @@ stdenv.mkDerivation (rec {
sed -i '96d' doc/ProofGeneral.texi
'';
patches = [ ./pg.patch ];
preBuild = ''
make clean;
'';
installPhase =
if enableDoc
then
# Copy `texinfo.tex' in the right place so that `texi2pdf' works.
'' cp -v "${automake}/share/"automake-*/texinfo.tex doc
make install install-doc
'';
''
else "make install";
meta = {
description = "Proof General, an Emacs front-end for proof assistants";

16
pkgs/applications/editors/emacs-modes/proofgeneral/pg.patch Normal file
View File

@ -0,0 +1,16 @@
diff -r c7d8bfff4c0a bin/proofgeneral
--- a/bin/proofgeneral Sat Sep 27 02:25:15 2014 +0100
+++ b/bin/proofgeneral Sat Sep 27 02:28:16 2014 +0100
@@ -73,11 +73,7 @@
# Try to find Proof General directory
if [ -z "$PGHOME" ] || [ ! -d "$PGHOME" ]; then
- # default relative to this script, otherwise PGHOMEDEFAULT
- MYDIR="`readlink --canonicalize "$0" | sed -ne 's,/bin/proofgeneral$,,p'`"
- if [ -d "$MYDIR" ]; then
- PGHOME="$MYDIR"
- elif [ -d "$PGHOMEDEFAULT" ]; then
+ if [ -d "$PGHOMEDEFAULT" ]; then
PGHOME="$PGHOMEDEFAULT"
else
echo "Cannot find the Proof General lisp files: Set PGHOME or use --pghome."

6
pkgs/applications/science/logic/coq/8.3.nix
View File

@ -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 ];
};
}

28
pkgs/applications/science/logic/coq/HEAD.nix
View File

@ -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;
};
}

30
pkgs/applications/science/logic/coq/default.nix
View File

@ -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;
};
}

50
pkgs/applications/science/logic/ssreflect/default.nix
View File

@ -1,50 +0,0 @@
# TODO:
# - coq needs to be invoked with the explicit path to the ssreflect theory
# e.g. coqide -R ~/.nix-profile/lib/coq/user-contrib/ ''
{stdenv, fetchurl, ocaml, camlp5, coq, makeWrapper}:
let
pname = "ssreflect";
version = "1.5";
name = "${pname}-${version}";
webpage = http://www.msr-inria.inria.fr/Projects/math-components;
in
stdenv.mkDerivation {
inherit name;
src = fetchurl {
url = "http://ssr.msr-inria.inria.fr/FTP/${name}.tar.gz";
sha256 = "0hm1ha7sxqfqhc7iwhx6zdz3nki4rj5nfd3ab24hmz8v7mlpinds";
};
buildInputs = [ ocaml camlp5 coq makeWrapper ];
patches = [ ./static.patch ];
installPhase = ''
COQLIB=$out/lib/coq/ make -f Makefile.coq install -e
mkdir -p $out/bin
cp bin/* $out/bin
for i in $out/bin/*; do
wrapProgram "$i" \
--add-flags "-R" \
--add-flags "$out/lib/coq/user-contrib/Ssreflect" \
--add-flags "Ssreflect"
done
makeWrapper "${coq}/bin/coqide" "$out/bin/ssrcoqide" --add-flags "-coqtop" --add-flags "$out/bin/ssrcoq"
'';
meta = {
description = "Small Scale Reflection extension for Coq";
longDescription = ''
Small Scale Reflection (ssreflect) is an extension of the Coq Theorem
Prover which enable a formal proof methodology based on the pervasive
use of computation with symbolic representation
'';
homepage = webpage;
license = "CeCILL B FREE SOFTWARE LICENSE or CeCILL FREE SOFTWARE LICENSE";
maintainers = [ stdenv.lib.maintainers.roconnor ];
};
}

21
pkgs/applications/science/logic/ssreflect/static.patch
View File

@ -1,21 +0,0 @@
--- ssreflect1.4-coq8.4/Make (revision 3823)
+++ ssreflect1.4-coq8.4/Make (working copy)
@@ -1,10 +1,10 @@
-### 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
-##
+## 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
+#
## What follows should be left untouched by the final user of ssreflect
-R theories Ssreflect

24
pkgs/development/coq-modules/containers/default.nix Normal file
View File

@ -0,0 +1,24 @@
{stdenv, fetchurl, coq}:
stdenv.mkDerivation {
name = "coq-containers-${coq.coq-version}";
src = fetchurl {
url = http://coq.inria.fr/pylons/contribs/files/Containers/v8.4/Containers.tar.gz;
sha256 = "1y9x2lwrskv2231z9ac3kv4bmg6h1415xpp4gl7v5w90ba6p6w8w";
};
buildInputs = [ coq.ocaml coq.camlp5 ];
propagatedBuildInputs = [ coq ];
installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
meta = with stdenv.lib; {
homepage = http://coq.inria.fr/pylons/pylons/contribs/view/Containers/v8.4;
description = "A typeclass-based Coq library of finite sets/maps";
maintainers = with maintainers; [ vbgl ];
platforms = coq.meta.platforms;
};
}

24
pkgs/development/coq-modules/mathcomp/default.nix Normal file
View File

@ -0,0 +1,24 @@
{stdenv, fetchurl, coq, ssreflect}:
stdenv.mkDerivation {
name = "coq-mathcomp-1.5";
src = fetchurl {
url = http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.5.tar.gz;
sha256 = "1297svwi18blrlyd8vsqilar2h5nfixlvlifdkbx47aljq4m5bam";
};
propagatedBuildInputs = [ coq ssreflect ];
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 ];
platforms = coq.meta.platforms;
hydraPlatforms = [];
};
}

26
pkgs/development/coq-modules/ssreflect/default.nix Normal file
View File

@ -0,0 +1,26 @@
{stdenv, fetchurl, coq}:
assert coq.coq-version == "8.4";
stdenv.mkDerivation {
name = "coq-ssreflect-1.5";
src = fetchurl {
url = http://ssr.msr-inria.inria.fr/FTP/ssreflect-1.5.tar.gz;
sha256 = "0hm1ha7sxqfqhc7iwhx6zdz3nki4rj5nfd3ab24hmz8v7mlpinds";
};
buildInputs = [ coq.ocaml coq.camlp5 ];
propagatedBuildInputs = [ coq ];
installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
meta = with stdenv.lib; {
homepage = http://ssr.msr-inria.inria.fr/;
license = licenses.cecill-b;
maintainers = with maintainers; [ vbgl ];
platforms = coq.meta.platforms;
};
}

16
pkgs/top-level/all-packages.nix
View File

@ -11456,6 +11456,18 @@ let
lablgtk = ocamlPackages_3_12_1.lablgtk_2_14;
};
mkCoqPackages_8_4 = self: let callPackage = newScope self; in {
containers = callPackage ../development/coq-modules/containers {};
mathcomp = callPackage ../development/coq-modules/mathcomp {};
ssreflect = callPackage ../development/coq-modules/ssreflect {};
};
coqPackages = recurseIntoAttrs (mkCoqPackages_8_4 coqPackages);
cvc3 = callPackage ../applications/science/logic/cvc3 {};
ekrhyper = callPackage ../applications/science/logic/ekrhyper {};
@ -11525,10 +11537,6 @@ let
spass = callPackage ../applications/science/logic/spass {};
ssreflect = callPackage ../applications/science/logic/ssreflect {
camlp5 = ocamlPackages.camlp5_transitional;
};
tptp = callPackage ../applications/science/logic/tptp {};
twelf = callPackage ../applications/science/logic/twelf {