fix(build): broken dependencies between lean executable and .olean, *_decls.cpp and *_decls.h files

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/builtin/CMakeLists.txt

@@ -27,10 +27,10 @@ function(add_theory_core FILE ARG EXTRA_DEPS)
   get_filename_component(BASENAME ${FILE} NAME_WE)
   set(FNAME "${BASENAME}.olean")
   add_custom_command(OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/${FNAME}
-    COMMAND ${SHELL_DIR}/lean ${ARG} -q -o ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} ${CMAKE_CURRENT_SOURCE_DIR}/${FILE}
+    COMMAND ${SHELL_DIR}/lean.sh ${ARG} -q -o ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} ${CMAKE_CURRENT_SOURCE_DIR}/${FILE}
     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}/obj/${FNAME}
-    DEPENDS ${CMAKE_CURRENT_SOURCE_DIR}/${FILE} ${SHELL_DIR}/lean ${EXTRA_DEPS})
+    DEPENDS ${CMAKE_CURRENT_SOURCE_DIR}/${FILE} ${SHELL_DIR}/lean.sh ${EXTRA_DEPS})
   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)
@@ -73,11 +73,16 @@ function(update_interface FILE DEST ARG)
   get_filename_component(BASENAME ${FILE} NAME_WE)
   set(CPPFILE "${LEAN_SOURCE_DIR}/${DEST}/${BASENAME}_decls.cpp")
   set(HFILE "${LEAN_SOURCE_DIR}/${DEST}/${BASENAME}_decls.h")
-  add_custom_command(OUTPUT ${CPPFILE} ${HFILE}
-    COMMAND ${SHELL_DIR}/lean ${ARG} -q ${CMAKE_CURRENT_SOURCE_DIR}/${FILE} ${CMAKE_CURRENT_SOURCE_DIR}/name_conv.lua ${CMAKE_CURRENT_SOURCE_DIR}/lean2cpp.lean > ${CPPFILE}
-    COMMAND ${SHELL_DIR}/lean ${ARG} -q ${CMAKE_CURRENT_SOURCE_DIR}/${FILE} ${CMAKE_CURRENT_SOURCE_DIR}/name_conv.lua ${CMAKE_CURRENT_SOURCE_DIR}/lean2h.lean > ${HFILE}
-    DEPENDS ${FILE})
-  add_custom_target("${BASENAME}_decls" DEPENDS ${CPPFILE})
+  # We also create a fake .h file, it serves as the output for the following
+  # custom command. We don't use CPPFILE and HFILE as the output to avoid
+  # a cyclic dependency.
+  set(HFILE_fake "${LEAN_BINARY_DIR}/${DEST}/${BASENAME}_fake.h")
+  add_custom_command(OUTPUT ${HFILE_fake}
+    COMMAND ${CMAKE_CURRENT_SOURCE_DIR}/lean2cpp.sh "${SHELL_DIR}/lean.sh" "${CMAKE_CURRENT_SOURCE_DIR}" "${CMAKE_CURRENT_BINARY_DIR}/${FILE}" "${CPPFILE}" "${ARG}$"
+    COMMAND ${CMAKE_CURRENT_SOURCE_DIR}/lean2h.sh   "${SHELL_DIR}/lean.sh" "${CMAKE_CURRENT_SOURCE_DIR}" "${CMAKE_CURRENT_BINARY_DIR}/${FILE}" "${HFILE}"   "${ARG}$"
+    COMMAND ${CMAKE_COMMAND} -E copy ${HFILE} ${HFILE_fake}
+    DEPENDS ${FILE} ${SHELL_DIR}/lean.sh)
+  add_custom_target("${BASENAME}_decls" DEPENDS ${HFILE_fake})
   add_dependencies(builtin ${BASENAME}_decls)
 endfunction()
 
@@ -90,7 +95,7 @@ add_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}/Nat.olean")
 
-update_interface("kernel.lean" "kernel" "-n")
-update_interface("Nat.lean"    "library/arith" "-n")
-update_interface("Int.lean"    "library/arith" "")
-update_interface("Real.lean"   "library/arith" "")
+update_interface("kernel.olean" "kernel" "-n")
+update_interface("Nat.olean"    "library/arith" "-n")
+update_interface("Int.olean"    "library/arith" "")
+update_interface("Real.olean"   "library/arith" "")

src/builtin/lean2cpp.sh

@@ -0,0 +1,13 @@
+#!/bin/sh
+LEAN=$1         # Lean executable
+SOURCE_DIR=$2   # Where the .lean and .lua auxiliary files are located
+LEAN_FILE=$3    # Lean file to be exported
+DEST=$4         # where to put the CPP file
+ARGS=$5         # extra arguments
+if $LEAN -q $ARGS $LEAN_FILE $SOURCE_DIR/name_conv.lua $SOURCE_DIR/lean2cpp.lean > $DEST.tmp
+then
+    mv $DEST.tmp $DEST
+else
+    echo "Failed to generate $DEST"
+    exit 1
+fi

src/builtin/lean2h.sh

@@ -0,0 +1,13 @@
+#!/bin/sh
+LEAN=$1         # Lean executable
+SOURCE_DIR=$2   # Where the .lean and .lua auxiliary files are located
+LEAN_FILE=$3    # Lean file to be exported
+DEST=$4         # where to put the CPP file
+ARGS=$5         # extra arguments
+if $LEAN -q $ARGS $LEAN_FILE $SOURCE_DIR/name_conv.lua $SOURCE_DIR/lean2h.lean > $DEST.tmp
+then
+    mv $DEST.tmp $DEST
+else
+    echo "Failed to generate $DEST"
+    exit 1
+fi

src/shell/CMakeLists.txt

@@ -106,3 +106,16 @@ if((${CYGWIN} EQUAL "1") OR (${CMAKE_SYSTEM_NAME} MATCHES "Linux"))
     ENDFOREACH(T)
   endif()
 endif()
+
+# Create the script lean.sh
+# This is used to create a soft dependency on the Lean executable
+# Some rules can only be applied if the lean executable exists,
+# but we don't want a dependency on the executable because
+# the rules would be applied whenever the executable is rebuilt.
+# These are the rules for automatically generating .olean files and
+# C++/Lean interface files.
+add_custom_command(OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/lean.sh
+    COMMAND ${CMAKE_CURRENT_SOURCE_DIR}/mk_lean_sh.sh ${CMAKE_CURRENT_BINARY_DIR}
+    DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/lean)
+add_custom_target(lean_sh DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/lean.sh)
+

src/shell/mk_lean_sh.sh

@@ -0,0 +1,13 @@
+#!/bin/sh
+# Auxiliary script that creates the file `lean.sh` if it doesn't
+# exist yet
+DEST=$1
+if [ -x "$DEST/lean.sh" ]; then
+    # Nothing to be done, file already exists
+    exit 0
+else
+    cat > $DEST/lean.sh <<EOF
+if ! $DEST/lean \$* ; then echo "FAILED: \$*"; exit 1; fi
+EOF
+    chmod +x $DEST/lean.sh
+fi