diff options
author | John Wiegley <johnw@newartisans.com> | 2014-09-15 21:47:37 +0100 |
---|---|---|
committer | John Wiegley <johnw@newartisans.com> | 2014-09-15 21:50:07 +0100 |
commit | 10afb382b713add8c4a590665b76696c82bbab21 (patch) | |
tree | 86bdaa11eea4dda8bbf575ff7629dfee5773e0a6 /pkgs/applications/science/logic/ott | |
parent | 8e60e221b5b50a96d5c661b876fbd98b9231bcf6 (diff) | |
download | nixpkgs-10afb382b713add8c4a590665b76696c82bbab21.tar nixpkgs-10afb382b713add8c4a590665b76696c82bbab21.tar.gz nixpkgs-10afb382b713add8c4a590665b76696c82bbab21.tar.bz2 nixpkgs-10afb382b713add8c4a590665b76696c82bbab21.tar.lz nixpkgs-10afb382b713add8c4a590665b76696c82bbab21.tar.xz nixpkgs-10afb382b713add8c4a590665b76696c82bbab21.tar.zst nixpkgs-10afb382b713add8c4a590665b76696c82bbab21.zip |
ott: 0.25 new expression
Diffstat (limited to 'pkgs/applications/science/logic/ott')
-rw-r--r-- | pkgs/applications/science/logic/ott/default.nix | 43 |
1 files changed, 43 insertions, 0 deletions
diff --git a/pkgs/applications/science/logic/ott/default.nix b/pkgs/applications/science/logic/ott/default.nix new file mode 100644 index 00000000000..afe827f3ad9 --- /dev/null +++ b/pkgs/applications/science/logic/ott/default.nix @@ -0,0 +1,43 @@ +# - coqide compilation can be disabled by setting lablgtk to null; + +{stdenv, fetchurl, pkgconfig, ocaml, camlp5}: + +stdenv.mkDerivation rec { + name = "ott-${version}"; + version = "0.25"; + + src = fetchurl { + url = "http://www.cl.cam.ac.uk/~pes20/ott/ott_distro_${version}.tar.gz"; + sha256 = "0i8ad1yrz9nrrgpi8db4z0aii5s0sy35mmzdfw5nq183mvbx8qqd"; + }; + + buildInputs = [ pkgconfig ocaml camlp5 ]; + + installPhase = '' + mkdir -p $out/bin + cp src/ott.opt $out/bin + ln -s $out/bin/ott.opt $out/bin/ott + + mkdir -p $out/share/emacs/site-lisp + cp emacs/ottmode.el $out/share/emacs/site-lisp + ''; + + meta = { + description = "Ott: tool for the working semanticist"; + longDescription = '' + Ott is a tool for writing definitions of programming languages and + calculi. It takes as input a definition of a language syntax and + semantics, in a concise and readable ASCII notation that is close to + what one would write in informal mathematics. It generates LaTeX to + build a typeset version of the definition, and Coq, HOL, and Isabelle + versions of the definition. Additionally, it can be run as a filter, + taking a LaTeX/Coq/Isabelle/HOL source file with embedded (symbolic) + terms of the defined language, parsing them and replacing them by + target-system terms. + ''; + homepage = http://www.cl.cam.ac.uk/~pes20/ott; + license = "BSD3"; + maintainers = with stdenv.lib.maintainers; [ jwiegley ]; + platforms = stdenv.lib.platforms.unix; + }; +} |