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
|
{
lib,
stdenv,
fetchFromGitHub,
jdk,
gradle_8,
jre,
makeWrapper,
makeDesktopItem,
copyDesktopItems,
testers,
z3,
cvc5,
key,
substitute,
}:
let
gradle = gradle_8;
in
stdenv.mkDerivation rec {
pname = "key";
version = "2.12.3";
src = fetchFromGitHub {
owner = "KeYProject";
repo = "key";
tag = "KEY-${version}";
hash = "sha256-1pN0lmr/teVitpMIM9M9lSTkmnVcZwdAQay2pzgJDCk=";
};
patches = [
# Remove linting framework, causes issues with the update script.
(substitute {
src = ./remove-eisop-checker.patch;
substitutions = [
"--subst-var-by"
"version"
version
];
})
];
nativeBuildInputs = [
jdk
gradle
makeWrapper
copyDesktopItems
];
desktopItems = [
(makeDesktopItem {
name = "KeY";
exec = meta.mainProgram;
icon = "key";
comment = meta.description;
desktopName = "KeY";
genericName = "KeY";
categories = [ "Science" ];
})
];
mitmCache = gradle.fetchDeps {
inherit pname;
data = ./deps.json;
};
__darwinAllowLocalNetworking = true;
# TODO: on update to 2.12.4+, try again
# (currently some tests are failing)
doCheck = false;
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 ${lib.getExe jre} $out/bin/KeY \
--prefix PATH : ${
lib.makeBinPath [
z3
cvc5
]
} \
--add-flags "-cp $out/share/java/KeY.jar de.uka.ilkd.key.core.Main"
runHook postInstall
'';
passthru.tests.version = testers.testVersion {
package = key;
command = "KeY --help";
};
meta = {
description = "Java formal verification tool";
homepage = "https://www.key-project.org"; # also https://formal.iti.kit.edu/key/
changelog = "https://keyproject.github.io/key-docs/changelog/";
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 = lib.licenses.gpl2Only;
maintainers = with lib.maintainers; [
fgaz
fliegendewurst
];
mainProgram = "KeY";
platforms = jdk.meta.platforms;
};
}
|
