Documentation

Lean.Util.Path

partial def Lean.forEachModuleInDir {m : TypeType u_1} [Monad m] [MonadLiftT IO m] (dir : System.FilePath) (f : Namem PUnit) :

Executes f with the corresponding module name for each .lean file contained in dir.

For example, if dir contains A/B/C.lean, f is called with A.B.C.

Equations
    Instances For
      Equations
        Instances For
          @[reducible, inline]

          A `.olean' search path.

          Equations
            Instances For

              If the package of mod can be found in sp, return the path with extension ext (lean or olean) corresponding to mod. Otherwise, return none. Does not check whether the returned path exists.

              Equations
                Instances For

                  Like findWithExt, but ensures the returned path exists.

                  Equations
                    Instances For
                      @[export lean_get_prefix]
                      Equations
                        Instances For
                          @[export lean_get_libdir]
                          Equations
                            Instances For
                              Equations
                                Instances For
                                  Equations
                                    Instances For
                                      def Lean.initSearchPath (leanSysroot : System.FilePath) (sp : SearchPath := ) :

                                      Initialize Lean's search path given Lean's system root and an initial search path. The system root can be obtained via getBuildDir (for internal use) or findSysroot (for external users).

                                      Equations
                                        Instances For

                                          Find the compiled .olean of a module in the LEAN_PATH search path.

                                          Equations
                                            Instances For

                                              Find the .lean source of a module in a LEAN_SRC_PATH search path.

                                              Equations
                                                Instances For
                                                  Equations
                                                    Instances For
                                                      @[export lean_module_name_of_file]

                                                      Infer module name of source file name.

                                                      Equations
                                                        Instances For
                                                          Equations
                                                            Instances For
                                                              def Lean.findSysroot (lean : String := "lean") :

                                                              Find the system root of the given lean command by calling lean --print-prefix and returning the path it prints. Defaults to trying the lean in PATH. If set, the LEAN_SYSROOT environment variable takes precedence. Note that the called lean binary might not be part of the system root, e.g. in the case of elan's proxy binary. Users internal to Lean should use Lean.getBuildDir instead.

                                                              Equations
                                                                Instances For