nix coq environment

coq-menhirlib.nix

{ stdenv, coq }:
stdenv.mkDerivation {
  pname = "coq${coq.coq-version}-coq-menhirlib";
  version = "20211125";
  src = builtins.fetchTarball {
    url = "https://gitlab.inria.fr/fpottier/menhir/-/archive/20211125/archive.tar.gz";
    sha256 = "0ls13myx5g4d32rq5prnikql0wvsrisll88xhbwi3w9v13lwnal0";
  };
  buildInputs = [ coq ];

  _CoqProject = ''
    -R . MenhirLib
    Alphabet.v
    Automaton.v
    Grammar.v
    Interpreter_complete.v
    Interpreter_correct.v
    Interpreter.v
    Main.v
    Validator_classes.v
    Validator_complete.v
    Validator_safe.v
    Version.v
  '';
  buildPhase = ''
    cd coq-menhirlib/src
    pwd
    echo "$_CoqProject" > _CoqProject
    coq_makefile -f _CoqProject -o Makefile.coq
    make -f Makefile.coq
    cd ../..
  '';
  installPhase = ''
    cd coq-menhirlib/src
    make -f Makefile.coq COQLIB=$out/lib/coq/${coq.coq-version}/ install
  '';
}

coq-ordinal.nix

{ stdenv, fetchFromGitHub, coq }:
stdenv.mkDerivation {
  pname = "coq${coq.coq-version}-ordinal";
  version = "0.5.0";
  src = fetchFromGitHub {
    owner = "minkiminki";
    repo = "Ordinal";
    rev = "7d82d73db3fa248d4d19686fc2eff9836f684302";
    sha256 = "Jq0LnR7TgRVcPqh8Ha6tIIK3KfRUgmzA9EhxeySgPnM=";
  };
  buildInputs = [ coq ];
  installPhase = ''
    make -f Makefile.coq COQMF_COQLIB=$out/lib/coq/${coq.coq-version}/ install
  '';
}

shell.nix

{ pkgs ? import <nixpkgs> { } }:
let
  mkBuildInputs = coq:
    let
      super = pkgs.mkCoqPackages coq;
      callPackage = pkgs.lib.callPackageWith (pkgs // set);
      set = rec {
        inherit coq;
        menhir = coq.ocamlPackages.menhir;
        menhirLib = coq.ocamlPackages.menhirLib;
        coq-ext-lib =
          callPackage super.coq-ext-lib.override { version = "0.11.3"; };
        paco = callPackage super.paco.override { version = "4.1.1"; };
        ITree = callPackage super.ITree.override { version = "3.2.0"; };
        stdpp = callPackage super.stdpp.override { version = "1.5.0"; };
        iris = callPackage super.iris.override { version = "3.4.0"; };
        flocq = super.flocq;
        coq-menhirlib = callPackage ./coq-menhirlib { };
        compcert = (super.compcert.overrideAttrs (old: {
          buildInputs = old.buildInputs ++ [ coq-menhirlib ];
          configurePhase = ''
            ./configure -clightgen \
            -prefix $out \
            -coqdevdir $lib/lib/coq/${coq.coq-version}/user-contrib/compcert/ \
            -toolprefix ${pkgs.stdenv.cc}/bin/ \
            -use-external-Flocq \
            -use-external-MenhirLib \
            ${if pkgs.stdenv.isDarwin then "x86_64-macosx" else "x86_64-linux"}
          '';
        })).override {
          version = "3.9";
          inherit flocq;
        };
        ordinal = callPackage ./coq-ordinal { };
      };
    in pkgs.lib.attrValues set;
in pkgs.mkShell {
  nativeBuildInputs = [ pkgs.ocamlPackages.ocamlbuild ];
  buildInputs = mkBuildInputs pkgs.coq_8_13;
}