verasco: remove unmaintained project
Verasco is no longer maintained by upstream and blocks updates of some libraries. Removing it also makes it possible to remove coq 8.4.
This commit is contained in:
@@ -1,51 +0,0 @@
|
||||
{ stdenv, lib, fetchurl
|
||||
, coq, ocaml, findlib, menhir, zarith
|
||||
, tools ? stdenv.cc
|
||||
}:
|
||||
|
||||
assert lib.versionAtLeast ocaml.version "4.02";
|
||||
|
||||
stdenv.mkDerivation rec {
|
||||
name = "verasco-1.3";
|
||||
src = fetchurl {
|
||||
url = "http://compcert.inria.fr/verasco/release/${name}.tgz";
|
||||
sha256 = "0zvljrpwnv443k939zlw1f7ijwx18nhnpr8jl3f01jc5v66hr2k8";
|
||||
};
|
||||
|
||||
buildInputs = [ coq ocaml findlib menhir zarith ];
|
||||
|
||||
preConfigure = ''
|
||||
substituteInPlace ./configure --replace '{toolprefix}gcc' '{toolprefix}cc'
|
||||
'';
|
||||
|
||||
configureFlags = [
|
||||
"-toolprefix ${tools}/bin/"
|
||||
(if stdenv.isDarwin then "ia32-macosx" else "ia32-linux")
|
||||
];
|
||||
|
||||
prefixKey = "-prefix ";
|
||||
|
||||
enableParallelBuilding = true;
|
||||
buildFlags = "proof extraction ccheck";
|
||||
|
||||
installPhase = ''
|
||||
mkdir -p $out/bin
|
||||
cp ccheck $out/bin/
|
||||
ln -s $out/bin/ccheck $out/bin/verasco
|
||||
if [ -e verasco.ini ]
|
||||
then
|
||||
mkdir -p $out/share
|
||||
cp verasco.ini $out/share/
|
||||
fi
|
||||
mkdir -p $out/lib/compcert
|
||||
cp -riv runtime/include $out/lib/compcert
|
||||
'';
|
||||
|
||||
meta = {
|
||||
homepage = http://compcert.inria.fr/verasco/;
|
||||
description = "A static analyzer for the CompCert subset of ISO C 1999";
|
||||
maintainers = with stdenv.lib.maintainers; [ vbgl ];
|
||||
license = stdenv.lib.licenses.unfree;
|
||||
platforms = with stdenv.lib.platforms; darwin ++ linux;
|
||||
};
|
||||
}
|
||||
@@ -8984,10 +8984,6 @@ with pkgs;
|
||||
|
||||
qcachegrind = libsForQt5.callPackage ../development/tools/analysis/qcachegrind {};
|
||||
|
||||
verasco = ocaml-ng.ocamlPackages_4_02.verasco.override {
|
||||
coq = coq_8_4;
|
||||
};
|
||||
|
||||
visualvm = callPackage ../development/tools/java/visualvm { };
|
||||
|
||||
vultr = callPackage ../development/tools/vultr { };
|
||||
|
||||
@@ -1024,16 +1024,6 @@ let
|
||||
|
||||
omake_rc1 = callPackage ../development/tools/ocaml/omake/0.9.8.6-rc1.nix { };
|
||||
|
||||
verasco = callPackage ../development/tools/analysis/verasco ((
|
||||
if system == "x86_64-linux"
|
||||
then { tools = pkgs.pkgsi686Linux.stdenv.cc; }
|
||||
else {}
|
||||
) // {
|
||||
menhir = callPackage ../development/ocaml-modules/menhir {
|
||||
version = "20170712";
|
||||
};
|
||||
});
|
||||
|
||||
google-drive-ocamlfuse = callPackage ../applications/networking/google-drive-ocamlfuse { };
|
||||
|
||||
|
||||
|
||||
Reference in New Issue
Block a user