coqPackages.MenhirLib: init at 20240715

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).

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
+    { }
+)

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;