diff options
| author | John Wiegley <johnw@newartisans.com> | 2014-06-26 15:54:12 -0700 |
|---|---|---|
| committer | John Wiegley <johnw@newartisans.com> | 2014-06-26 15:54:45 -0700 |
| commit | ad96cc8bf9af05f1b193ecf11e7db66844a8b6b2 (patch) | |
| tree | d8ba0fabd41c173c76da14ae03668f75fd1a910f /pkgs | |
| parent | e36e853817b4c2da3b202c5e19d5f2111aafac9a (diff) | |
| download | nixlib-ad96cc8bf9af05f1b193ecf11e7db66844a8b6b2.tar nixlib-ad96cc8bf9af05f1b193ecf11e7db66844a8b6b2.tar.gz nixlib-ad96cc8bf9af05f1b193ecf11e7db66844a8b6b2.tar.bz2 nixlib-ad96cc8bf9af05f1b193ecf11e7db66844a8b6b2.tar.lz nixlib-ad96cc8bf9af05f1b193ecf11e7db66844a8b6b2.tar.xz nixlib-ad96cc8bf9af05f1b193ecf11e7db66844a8b6b2.tar.zst nixlib-ad96cc8bf9af05f1b193ecf11e7db66844a8b6b2.zip | |
twelf: new expression; prover for PL theory and logic
Diffstat (limited to 'pkgs')
| -rw-r--r-- | pkgs/applications/science/logic/twelf/default.nix | 46 | ||||
| -rw-r--r-- | pkgs/top-level/all-packages.nix | 6 |
2 files changed, 52 insertions, 0 deletions
diff --git a/pkgs/applications/science/logic/twelf/default.nix b/pkgs/applications/science/logic/twelf/default.nix new file mode 100644 index 000000000000..f5d2d44df425 --- /dev/null +++ b/pkgs/applications/science/logic/twelf/default.nix @@ -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; + }; +} diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index e55f34d45724..fbbfa940abb2 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -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 {}; |