query
On this page

mkRocqPackages

pkgs.mkRocqPackages

Docs pulled from | This Revision | 10 minutes ago


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

Implementation

The following is the current implementation of this function.

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