cafkafk/nixpkgs
cafkafk/nixpkgs
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

Change the name of the coq derivation to coq-devel-8.3pre1

Browse source 
i.e., remove the version from the name.  Nix has its own mechanism to
prevent a packages to be upgraded.  Instead we distinguish development
version (coq-dev-VERSION) from stable versions (coq-VERSION).

Also remove derivation for coq-8.3-beta0-1 which is now superseded by
coq-devel-8.3pre1.


svn path=/nixpkgs/trunk/; revision=23813
This commit is contained in:
Marco Maggesi 2010-09-15 19:39:48 +00:00
parent 139de1ea2f
commit 44f2d4439f
4 changed files with 3 additions and 80 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
pkgs/applications/science/logic/coq/8.3rc1.nix
View file

@ -5,7 +5,7 @@
{stdenv, fetchurl, ocaml, camlp5, lablgtk, ncurses}:
stdenv.mkDerivation {
name = "coq8.3-8.3pre1";
name = "coq-devel-8.3pre1";
src = fetchurl {
url = http://coq.inria.fr/distrib/V8.3-rc1/files/coq-8.3-rc1.tar.gz;
@ -40,7 +40,7 @@ stdenv.mkDerivation {
buildFlags = "world"; # Debug with "world VERBOSE=1";
meta = {
description = "Coq proof assistant";
description = "Coq proof assistant (development version)";
longDescription = ''
Coq is a formal proof management system. It provides a formal language
to write mathematical definitions, executable algorithms and theorems

53
pkgs/applications/science/logic/coq/beta.nix
View file

@ -1,53 +0,0 @@
# TODO:
# - coqide compilation should be optional or (better) separate;
# - coqide libraries are not installed;
{stdenv, fetchurl, ocaml, camlp5, lablgtk, ncurses}:
stdenv.mkDerivation {
name = "coq-8.3-beta0-1";
src = fetchurl {
url = http://coq.inria.fr/distrib/V8.3-beta0/files/coq-8.3-beta0-1.tar.gz;
sha256 = "01m1x0gpzfsiybyqanm82ls8q63q0g2d9vvfs99zf4z1nny7vlf1";
};
buildInputs = [ ocaml camlp5 ncurses lablgtk ];
prefixKey = "-prefix ";
preConfigure = ''
ARCH=`uname -s`
CAMLDIR=`type -p ocamlc`
'';
configureFlags =
"-arch $ARCH " +
"-camldir $CAMLDIR " +
"-camldir ${ocaml}/bin " +
"-camlp5dir ${camlp5}/lib/ocaml/camlp5 " +
"-lablgtkdir ${lablgtk}/lib/ocaml/lablgtk2 " +
"-opt -coqide opt";
buildFlags = "world"; # Debug with "world VERBOSE=1";
patches = [ ./coq-8.3-beta0-1.patch ];
postPatch = ''
substituteInPlace scripts/coqmktop.ml --replace \
"\"-I\"; \"+lablgtk2\"" \
"\"-I\"; \"${lablgtk}/lib/ocaml/lablgtk2\"; \"-I\"; \"${lablgtk}/lib/ocaml/stublibs\""
'';
meta = {
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 = "LGPL";
};
}

20
pkgs/applications/science/logic/coq/coq-8.3-beta0-1.patch
View file

@ -1,20 +0,0 @@
diff -Nurp coq-8.3-beta0-1/configure coq-8.3-beta0-1-nix/configure
--- coq-8.3-beta0-1/configure 2010-02-16 12:37:58.000000000 +0100
+++ coq-8.3-beta0-1-nix/configure 2010-05-11 17:47:44.000000000 +0200
@@ -394,7 +394,6 @@ case $camldir_spec in
ocamlyaccexec=$CAMLBIN/ocamlyacc
ocamlmktopexec=$CAMLBIN/ocamlmktop
ocamlmklibexec=$CAMLBIN/ocamlmklib
- camlp4oexec=$CAMLBIN/camlp4o
esac
if test ! -f "$CAMLC" ; then
@@ -626,7 +625,7 @@ case $COQIDE in
no) LABLGTKLIB=+lablgtk2 # Pour le message
LABLGTKINCLUDES="-I $LABLGTKLIB";; # Pour le makefile
yes) LABLGTKLIB="$lablgtkdir" # Pour le message
- LABLGTKINCLUDES="-I \"$LABLGTKLIB\"";; # Pour le makefile
+ LABLGTKINCLUDES="-I $LABLGTKLIB";; # Pour le makefile
esac;;
no) LABLGTKINCLUDES="";;
esac

6
pkgs/top-level/all-packages.nix
View file

@ -6675,11 +6675,7 @@ let
camlp5 = camlp5_transitional;
};
coq8_3 = callPackage ../applications/science/logic/coq/8.3rc1.nix {
camlp5 = camlp5_transitional;
};
coq_beta = callPackage ../applications/science/logic/coq/beta.nix {
coq_devel = callPackage ../applications/science/logic/coq/8.3rc1.nix {
camlp5 = camlp5_transitional;
};