Documentation

Lake.Config.LeanExe

structure Lake.LeanExe :

A Lean executable -- its package plus its configuration.

Instances For
    @[inline]

    The Lean executables of the package (as an Array).

    Equations
    Instances For
      @[inline]

      Try to find a Lean executable in the package with the given name.

      Equations
      Instances For

        Converts the executable configuration into a library with a single module (the root).

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

          The executable's well-formed name.

          Equations
          Instances For
            @[inline]

            Converts the executable into a library with a single module (the root).

            Equations
            Instances For
              @[inline]

              The executable's root module.

              Equations
              Instances For

                Return the the root module if the name matches, otherwise return none.

                Equations
                Instances For
                  @[inline]

                  The file name of binary executable (i.e., exeName plus the platform's exeExtension).

                  Equations
                  Instances For
                    @[inline]

                    The path to the executable in the package's binDir.

                    Equations
                    Instances For

                      The arguments to pass to leanc when linking the binary executable.

                      That is, -rdynamic (if non-Windows and supportInterpreter) plus the package's and then the executable's moreLinkArgs.

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

                        The arguments to weakly pass to leanc when linking the binary executable. That is, the package's weakLinkArgs plus the executable's weakLinkArgs.

                        Equations
                        Instances For

                          Locate the named module in the package (if it is buildable and local to it).

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