Documentation

Lean.Server.FileWorker.SetupFile

Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      partial def Lean.Server.FileWorker.runLakeSetupFile.processStderr (lakePath : Lake.FilePath) (handleStderr : StringIO Unit) (args : Array String) (lakeProc : IO.Process.Child { stdin := IO.Process.Stdio.null, stdout := IO.Process.Stdio.piped, stderr := IO.Process.Stdio.piped, cmd := lakePath.toString, args := args, cwd := none, env := #[], setsid := false }.toStdioConfig) (acc : String) :

      Categorizes possible outcomes of running lake setup-file.

      Instances For

        Result of running lake setup-file.

        Instances For
          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
              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

                  Uses lake setup-file to compile dependencies on the fly and add them to LEAN_PATH. Compilation progress is reported to handleStderr. Returns the search path for source files and the options for the file.

                  Instances For