@@ -1,20 +1,20 @@
1−{ lib, stdenv, fetchurl, perl, perlPackages, makeWrapper, nettools, java, polyml, z3, rlwrap }:
1+{ lib, stdenv, fetchurl, perl, perlPackages, makeWrapper, nettools, java, polyml, z3, rlwrap, makeDesktopItem }:
22# nettools needed for hostname
33
44stdenv.mkDerivation rec {
55 pname = "isabelle";
6− version = "2020";
6+ version = "2021";
77
88 dirname = "Isabelle${version}";
99
1010 src = if stdenv.isDarwin
1111 then fetchurl {
1212 url = "https://isabelle.in.tum.de/website-${dirname}/dist/${dirname}_macos.tar.gz";
13− sha256 = "1sfr5filsaqj93g5y4p9n8g5652dhr4whj25x4lifdxr2pp560xx";
13+ sha256 = "1c2qm2ksmpyxyccyyn4lyj2wqj5m74nz2i0c5abrd1hj45zcnh1m";
1414 }
1515 else fetchurl {
1616 url = "https://isabelle.in.tum.de/website-${dirname}/dist/${dirname}_linux.tar.gz";
17− sha256 = "1bibabhlsvf6qsjjkgxcpq3cvl1z7r8yfcgqbhbvsiv69n3gyfk3";
17+ sha256 = "1isgc9w4q95638dcag9gxz1kmf97pkin3jz1dm2lhd64b2k12y2x";
1818 };
1919
2020 nativeBuildInputs = [ makeWrapper ];
@@ -48,6 +48,8 @@ stdenv.mkDerivation rec {
4848 ISABELLE_JDK_HOME=${java}
4949 EOF
5050
51+ sed -i -e 's/naproche_server : bool = true/naproche_server : bool = false/' contrib/naproche-*/etc/options
52+
5153 echo ISABELLE_LINE_EDITOR=${rlwrap}/bin/rlwrap >>etc/settings
5254
5355 for comp in contrib/jdk* contrib/polyml-* contrib/z3-*; do
@@ -66,9 +68,26 @@ stdenv.mkDerivation rec {
6668 cd $out/$dirname
6769 bin/isabelle install $out/bin
6870
71+ # icon
72+ mkdir -p "$out/share/icons/hicolor/isabelle/apps"
73+ cp "$out/Isabelle${version}/lib/icons/isabelle.xpm" "$out/share/icons/hicolor/isabelle/apps/"
74+
75+ # desktop item
76+ mkdir -p "$out/share"
77+ cp -r "${desktopItem}/share/applications" "$out/share/applications"
78+
6979 wrapProgram $out/$dirname/src/HOL/Tools/ATP/scripts/remote_atp --set PERL5LIB ${perlPackages.makeFullPerlPath [ perlPackages.LWP ]}
7080 '';
7181
82+ desktopItem = makeDesktopItem {
83+ name = "isabelle";
84+ exec = "isabelle jedit";
85+ icon = "isabelle";
86+ desktopName = "Isabelle";
87+ comment = meta.description;
88+ categories = "Education;Science;Math;";
89+ };
90+
7291 meta = with lib; {
7392 description = "A generic proof assistant";
7493