From ea8798acc6475812e97631855bd98ce80618f5a6 Mon Sep 17 00:00:00 2001 From: John Wiegley Date: Tue, 1 Aug 2017 09:30:07 -0700 Subject: [PATCH] coq2html: New expression --- .../science/logic/coq2html/default.nix | 38 +++++++++++++++++++ pkgs/top-level/all-packages.nix | 4 ++ 2 files changed, 42 insertions(+) create mode 100644 pkgs/applications/science/logic/coq2html/default.nix diff --git a/pkgs/applications/science/logic/coq2html/default.nix b/pkgs/applications/science/logic/coq2html/default.nix new file mode 100644 index 00000000000..9687ac66ead --- /dev/null +++ b/pkgs/applications/science/logic/coq2html/default.nix @@ -0,0 +1,38 @@ +{ stdenv, lib, make, fetchgit, ocaml }: + +let + version = "20170720"; +in + +stdenv.mkDerivation { + name = "coq2html-${version}"; + + src = fetchgit { + url = "https://github.com/xavierleroy/coq2html"; + rev = "e2b94093c6b9a877717f181765e30577de22439e"; + sha256 = "1x466j0pyjggyz0870pdllv9f5vpnfrgkd0w7ajvm9rkwyp3f610"; + }; + + buildInputs = [ make ocaml ]; + + installPhase = '' + mkdir -p $out/bin + cp coq2html $out/bin + ''; + + meta = with stdenv.lib; { + description = "coq2html is an HTML documentation generator for Coq source files"; + longDescription = '' + coq2html is an HTML documentation generator for Coq source files. It is + an alternative to the standard coqdoc documentation generator + distributed along with Coq. The major feature of coq2html is its ability + to fold proof scripts: in the generated HTML, proof scripts are + initially hidden, but can be revealed one by one by clicking on the + "Proof" keyword. + ''; + homepage = https://github.com/xavierleroy/coq2html; + license = licenses.gpl2; + maintainers = with maintainers; [ jwiegley ]; + platforms = platforms.unix; + }; +} diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index 21ee6afaf24..c4b2defc114 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -18150,6 +18150,10 @@ with pkgs; coq_HEAD = callPackage ../applications/science/logic/coq/HEAD.nix {}; coq = coqPackages.coq; + coq2html = callPackage ../applications/science/logic/coq2html { + make = pkgs.gnumake3; + }; + cryptoverif = callPackage ../applications/science/logic/cryptoverif { }; cubicle = callPackage ../applications/science/logic/cubicle { };