isabelle: 2021-1 -> 2022

{ lib, stdenv, fetchurl, coreutils, nettools, java, scala, polyml, z3, veriT, vampire, eprover-ho, naproche, rlwrap, perl, makeDesktopItem, isabelle-components, isabelle, symlinkJoin, fetchhg }:

# nettools needed for hostname

{ lib

, stdenv

, fetchurl

, coreutils

, nettools

, java

, scala_3

, polyml

, z3

, veriT

, vampire

, eprover-ho

, naproche

, rlwrap

, perl

, makeDesktopItem

, isabelle-components

, isabelle

, symlinkJoin

, fetchhg

}:

let

  sha1 = stdenv.mkDerivation {

  };

in stdenv.mkDerivation rec {

  pname = "isabelle";

  version = "2021-1";

  version = "2022";

  dirname = "Isabelle${version}";

      fetchurl

        {

          url = "https://isabelle.in.tum.de/website-${dirname}/dist/${dirname}_macos.tar.gz";

          sha256 = "0n1ls9vwf0ps1x8zpb7c1xz1wkasgvc34h5bz280hy2z6iqwmwbc";

          sha256 = "0b84rx9b7b5y8m1sg7xdp17j6yngd2dkx6v5bkd8h7ly102lai18";

        }

    else

      fetchurl {

        url = "https://isabelle.in.tum.de/website-${dirname}/dist/${dirname}_linux.tar.gz";

        sha256 = "0jfaqckhg388jh9b4msrpkv6wrd6xzlw18m0bngbby8k8ywalp9i";

        sha256 = "1ih4gykkp1an43qdgc5xzyvf30fhs0dah3y0a5ksbmvmjsfnxyp7";

      };

  nativeBuildInputs = [ java ];

  buildInputs = [ polyml z3 veriT vampire eprover-ho nettools ]

    ++ lib.optionals (!stdenv.isDarwin) [ java ];

  sourceRoot = "${dirname}${lib.optionalString stdenv.isDarwin ".app"}";

  sourceRoot = dirname;

  postUnpack = if stdenv.isDarwin then ''

    mv $sourceRoot ${dirname}

    sourceRoot=${dirname}

  '' else null;

  postUnpack = lib.optionalString stdenv.isDarwin ''

    mv $sourceRoot.app $sourceRoot

  '';

  postPatch = ''

    patchShebangs .

    patchShebangs lib/Tools/ bin/

    cat >contrib/z3*/etc/settings <<EOF

      Z3_HOME=${z3}

    substituteInPlace src/Tools/Setup/src/Environment.java \

      --replace 'cmd.add("/usr/bin/env");' "" \

      --replace 'cmd.add("bash");' "cmd.add(\"$SHELL\");"

      --replace 'cmd.add("bash");' "cmd.add(\"$SHELL\");" \

      --replace 'private static read_file(path: Path): String =' 'private static String read_file(Path path) throws IOException'

    substituteInPlace src/Pure/General/sha1.ML \

      --replace '"$ML_HOME/" ^ (if ML_System.platform_is_windows then "sha1.dll" else "libsha1.so")' '"${sha1}/lib/libsha1.so"'

  '' + lib.optionalString (stdenv.hostPlatform.system == "x86_64-darwin") ''

    substituteInPlace lib/scripts/isabelle-platform \

      --replace 'ISABELLE_APPLE_PLATFORM64=arm64-darwin' ""

  '' + (if ! stdenv.isLinux then "" else ''

  '' + lib.optionalString stdenv.isLinux ''

    arch=${if stdenv.hostPlatform.system == "x86_64-linux" then "x86_64-linux" else "x86-linux"}

    for f in contrib/*/$arch/{bash_process,epclextract,nunchaku,SPASS,zipperposition}; do

      patchelf --set-interpreter $(cat ${stdenv.cc}/nix-support/dynamic-linker) "$f"

    done

    for f in contrib/*/platform_$arch/{bash_process,epclextract,nunchaku,SPASS,zipperposition}; do

      patchelf --set-interpreter $(cat ${stdenv.cc}/nix-support/dynamic-linker) "$f"

    done

    for d in contrib/kodkodi-*/jni/$arch; do

      patchelf --set-rpath "${lib.concatStringsSep ":" [ "${java}/lib/openjdk/lib/server" "${stdenv.cc.cc.lib}/lib" ]}" $d/*.so

    done

  '');

  '';

  buildPhase = ''

    export HOME=$TMP # The build fails if home is not set

    do

      ARGS["''${#ARGS[@]}"]="src/Tools/Setup/$SRC"

    done

    ${java}/bin/javac -d "$TARGET_DIR" -classpath ${scala}/lib/scala-compiler.jar "''${ARGS[@]}"

    ${java}/bin/jar -c -f "$TARGET_DIR/isabelle_setup.jar" -e "isabelle.setup.Setup" -C "$TARGET_DIR" isabelle

    echo "Building isabelle setup"

    javac -d "$TARGET_DIR" -classpath "${scala_3.bare}/lib/scala3-interfaces-${scala_3.version}.jar:${scala_3.bare}/lib/scala3-compiler_3-${scala_3.version}.jar" "''${ARGS[@]}"

    jar -c -f "$TARGET_DIR/isabelle_setup.jar" -e "isabelle.setup.Setup" -C "$TARGET_DIR" isabelle

    rm -rf "$TARGET_DIR/isabelle"

    # Prebuild HOL Session

    echo "Building HOL heap"

    bin/isabelle build -v -o system_heaps -b HOL

  '';

  isabelle = callPackage ../applications/science/logic/isabelle {

    polyml = polyml.overrideAttrs (_: {

      pname = "polyml-for-isabelle";

      version = "2021-1";

      version = "2022";

      configureFlags = [ "--enable-intinf-as-int" "--with-gmp" "--disable-shared" ];

      buildFlags = [ "compiler" ];

      src = fetchFromGitHub {

        owner = "polyml";

        repo = "polyml";

        rev = "39d96a2def903ed019c6855e3b688df5070d633a";

        sha256 = "sha256-S7d2Vr/nB+rCX9d4qQj4f7edVZKocKIjc5rrx9A/B4Q=";

        rev = "bafe319bc3a65bf63bd98a4721a6f4dd9e0eabd6";

        sha256 = "1ygs09zzq8icq1gc8qf4sb24lxx7sbcyd5hw3vw67a3ryaki0qw2";

      };

    });