From a017801983ffd22b2720930e80f712050aa401dd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 30 Dec 2013 12:40:42 -0800
Subject: [PATCH] chore(builtin): cleanup dependencies

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/builtin/CMakeLists.txt  |  34 +++++++++++++---------------------
 src/builtin/specialfn.olean | Bin 1086 -> 1122 bytes
 2 files changed, 13 insertions(+), 21 deletions(-)

diff --git a/src/builtin/CMakeLists.txt b/src/builtin/CMakeLists.txt
index 3e9784c07..437c48113 100644
--- a/src/builtin/CMakeLists.txt
+++ b/src/builtin/CMakeLists.txt
@@ -31,7 +31,7 @@ function(add_theory_core FILE ARG EXTRA_DEPS)
     COMMAND ${CMAKE_COMMAND} -E copy ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} ${SHELL_DIR}/${FNAME}
     COMMAND ${CMAKE_COMMAND} -E copy ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} ${CMAKE_CURRENT_SOURCE_DIR}/${FNAME}
     DEPENDS ${CMAKE_CURRENT_SOURCE_DIR}/${FILE} ${SHELL_DIR}/lean ${EXTRA_DEPS})
-  add_custom_target("${BASENAME}_builtin" DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/${FNAME})
+  add_custom_target("${BASENAME}_builtin" DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} ${EXTRA_DEPS})
   add_dependencies(builtin ${BASENAME}_builtin)
   install(FILES ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} DESTINATION library)
 endfunction()
@@ -50,35 +50,27 @@ function(copy_olean FILE)
   install(FILES ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} DESTINATION library)
 endfunction()
 
-function(add_kernel_theory FILE)
+function(add_kernel_theory FILE DEPS)
   if(CMAKE_CROSSCOMPILING)
     copy_olean(${FILE})
   else()
-    add_theory_core(${FILE} "-n" "${CMAKE_CURRENT_BINARY_DIR}/macros.lua")
+    add_theory_core(${FILE} "-n" "${DEPS}")
   endif()
 endfunction()
 
-function(add_theory FILE)
+function(add_theory FILE DEPS)
   if(CMAKE_CROSSCOMPILING)
     copy_olean(${FILE})
   else()
-    add_theory_core(${FILE} "" "${CMAKE_CURRENT_BINARY_DIR}/kernel.olean")
+    add_theory_core(${FILE} "" "${DEPS}")
   endif()
 endfunction()
 
-add_kernel_theory("kernel.lean")
-add_kernel_theory("nat.lean")
-add_dependencies(nat_builtin kernel_builtin)
-add_kernel_theory("int.lean")
-add_dependencies(int_builtin nat_builtin)
-add_kernel_theory("real.lean")
-add_dependencies(real_builtin int_builtin)
-add_kernel_theory("specialfn.lean")
-add_dependencies(specialfn_builtin real_builtin)
-add_theory("cast.lean")
-# TODO(Leo): Remove the following dependencies after cleanup
-add_dependencies(cast_builtin kernel_builtin)
-add_dependencies(cast_builtin nat_builtin)
-add_dependencies(cast_builtin int_builtin)
-add_dependencies(cast_builtin real_builtin)
-add_dependencies(cast_builtin specialfn_builtin)
+add_kernel_theory("kernel.lean"    "${CMAKE_CURRENT_BINARY_DIR}/macros.lua")
+add_kernel_theory("nat.lean"       "${CMAKE_CURRENT_BINARY_DIR}/kernel.olean")
+add_kernel_theory("int.lean"       "${CMAKE_CURRENT_BINARY_DIR}/nat.olean")
+add_kernel_theory("real.lean"      "${CMAKE_CURRENT_BINARY_DIR}/int.olean")
+
+add_theory("specialfn.lean" "${CMAKE_CURRENT_BINARY_DIR}/real.olean")
+add_theory("cast.lean"      "${CMAKE_CURRENT_BINARY_DIR}/kernel.olean")
+
diff --git a/src/builtin/specialfn.olean b/src/builtin/specialfn.olean
index 4c47160c6f310fa8e2d1f4915cfcd67969451a16..dc8c45c76644abdf2e333d4e004c190ddfa720a4 100644
GIT binary patch
delta 40
pcmdnT@rYxBq-=I-QC?~egJ*6*eo+ZSUSbK1nVDC@uu({d1pp-_4Q~Jd

delta 10
RcmaFFv5#Yd<VIUn762CX191QV