From f7818757efb85b03a271cf10378d69f89700243a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 26 May 2020 13:50:04 -0700
Subject: [PATCH] chore: add `Lean` package to `CMakeLists.txt`

---
 src/CMakeLists.txt       | 8 +++++++-
 src/Lean.lean            | 3 ++-
 src/shell/CMakeLists.txt | 2 +-
 3 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 37aa322944..0781031d8c 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -536,6 +536,7 @@ install(FILES ${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a DESTINATION lib/lean)
 if(${STAGE} EQUAL 0)
   add_library(Init STATIC $<TARGET_OBJECTS:stage0>)
   add_library(Std STATIC $<TARGET_OBJECTS:stage0>)
+  add_library(Lean STATIC $<TARGET_OBJECTS:stage0>)
 else()
 # created by the previous stage
   add_library(Init STATIC IMPORTED)
@@ -545,11 +546,16 @@ else()
   add_library(Std STATIC IMPORTED)
   set_target_properties(Std PROPERTIES
     IMPORTED_LOCATION "${PREV_STAGE}/lib/lean/libStd.a")
+
+  add_library(Lean STATIC IMPORTED)
+  set_target_properties(Lean PROPERTIES
+    IMPORTED_LOCATION "${PREV_STAGE}/lib/lean/libLean.a")
 endif()
 # leancpp and Init are cyclically dependent
 target_link_libraries(Init INTERFACE leancpp)
 target_link_libraries(Std INTERFACE leancpp)
-target_link_libraries(leancpp INTERFACE Init Std ${EXTRA_LIBS})
+target_link_libraries(Lean INTERFACE leancpp Std)
+target_link_libraries(leancpp INTERFACE Init Std Lean ${EXTRA_LIBS})
 
 if(LLVM)
   target_link_libraries(leancpp INTERFACE ${llvm_libs})
diff --git a/src/Lean.lean b/src/Lean.lean
index 7c37be7869..7487f955b4 100644
--- a/src/Lean.lean
+++ b/src/Lean.lean
@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
@@ -24,3 +24,4 @@ Authors: Leonardo de Moura
 -- import Lean.Structure
 -- import Lean.Delaborator
 -- import Lean.PrettyPrinter
+import Init.Lean
diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index 8327bd01ba..c1f933baac 100644
--- a/src/shell/CMakeLists.txt
+++ b/src/shell/CMakeLists.txt
@@ -1,6 +1,6 @@
 add_executable(lean lean.cpp)
 set_target_properties(lean PROPERTIES RUNTIME_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/bin")
-target_link_libraries(lean leancpp Init Std)
+target_link_libraries(lean leancpp Init Std Lean)
 
 # create import library on Windows to link plugins against
 set_target_properties(lean PROPERTIES ENABLE_EXPORTS ON)