isabelle: Make closer to upstream
This makes isabelle use the versions of polyml and z3 that are also used upstream. Additionally it packages the sha1 library that isabelle uses. Co-authored-by: 1000teslas <47207223+1000teslas@users.noreply.github.com>
This commit is contained in:
parent
87da0aaf8d
commit
9aa4c5dbfc
|
@ -1,7 +1,33 @@
|
|||
{ lib, stdenv, fetchurl, coreutils, nettools, java, scala, polyml, z3, veriT, vampire, eprover-ho, naproche, rlwrap, perl, makeDesktopItem, isabelle-components, isabelle, symlinkJoin }:
|
||||
{ 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
|
||||
|
||||
stdenv.mkDerivation rec {
|
||||
let
|
||||
sha1 = stdenv.mkDerivation {
|
||||
pname = "isabelle-sha1";
|
||||
version = "2021-1";
|
||||
|
||||
src = fetchhg {
|
||||
url = "https://isabelle.sketis.net/repos/sha1";
|
||||
rev = "e0239faa6f42";
|
||||
sha256 = "sha256-4sxHzU/ixMAkSo67FiE6/ZqWJq9Nb9OMNhMoXH2bEy4=";
|
||||
};
|
||||
|
||||
buildPhase = (if stdenv.isDarwin then ''
|
||||
LDFLAGS="-dynamic -undefined dynamic_lookup -lSystem"
|
||||
'' else ''
|
||||
LDFLAGS="-fPIC -shared"
|
||||
'') + ''
|
||||
CFLAGS="-fPIC -I."
|
||||
$CC $CFLAGS -c sha1.c -o sha1.o
|
||||
$LD $LDFLAGS sha1.o -o libsha1.so
|
||||
'';
|
||||
|
||||
installPhase = ''
|
||||
mkdir -p $out/lib
|
||||
cp libsha1.so $out/lib/
|
||||
'';
|
||||
};
|
||||
in stdenv.mkDerivation rec {
|
||||
pname = "isabelle";
|
||||
version = "2021-1";
|
||||
|
||||
|
@ -82,6 +108,9 @@ stdenv.mkDerivation rec {
|
|||
--replace 'cmd.add("/usr/bin/env");' "" \
|
||||
--replace 'cmd.add("bash");' "cmd.add(\"$SHELL\");"
|
||||
|
||||
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"'
|
||||
|
||||
rm -r heaps
|
||||
'' + (if ! stdenv.isLinux then "" else ''
|
||||
arch=${if stdenv.hostPlatform.system == "x86_64-linux" then "x86_64-linux" else "x86-linux"}
|
||||
|
|
|
@ -32975,12 +32975,28 @@ with pkgs;
|
|||
ifstat-legacy = callPackage ../tools/networking/ifstat-legacy { };
|
||||
|
||||
isabelle = callPackage ../applications/science/logic/isabelle {
|
||||
polyml = lib.overrideDerivation polyml (_: {
|
||||
polyml = polyml.overrideAttrs (_: {
|
||||
pname = "polyml-for-isabelle";
|
||||
version = "2021-1";
|
||||
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=";
|
||||
};
|
||||
});
|
||||
|
||||
java = openjdk17;
|
||||
z3 = z3_4_4_0;
|
||||
z3 = z3_4_4_0.overrideAttrs (_: {
|
||||
src = fetchFromGitHub {
|
||||
owner = "Z3Prover";
|
||||
repo = "z3";
|
||||
rev = "0482e7fe727c75e259ac55a932b28cf1842c530e";
|
||||
sha256 = "1m53avlljxqd2p8w266ksmjywjycsd23h224yn786qsnf36dr63x";
|
||||
};
|
||||
});
|
||||
};
|
||||
isabelle-components = recurseIntoAttrs (callPackage ../applications/science/logic/isabelle/components { });
|
||||
|
||||
|
|
Loading…
Reference in a new issue