Merge pull request #152921 from jvanbruegge/isabelle-2021-1

isabelle: 2021 -> 2021-1

2 files changed, 14 insertions, 12 deletions

diff --git a/pkgs/applications/science/logic/isabelle/default.nix b/pkgs/applications/science/logic/isabelle/default.nix
index f9337f69025..e69c76352b9 100644
--- a/pkgs/applications/science/logic/isabelle/default.nix
+++ b/pkgs/applications/science/logic/isabelle/default.nix
@@ -1,24 +1,24 @@
-{ lib, stdenv, fetchurl, perl, perlPackages, makeWrapper, nettools, java, polyml, z3, rlwrap, makeDesktopItem }:
+{ lib, stdenv, fetchurl, perl, perlPackages, makeWrapper, nettools, java, polyml, z3, veriT, rlwrap, makeDesktopItem }:
 # nettools needed for hostname
 
 stdenv.mkDerivation rec {
   pname = "isabelle";
-  version = "2021";
+  version = "2021-1";
 
   dirname = "Isabelle${version}";
 
   src = if stdenv.isDarwin
     then fetchurl {
       url = "https://isabelle.in.tum.de/website-${dirname}/dist/${dirname}_macos.tar.gz";
-      sha256 = "1c2qm2ksmpyxyccyyn4lyj2wqj5m74nz2i0c5abrd1hj45zcnh1m";
+      sha256 = "0n1ls9vwf0ps1x8zpb7c1xz1wkasgvc34h5bz280hy2z6iqwmwbc";
     }
     else fetchurl {
       url = "https://isabelle.in.tum.de/website-${dirname}/dist/${dirname}_linux.tar.gz";
-      sha256 = "1isgc9w4q95638dcag9gxz1kmf97pkin3jz1dm2lhd64b2k12y2x";
+      sha256 = "0jfaqckhg388jh9b4msrpkv6wrd6xzlw18m0bngbby8k8ywalp9i";
     };
 
   nativeBuildInputs = [ makeWrapper ];
-  buildInputs = [ perl polyml z3 ]
+  buildInputs = [ perl polyml z3 veriT ]
              ++ lib.optionals (!stdenv.isDarwin) [ nettools java ];
 
   sourceRoot = dirname;
@@ -33,6 +33,10 @@ stdenv.mkDerivation rec {
       Z3_INSTALLED=yes
     EOF
 
+    cat >contrib/verit-*/etc/settings <<EOF
+      ISABELLE_VERIT=${veriT}/bin/veriT
+    EOF
+
     cat >contrib/polyml-*/etc/settings <<EOF
       ML_SYSTEM_64=true
       ML_SYSTEM=${polyml.name}
@@ -52,7 +56,7 @@ stdenv.mkDerivation rec {
 
     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-* contrib/verit-*; do
       rm -rf $comp/x86*
     done
     '' + (if ! stdenv.isLinux then "" else ''
@@ -75,8 +79,6 @@ stdenv.mkDerivation rec {
     # desktop item
     mkdir -p "$out/share"
     cp -r "${desktopItem}/share/applications" "$out/share/applications"
-
-    wrapProgram $out/$dirname/src/HOL/Tools/ATP/scripts/remote_atp --set PERL5LIB ${perlPackages.makeFullPerlPath [ perlPackages.LWP ]}
   '';
 
   desktopItem = makeDesktopItem {
diff --git a/pkgs/applications/science/logic/verit/default.nix b/pkgs/applications/science/logic/verit/default.nix
index 81acbe4f2d0..6c0d1061dca 100644
--- a/pkgs/applications/science/logic/verit/default.nix
+++ b/pkgs/applications/science/logic/verit/default.nix
@@ -2,11 +2,11 @@
 
 stdenv.mkDerivation {
   pname = "veriT";
-  version = "2016";
+  version = "2021.06.2";
 
   src = fetchurl {
-    url = "http://www.verit-solver.org/distrib/veriT-stable2016.tar.gz";
-    sha256 = "0gvp4diz0qjg0y5ry0p1z7dkdkxw8l7jb8cdhvcnhl06jx977v4b";
+    url = "https://verit.loria.fr/download/2021.06.2/verit-2021.06.2-rmx.tar.gz";
+    sha256 = "1yjvvxnsix0rhilc81ycx1s85dymq366c6zh1hwwd8qxp7k1zca2";
   };
 
   nativeBuildInputs = [ autoreconfHook flex bison ];
@@ -23,7 +23,7 @@ stdenv.mkDerivation {
 
   meta = with lib; {
     description = "An open, trustable and efficient SMT-solver";
-    homepage = "http://www.verit-solver.org/";
+    homepage = "https://verit.loria.fr/";
     license = licenses.bsd3;
     platforms = platforms.unix;
     maintainers = [ maintainers.gebner ];