alt-ergo: 1.30->2.2.0, ocplib-simplex: 0.3->0.4
This commit is contained in:
parent
0ba1f0aa72
commit
6738033727
|
@ -500,6 +500,12 @@ lib.mapAttrs (n: v: v // { shortName = n; }) rec {
|
||||||
fullName = "Non-Profit Open Software License 3.0";
|
fullName = "Non-Profit Open Software License 3.0";
|
||||||
};
|
};
|
||||||
|
|
||||||
|
ocamlpro_nc = {
|
||||||
|
fullName = "OCamlPro Non Commercial license version 1";
|
||||||
|
url = "https://alt-ergo.ocamlpro.com/http/alt-ergo-2.2.0/OCamlPro-Non-Commercial-License.pdf";
|
||||||
|
free = false;
|
||||||
|
};
|
||||||
|
|
||||||
ofl = spdx {
|
ofl = spdx {
|
||||||
spdxId = "OFL-1.1";
|
spdxId = "OFL-1.1";
|
||||||
fullName = "SIL Open Font License 1.1";
|
fullName = "SIL Open Font License 1.1";
|
||||||
|
|
|
@ -2,21 +2,21 @@
|
||||||
|
|
||||||
stdenv.mkDerivation rec {
|
stdenv.mkDerivation rec {
|
||||||
name = "alt-ergo-${version}";
|
name = "alt-ergo-${version}";
|
||||||
version = "1.30";
|
version = "2.2.0";
|
||||||
|
|
||||||
src = fetchurl {
|
src = fetchurl {
|
||||||
url = "https://alt-ergo.ocamlpro.com/download_manager.php?target=${name}.tar.gz";
|
url = "https://alt-ergo.ocamlpro.com/download_manager.php?target=${name}.tar.gz";
|
||||||
name = "${name}.tar.gz";
|
name = "${name}.tar.gz";
|
||||||
sha256 = "025pacb4ax864fn5x8k78mw6hiig4jcazblj18gzxspg4f1l5n1g";
|
sha256 = "106zfgisq6qxr7dlk8z7gi68ly7qff4frn8wab2g8z2nkkwla92w";
|
||||||
};
|
};
|
||||||
|
|
||||||
buildInputs = with ocamlPackages;
|
buildInputs = with ocamlPackages;
|
||||||
[ ocaml findlib camlzip ocamlgraph zarith lablgtk ocplib-simplex ];
|
[ ocaml findlib camlzip ocamlgraph zarith lablgtk ocplib-simplex psmt2-frontend menhir num ];
|
||||||
|
|
||||||
meta = {
|
meta = {
|
||||||
description = "High-performance theorem prover and SMT solver";
|
description = "High-performance theorem prover and SMT solver";
|
||||||
homepage = "https://alt-ergo.ocamlpro.com/";
|
homepage = "https://alt-ergo.ocamlpro.com/";
|
||||||
license = stdenv.lib.licenses.cecill-c; # LGPL-2 compatible
|
license = stdenv.lib.licenses.ocamlpro_nc;
|
||||||
platforms = stdenv.lib.platforms.linux ++ stdenv.lib.platforms.darwin;
|
platforms = stdenv.lib.platforms.linux ++ stdenv.lib.platforms.darwin;
|
||||||
maintainers = [ stdenv.lib.maintainers.thoughtpolice ];
|
maintainers = [ stdenv.lib.maintainers.thoughtpolice ];
|
||||||
};
|
};
|
||||||
|
|
|
@ -2,7 +2,7 @@
|
||||||
|
|
||||||
let
|
let
|
||||||
pname = "ocplib-simplex";
|
pname = "ocplib-simplex";
|
||||||
version = "0.3";
|
version = "0.4";
|
||||||
in
|
in
|
||||||
|
|
||||||
stdenv.mkDerivation {
|
stdenv.mkDerivation {
|
||||||
|
@ -11,13 +11,15 @@ stdenv.mkDerivation {
|
||||||
src = fetchFromGitHub {
|
src = fetchFromGitHub {
|
||||||
owner = "OCamlPro-Iguernlala";
|
owner = "OCamlPro-Iguernlala";
|
||||||
repo = pname;
|
repo = pname;
|
||||||
rev = version;
|
rev = "v${version}";
|
||||||
sha256 = "1fmz38w2cj9fny4adqqyil59dvndqkr59s7wk2gqs47r72b6sisa";
|
sha256 = "09niyidrjzrj8g1qwx4wgsdf5m6cwrnzg7zsgala36jliic4di60";
|
||||||
};
|
};
|
||||||
|
|
||||||
nativeBuildInputs = [ autoreconfHook ];
|
nativeBuildInputs = [ autoreconfHook ];
|
||||||
buildInputs = [ ocaml findlib ];
|
buildInputs = [ ocaml findlib ];
|
||||||
|
|
||||||
|
installFlags = "LIBDIR=$(OCAMLFIND_DESTDIR)";
|
||||||
|
|
||||||
createFindlibDestdir = true;
|
createFindlibDestdir = true;
|
||||||
|
|
||||||
meta = {
|
meta = {
|
||||||
|
|
|
@ -21171,9 +21171,7 @@ with pkgs;
|
||||||
ocamlPackages = ocaml-ng.ocamlPackages_4_05;
|
ocamlPackages = ocaml-ng.ocamlPackages_4_05;
|
||||||
};
|
};
|
||||||
|
|
||||||
alt-ergo = callPackage ../applications/science/logic/alt-ergo {
|
alt-ergo = callPackage ../applications/science/logic/alt-ergo {};
|
||||||
ocamlPackages = ocaml-ng.ocamlPackages_4_05;
|
|
||||||
};
|
|
||||||
|
|
||||||
aspino = callPackage ../applications/science/logic/aspino {};
|
aspino = callPackage ../applications/science/logic/aspino {};
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue