tjh.dev
nixpkgs mirror (for testing)
github.com/NixOS/nixpkgs
nix
1{
2 lib,
3 stdenv,
4 fetchFromGitHub,
5 pkg-config,
6 ocamlPackages,
7 opaline,
8}:
9
10stdenv.mkDerivation (finalAttrs: {
11 pname = "ott";
12 version = "0.34";
13
14 src = fetchFromGitHub {
15 owner = "ott-lang";
16 repo = "ott";
17 rev = finalAttrs.version;
18 hash = "sha256-S6EMQgEBrtXB9hTM7x6irZPsI9c9JHeuCk/9pcpQMNg=";
19 };
20
21 strictDeps = true;
22
23 nativeBuildInputs = [
24 pkg-config
25 opaline
26 ]
27 ++ (with ocamlPackages; [
28 findlib
29 ocaml
30 ]);
31 buildInputs = with ocamlPackages; [ ocamlgraph ];
32
33 installTargets = "ott.install";
34
35 postInstall = ''
36 opaline -prefix $out
37 ''
38 # There is `emacsPackages.ott-mode` for this now.
39 + ''
40 rm -r $out/share/emacs
41 '';
42
43 meta = {
44 description = "Tool for the working semanticist";
45 mainProgram = "ott";
46 longDescription = ''
47 Ott is a tool for writing definitions of programming languages and
48 calculi. It takes as input a definition of a language syntax and
49 semantics, in a concise and readable ASCII notation that is close to
50 what one would write in informal mathematics. It generates LaTeX to
51 build a typeset version of the definition, and Coq, HOL, and Isabelle
52 versions of the definition. Additionally, it can be run as a filter,
53 taking a LaTeX/Coq/Isabelle/HOL source file with embedded (symbolic)
54 terms of the defined language, parsing them and replacing them by
55 target-system terms.
56 '';
57 homepage = "http://www.cl.cam.ac.uk/~pes20/ott";
58 license = lib.licenses.bsd3;
59 maintainers = with lib.maintainers; [ jwiegley ];
60 platforms = lib.platforms.unix;
61 };
62})