pkgs.mkRocqPackages

The function mkRocqPackages takes as input a derivation for Rocq and produces a set of libraries built with that specific Rocq. More libraries are known to this function than what is compatible with that version of Rocq. Therefore, libraries that are not known to be compatible are removed (filtered out) from the resulting set. For meta-programming purposes (inspecting the derivations rather than building the libraries) this filtering can be disabled by setting a dontFilter attribute into the Rocq derivation.

Inputs

rocq-core

1. Function argument

Noogle detected

mkRocqPackages =
    rocq-core:
    let
      self = lib.makeScope newScope (lib.flip mkRocqPackages' rocq-core);
    in
    self.filterPackages (!rocq-core.dontFilter or false);