mirror of
https://github.com/ilyakooo0/nixpkgs.git
synced 2024-09-21 04:28:40 +03:00
Merge pull request #191966 from jvanbruegge/isabelle-2022
This commit is contained in:
commit
e461e83aa7
@ -2,16 +2,28 @@
|
|||||||
|
|
||||||
stdenv.mkDerivation rec {
|
stdenv.mkDerivation rec {
|
||||||
pname = "isabelle-linter";
|
pname = "isabelle-linter";
|
||||||
version = "Isabelle2021-1-v1.0.0";
|
version = "unstable-2022-09-05";
|
||||||
|
|
||||||
src = fetchFromGitHub {
|
src = fetchFromGitHub {
|
||||||
owner = "isabelle-prover";
|
owner = "isabelle-prover";
|
||||||
repo = "isabelle-linter";
|
repo = "isabelle-linter";
|
||||||
rev = version;
|
rev = "0424fc05426d5f7a23adf19ad08c690c17184e86";
|
||||||
sha256 = "0v6scc2rhj6bjv530gzz6i57czzcgpkw7a9iqnfdnm5gvs5qjk7a";
|
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; {
|
meta = with lib; {
|
||||||
description = "Linter component for Isabelle.";
|
description = "Linter component for Isabelle.";
|
||||||
|
@ -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
|
|
||||||
''
|
|
@ -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 }:
|
{ lib
|
||||||
# nettools needed for hostname
|
, stdenv
|
||||||
|
, fetchurl
|
||||||
|
, coreutils
|
||||||
|
, nettools
|
||||||
|
, java
|
||||||
|
, scala_3
|
||||||
|
, polyml
|
||||||
|
, z3
|
||||||
|
, veriT
|
||||||
|
, vampire
|
||||||
|
, eprover-ho
|
||||||
|
, naproche
|
||||||
|
, rlwrap
|
||||||
|
, perl
|
||||||
|
, makeDesktopItem
|
||||||
|
, isabelle-components
|
||||||
|
, isabelle
|
||||||
|
, symlinkJoin
|
||||||
|
, fetchhg
|
||||||
|
}:
|
||||||
|
|
||||||
let
|
let
|
||||||
sha1 = stdenv.mkDerivation {
|
sha1 = stdenv.mkDerivation {
|
||||||
@ -29,7 +48,7 @@ let
|
|||||||
};
|
};
|
||||||
in stdenv.mkDerivation rec {
|
in stdenv.mkDerivation rec {
|
||||||
pname = "isabelle";
|
pname = "isabelle";
|
||||||
version = "2021-1";
|
version = "2022";
|
||||||
|
|
||||||
dirname = "Isabelle${version}";
|
dirname = "Isabelle${version}";
|
||||||
|
|
||||||
@ -39,26 +58,27 @@ in stdenv.mkDerivation rec {
|
|||||||
fetchurl
|
fetchurl
|
||||||
{
|
{
|
||||||
url = "https://isabelle.in.tum.de/website-${dirname}/dist/${dirname}_macos.tar.gz";
|
url = "https://isabelle.in.tum.de/website-${dirname}/dist/${dirname}_macos.tar.gz";
|
||||||
sha256 = "0n1ls9vwf0ps1x8zpb7c1xz1wkasgvc34h5bz280hy2z6iqwmwbc";
|
sha256 = "0b84rx9b7b5y8m1sg7xdp17j6yngd2dkx6v5bkd8h7ly102lai18";
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
fetchurl {
|
fetchurl {
|
||||||
url = "https://isabelle.in.tum.de/website-${dirname}/dist/${dirname}_linux.tar.gz";
|
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 ]
|
buildInputs = [ polyml z3 veriT vampire eprover-ho nettools ]
|
||||||
++ lib.optionals (!stdenv.isDarwin) [ java ];
|
++ lib.optionals (!stdenv.isDarwin) [ java ];
|
||||||
|
|
||||||
sourceRoot = "${dirname}${lib.optionalString stdenv.isDarwin ".app"}";
|
sourceRoot = dirname;
|
||||||
|
|
||||||
postUnpack = if stdenv.isDarwin then ''
|
postUnpack = lib.optionalString stdenv.isDarwin ''
|
||||||
mv $sourceRoot ${dirname}
|
mv $sourceRoot.app $sourceRoot
|
||||||
sourceRoot=${dirname}
|
'';
|
||||||
'' else null;
|
|
||||||
|
|
||||||
postPatch = ''
|
postPatch = ''
|
||||||
patchShebangs .
|
patchShebangs lib/Tools/ bin/
|
||||||
|
|
||||||
cat >contrib/z3*/etc/settings <<EOF
|
cat >contrib/z3*/etc/settings <<EOF
|
||||||
Z3_HOME=${z3}
|
Z3_HOME=${z3}
|
||||||
@ -111,7 +131,8 @@ in stdenv.mkDerivation rec {
|
|||||||
|
|
||||||
substituteInPlace src/Tools/Setup/src/Environment.java \
|
substituteInPlace src/Tools/Setup/src/Environment.java \
|
||||||
--replace 'cmd.add("/usr/bin/env");' "" \
|
--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 \
|
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"'
|
--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") ''
|
'' + lib.optionalString (stdenv.hostPlatform.system == "x86_64-darwin") ''
|
||||||
substituteInPlace lib/scripts/isabelle-platform \
|
substituteInPlace lib/scripts/isabelle-platform \
|
||||||
--replace 'ISABELLE_APPLE_PLATFORM64=arm64-darwin' ""
|
--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"}
|
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
|
for f in contrib/*/$arch/{bash_process,epclextract,nunchaku,SPASS,zipperposition}; do
|
||||||
patchelf --set-interpreter $(cat ${stdenv.cc}/nix-support/dynamic-linker) "$f"
|
patchelf --set-interpreter $(cat ${stdenv.cc}/nix-support/dynamic-linker) "$f"
|
||||||
done
|
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
|
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
|
patchelf --set-rpath "${lib.concatStringsSep ":" [ "${java}/lib/openjdk/lib/server" "${stdenv.cc.cc.lib}/lib" ]}" $d/*.so
|
||||||
done
|
done
|
||||||
'');
|
'';
|
||||||
|
|
||||||
buildPhase = ''
|
buildPhase = ''
|
||||||
export HOME=$TMP # The build fails if home is not set
|
export HOME=$TMP # The build fails if home is not set
|
||||||
@ -145,11 +169,12 @@ in stdenv.mkDerivation rec {
|
|||||||
do
|
do
|
||||||
ARGS["''${#ARGS[@]}"]="src/Tools/Setup/$SRC"
|
ARGS["''${#ARGS[@]}"]="src/Tools/Setup/$SRC"
|
||||||
done
|
done
|
||||||
${java}/bin/javac -d "$TARGET_DIR" -classpath ${scala}/lib/scala-compiler.jar "''${ARGS[@]}"
|
echo "Building isabelle setup"
|
||||||
${java}/bin/jar -c -f "$TARGET_DIR/isabelle_setup.jar" -e "isabelle.setup.Setup" -C "$TARGET_DIR" isabelle
|
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"
|
rm -rf "$TARGET_DIR/isabelle"
|
||||||
|
|
||||||
# Prebuild HOL Session
|
echo "Building HOL heap"
|
||||||
bin/isabelle build -v -o system_heaps -b HOL
|
bin/isabelle build -v -o system_heaps -b HOL
|
||||||
'';
|
'';
|
||||||
|
|
||||||
|
@ -2,13 +2,13 @@
|
|||||||
|
|
||||||
with haskellPackages; mkDerivation {
|
with haskellPackages; mkDerivation {
|
||||||
pname = "Naproche-SAD";
|
pname = "Naproche-SAD";
|
||||||
version = "2022-04-19";
|
version = "2022-10-24";
|
||||||
|
|
||||||
src = fetchFromGitHub {
|
src = fetchFromGitHub {
|
||||||
owner = "naproche";
|
owner = "naproche";
|
||||||
repo = "naproche";
|
repo = "naproche";
|
||||||
rev = "2514c04e715395b7a839e11b63046eafb9c6a1da";
|
rev = "c8c4ca2d5fdb92bf17e0e54c99bd2a9691255d80";
|
||||||
sha256 = "1bdgyk4fk65xi7n778rbgddpg4zhggj8wjslxbizrzi81my9a3vm";
|
sha256 = "0xvh6kkl5k5ygp2nrbq3k0snvzczbmcp1yrwdkah3fzhf9i3yykx";
|
||||||
};
|
};
|
||||||
|
|
||||||
isExecutable = true;
|
isExecutable = true;
|
||||||
|
@ -21,4 +21,4 @@ stdenv.mkDerivation {
|
|||||||
'';
|
'';
|
||||||
|
|
||||||
inherit (bare) meta;
|
inherit (bare) meta;
|
||||||
}
|
} // { inherit bare; }
|
||||||
|
@ -35936,14 +35936,14 @@ with pkgs;
|
|||||||
isabelle = callPackage ../applications/science/logic/isabelle {
|
isabelle = callPackage ../applications/science/logic/isabelle {
|
||||||
polyml = polyml.overrideAttrs (_: {
|
polyml = polyml.overrideAttrs (_: {
|
||||||
pname = "polyml-for-isabelle";
|
pname = "polyml-for-isabelle";
|
||||||
version = "2021-1";
|
version = "2022";
|
||||||
configureFlags = [ "--enable-intinf-as-int" "--with-gmp" "--disable-shared" ];
|
configureFlags = [ "--enable-intinf-as-int" "--with-gmp" "--disable-shared" ];
|
||||||
buildFlags = [ "compiler" ];
|
buildFlags = [ "compiler" ];
|
||||||
src = fetchFromGitHub {
|
src = fetchFromGitHub {
|
||||||
owner = "polyml";
|
owner = "polyml";
|
||||||
repo = "polyml";
|
repo = "polyml";
|
||||||
rev = "39d96a2def903ed019c6855e3b688df5070d633a";
|
rev = "bafe319bc3a65bf63bd98a4721a6f4dd9e0eabd6";
|
||||||
sha256 = "sha256-S7d2Vr/nB+rCX9d4qQj4f7edVZKocKIjc5rrx9A/B4Q=";
|
sha256 = "1ygs09zzq8icq1gc8qf4sb24lxx7sbcyd5hw3vw67a3ryaki0qw2";
|
||||||
};
|
};
|
||||||
});
|
});
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user