Unverified Commit e175357f authored by Weijia Wang's avatar Weijia Wang Committed by GitHub
Browse files

isabelle: 2024 -> 2025 (#389562)

parents 46ab28f7 fa09ff7a
Loading
Loading
Loading
Loading
+3 −3
Original line number Diff line number Diff line
@@ -7,13 +7,13 @@

stdenv.mkDerivation rec {
  pname = "isabelle-linter";
  version = "2024-1.0.1";
  version = "2025-1.0.0";

  src = fetchFromGitHub {
    owner = "isabelle-prover";
    repo = "isabelle-linter";
    rev = "Isabelle2024-v1.0.1";
    hash = "sha256-oTrwcfJgbkpkIweDIyc6lZjAvdS9J4agPoJgZzH+PuQ=";
    rev = "Isabelle2025-v1.0.0";
    hash = "sha256-cH9EoIbKa6cqLjw83gnYvCy+Dq0d5fFmJCabdPrRJeI=";
  };

  nativeBuildInputs = [ isabelle ];
+17 −15
Original line number Diff line number Diff line
@@ -2,6 +2,7 @@
  lib,
  stdenv,
  fetchurl,
  fetchFromGitHub,
  coreutils,
  nettools,
  java,
@@ -10,7 +11,6 @@
  veriT,
  vampire,
  eprover-ho,
  naproche,
  rlwrap,
  perl,
  procps,
@@ -21,6 +21,15 @@
}:

let
  vampire' = vampire.overrideAttrs (_: {
    src = fetchFromGitHub {
      owner = "vprover";
      repo = "vampire";
      tag = "v4.8HO4Sledgahammer";
      hash = "sha256-CmppaGa4M9tkE1b25cY1LSPFygJy5yV4kpHKbPqvcVE=";
    };
  });

  sha1 = stdenv.mkDerivation {
    pname = "isabelle-sha1";
    version = "2024";
@@ -46,7 +55,7 @@ let
in
stdenv.mkDerivation (finalAttrs: rec {
  pname = "isabelle";
  version = "2024";
  version = "2025";

  dirname = "Isabelle${version}";

@@ -54,17 +63,17 @@ stdenv.mkDerivation (finalAttrs: rec {
    if stdenv.hostPlatform.isDarwin then
      fetchurl {
        url = "https://isabelle.in.tum.de/website-${dirname}/dist/${dirname}_macos.tar.gz";
        hash = "sha256-IgNfmW9x6h8DBj9vFEGV62oEl01NkW7QdyzXlWmii8c=";
        hash = "sha256-6ldUwiiFf12dOuJU7JgUeX8kU+opDfILL23LLvDi5/g=";
      }
    else if stdenv.hostPlatform.isx86 then
      fetchurl {
        url = "https://isabelle.in.tum.de/website-${dirname}/dist/${dirname}_linux.tar.gz";
        hash = "sha256-YDqq+KvqNll687BlHSwWKobAoN1EIHZvR+VyQDljkmc=";
        hash = "sha256-PR1m3jcYI/4xqormZjj3NXW6wkTwCzGu4dy2LzgUfFY=";
      }
    else
      fetchurl {
        url = "https://isabelle.in.tum.de/website-${dirname}/dist/${dirname}_linux_arm.tar.gz";
        hash = "sha256-jXWVv18WwrVnqVX1s4Lnyf7DkOzPa3EdLXYxgtKD+YA=";
        hash = "sha256-p/Hp+7J5gJy5s6BVD5Ma1Mu2OS53I8BS7gKSOYYB0PE=";
      };

  nativeBuildInputs = [ java ];
@@ -72,7 +81,7 @@ stdenv.mkDerivation (finalAttrs: rec {
  buildInputs = [
    polyml
    veriT
    vampire
    vampire'
    eprover-ho
    nettools
  ];
@@ -103,8 +112,8 @@ stdenv.mkDerivation (finalAttrs: rec {
      EOF

      cat >contrib/vampire-*/etc/settings <<EOF
        VAMPIRE_HOME=${vampire}/bin
        VAMPIRE_VERSION=${vampire.version}
        VAMPIRE_HOME=${vampire'}/bin
        VAMPIRE_VERSION=${vampire'.version}
        VAMPIRE_EXTRA_OPTIONS="--mode casc"
      EOF

@@ -123,13 +132,6 @@ stdenv.mkDerivation (finalAttrs: rec {
        ISABELLE_JDK_HOME=${java}
      EOF

    ''
    + lib.optionalString stdenv.hostPlatform.isx86 ''
      rm contrib/naproche-*/x86*/Naproche-SAD
      ln -s ${naproche}/bin/Naproche-SAD contrib/naproche-*/x86*/
    ''
    + ''

      echo ISABELLE_LINE_EDITOR=${rlwrap}/bin/rlwrap >>etc/settings

      for comp in contrib/jdk* contrib/polyml-* contrib/verit-* contrib/vampire-* contrib/e-*; do
+1 −7
Original line number Diff line number Diff line
@@ -18175,19 +18175,13 @@ with pkgs;
  isabelle = callPackage ../by-name/is/isabelle/package.nix {
    polyml = polyml.overrideAttrs {
      pname = "polyml-for-isabelle";
      version = "2024";
      version = "2025";
      configureFlags = [
        "--enable-intinf-as-int"
        "--with-gmp"
        "--disable-shared"
      ];
      buildFlags = [ "compiler" ];
      src = fetchFromGitHub {
        owner = "polyml";
        repo = "polyml";
        rev = "v5.9.1";
        hash = "sha256-72wm8dt+Id59A5058mVE5P9TkXW5/LZRthZoxUustVA=";
      };
    };
    java = openjdk21;