Documentation

Lake.Build.Basic

Exit code to return if --no-build is set and a build is required.

Equations
Instances For

    Configuration options for a Lake build.

    • oldMode : Bool

      Use modification times for trace checking.

    • trustHash : Bool

      Whether to trust .hash files.

    • noBuild : Bool

      Early exit if a target has to be rebuilt.

    • verbosity : Lake.Verbosity

      Verbosity level (-q, -v, or neither).

    • failLv : Lake.LogLevel

      Fail the top-level build if entries of at least this level have been logged.

      Unlike some build systems, this does NOT convert such log entries to errors, and it does not abort jobs when warnings are logged (i.e., dependent jobs will still continue unimpeded).

    • The minimum log level for an log entry to be reported.

    • The stream to which Lake reports build progress. By default, Lake uses stderr.

    • ansiMode : Lake.AnsiMode

      Whether to use ANSI escape codes in build output.

    Instances For

      Whether the build should show progress information.

      Verbosity.quiet hides progress and, for a noBuild, Verbosity.verbose shows progress.

      Equations
      Instances For
        structure Lake.JobCore (α : Type u) :

        The core structure of a Lake job.

        • task : α

          The Lean Task object for the job.

        • caption : String

          A caption for the job in Lake's build monitor. Will be formatted like ✔ [3/5] Ran <caption>.

        • optional : Bool

          Whether this job failing should cause the build to fail.

        Instances For
          instance Lake.instInhabitedJobCore :
          {a : Type u_1} → [inst : Inhabited a] → Inhabited (Lake.JobCore a)
          Equations
          • Lake.instInhabitedJobCore = { default := { task := default, caption := default, optional := default } }

          A Lake job task with an opaque value type in Type.

          Equations
          Instances For
            @[reducible, inline]

            A Lake job with an opaque value type in Type.

            Equations
            Instances For

              A Lake context with a build configuration and additional build data.

              Instances For
                @[reducible, inline]
                abbrev Lake.BuildT (m : TypeType u_1) (α : Type) :
                Type u_1

                A transformer to equip a monad with a BuildContext.

                Equations
                Instances For
                  @[reducible, inline]
                  abbrev Lake.MonadBuild (m : TypeType u) :

                  A monad equipped with a Lake build context.

                  Equations
                  Instances For
                    @[inline]
                    Equations
                    Instances For
                      @[inline]
                      Equations
                      Instances For
                        @[inline]
                        Equations
                        Instances For
                          @[inline]
                          def Lake.getIsOldMode {m : TypeType u_1} [Functor m] [Lake.MonadBuild m] :
                          Equations
                          Instances For
                            @[inline]
                            def Lake.getTrustHash {m : TypeType u_1} [Functor m] [Lake.MonadBuild m] :
                            Equations
                            Instances For
                              @[inline]
                              def Lake.getNoBuild {m : TypeType u_1} [Functor m] [Lake.MonadBuild m] :
                              Equations
                              Instances For
                                @[inline]
                                Equations
                                Instances For
                                  @[inline]
                                  def Lake.getIsVerbose {m : TypeType u_1} [Functor m] [Lake.MonadBuild m] :
                                  Equations
                                  Instances For
                                    @[inline]
                                    def Lake.getIsQuiet {m : TypeType u_1} [Functor m] [Lake.MonadBuild m] :
                                    Equations
                                    Instances For
                                      @[reducible, inline]
                                      abbrev Lake.CoreBuildM (α : Type) :

                                      The internal core monad of Lake builds. Not intended for user use.

                                      Equations
                                      Instances For
                                        @[inline, deprecated]
                                        def Lake.logStep {m : TypeType u_1} [Monad m] [Lake.MonadLog m] (message : String) :

                                        Logs a build step with message.

                                        Deprecated: Build steps are now managed by a top-level build monitor. As a result, this no longer functions the way it used to. It now just logs the message via logVerbose.

                                        Equations
                                        Instances For