flake.nix

{
  inputs.nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable";
  inputs.flake-utils.url = "github:numtide/flake-utils";

  outputs = inputs:
    inputs.flake-utils.lib.eachDefaultSystem (
      system: let
        pkgs = import inputs.nixpkgs {inherit system;};
        # Function to override versions of coq packages. This function takes two arguments:
        # - coqPackages: The set of all Coq packages.
        # - versions: An attribute set of packages with their versions we want to override.
        patchCoqPackages = coqPackages: versions:
          coqPackages.overrideScope' (
            _self: super:
              pkgs.lib.foldlAttrs
              # foldAttrs is used to iterate over the versions set and apply a function
              # to each attribute. This function takes three arguments: the accumulator set,
              # the attribute name (package name), and the attribute value (version).
              (acc: pkg: version:
                # This function returns a new set with the current attribute added to the
                # accumulator set. The attribute name is the package name, and the value
                # is the overridden package.
                  acc // {${pkg} = super.${pkg}.override {inherit version;};})
              # The initial value of the accumulator set.
              {}
              # The attribute set to iterate over.
              versions
          );

        iris41 = {
          iris = "4.1.0";
          stdpp = "1.9.0";
        };

        iris42 = {
          iris = "4.2.0";
          stdpp = "1.10.0";
        };

        coqPackages817 = with (patchCoqPackages pkgs.coqPackages_8_17 iris41); [coq equations stdpp iris];
        coqPackages818 = with (patchCoqPackages pkgs.coqPackages_8_18 iris41); [coq equations stdpp iris];
        coqPackages819 = with (patchCoqPackages pkgs.coqPackages_8_18 iris42); [coq equations stdpp iris];

        emacsPackage = (pkgs.emacsPackagesFor pkgs.emacs).emacsWithPackages (ep:
          with ep; [
            company-coq
            magit
            proof-general
          ]);
      in {
        devShells = rec {
          default = coq817;
          coq817 = pkgs.mkShell {buildInputs = coqPackages817;};
          coq818 = pkgs.mkShell {buildInputs = coqPackages818;};
          coq819 = pkgs.mkShell {buildInputs = coqPackages819;};

          emacs817 = pkgs.mkShell {buildInputs = coqPackages817 ++ [emacsPackage];};
          emacs818 = pkgs.mkShell {buildInputs = coqPackages818 ++ [emacsPackage];};
          emacs819 = pkgs.mkShell {buildInputs = coqPackages819 ++ [emacsPackage];};
        };
      }
    );
}