From c32cd22504c6a600c12010d87d5feb0f1ad95dda Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Wed, 6 Oct 2021 17:01:52 -0400
Subject: [PATCH] feat: store detected Lean/Lake install in `BuildContext`

includes new `getLeanIncludeDir` for `BuildM` (leanprover/lake#18)
---
 Lake/BuildMonad.lean | 22 ++++++++++++++++-
 Lake/Cli.lean        | 57 +++++++++++++++++++++++++++++++-------------
 2 files changed, 62 insertions(+), 17 deletions(-)

diff --git a/Lake/BuildMonad.lean b/Lake/BuildMonad.lean
index 552ce61822..31ab96da3f 100644
--- a/Lake/BuildMonad.lean
+++ b/Lake/BuildMonad.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
 import Lake.Task
+import Lake.InstallPath
 
 open System
 namespace Lake
@@ -19,6 +20,8 @@ constant BuildMethodsRefPointed : PointedType.{0}
 def BuildMethodsRef : Type := BuildMethodsRefPointed.type
 
 structure BuildContext where
+  leanInstall : LeanInstall
+  lakeInstall : LakeInstall
   methodsRef : BuildMethodsRef
 
 abbrev BuildM := ReaderT BuildContext IO
@@ -64,7 +67,7 @@ end BuildContext
 namespace BuildM
 
 def getMethods : BuildM BuildMethods :=
-  read >>= (·.methods)
+  BuildContext.methods <$> read
 
 def logInfo (msg : String) : BuildM PUnit := do
   (← getMethods).logInfo msg
@@ -72,6 +75,21 @@ def logInfo (msg : String) : BuildM PUnit := do
 def logError (msg : String) : BuildM PUnit := do
   (← getMethods).logError msg
 
+def getLeanInstall : BuildM LeanInstall :=
+  BuildContext.leanInstall <$> read
+
+def getLeanIncludeDir : BuildM FilePath :=
+  LeanInstall.includeDir <$> getLeanInstall
+
+def getLeanc : BuildM FilePath :=
+  LeanInstall.leanc  <$> getLeanInstall
+
+def getLean : BuildM FilePath :=
+  LeanInstall.lean  <$> getLeanInstall
+
+def getLakeInstall : BuildM LakeInstall :=
+  BuildContext.lakeInstall <$> read
+
 def convErrors (self : BuildM α) : BuildM α := do
   try self catch e =>
     /-
@@ -89,6 +107,8 @@ def runIn (ctx : BuildContext) (self : BuildM α) : IO α :=
 
 end BuildM
 
+export BuildM (getLeanInstall getLeanIncludeDir getLean getLeanc getLakeInstall)
+
 def failOnBuildCycle [ToString k] : Except (List k) α → BuildM α
 | Except.ok a => a
 | Except.error cycle => do
diff --git a/Lake/Cli.lean b/Lake/Cli.lean
index 85ecbafc19..27c652a9f7 100644
--- a/Lake/Cli.lean
+++ b/Lake/Cli.lean
@@ -129,17 +129,37 @@ def output (msg : String) : CliM UInt32 := do
 def execIO (x : IO α) : CliM UInt32 := do
   try Functor.mapConst 0 x catch e => error (toString e)
 
+/--
+  Get the install configuration of Lean and Lake.
+  Error if either could not be detected.
+-/
+def getInstall : CliM (LeanInstall × LakeInstall) := do
+  if let some leanInstall ← getLeanInstall? then
+    if let some lakeInstall ← getLakeInstall? then
+      return (leanInstall, lakeInstall)
+    else
+      throw <| IO.userError <|
+        "could not detect the configuration of the Lake installation"
+  else
+    throw <| IO.userError <| "could not detect a Lean installation"
+
 /--
   Perform the given build action and then return code 0.
   If it throws an error, invoke `error` with the the error's message.
 -/
 def execBuild (x : BuildM α) : CliM UInt32 := do
-  execIO <| x.runIn {
-    methodsRef := BuildMethodsRef.mk {
-      logInfo  := fun msg => IO.println msg
-      logError := fun msg => IO.eprintln msg
-    }
-  }
+  try
+    let (leanInstall, lakeInstall) ← getInstall
+    execIO do
+      x.runIn {
+        leanInstall, lakeInstall
+        methodsRef := BuildMethodsRef.mk {
+          logInfo  := fun msg => IO.println msg
+          logError := fun msg => IO.eprintln msg
+        }
+      }
+  catch e =>
+    error (toString e)
 
 /-- Run the given script from the given package with the given arguments. -/
 def script (pkg : Package) (name : String) (args : List String) :  CliM UInt32 := do
@@ -176,17 +196,22 @@ def verifyInstall : CliM UInt32 := do
   verifyLeanVersion
 
 def printPaths (pkg : Package) (imports : List String := []) : CliM UInt32 :=
-  execIO do
-    let deps ← pkg.buildImportsAndDeps imports |>.runIn {
-      methodsRef := BuildMethodsRef.mk {
-        logInfo  := fun msg => IO.eprintln msg
-        logError := fun msg => IO.eprintln msg
+   try
+    let (leanInstall, lakeInstall) ← getInstall
+    execIO do
+      let deps ← pkg.buildImportsAndDeps imports |>.runIn {
+        leanInstall, lakeInstall
+        methodsRef := BuildMethodsRef.mk {
+          logInfo  := fun msg => IO.eprintln msg
+          logError := fun msg => IO.eprintln msg
+        }
       }
-    }
-    IO.println <| Json.compress <| Json.mkObj [
-      ("LEAN_PATH", SearchPath.toString <| pkg.oleanDir :: deps.map (·.oleanDir)),
-      ("LEAN_SRC_PATH", SearchPath.toString <| pkg.srcDir :: deps.map (·.srcDir))
-    ]
+      IO.println <| Json.compress <| Json.mkObj [
+        ("LEAN_PATH", SearchPath.toString <| pkg.oleanDir :: deps.map (·.oleanDir)),
+        ("LEAN_SRC_PATH", SearchPath.toString <| pkg.srcDir :: deps.map (·.srcDir))
+      ]
+  catch e =>
+    error (toString e)
 
 def command : (cmd : String) → CliM UInt32
 | "new"         => do noArgsRem <| execIO <| new (← takeArg)