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 | |
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
-rw-r--r-- | pkgs/applications/science/logic/ott/default.nix | 43 | ||||
-rw-r--r-- | pkgs/top-level/all-packages.nix | 4 |
2 files changed, 47 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; + }; +} diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index 1c9fb7018c9..1d4a6b59a0c 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -11264,6 +11264,10 @@ let opensmt = callPackage ../applications/science/logic/opensmt { }; + ott = callPackage ../applications/science/logic/ott { + camlp5 = ocamlPackages.camlp5_transitional; + }; + otter = callPackage ../applications/science/logic/otter {}; picosat = callPackage ../applications/science/logic/picosat {}; |