tjh.dev
1{
2 lib,
3 stdenv,
4 fetchurl,
5 fetchpatch,
6 pkg-config,
7 smlnj,
8 rsync,
9}:
10
11stdenv.mkDerivation rec {
12 pname = "twelf";
13 version = "1.7.1";
14
15 src = fetchurl {
16 url = "http://twelf.plparty.org/releases/twelf-src-${version}.tar.gz";
17 sha256 = "0fi1kbs9hrdrm1x4k13angpjasxlyd1gc3ys8ah54i75qbcd9c4i";
18 };
19
20 patches = [
21 # Fix Emacs old-style backquotes: https://github.com/standardml/twelf/pull/3
22 (fetchpatch {
23 url = "https://github.com/standardml/twelf/commit/7b3f3dbb8b8ec8d16d843875fce1e2bd6a50e3ae.patch";
24 hash = "sha256-cSrgQFRPL+4zRtFXv3rLsAasjLfal0TZpXasEUtUSHc=";
25 })
26 ];
27
28 nativeBuildInputs = [ pkg-config ];
29 buildInputs = [
30 smlnj
31 rsync
32 ];
33
34 buildPhase = ''
35 export SMLNJ_HOME=${smlnj}
36 make smlnj
37 '';
38
39 installPhase = ''
40 mkdir -p $out/bin
41 rsync -av bin/{*,.heap} $out/bin/
42 bin/.mkexec ${smlnj}/bin/sml $out/ twelf-server twelf-server
43
44 substituteInPlace emacs/twelf-init.el \
45 --replace '(concat twelf-root "emacs")' '(concat twelf-root "share/emacs/site-lisp/twelf")'
46
47 mkdir -p $out/share/emacs/site-lisp/twelf/
48 rsync -av emacs/ $out/share/emacs/site-lisp/twelf/
49
50 mkdir -p $out/share/twelf/examples
51 rsync -av examples/ $out/share/twelf/examples/
52 mkdir -p $out/share/twelf/vim
53 rsync -av vim/ $out/share/twelf/vim/
54 '';
55
56 meta = {
57 description = "Logic proof assistant";
58 longDescription = ''
59 Twelf is a language used to specify, implement, and prove properties of
60 deductive systems such as programming languages and logics. Large
61 research projects using Twelf include the TALT typed assembly language,
62 a foundational proof-carrying-code system, and a type safety proof for
63 Standard ML.
64 '';
65 homepage = "http://twelf.org/wiki/Main_Page";
66 license = lib.licenses.mit;
67 maintainers = with lib.maintainers; [ jwiegley ];
68 platforms = lib.platforms.unix;
69 };
70}