Documentation

Lake.Build.Key

inductive Lake.BuildKey :

The type of keys in the Lake build store.

Instances For

    A build key with some missing info.

    • Package names may be elided (replaced by Name.anonymous).
    • Facet names are unqualified (they do not include the input target kind) and may also be ellided.
    • Module package targets are supported via a fake packageTarget with a target name ending in moduleTargetIndicator.
    Equations
      Instances For
        @[inline]

        Cast a BuildKey to a PartialBuildKey.

        Equations
          Instances For

            Parses a PartialBuildKey from a String. Uses the same syntax as the lake build / lake query CLI.

            Equations
              Instances For
                Equations
                  Instances For
                    @[reducible, match_pattern, inline]
                    Equations
                      Instances For
                        @[reducible, match_pattern, inline]
                        Equations
                          Instances For
                            @[reducible, match_pattern, inline]
                            abbrev Lake.BuildKey.targetFacet (package target facet : Lean.Name) :
                            Equations
                              Instances For
                                @[reducible, match_pattern, inline]
                                abbrev Lake.BuildKey.customTarget (package target : Lean.Name) :
                                Equations
                                  Instances For
                                    Equations
                                      Instances For

                                        Like the default toString, but without disambiguation markers.

                                        Equations
                                          Instances For
                                            Equations
                                              Instances For