b12f/nixpkgs
1
0
Fork 0
Code Issues Pull requests Packages Projects Releases Wiki Activity

Merge pull request #157629 from 1000teslas/isabelle

Browse source 
isabelle: make closer to upstream
This commit is contained in:
Sandro 2022-04-20 19:46:16 +02:00 committed by GitHub
parent b9e4383b0a 9aa4c5dbfc
commit 0311a5a0af
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 49 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

33
pkgs/applications/science/logic/isabelle/default.nix
View file

@ -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"}

20
pkgs/top-level/all-packages.nix
View file

@ -32986,12 +32986,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 { });