git.iko.soy/typeable/nixpkgs
on master help sign in
Merge pull request #159997 from jvanbruegge/isabelle-linter
commitf338d0737c08196cd7e2930b5cb0a906e76b47c5 authorSandro <sandro.jaeckel@gmail.com> dateSat 26 Mar 2022, 15:58 (5 years ago) parent83770140391279
5 files changed+90−1
compare with master
unifiedsplit
pkgs/applications/science/logic/isabelle/components/default.nix+5 pkgs/applications/science/logic/isabelle/components/isabelle-linter.nix+22 pkgs/applications/science/logic/isabelle/components/mkBuild.nix+36 pkgs/applications/science/logic/isabelle/default.nix+26−1 pkgs/top-level/all-packages.nix+1
pkgs/applications/science/logic/isabelle/components/default.nixnew file+5
@@ -0,0 +1,5 @@
1+{ callPackage }:
2+
3+{
4+ isabelle-linter = callPackage ./isabelle-linter.nix {};
5+}
pkgs/applications/science/logic/isabelle/components/isabelle-linter.nixnew file+22
@@ -0,0 +1,22 @@
1+{ stdenv, lib, fetchFromGitHub, isabelle }:
2+
3+stdenv.mkDerivation rec {
4+ pname = "isabelle-linter";
5+ version = "Isabelle2021-1-v1.0.0";
6+
7+ src = fetchFromGitHub {
8+ owner = "isabelle-prover";
9+ repo = "isabelle-linter";
10+ rev = version;
11+ sha256 = "0v6scc2rhj6bjv530gzz6i57czzcgpkw7a9iqnfdnm5gvs5qjk7a";
12+ };
13+
14+ installPhase = import ./mkBuild.nix { inherit isabelle; path = "${pname}-${version}"; };
15+
16+ meta = with lib; {
17+ description = "Linter component for Isabelle.";
18+ homepage = "https://github.com/isabelle-prover/isabelle-linter";
19+ maintainers = with maintainers; [ jvanbruegge ];
20+ license = licenses.mit;
21+ };
22+}
pkgs/applications/science/logic/isabelle/components/mkBuild.nixnew file+36
@@ -0,0 +1,36 @@
1+{ isabelle, path }:
2+
3+let
4+ dir = "$out/isabelle/${isabelle.dirname}";
5+ iDir = "${isabelle}/${isabelle.dirname}";
6+in ''
7+ shopt -s extglob
8+ mkdir -p ${dir}/lib/classes
9+
10+ cDir=$out/${isabelle.dirname}/contrib/${path}
11+ mkdir -p $cDir
12+ cp -r !(isabelle) $cDir
13+
14+ cd ${dir}
15+ ln -s ${iDir}/!(lib|bin) ./
16+ ln -s ${iDir}/lib/!(classes) lib/
17+ ln -s ${iDir}/lib/classes/* lib/classes/
18+
19+ mkdir bin/
20+ cp ${iDir}/bin/* bin/
21+
22+ export HOME=$TMP
23+ bin/isabelle components -u $cDir
24+ bin/isabelle scala_build
25+
26+ cd lib/classes
27+ for f in ${iDir}/lib/classes/*; do
28+ rm $(basename $f)
29+ done
30+
31+ lDir=$out/${isabelle.dirname}/lib/classes/
32+ mkdir -p $lDir
33+ cp -r * $lDir
34+ cd $out
35+ rm -rf isabelle
36+''
pkgs/applications/science/logic/isabelle/default.nix+26−1
@@ -1,4 +1,4 @@
1−{ lib, stdenv, fetchurl, coreutils, nettools, java, scala, polyml, z3, veriT, vampire, eprover-ho, naproche, rlwrap, perl, makeDesktopItem }:
1+{ lib, stdenv, fetchurl, coreutils, nettools, java, scala, polyml, z3, veriT, vampire, eprover-ho, naproche, rlwrap, perl, makeDesktopItem, isabelle-components, isabelle, symlinkJoin }:
22# nettools needed for hostname
33
44stdenv.mkDerivation rec {
@@ -153,4 +153,29 @@ stdenv.mkDerivation rec {
153153 maintainers = [ maintainers.jwiegley maintainers.jvanbruegge ];
154154 platforms = platforms.linux;
155155 };
156+} // {
157+ withComponents = f:
158+ let
159+ base = "$out/${isabelle.dirname}";
160+ components = f isabelle-components;
161+ in symlinkJoin {
162+ name = "isabelle-with-components-${isabelle.version}";
163+ paths = [ isabelle ] ++ components;
164+
165+ postBuild = ''
166+ rm $out/bin/*
167+
168+ cd ${base}
169+ rm bin/*
170+ cp ${isabelle}/${isabelle.dirname}/bin/* bin/
171+ rm etc/components
172+ cat ${isabelle}/${isabelle.dirname}/etc/components > etc/components
173+
174+ export HOME=$TMP
175+ bin/isabelle install $out/bin
176+ patchShebangs $out/bin
177+ '' + lib.concatMapStringsSep "\n" (c: ''
178+ echo contrib/${c.pname}-${c.version} >> ${base}/etc/components
179+ '') components;
180+ };
156181}
pkgs/top-level/all-packages.nix+1
@@ -32733,6 +32733,7 @@ with pkgs;
3273332733 java = openjdk17;
3273432734 z3 = z3_4_4_0;
3273532735 };
32736+ isabelle-components = recurseIntoAttrs (callPackage ../applications/science/logic/isabelle/components { });
3273632737
3273732738 iprover = callPackage ../applications/science/logic/iprover { };
3273832739