Documentation

Lake.Config.LeanExe

@[reducible, inline]

A Lean executable -- its package plus its configuration.

Equations
    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
                Instances For
                  @[inline]

                  The executable's user-defined configuration.

                  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 root module if the name matches; otherwise, return none.

                              Equations
                                Instances For

                                  Return the root module if the file stem of the path matches the source file. Otherwise, returns 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
                                              @[inline]

                                              The executable's supportInterpreter configuration.

                                              Equations
                                                Instances For

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

                                                  By default, the package's plus the executable's moreLinkArgs. If supportInterpreter := true, Lake prepends -rdynamic on non-Windows systems.

                                                  Equations
                                                    Instances For
                                                      @[inline]

                                                      Whether the Lean shared library should be dynamically linked to the executable.

                                                      If supportInterpreter := true, Lean symbols must be visible to the interpreter. On Windows, it is not possible to statically include these symbols in the executable due to symbol limits, so Lake dynamically links to the Lean shared library. Otherwise, Lean is linked statically.

                                                      Equations
                                                        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, buildable, but not necessarily importable, module in the package.

                                                              Equations
                                                                Instances For

                                                                  Returns the buildable module in the package whose source file is path.

                                                                  Equations
                                                                    Instances For