tjh.dev
1{
2 lib,
3 stdenv,
4 fetchFromGitHub,
5 jdk,
6 gradle_8,
7 jre,
8 makeWrapper,
9 makeDesktopItem,
10 copyDesktopItems,
11 testers,
12 z3,
13 cvc5,
14 key,
15 substitute,
16}:
17
18let
19 gradle = gradle_8;
20
21in
22stdenv.mkDerivation rec {
23 pname = "key";
24 version = "2.12.3";
25 src = fetchFromGitHub {
26 owner = "KeYProject";
27 repo = "key";
28 tag = "KEY-${version}";
29 hash = "sha256-1pN0lmr/teVitpMIM9M9lSTkmnVcZwdAQay2pzgJDCk=";
30 };
31
32 patches = [
33 # Remove linting framework, causes issues with the update script.
34 (substitute {
35 src = ./remove-eisop-checker.patch;
36 substitutions = [
37 "--subst-var-by"
38 "version"
39 version
40 ];
41 })
42 ];
43
44 nativeBuildInputs = [
45 jdk
46 gradle
47 makeWrapper
48 copyDesktopItems
49 ];
50
51 desktopItems = [
52 (makeDesktopItem {
53 name = "KeY";
54 exec = meta.mainProgram;
55 icon = "key";
56 comment = meta.description;
57 desktopName = "KeY";
58 genericName = "KeY";
59 categories = [ "Science" ];
60 })
61 ];
62
63 mitmCache = gradle.fetchDeps {
64 inherit pname;
65 data = ./deps.json;
66 };
67
68 __darwinAllowLocalNetworking = true;
69
70 # TODO: on update to 2.12.4+, try again
71 # (currently some tests are failing)
72 doCheck = false;
73
74 installPhase = ''
75 runHook preInstall
76
77 mkdir -p $out/share/java
78 cp key.ui/build/libs/key-*-exe.jar $out/share/java/KeY.jar
79 mkdir -p $out/bin
80 mkdir -p $out/share/icons/hicolor/256x256/apps
81 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
82 makeWrapper ${lib.getExe jre} $out/bin/KeY \
83 --prefix PATH : ${
84 lib.makeBinPath [
85 z3
86 cvc5
87 ]
88 } \
89 --add-flags "-cp $out/share/java/KeY.jar de.uka.ilkd.key.core.Main"
90
91 runHook postInstall
92 '';
93
94 passthru.tests.version = testers.testVersion {
95 package = key;
96 command = "KeY --help";
97 };
98
99 meta = {
100 description = "Java formal verification tool";
101 homepage = "https://www.key-project.org"; # also https://formal.iti.kit.edu/key/
102 changelog = "https://keyproject.github.io/key-docs/changelog/";
103 longDescription = ''
104 The KeY System is a formal software development tool that aims to
105 integrate design, implementation, formal specification, and formal
106 verification of object-oriented software as seamlessly as possible.
107 At the core of the system is a novel theorem prover for the first-order
108 Dynamic Logic for Java with a user-friendly graphical interface.
109 '';
110 license = lib.licenses.gpl2Only;
111 maintainers = with lib.maintainers; [
112 fgaz
113 fliegendewurst
114 ];
115 mainProgram = "KeY";
116 platforms = jdk.meta.platforms;
117 };
118}