diff --git a/pkgs/development/coq-modules/ceres-bs/default.nix b/pkgs/development/coq-modules/ceres-bs/default.nix new file mode 100644 index 000000000000..f1e09094334d --- /dev/null +++ b/pkgs/development/coq-modules/ceres-bs/default.nix @@ -0,0 +1,42 @@ +{ + lib, + mkCoqDerivation, + coq, + metarocq, + stdlib, + version ? null, +}: + +mkCoqDerivation { + + pname = "ceres-bs"; + repo = "rocq-ceres-bytestring"; + opam-name = "rocq-ceres-bytestring"; + owner = "peregrine-project"; + + inherit version; + defaultVersion = + let + case = case: out: { inherit case out; }; + in + with lib.versions; + lib.switch coq.version [ + (case (range "9.0" "9.1") "1.0.0") + ] null; + release."1.0.0".sha256 = "sha256-aB/YWw4E1myIYDRlNs/dEXoI9HDKl1/lsPGMYzjyJsU="; + releaseRev = v: "v${v}"; + + useDune = true; + + propagatedBuildInputs = [ + coq.ocamlPackages.findlib + stdlib + metarocq + ]; + + meta = { + description = "Library for serialization via S-expressions using bytestrings. Alternative to coq-ceres which uses String from standard library."; + license = lib.licenses.mit; + maintainers = with lib.maintainers; [ _4ever2 ]; + }; +} diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix index f9464c39fae8..32bd68a998ab 100644 --- a/pkgs/top-level/coq-packages.nix +++ b/pkgs/top-level/coq-packages.nix @@ -70,6 +70,7 @@ let null; category-theory = callPackage ../development/coq-modules/category-theory { }; ceres = callPackage ../development/coq-modules/ceres { }; + ceres-bs = callPackage ../development/coq-modules/ceres-bs { }; Cheerios = callPackage ../development/coq-modules/Cheerios { }; coinduction = callPackage ../development/coq-modules/coinduction { }; CoLoR = callPackage ../development/coq-modules/CoLoR (