ilyakooo0/nixpkgs
1
0
Fork 0
mirror of https://github.com/ilyakooo0/nixpkgs.git synced 2024-12-28 14:22:50 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #87224 from Sohalt/isabelle

Browse Source 
isabelle: 2018 -> 2020
This commit is contained in:
Lassulus 2020-08-23 11:28:53 +02:00 committed by GitHub
commit 15d98507ee
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 13 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
pkgs/applications/science/logic/isabelle/default.nix
View File

@ -3,18 +3,18 @@
stdenv.mkDerivation rec {
pname = "isabelle";
version = "2018";
version = "2020";
dirname = "Isabelle${version}";
src = if stdenv.isDarwin
then fetchurl {
url = "http://isabelle.in.tum.de/website-${dirname}/dist/${dirname}.dmg";
sha256 = "0jwnvsf5whklq14ihaxs7b9nbic94mm56nvxljrdbvl6y628j9r5";
url = "https://isabelle.in.tum.de/website-${dirname}/dist/${dirname}_macos.tar.gz";
sha256 = "1sfr5filsaqj93g5y4p9n8g5652dhr4whj25x4lifdxr2pp560xx";
}
else fetchurl {
url = "https://isabelle.in.tum.de/website-${dirname}/dist/${dirname}_linux.tar.gz";
sha256 = "1928lwrw1v1p9s23kix30ncpqm8djmrnjixj82f3ni2a8sc3hrsp";
sha256 = "1bibabhlsvf6qsjjkgxcpq3cvl1z7r8yfcgqbhbvsiv69n3gyfk3";
};
buildInputs = [ perl polyml z3 ]
@ -42,14 +42,14 @@ stdenv.mkDerivation rec {
ML_SOURCES="\$POLYML_HOME/src"
EOF
cat >contrib/jdk/etc/settings <<EOF
cat >contrib/jdk*/etc/settings <<EOF
ISABELLE_JAVA_PLATFORM=${stdenv.system}
ISABELLE_JDK_HOME=${java}
EOF
echo ISABELLE_LINE_EDITOR=${rlwrap}/bin/rlwrap >>etc/settings
for comp in contrib/jdk contrib/polyml-* contrib/z3-*; do
for comp in contrib/jdk* contrib/polyml-* contrib/z3-*; do
rm -rf $comp/x86*
done
'' + (if ! stdenv.isLinux then "" else ''
@ -66,7 +66,7 @@ stdenv.mkDerivation rec {
bin/isabelle install $out/bin
'';
meta = {
meta = with stdenv.lib; {
description = "A generic proof assistant";
longDescription = ''
@ -74,9 +74,9 @@ stdenv.mkDerivation rec {
to be expressed in a formal language and provides tools for proving those
formulas in a logical calculus.
'';
homepage = "http://isabelle.in.tum.de/";
license = "LGPL";
maintainers = [ stdenv.lib.maintainers.jwiegley ];
platforms = stdenv.lib.platforms.linux;
homepage = "https://isabelle.in.tum.de/";
license = licenses.bsd3;
maintainers = [ maintainers.jwiegley ];
platforms = platforms.linux;
};
}

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

@ -25827,11 +25827,11 @@ in
ifstat-legacy = callPackage ../tools/networking/ifstat-legacy { };
isabelle = callPackage ../applications/science/logic/isabelle {
polyml = stdenv.lib.overrideDerivation polyml57 (attrs: {
polyml = stdenv.lib.overrideDerivation polyml (attrs: {
configureFlags = [ "--enable-intinf-as-int" "--with-gmp" "--disable-shared" ];
});
java = if stdenv.isLinux then jre else jdk;
java = openjdk11;
};
iprover = callPackage ../applications/science/logic/iprover { };