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
          • self.name = self.config.name
          Instances For
            @[inline]

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

            Equations
            • self.toLeanLib = { pkg := self.pkg, config := self.config.toLeanLibConfig }
            Instances For
              @[inline]

              The executable's root module.

              Equations
              • self.root = { lib := self.toLeanLib, name := self.config.root, keyName := self.pkg.name ++ self.config.root }
              Instances For

                Return 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
                    • self.file = self.pkg.binDir / self.fileName
                    Instances For
                      @[inline]

                      The executable's supportInterpreter configuration.

                      Equations
                      • self.supportInterpreter = self.config.supportInterpreter
                      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 links directly to the Lean shared libraries on Windows by prepending -leanshared and adds -rdynamic on other systems.

                        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
                          • self.weakLinkArgs = self.pkg.weakLinkArgs ++ self.config.weakLinkArgs
                          Instances For

                            Locate the named, buildable, but not necessarily importable, module in the package.

                            Equations
                            Instances For