Documentation

Lake.Build.Targets

Build Target Fetching #

Utilities for fetching package, library, module, and executable targets and facets.

Package Facets & Targets #

Fetch the build job of the specified package target.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    Fetch the build result of a target.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      Fetch the build job of the target.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[inline]

        Fetch the build result of a package facet.

        Equations
        Instances For

          Fetch the build job of a package facet.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            Fetch the build job of a library facet.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              Module Facets #

              @[inline]

              Fetch the build result of a module facet.

              Equations
              Instances For

                Fetch the build job of a module facet.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  Fetch the build job of a module facet.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For

                    Lean Library Facets #

                    @[inline]

                    Get the Lean library in the workspace with the configuration's name.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[inline]

                      Fetch the build result of a library facet.

                      Equations
                      Instances For

                        Fetch the build job of a library facet.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For

                          Fetch the build job of a library facet.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For

                            Lean Executable Target #

                            @[inline]

                            Get the Lean executable in the workspace with the configuration's name.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              @[inline]

                              Fetch the build of the Lean executable.

                              Equations
                              Instances For