diff options
author | Sandro <sandro.jaeckel@gmail.com> | 2022-12-03 00:45:47 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2022-12-03 00:45:47 +0100 |
commit | e461e83aa7a5f449e1d1d7c8e3f817004bdeedd2 (patch) | |
tree | a4acda63fc8b667071abcd8cf9201168c589b69c /pkgs/applications/science | |
parent | 76aad1f1e6e6ebf96d05b96e9c1f800094a26180 (diff) | |
parent | fa28ed48582cb30afdce232a3313bb6fe32644e4 (diff) |
Merge pull request #191966 from jvanbruegge/isabelle-2022
Diffstat (limited to 'pkgs/applications/science')
4 files changed, 61 insertions, 60 deletions
diff --git a/pkgs/applications/science/logic/isabelle/components/isabelle-linter.nix b/pkgs/applications/science/logic/isabelle/components/isabelle-linter.nix index 7fca547f67c8e..565537cf439c0 100644 --- a/pkgs/applications/science/logic/isabelle/components/isabelle-linter.nix +++ b/pkgs/applications/science/logic/isabelle/components/isabelle-linter.nix @@ -2,16 +2,28 @@ stdenv.mkDerivation rec { pname = "isabelle-linter"; - version = "Isabelle2021-1-v1.0.0"; + version = "unstable-2022-09-05"; src = fetchFromGitHub { owner = "isabelle-prover"; repo = "isabelle-linter"; - rev = version; - sha256 = "0v6scc2rhj6bjv530gzz6i57czzcgpkw7a9iqnfdnm5gvs5qjk7a"; + rev = "0424fc05426d5f7a23adf19ad08c690c17184e86"; + sha256 = "02afbgmi195ibichjkpni2wjgjkszv7i6qkmmprwrmb4jd2wdvd5"; }; - installPhase = import ./mkBuild.nix { inherit isabelle; path = "${pname}-${version}"; }; + nativeBuildInputs = [ isabelle ]; + + buildPhase = '' + export HOME=$TMP + isabelle components -u $(pwd) + isabelle scala_build + ''; + + installPhase = '' + dir=$out/Isabelle${isabelle.version}/contrib/${pname}-${version} + mkdir -p $dir + cp -r * $dir/ + ''; meta = with lib; { description = "Linter component for Isabelle."; diff --git a/pkgs/applications/science/logic/isabelle/components/mkBuild.nix b/pkgs/applications/science/logic/isabelle/components/mkBuild.nix deleted file mode 100644 index a05b5196b0076..0000000000000 --- a/pkgs/applications/science/logic/isabelle/components/mkBuild.nix +++ /dev/null @@ -1,36 +0,0 @@ -{ isabelle, path }: - -let - dir = "$out/isabelle/${isabelle.dirname}"; - iDir = "${isabelle}/${isabelle.dirname}"; -in '' - shopt -s extglob - mkdir -p ${dir}/lib/classes - - cDir=$out/${isabelle.dirname}/contrib/${path} - mkdir -p $cDir - cp -r !(isabelle) $cDir - - cd ${dir} - ln -s ${iDir}/!(lib|bin) ./ - ln -s ${iDir}/lib/!(classes) lib/ - ln -s ${iDir}/lib/classes/* lib/classes/ - - mkdir bin/ - cp ${iDir}/bin/* bin/ - - export HOME=$TMP - bin/isabelle components -u $cDir - bin/isabelle scala_build - - cd lib/classes - for f in ${iDir}/lib/classes/*; do - rm $(basename $f) - done - - lDir=$out/${isabelle.dirname}/lib/classes/ - mkdir -p $lDir - cp -r * $lDir - cd $out - rm -rf isabelle -'' diff --git a/pkgs/applications/science/logic/isabelle/default.nix b/pkgs/applications/science/logic/isabelle/default.nix index 009af3463a25a..1bb7ede6da7b7 100644 --- a/pkgs/applications/science/logic/isabelle/default.nix +++ b/pkgs/applications/science/logic/isabelle/default.nix @@ -1,5 +1,24 @@ -{ 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 { @@ -29,7 +48,7 @@ let }; in stdenv.mkDerivation rec { pname = "isabelle"; - version = "2021-1"; + version = "2022"; dirname = "Isabelle${version}"; @@ -39,26 +58,27 @@ in stdenv.mkDerivation rec { 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} @@ -111,7 +131,8 @@ in stdenv.mkDerivation rec { 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"' @@ -120,15 +141,18 @@ in stdenv.mkDerivation rec { '' + 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 @@ -145,11 +169,12 @@ in stdenv.mkDerivation rec { 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 ''; diff --git a/pkgs/applications/science/logic/naproche/default.nix b/pkgs/applications/science/logic/naproche/default.nix index 047ed73262eee..ecc347080081b 100644 --- a/pkgs/applications/science/logic/naproche/default.nix +++ b/pkgs/applications/science/logic/naproche/default.nix @@ -2,13 +2,13 @@ with haskellPackages; mkDerivation { pname = "Naproche-SAD"; - version = "2022-04-19"; + version = "2022-10-24"; src = fetchFromGitHub { owner = "naproche"; repo = "naproche"; - rev = "2514c04e715395b7a839e11b63046eafb9c6a1da"; - sha256 = "1bdgyk4fk65xi7n778rbgddpg4zhggj8wjslxbizrzi81my9a3vm"; + rev = "c8c4ca2d5fdb92bf17e0e54c99bd2a9691255d80"; + sha256 = "0xvh6kkl5k5ygp2nrbq3k0snvzczbmcp1yrwdkah3fzhf9i3yykx"; }; isExecutable = true; |