{
  lib,
  mkCoqDerivation,
  coq,
  version ? null,
  equations,
  mathcomp-boot,
  mathcomp-analysis,
  mathcomp-experimental-reals,
  extructures,
  deriving,
  mathcomp-word,
}:

(mkCoqDerivation {
  pname = "ssprove";
  owner = "SSProve";

  inherit version;
  defaultVersion =
    let
      case = coq: mc: out: {
        cases = [
          coq
          mc
        ];
        inherit out;
      };
    in
    with lib.versions;
    lib.switch
      [ coq.coq-version mathcomp-boot.version ]
      [
        (case (range "8.20" "9.1") (range "2.3.0" "2.5.0") "0.3.0")
        (case (range "8.18" "9.1") (range "2.3.0" "2.4.0") "0.2.4")
        (case (range "8.18" "8.20") (range "2.3.0" "2.3.0") "0.2.3")
        (case (range "8.18" "8.20") (range "2.1.0" "2.2.0") "0.2.2")
        # This is the original dependency:
        # (case "8.17" "1.18.0" "0.1.0")
        # But it is not loadable. The math-comp nixpkgs configuration
        # will always only output version 1.18.0 for Coq 8.17.
        # Hence, the Coq 8.17 and math-comp 1.17.0 must be explicitly set
        # to load it.
        # (This version is not on the math-comp CI and hence not checked.)
        (case "8.17" "1.17.0" "0.1.0")
      ]
      null;

  releaseRev = v: "v${v}";

  release."0.3.0".sha256 = "sha256-ioPqavLOc8ZEzroalLR4dpqDbnOyzzOmWSF9+J1yPdQ=";
  release."0.2.4".sha256 = "sha256-uglr47aDgSkKi2JyVyN+2BrokZISZUAE8OUylGjy7ds=";
  release."0.2.3".sha256 = "sha256-Y3dmNIF36IuIgrVILteofOv8e5awKfq93S4YN7enswI=";
  release."0.2.2".sha256 = "sha256-tBF8equJd6hKZojpe+v9h6Tg9xEnMTVFgOYK7ZnMfxk=";
  release."0.2.1".sha256 = "sha256-X00q5QFxdcGWeNqOV/PLTOqQyyfqFEinbGUTO7q8bC4=";
  release."0.2.0".sha256 = "sha256-GDkWH0LUsW165vAUoYC5of9ndr0MbfBtmrPhsJVXi3o=";
  release."0.1.0".sha256 = "sha256-Yj+k+mBsudi3d6bRVlZLyM4UqQnzAX5tHvxtKoIuNTE=";

  propagatedBuildInputs = [
    equations
    mathcomp-boot
    mathcomp-analysis
    mathcomp-experimental-reals
    extructures
    deriving
    mathcomp-word
  ];

  meta = {
    description = "SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq";
    license = lib.licenses.mit;
    maintainers = [
      {
        name = "Sebastian Ertel";
        email = "sebastian.ertel@gmail.com";
        github = "sertel";
        githubId = 3703100;
      }
    ];
  };

})