1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
|
{ lib, stdenv
, fetchurl
, jdk
, gradle_7
, perl
, jre
, makeWrapper
, makeDesktopItem
, copyDesktopItems
, testVersion
, key
}:
let
pname = "key";
version = "2.10.0";
src = fetchurl {
url = "https://www.key-project.org/dist/${version}/key-${version}-sources.tgz";
sha256 = "1f201cbcflqd1z6ysrkh3mff5agspw3v74ybdc3s2lfdyz3b858w";
};
sourceRoot = "key-${version}/key";
# fake build to pre-download deps into fixed-output derivation
deps = stdenv.mkDerivation {
pname = "${pname}-deps";
inherit version src sourceRoot;
nativeBuildInputs = [ gradle_7 perl ];
buildPhase = ''
export GRADLE_USER_HOME=$(mktemp -d)
# https://github.com/gradle/gradle/issues/4426
${lib.optionalString stdenv.isDarwin "export TERM=dumb"}
gradle --no-daemon classes testClasses
'';
# perl code mavenizes pathes (com.squareup.okio/okio/1.13.0/a9283170b7305c8d92d25aff02a6ab7e45d06cbe/okio-1.13.0.jar -> com/squareup/okio/okio/1.13.0/okio-1.13.0.jar)
installPhase = ''
find $GRADLE_USER_HOME/caches/modules-2 -type f -regex '.*\.\(jar\|pom\)' \
| perl -pe 's#(.*/([^/]+)/([^/]+)/([^/]+)/[0-9a-f]{30,40}/([^/\s]+))$# ($x = $2) =~ tr|\.|/|; "install -Dm444 $1 \$out/$x/$3/$4/$5" #e' \
| sh
'';
outputHashMode = "recursive";
outputHashAlgo = "sha256";
outputHash = "sha256-GjBUwJxeyJA6vGrPQVtNpcHb4CJlNlY4kHt1PT21xjo=";
};
in stdenv.mkDerivation rec {
inherit pname version src sourceRoot;
nativeBuildInputs = [
jdk
gradle_7
makeWrapper
copyDesktopItems
];
executable-name = "KeY";
desktopItems = [
(makeDesktopItem {
name = "KeY";
exec = executable-name;
icon = "key";
comment = meta.description;
desktopName = "KeY";
genericName = "KeY";
categories = [ "Science" ];
})
];
# disable tests (broken on darwin)
gradleAction = if stdenv.isDarwin then "assemble" else "build";
buildPhase = ''
runHook preBuild
export GRADLE_USER_HOME=$(mktemp -d)
# https://github.com/gradle/gradle/issues/4426
${lib.optionalString stdenv.isDarwin "export TERM=dumb"}
# point to offline repo
sed -ie "s#repositories {#repositories { maven { url '${deps}' }#g" build.gradle
cat <(echo "pluginManagement { repositories { maven { url '${deps}' } } }") settings.gradle > settings_new.gradle
mv settings_new.gradle settings.gradle
gradle --offline --no-daemon ${gradleAction}
runHook postBuild
'';
installPhase = ''
runHook preInstall
mkdir -p $out/share/java
cp key.ui/build/libs/key-*-exe.jar $out/share/java/KeY.jar
mkdir -p $out/bin
mkdir -p $out/share/icons/hicolor/256x256/apps
cp key.ui/src/main/resources/de/uka/ilkd/key/gui/images/key-color-icon-square.png $out/share/icons/hicolor/256x256/apps/key.png
makeWrapper ${jre}/bin/java $out/bin/KeY \
--add-flags "-cp $out/share/java/KeY.jar de.uka.ilkd.key.core.Main"
runHook postInstall
'';
passthru.tests.version =
testVersion {
package = key;
command = "KeY --help";
};
meta = with lib; {
description = "Java formal verification tool";
homepage = "https://www.key-project.org"; # also https://formal.iti.kit.edu/key/
longDescription = ''
The KeY System is a formal software development tool that aims to
integrate design, implementation, formal specification, and formal
verification of object-oriented software as seamlessly as possible.
At the core of the system is a novel theorem prover for the first-order
Dynamic Logic for Java with a user-friendly graphical interface.
'';
license = licenses.gpl2;
maintainers = with maintainers; [ fgaz ];
platforms = platforms.all;
};
}
|