coqPackages.Ordinal: init at 0.5.3

nixos/doc/manual/release-notes/rl-2411.section.md

@@ -135,6 +135,8 @@
 
 - [Radicle](https://radicle.xyz), an open source, peer-to-peer code collaboration stack built on Git. Available as [services.radicle](#opt-services.radicle.enable).
 
+- [Ordinal](https://github.com/snu-sf/Ordinal), A library for ordinal numbers in the Coq proof assistant.
+
 - [ddns-updater](https://github.com/qdm12/ddns-updater), a service with a WebUI to update DNS records periodically for many providers. Available as [services.ddns-updater](#opt-services.ddns-updater.enable).
 
 - [Immersed](https://immersed.com/), a closed-source coworking platform. Available as [programs.immersed](#opt-programs.immersed.enable).

pkgs/development/coq-modules/Ordinal/default.nix

@@ -0,0 +1,35 @@
+{
+  lib,
+  mkCoqDerivation,
+  coq,
+  version ? null,
+}:
+mkCoqDerivation {
+  pname = "Ordinal";
+  owner = "snu-sf";
+  inherit version;
+  defaultVersion =
+    with lib.versions;
+    lib.switch coq.version [
+      {
+        case = range "8.12" "8.18";
+        out = "0.5.3";
+      }
+    ] null;
+  release = {
+    "0.5.3".sha256 = "sha256-Myxwy749ZCBpqia6bf91cMTyJn0nRzXskD7Ue8kc37c=";
+    "0.5.2".sha256 = "sha256-jf16EyLAnKm+42K+gTTHVFJqeOVQfIY2ozbxIs5x5DE=";
+    "0.5.1".sha256 = "sha256-ThJ+jXmtkAd3jElpQZqfzqqc3EfoKY0eMpTHnbrracY=";
+    "0.5.0".sha256 = "sha256-Jq0LnR7TgRVcPqh8Ha6tIIK3KfRUgmzA9EhxeySgPnM=";
+  };
+  releaseRev = v: "v${v}";
+  installPhase = ''
+    make -f Makefile.coq COQMF_COQLIB=$out/lib/coq/${coq.coq-version}/ install
+  '';
+  meta = {
+    homepage = "https://github.com/snu-sf/Ordinal";
+    description = "Ordinal Numbers in Coq";
+    license = lib.licenses.mit;
+    maintainers = with lib.maintainers; [ damhiya ];
+  };
+}

pkgs/top-level/coq-packages.nix

@@ -132,6 +132,7 @@ let
       mtac2 = callPackage ../development/coq-modules/mtac2 {};
       multinomials = callPackage ../development/coq-modules/multinomials {};
       odd-order = callPackage ../development/coq-modules/odd-order { };
+      Ordinal = callPackage ../development/coq-modules/Ordinal {};
       paco = callPackage ../development/coq-modules/paco {};
       paramcoq = callPackage ../development/coq-modules/paramcoq {};
       parsec = callPackage ../development/coq-modules/parsec {};