From 0c7e82e299a6dff270a279a47815da10bbcdb086 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= <theo.zimmermann@inria.fr>
Date: Wed, 9 Jun 2021 15:15:11 +0200
Subject: [PATCH 1/2] coqPackages.serapi: init at multiple versions

---
 .../coq-modules/serapi/default.nix            | 72 +++++++++++++++++++
 pkgs/top-level/coq-packages.nix               |  1 +
 2 files changed, 73 insertions(+)
 create mode 100644 pkgs/development/coq-modules/serapi/default.nix

diff --git a/pkgs/development/coq-modules/serapi/default.nix b/pkgs/development/coq-modules/serapi/default.nix
new file mode 100644
index 000000000000..5505713eb479
--- /dev/null
+++ b/pkgs/development/coq-modules/serapi/default.nix
@@ -0,0 +1,72 @@
+{ lib, fetchzip, mkCoqDerivation, coq, version ? null }:
+
+let
+  ocamlPackages =
+    coq.ocamlPackages.overrideScope'
+      (self: super: {
+        ppxlib = super.ppxlib.override { version = "0.15.0"; };
+        # the following does not work
+        ppx_sexp_conv = super.ppx_sexp_conv.overrideAttrs (_: {
+          src = fetchzip {
+            url = "https://github.com/janestreet/ppx_sexp_conv/archive/v0.14.1.tar.gz";
+            sha256 = "04bx5id99clrgvkg122nx03zig1m7igg75piphhyx04w33shgkz2";
+          };
+        });
+      });
+
+  release = {
+    "8.13.0+0.13.0".sha256 = "sha256:0k69907xn4k61w4mkhwf8kh8drw9pijk9ynijsppihw98j8w38fy";
+    "8.12.0+0.12.1".sha256 = "sha256:048x3sgcq4h845hi6hm4j4dsfca8zfj70dm42w68n63qcm6xf9hn";
+    "8.11.0+0.11.1".sha256 = "sha256:1phmh99yqv71vlwklqgfxiq2vj99zrzxmryj2j4qvg5vav3y3y6c";
+    "8.10.0+0.7.2".sha256  = "sha256:1ljzm63hpd0ksvkyxcbh8rdf7p90vg91gb4h0zz0941v1zh40k8c";
+  };
+in
+
+(with lib; mkCoqDerivation rec {
+  pname = "serapi";
+  inherit version release;
+
+  defaultVersion =  with versions; switch coq.version [
+      { case = isEq "8.13"; out = "8.13.0+0.13.0"; }
+      { case = isEq "8.12"; out = "8.12.0+0.12.1"; }
+      { case = isEq "8.11"; out = "8.11.0+0.11.1"; }
+      { case = isEq "8.10"; out = "8.10.0+0.7.2";  }
+    ] null;
+
+  useDune2 = true;
+
+  propagatedBuildInputs =
+    with ocamlPackages; [
+      cmdliner
+      findlib # run time dependency of SerAPI
+      ppx_deriving
+      ppx_deriving_yojson
+      ppx_import
+      ppx_sexp_conv
+      sexplib
+      yojson
+      zarith # needed because of Coq
+    ];
+
+  installPhase = ''
+    runHook preInstall
+    dune install --prefix $out --libdir $OCAMLFIND_DESTDIR coq-serapi
+    runHook postInstall
+  '';
+
+  meta = with lib; {
+    homepage = https://github.com/ejgallego/coq-serapi;
+    description = "SerAPI is a library for machine-to-machine interaction with the Coq proof assistant";
+    license = licenses.lgpl21Plus;
+    maintainers = [ maintainers.Zimmi48 ];
+  };
+}).overrideAttrs(o:
+  let inherit (o) version; in {
+  src = fetchzip {
+    url = "https://github.com/ejgallego/coq-serapi/releases/download/${version}/coq-serapi-${
+        if version == "8.11.0+0.11.1" then version
+        else builtins.replaceStrings [ "+" ] [ "." ] version
+      }.tbz";
+    sha256 = release."${version}".sha256;
+  };
+})
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index 63f52fec2cb4..2b707d3d3efd 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -80,6 +80,7 @@ let
       reglang = callPackage ../development/coq-modules/reglang {};
       relation-algebra = callPackage ../development/coq-modules/relation-algebra {};
       semantics = callPackage ../development/coq-modules/semantics {};
+      serapi = callPackage ../development/coq-modules/serapi {};
       simple-io = callPackage ../development/coq-modules/simple-io { };
       stdpp = callPackage ../development/coq-modules/stdpp { };
       StructTact = callPackage ../development/coq-modules/StructTact {};

From 1dcebe9cf57f173ad80b9e307cdfa2799ccb2057 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= <theo.zimmermann@inria.fr>
Date: Tue, 20 Jul 2021 12:27:32 +0200
Subject: [PATCH 2/2] python3Packages.alectryon: init at 1.3.1

---
 .../python-modules/alectryon/default.nix      | 29 +++++++++++++++++++
 pkgs/top-level/python-packages.nix            |  2 ++
 2 files changed, 31 insertions(+)
 create mode 100644 pkgs/development/python-modules/alectryon/default.nix

diff --git a/pkgs/development/python-modules/alectryon/default.nix b/pkgs/development/python-modules/alectryon/default.nix
new file mode 100644
index 000000000000..30ae647b0510
--- /dev/null
+++ b/pkgs/development/python-modules/alectryon/default.nix
@@ -0,0 +1,29 @@
+{ lib, buildPythonPackage, fetchPypi, pygments, dominate, beautifulsoup4, docutils, sphinx }:
+
+buildPythonPackage rec {
+  pname = "alectryon";
+  owner = "cpitclaudel";
+  version = "1.3.1";
+
+  src = fetchPypi {
+    inherit pname version;
+    sha256 = "sha256:0mca25jv917myb4n91ccpl5fz058aiqsn8cniflwfw5pp6lqnfg7";
+  };
+
+  propagatedBuildInputs = [
+    pygments
+    dominate
+    beautifulsoup4
+    docutils
+    sphinx
+  ];
+
+  doCheck = false;
+
+  meta = with lib; {
+    homepage = "https://github.com/cpitclaudel/alectryon";
+    description = "A collection of tools for writing technical documents that mix Coq code and prose";
+    license = licenses.mit;
+    maintainers = with maintainers; [ Zimmi48 ];
+  };
+}
diff --git a/pkgs/top-level/python-packages.nix b/pkgs/top-level/python-packages.nix
index f6fe67374fac..e64b45f8e633 100644
--- a/pkgs/top-level/python-packages.nix
+++ b/pkgs/top-level/python-packages.nix
@@ -397,6 +397,8 @@ in {
 
   alarmdecoder = callPackage ../development/python-modules/alarmdecoder { };
 
+  alectryon = callPackage ../development/python-modules/alectryon { };
+
   alembic = callPackage ../development/python-modules/alembic { };
 
   algebraic-data-types = callPackage ../development/python-modules/algebraic-data-types { };