twelf: new expression; prover for PL theory and logic
This commit is contained in:
parent
e36e853817
commit
ad96cc8bf9
46
pkgs/applications/science/logic/twelf/default.nix
Normal file
46
pkgs/applications/science/logic/twelf/default.nix
Normal file
@ -0,0 +1,46 @@
|
||||
{ stdenv, fetchurl, pkgconfig, smlnj, rsync }:
|
||||
|
||||
stdenv.mkDerivation rec {
|
||||
name = "twelf-${version}";
|
||||
version = "1.7.1";
|
||||
|
||||
src = fetchurl {
|
||||
url = "//twelf.plparty.org/releases/twelf-src-1.7.1.tar.gz";
|
||||
sha256 = "0fi1kbs9hrdrm1x4k13angpjasxlyd1gc3ys8ah54i75qbcd9c4i";
|
||||
};
|
||||
|
||||
buildInputs = [ pkgconfig smlnj rsync ];
|
||||
|
||||
buildPhase = ''
|
||||
export SMLNJ_HOME=${smlnj}
|
||||
make smlnj
|
||||
'';
|
||||
|
||||
installPhase = ''
|
||||
ensureDir $out/bin
|
||||
rsync -av bin/* $out/bin/
|
||||
|
||||
ensureDir $out/share/emacs/site-lisp/twelf/
|
||||
rsync -av emacs/ $out/share/emacs/site-lisp/twelf/
|
||||
|
||||
ensureDir $out/share/twelf/examples
|
||||
rsync -av examples/ $out/share/twelf/examples/
|
||||
ensureDir $out/share/twelf/vim
|
||||
rsync -av vim/ $out/share/twelf/vim/
|
||||
'';
|
||||
|
||||
meta = {
|
||||
description = "Twelf logic proof assistant";
|
||||
longDescription = ''
|
||||
Twelf is a language used to specify, implement, and prove properties of
|
||||
deductive systems such as programming languages and logics. Large
|
||||
research projects using Twelf include the TALT typed assembly language,
|
||||
a foundational proof-carrying-code system, and a type safety proof for
|
||||
Standard ML.
|
||||
'';
|
||||
homepage = http://twelf.org/wiki/Main_Page;
|
||||
license = "MIT";
|
||||
maintainers = with stdenv.lib.maintainers; [ jwiegley ];
|
||||
platforms = stdenv.lib.platforms.unix;
|
||||
};
|
||||
}
|
@ -10732,6 +10732,12 @@ let
|
||||
|
||||
tptp = callPackage ../applications/science/logic/tptp {};
|
||||
|
||||
twelf = callPackage ../applications/science/logic/twelf {
|
||||
smlnj = if stdenv.isDarwin
|
||||
then smlnjBootstrap
|
||||
else smlnj;
|
||||
};
|
||||
|
||||
verifast = callPackage ../applications/science/logic/verifast {};
|
||||
|
||||
why3 = callPackage ../applications/science/logic/why3 {};
|
||||
|
Loading…
Reference in New Issue
Block a user