{
  lib,
  mkCoqDerivation,
  coq,
  compcert,
  ITree,
  version ? null,
}:

# A few modules that are not built and installed by default
#  but that may be useful to some users.
# They depend on ITree.
let
  extra_floyd_files = [
    "ASTsize.v"
    "io_events.v"
    "powerlater.v"
  ]
  # floyd/printf.v is broken in VST 2.9
  ++ lib.optional (!lib.versions.isGe "8.13" coq.coq-version) "printf.v"
  ++ [
    "quickprogram.v"
  ];
in

mkCoqDerivation {
  pname = "coq${coq.coq-version}-VST";
  namePrefix = [ ];
  displayVersion = {
    coq = false;
  };
  owner = "PrincetonUniversity";
  repo = "VST";
  inherit version;
  defaultVersion =
    let
      case = case: out: { inherit case out; };
    in
    with lib.versions;
    lib.switch coq.coq-version [
      (case (range "9.0" "9.1") "2.16")
      (case (range "8.19" "8.20") "2.15")
      (case (range "8.15" "8.19") "2.14")
      (case (range "8.15" "8.17") "2.13")
      (case (range "8.14" "8.16") "2.10")
      (case (range "8.13" "8.15") "2.9")
      (case (range "8.12" "8.13") "2.8")
    ] null;
  release."2.16".sha256 = "sha256-/IlFLiojtuENHE9d+j55Z2rYw5HUkltwVim75w/UFVE=";
  release."2.15".sha256 = "sha256-51k2W4efMaEO4nZ0rdkRT9rA8ZJLpot1YpFmd6RIAXw=";
  release."2.14".sha256 = "sha256-NHc1ZQ2VmXZy4lK2+mtyeNz1Qr9Nhj2QLxkPhhQB7Iw=";
  release."2.13".sha256 = "sha256-i6rvP3cpayBln5KHZOpeNfraYU5h0O9uciBQ4jRH4XA=";
  release."2.12".sha256 = "sha256-4HL0U4HA5/usKNXC0Dis1UZY/Hb/LRd2IGOrqrvdWkw=";
  release."2.11.1".sha256 = "sha256-unpNstZBnRT4dIqAYOv9n1J0tWJMeRuaaa2RG1U0Xs0=";
  release."2.10".sha256 = "sha256-RIxfPWoHnV1CFkpxCusoGY/LIk07TgC7wWGRP4BSq8w=";
  release."2.9".sha256 = "sha256:1adwzbl1pprrrwrm7cm493098fizxanxpv7nyfbvwdhgbhcnv6qf";
  release."2.8".sha256 = "sha256-cyK88uzorRfjapNQ6XgQEmlbWnDsiyLve5po1VG52q0=";
  releaseRev = v: "v${v}";
  buildInputs = [ ITree ];
  propagatedBuildInputs = [ compcert ];

  preConfigure = ''
    patchShebangs util
  ''
  +
    lib.optionalString
      (coq.coq-version != null && coq.coq-version != "dev" && lib.versions.isLe "9.1" coq.coq-version)
      ''
        substituteInPlace Makefile \
          --replace-fail 'FLOYD_FILES=' 'FLOYD_FILES= ${toString extra_floyd_files}'
      '';

  makeFlags = [
    "BITSIZE=64"
    "COMPCERT=inst_dir"
    "COMPCERT_INST_DIR=${compcert.lib}/lib/coq/${coq.coq-version}/user-contrib/compcert"
    "INSTALLDIR=$(out)/lib/coq/${coq.coq-version}/user-contrib/VST"
    "IGNORECOQVERSION=true"
    "IGNORECOMPCERTVERSION=true"
  ];

  postInstall = ''
    for d in msl veric floyd sepcomp progs64
    do
      cp -r $d $out/lib/coq/${coq.coq-version}/user-contrib/VST/
    done
  '';

  meta = {
    description = "Verified Software Toolchain";
    homepage = "https://vst.cs.princeton.edu/";
    inherit (compcert.meta) platforms;
  };
}