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).

    Instances For
      @[inline]

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

      Instances For

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

        Instances For
          @[inline]

          The executable's well-formed name.

          Instances For
            @[inline]

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

            Instances For
              @[inline]

              The executable's root module.

              Instances For

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

                Instances For
                  @[inline]

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

                  Instances For
                    @[inline]

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

                    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.

                      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.

                        Instances For

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

                          Instances For