Documentation

Lake.Build.Common

Common Build Tools #

This file defines general utilities that abstract common build functionality and provides some common concrete build functions.

General Utilities #

Build trace for the host platform. If an artifact includes this in its trace, it is platform-dependent and will be rebuilt on different host platforms.

Equations
Instances For

    The build trace file format, which stores information about a (successful) build.

    Instances For
      Equations
      Instances For
        Equations
        Instances For

          Read persistent trace data from a file.

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

            Write persistent trace data to a file.

            Equations
            Instances For
              @[specialize #[]]
              def Lake.checkHashUpToDate {ι : Type u_1} [Lake.CheckExists ι] [Lake.GetMTime ι] (info : ι) (depTrace : Lake.BuildTrace) (depHash : Option Lake.Hash) (oldTrace : optParam Lake.MTime depTrace.mtime) :

              Checks if the info is up-to-date by comparing depTrace with depHash. If old mode is enabled (e.g., --old), uses the oldTrace modification time as the point of comparison instead.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[specialize #[]]
                def Lake.buildUnlessUpToDate? {ι : Type u_1} [Lake.CheckExists ι] [Lake.GetMTime ι] (info : ι) (depTrace : Lake.BuildTrace) (traceFile : System.FilePath) (build : Lake.JobM PUnit) (action : optParam Lake.JobAction Lake.JobAction.build) (oldTrace : optParam Lake.MTime depTrace.mtime) :

                Checks whether info is up-to-date, and runs build to recreate it if not. If rebuilt, saves the new depTrace and build log to traceFile. Returns whether info was already up-to-date.

                Up-to-date Checking

                If traceFile exists, checks that the hash in depTrace matches that of the traceFile. If not, and old mode is enabled (e.g., --old), falls back to the oldTrace modification time as the point of comparison. If up-to-date, replay the build log stored in traceFile.

                If traceFile does not exist, checks that info has a newer modification time then depTrace / oldTrace. No log will be replayed.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[inline]
                    def Lake.buildUnlessUpToDate {ι : Type u_1} [Lake.CheckExists ι] [Lake.GetMTime ι] (info : ι) (depTrace : Lake.BuildTrace) (traceFile : System.FilePath) (build : Lake.JobM PUnit) (action : optParam Lake.JobAction Lake.JobAction.build) (oldTrace : optParam Lake.MTime depTrace.mtime) :

                    Checks whether info is up-to-date, and runs build to recreate it if not. If rebuilt, saves the new depTrace and build log to traceFile.

                    See buildUnlessUpToDate? for more details on how Lake determines whether info is up-to-date.

                    Equations
                    Instances For

                      Computes the hash of a file and saves it to a .hash file.

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

                        Remove the cached hash of a file (its .hash file).

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

                          Fetches the hash of a file that may already be cached in a .hash file. If hash files are not trusted (e.g., with --rehash) or the .hash file does not exist, it will be created with a newly computed hash.

                          If text := true, file is hashed as a text file rather than a binary file.

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

                            Fetches the trace of a file that may have already have its hash cached in a .hash file. If no such .hash file exists, recomputes and creates it.

                            If text := true, file is hashed as text file rather than a binary file.

                            Equations
                            Instances For

                              Builds file using build unless it already exists and depTrace matches the trace stored in the .trace file. If built, save the new depTrace and cache file's hash in a .hash file. Otherwise, try to fetch the hash from the .hash file using fetchFileTrace. Build logs (if any) are saved to a .log.json file and replayed from there if the build is skipped.

                              For example, given file := "foo.c", compares depTrace with that in foo.c.trace with the hash cached in foo.c.hash and the log cached in foo.c.trace.

                              If text := true, file is hashed as a text file rather than a binary file.

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

                                Build file using build after dep completes if the dependency's trace (and/or extraDepTrace) has changed.

                                If text := true, file is handled as a text file rather than a binary file.

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

                                  Build file using build after deps have built if any of their traces change.

                                  If text := true, file is handled as a text file rather than a binary file.

                                  Equations
                                  Instances For
                                    @[inline]

                                    Build file using build after deps have built if any of their traces change.

                                    If text := true, file is handled as a text file rather than a binary file.

                                    Equations
                                    Instances For

                                      Common Builds #

                                      A build job for binary file that is expected to already exist (e.g., a data blob).

                                      Any byte difference in a binary file will trigger a rebuild of its dependents.

                                      Equations
                                      Instances For

                                        A build job for text file that is expected to already exist (e.g., a source file).

                                        Text file traces have normalized line endings to avoid unnecessary rebuilds across platforms.

                                        Equations
                                        Instances For
                                          @[inline]

                                          A build job for file that is expected to already exist (e.g., a data blob or source file).

                                          If text := true, the file is handled as a text file rather than a binary file. Any byte difference in a binary file will trigger a rebuild of its dependents. In contrast, text file traces have normalized line endings to avoid unnecessary rebuilds across platforms.

                                          Equations
                                          Instances For
                                            @[inline]
                                            def Lake.buildO (oFile : System.FilePath) (srcJob : Lake.BuildJob System.FilePath) (weakArgs : optParam (Array String) #[]) (traceArgs : optParam (Array String) #[]) (compiler : optParam System.FilePath { toString := "cc" }) (extraDepTrace : optParam (Lake.JobM Lake.BuildTrace) (pure Lake.BuildTrace.nil)) :

                                            Build an object file from a source file job using compiler. The invocation is:

                                            compiler -c -o oFile srcFile weakArgs... traceArgs...
                                            

                                            The traceArgs are included as part of the dependency trace hash, whereas the weakArgs are not. Thus, system-dependent options like -I or -L should be weakArgs to avoid build artifact incompatibility between systems (i.e., a change in the file path should not cause a rebuild).

                                            You can add more components to the trace via extraDepTrace, which will be computed in the resulting BuildJob before building.

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

                                              Build an object file from a source fie job (i.e, a lean -c output) using leanc.

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

                                                Build a static library from object file jobs using the ar packaged with Lean.

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

                                                  Build a shared library by linking the results of linkJobs using leanc.

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

                                                    Build an executable by linking the results of linkJobs using leanc.

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

                                                      Build a shared library from a static library using leanc.

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

                                                        Construct a Dynlib object for a shared library target.

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