From 5a3fe0fa465717c02234d4b06842acc66efd0005 Mon Sep 17 00:00:00 2001
From: damhiya <damhiya@gmail.com>
Date: Fri, 16 Aug 2024 02:42:17 +0900
Subject: [PATCH] coqPackages.MenhirLib: init at 20240715

---
 .../manual/release-notes/rl-2411.section.md   |  2 +
 .../coq-modules/MenhirLib/default.nix         | 50 +++++++++++++++++++
 pkgs/top-level/coq-packages.nix               |  1 +
 3 files changed, 53 insertions(+)
 create mode 100644 pkgs/development/coq-modules/MenhirLib/default.nix

diff --git a/nixos/doc/manual/release-notes/rl-2411.section.md b/nixos/doc/manual/release-notes/rl-2411.section.md
index 702d33d38899..e4b366b70528 100644
--- a/nixos/doc/manual/release-notes/rl-2411.section.md
+++ b/nixos/doc/manual/release-notes/rl-2411.section.md
@@ -73,6 +73,8 @@
 
 - [Playerctld](https://github.com/altdesktop/playerctl), a daemon to track media player activity. Available as [services.playerctld](option.html#opt-services.playerctld).
 
+- [MenhirLib](https://gitlab.inria.fr/fpottier/menhir/-/tree/master/coq-menhirlib) A support library for verified Coq parsers produced by Menhir.
+
 - [Glance](https://github.com/glanceapp/glance), a self-hosted dashboard that puts all your feeds in one place. Available as [services.glance](option.html#opt-services.glance).
 
 - [Apache Tika](https://github.com/apache/tika), a toolkit that detects and extracts metadata and text from over a thousand different file types. Available as [services.tika](option.html#opt-services.tika).
diff --git a/pkgs/development/coq-modules/MenhirLib/default.nix b/pkgs/development/coq-modules/MenhirLib/default.nix
new file mode 100644
index 000000000000..5b680c73da44
--- /dev/null
+++ b/pkgs/development/coq-modules/MenhirLib/default.nix
@@ -0,0 +1,50 @@
+{
+  lib,
+  mkCoqDerivation,
+  coq,
+  version ? null,
+}:
+let
+  MenhirLib = mkCoqDerivation {
+    pname = "MenhirLib";
+    owner = "fpottier";
+    repo = "menhir";
+    domain = "gitlab.inria.fr";
+    inherit version;
+    defaultVersion =
+      with lib.versions;
+      lib.switch coq.coq-version [
+        {
+          case = range "8.12" "8.20";
+          out = "20240715";
+        }
+        {
+          case = range "8.7" "8.11";
+          out = "20200624";
+        }
+      ] null;
+    release = {
+      "20240715".sha256 = "sha256-9CSxAIm0aEXkwF+aj8u/bqLG30y5eDNz65EnohJPjzI="; # coq 8.9 - 8.20
+      "20231231".sha256 = "sha256-veB0ORHp6jdRwCyDDAfc7a7ov8sOeHUmiELdOFf/QYk="; # coq 8.7 - 8.19
+      "20230608".sha256 = "sha256-dUPoIUVr3gqvE5bniyQh/b37tNfRsZN8X3e99GFkyLY="; # coq 8.7 - 8.18
+      "20230415".sha256 = "sha256-WjE3iOKlUb15MDG3+GOi+nertAw9L2Ryazi/0JEvjqc="; # coq 8.7 - 8.18
+      "20220210".sha256 = "sha256-Nljrgq8iW17qbn2PLIbjPd03WCcZm08d1DF6NrKOYTg="; # coq 8.7 - 8.18
+      "20211230".sha256 = "sha256-+ntl4ykkqJWEeJJzt6fO5r0X1J+4in2LJIj1N8R175w="; # coq 8.7 - 8.18
+      "20200624".sha256 = "sha256-8lMqwmOsqxU/45Xr+GeyU2aIjrClVdv3VamCCkF76jY="; # coq 8.7 - 8.13
+    };
+    preBuild = "cd coq-menhirlib/src";
+    meta = with lib; {
+      homepage = "https://gitlab.inria.fr/fpottier/menhir/-/tree/master/coq-menhirlib";
+      description = "A support library for verified Coq parsers produced by Menhir";
+      license = licenses.lgpl3Plus;
+      maintainers = with maintainers; [ ];
+    };
+  };
+in
+MenhirLib.overrideAttrs (
+  oldAttrs:
+  if oldAttrs.version <= "20211230" then
+    { installPhase = "make TARGET=$out/lib/coq/${coq.coq-version}/user-contrib/MenhirLib install"; }
+  else
+    { }
+)
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index 083ae126fb95..f52c1e5f21d8 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -101,6 +101,7 @@ let
       mathcomp-tarjan = callPackage ../development/coq-modules/mathcomp-tarjan {};
       mathcomp-word = callPackage ../development/coq-modules/mathcomp-word {};
       mathcomp-zify = callPackage ../development/coq-modules/mathcomp-zify {};
+      MenhirLib = callPackage ../development/coq-modules/MenhirLib {};
       metacoq = callPackage ../development/coq-modules/metacoq { };
       metacoq-template-coq = self.metacoq.template-coq;
       metacoq-pcuic        = self.metacoq.pcuic;