pkgs/by-name/is/isabelle/package.nix

   1 { lib
   2 , stdenv
   3 , fetchurl
   4 , coreutils
   5 , nettools
   6 , java
   7 , scala_3
   8 , polyml
   9 , veriT
  10 , vampire
  11 , eprover-ho
  12 , naproche
  13 , rlwrap
  14 , perl
  15 , procps
  16 , makeDesktopItem
  17 , isabelle-components
  18 , symlinkJoin
  19 , fetchhg
  20 }:
  21
  22 let
  23   sha1 = stdenv.mkDerivation {
  24     pname = "isabelle-sha1";
  25     version = "2024";
  26
  27     src = fetchhg {
  28       url = "https://isabelle.sketis.net/repos/sha1";
  29       rev = "0ce12663fe76";
  30       hash = "sha256-DB/ETVZhbT82IMZA97TmHG6gJcGpFavxDKDTwPzIF80=";
  31     };
  32
  33     buildPhase = (if stdenv.hostPlatform.isDarwin then ''
  34       LDFLAGS="-dynamic -undefined dynamic_lookup -lSystem"
  35     '' else ''
  36       LDFLAGS="-fPIC -shared"
  37     '') + ''
  38       CFLAGS="-fPIC -I."
  39       $CC $CFLAGS -c sha1.c -o sha1.o
  40       $LD $LDFLAGS sha1.o -o libsha1.so
  41     '';
  42
  43     installPhase = ''
  44       mkdir -p $out/lib
  45       cp libsha1.so $out/lib/
  46     '';
  47   };
  48 in stdenv.mkDerivation (finalAttrs: rec {
  49   pname = "isabelle";
  50   version = "2024";
  51
  52   dirname = "Isabelle${version}";
  53
  54   src =
  55     if stdenv.hostPlatform.isDarwin
  56     then
  57       fetchurl
  58         {
  59           url = "https://isabelle.in.tum.de/website-${dirname}/dist/${dirname}_macos.tar.gz";
  60           hash = "sha256-IgNfmW9x6h8DBj9vFEGV62oEl01NkW7QdyzXlWmii8c=";
  61         }
  62     else if stdenv.hostPlatform.isx86
  63     then
  64       fetchurl {
  65         url = "https://isabelle.in.tum.de/website-${dirname}/dist/${dirname}_linux.tar.gz";
  66         hash = "sha256-YDqq+KvqNll687BlHSwWKobAoN1EIHZvR+VyQDljkmc=";
  67       }
  68     else
  69       fetchurl {
  70         url = "https://isabelle.in.tum.de/website-${dirname}/dist/${dirname}_linux_arm.tar.gz";
  71         hash = "sha256-jXWVv18WwrVnqVX1s4Lnyf7DkOzPa3EdLXYxgtKD+YA=";
  72       };
  73
  74   nativeBuildInputs = [ java ];
  75
  76   buildInputs = [ polyml veriT vampire eprover-ho nettools ]
  77     ++ lib.optionals (!stdenv.hostPlatform.isDarwin) [ java procps ];
  78
  79   sourceRoot = "${dirname}${lib.optionalString stdenv.hostPlatform.isDarwin ".app"}";
  80
  81   doCheck = stdenv.hostPlatform.system != "aarch64-linux";
  82   checkPhase = "bin/isabelle build -v HOL-SMT_Examples";
  83
  84   postUnpack = lib.optionalString stdenv.hostPlatform.isDarwin ''
  85     mv $sourceRoot ${dirname}
  86     sourceRoot=${dirname}
  87   '';
  88
  89   postPatch = ''
  90     patchShebangs lib/Tools/ bin/
  91
  92     cat >contrib/verit-*/etc/settings <<EOF
  93       ISABELLE_VERIT=${veriT}/bin/veriT
  94     EOF
  95
  96     cat >contrib/e-*/etc/settings <<EOF
  97       E_HOME=${eprover-ho}/bin
  98       E_VERSION=${eprover-ho.version}
  99     EOF
 100
 101     cat >contrib/vampire-*/etc/settings <<EOF
 102       VAMPIRE_HOME=${vampire}/bin
 103       VAMPIRE_VERSION=${vampire.version}
 104       VAMPIRE_EXTRA_OPTIONS="--mode casc"
 105     EOF
 106
 107     cat >contrib/polyml-*/etc/settings <<EOF
 108       ML_SYSTEM_64=true
 109       ML_SYSTEM=${polyml.name}
 110       ML_PLATFORM=${stdenv.system}
 111       ML_HOME=${polyml}/bin
 112       ML_OPTIONS="--minheap 1000"
 113       POLYML_HOME="\$COMPONENT"
 114       ML_SOURCES="\$POLYML_HOME/src"
 115     EOF
 116
 117     cat >contrib/jdk*/etc/settings <<EOF
 118       ISABELLE_JAVA_PLATFORM=${stdenv.system}
 119       ISABELLE_JDK_HOME=${java}
 120     EOF
 121
 122   '' + lib.optionalString stdenv.hostPlatform.isx86 ''
 123     rm contrib/naproche-*/x86*/Naproche-SAD
 124     ln -s ${naproche}/bin/Naproche-SAD contrib/naproche-*/x86*/
 125   '' + ''
 126
 127     echo ISABELLE_LINE_EDITOR=${rlwrap}/bin/rlwrap >>etc/settings
 128
 129     for comp in contrib/jdk* contrib/polyml-* contrib/verit-* contrib/vampire-* contrib/e-*; do
 130       rm -rf $comp/${if stdenv.hostPlatform.isx86 then "x86" else "arm"}*
 131     done
 132
 133     substituteInPlace lib/Tools/env \
 134       --replace-fail /usr/bin/env ${coreutils}/bin/env
 135
 136     substituteInPlace src/Tools/Setup/src/Environment.java \
 137       --replace-fail 'cmd.add("/usr/bin/env");' "" \
 138       --replace-fail 'cmd.add("bash");' "cmd.add(\"$SHELL\");"
 139
 140     substituteInPlace src/Pure/General/sha1.ML \
 141       --replace-fail '"$ML_HOME/" ^ (if ML_System.platform_is_windows then "sha1.dll" else "libsha1.so")' '"${sha1}/lib/libsha1.so"'
 142
 143     rm -r heaps
 144   '' + lib.optionalString (stdenv.hostPlatform.system == "x86_64-darwin") ''
 145     substituteInPlace lib/scripts/isabelle-platform \
 146       --replace-fail 'ISABELLE_APPLE_PLATFORM64=arm64-darwin' ""
 147   '' + lib.optionalString stdenv.hostPlatform.isLinux ''
 148     arch=${if stdenv.hostPlatform.system == "aarch64-linux" then "arm64-linux" else stdenv.hostPlatform.system}
 149     for f in contrib/*/$arch/{z3,nunchaku,spass,zipperposition}; do
 150       patchelf --set-interpreter $(cat ${stdenv.cc}/nix-support/dynamic-linker) "$f"${lib.optionalString stdenv.hostPlatform.isAarch64 " || true"}
 151     done
 152     patchelf --set-interpreter $(cat ${stdenv.cc}/nix-support/dynamic-linker) contrib/bash_process-*/$arch/bash_process
 153     for d in contrib/kodkodi-*/jni/$arch; do
 154       patchelf --set-rpath "${lib.concatStringsSep ":" [ "${java}/lib/openjdk/lib/server" "${stdenv.cc.cc.lib}/lib" ]}" $d/*.so
 155     done
 156   '' + lib.optionalString (stdenv.hostPlatform.system == "x86_64-linux") ''
 157     patchelf --set-rpath "${stdenv.cc.cc.lib}/lib" contrib/z3-*/$arch/z3
 158   '';
 159
 160   buildPhase = ''
 161     export HOME=$TMP # The build fails if home is not set
 162     setup_name=$(basename contrib/isabelle_setup*)
 163
 164     #The following is adapted from https://isabelle.sketis.net/repos/isabelle/file/Isabelle2021-1/Admin/lib/Tools/build_setup
 165     TARGET_DIR="contrib/$setup_name/lib"
 166     rm -rf "$TARGET_DIR"
 167     mkdir -p "$TARGET_DIR/isabelle/setup"
 168     declare -a ARGS=("-Xlint:unchecked")
 169
 170     SOURCES="$(${perl}/bin/perl -e 'while (<>) { if (m/(\S+\.java)/)  { print "$1 "; } }' "src/Tools/Setup/etc/build.props")"
 171     for SRC in $SOURCES
 172     do
 173       ARGS["''${#ARGS[@]}"]="src/Tools/Setup/$SRC"
 174     done
 175     echo "Building isabelle setup"
 176     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[@]}"
 177     jar -c -f "$TARGET_DIR/isabelle_setup.jar" -e "isabelle.setup.Setup" -C "$TARGET_DIR" isabelle
 178     rm -rf "$TARGET_DIR/isabelle"
 179
 180     echo "Building HOL heap"
 181     bin/isabelle build -v -o system_heaps -b HOL
 182   '';
 183
 184   installPhase = ''
 185     mkdir -p $out/bin
 186     mv $TMP/$dirname $out
 187     cd $out/$dirname
 188     bin/isabelle install $out/bin
 189
 190     # icon
 191     mkdir -p "$out/share/icons/hicolor/isabelle/apps"
 192     cp "$out/Isabelle${version}/lib/icons/isabelle.xpm" "$out/share/icons/hicolor/isabelle/apps/"
 193
 194     # desktop item
 195     mkdir -p "$out/share"
 196     cp -r "${desktopItem}/share/applications" "$out/share/applications"
 197   '';
 198
 199   desktopItem = makeDesktopItem {
 200     name = "isabelle";
 201     exec = "isabelle jedit";
 202     icon = "isabelle";
 203     desktopName = "Isabelle";
 204     comment = meta.description;
 205     categories = [ "Education" "Science" "Math" ];
 206   };
 207
 208   meta = with lib; {
 209     description = "A generic proof assistant";
 210
 211     longDescription = ''
 212       Isabelle is a generic proof assistant.  It allows mathematical formulas
 213       to be expressed in a formal language and provides tools for proving those
 214       formulas in a logical calculus.
 215     '';
 216     homepage = "https://isabelle.in.tum.de/";
 217     sourceProvenance = with sourceTypes; [
 218       fromSource
 219       binaryNativeCode  # source bundles binary dependencies
 220     ];
 221     license = licenses.bsd3;
 222     maintainers = [ maintainers.jwiegley maintainers.jvanbruegge ];
 223     platforms = platforms.unix;
 224     broken = stdenv.hostPlatform.isDarwin;
 225   };
 226
 227   passthru.withComponents = f:
 228     let
 229       isabelle = finalAttrs.finalPackage;
 230       base = "$out/${isabelle.dirname}";
 231       components = f isabelle-components;
 232     in symlinkJoin {
 233       name = "isabelle-with-components-${isabelle.version}";
 234       paths = [ isabelle ] ++ (builtins.map (c: c.override { inherit isabelle; }) components);
 235
 236       postBuild = ''
 237         rm $out/bin/*
 238
 239         cd ${base}
 240         rm bin/*
 241         cp ${isabelle}/${isabelle.dirname}/bin/* bin/
 242         rm etc/components
 243         cat ${isabelle}/${isabelle.dirname}/etc/components > etc/components
 244
 245         export HOME=$TMP
 246         bin/isabelle install $out/bin
 247         patchShebangs $out/bin
 248       '' + lib.concatMapStringsSep "\n" (c: ''
 249         echo contrib/${c.pname}-${c.version} >> ${base}/etc/components
 250       '') components;
 251     };
 252 })