From 969a922145e3f7a96298143ac03cd31fb61ab5b9 Mon Sep 17 00:00:00 2001
From: Yatao Li <yatli@microsoft.com>
Date: Mon, 10 Sep 2018 13:19:48 +0800
Subject: [PATCH] api: dotnet: install nuget package and register local repo;
 xplat native assembly detection

---
 cmake/modules/FindDotnet.cmake        | 12 ++++++----
 src/api/dotnet/CMakeLists.txt         | 33 +++++++++++++++++++--------
 src/api/dotnet/Microsoft.Z3.csproj.in | 10 ++++----
 3 files changed, 37 insertions(+), 18 deletions(-)

diff --git a/cmake/modules/FindDotnet.cmake b/cmake/modules/FindDotnet.cmake
index 4ca792ed6..ed1186999 100644
--- a/cmake/modules/FindDotnet.cmake
+++ b/cmake/modules/FindDotnet.cmake
@@ -22,7 +22,8 @@
 #            [PLATFORM platform]
 #            [PACKAGE output_nuget_packages... ]
 #            [VERSION nuget_package_version]
-#            [DEPENDS depend_nuget_packages... ])
+#            [DEPENDS depend_nuget_packages... ]
+#            [SOURCES additional_file_dependencies... ])
 # ```
 # 
 # RUN_DOTNET -- Run a project with `dotnet run`. The `OUTPUT` argument represents artifacts 
@@ -41,7 +42,8 @@
 #            [CONFIG configuration]
 #            [PLATFORM platform]
 #            [PACKAGE output_nuget_packages... ]
-#            [DEPENDS depend_nuget_packages... ])
+#            [DEPENDS depend_nuget_packages... ]
+#            [SOURCES additional_file_dependencies... ])
 # ```
 #
 # DOTNET_REGISTER_LOCAL_REPOSITORY -- register a local NuGet package repository.
@@ -110,7 +112,6 @@ ENDFUNCTION()
 
 FUNCTION(DOTNET_GET_DEPS _DN_PROJECT arguments)
     FILE(GLOB_RECURSE DOTNET_deps *.cs *.fs *.xaml *.csproj *.fsproj *.tsl)
-    LIST(FILTER DOTNET_deps EXCLUDE REGEX /obj/)
     CMAKE_PARSE_ARGUMENTS(
         # prefix
         _DN 
@@ -119,10 +120,13 @@ FUNCTION(DOTNET_GET_DEPS _DN_PROJECT arguments)
         # oneValueArgs
         "CONFIG;PLATFORM;VERSION" 
         # multiValueArgs
-        "PACKAGE;DEPENDS;ARGUMENTS;OUTPUT"
+        "PACKAGE;DEPENDS;ARGUMENTS;OUTPUT;SOURCES"
         # the input arguments
         ${arguments})
 
+    LIST(APPEND DOTNET_deps ${_DN_SOURCES})
+    LIST(FILTER DOTNET_deps EXCLUDE REGEX /obj/)
+
     GET_FILENAME_COMPONENT(_DN_abs_proj "${_DN_PROJECT}" ABSOLUTE)
     GET_FILENAME_COMPONENT(_DN_proj_dir "${_DN_PROJECT}" DIRECTORY)
     GET_FILENAME_COMPONENT(_DN_projname "${DOTNET_PROJECT}" NAME)
diff --git a/src/api/dotnet/CMakeLists.txt b/src/api/dotnet/CMakeLists.txt
index 2d9b32a2f..6a70f43b5 100644
--- a/src/api/dotnet/CMakeLists.txt
+++ b/src/api/dotnet/CMakeLists.txt
@@ -137,21 +137,34 @@ endforeach()
 
 # FindDotnet.cmake forwards CMake build type to MSBuild.
 # And thus we can put the conditional properties in the project file.
-
+# Note, nuget package file names do not have the ${VER_REV} part.
+set(Z3_DOTNET_NUPKG_VERSION "${VER_MAJOR}.${VER_MINOR}.${VER_BUILD}")
 configure_file(${CMAKE_CURRENT_SOURCE_DIR}/Microsoft.Z3.csproj.in ${CMAKE_CURRENT_BINARY_DIR}/build/Microsoft.Z3.csproj)
 ADD_DOTNET(${CMAKE_CURRENT_BINARY_DIR}/build/Microsoft.Z3.csproj
-    # note, nuget package file names do not have the ${VER_REV} part.
-    VERSION "${VER_MAJOR}.${VER_MINOR}.${VER_BUILD}"
+    VERSION ${Z3_DOTNET_NUPKG_VERSION}
+    SOURCES ${CMAKE_CURRENT_SOURCE_DIR}/Microsoft.Z3.csproj.in
     PACKAGE Microsoft.Z3)
 
-add_custom_command(
-    OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/buildtimestamp
-    DEPENDS ${Z3_DOTNET_ASSEMBLY_SOURCES} ${CMAKE_CURRENT_SOURCE_DIR}/Microsoft.Z3.csproj.in
-    COMMAND ${CMAKE_COMMAND} -E touch ${CMAKE_CURRENT_BINARY_DIR}/buildtimestamp)
-add_custom_target(Z3_DOTNET_BUILD_DUMMY ALL DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/buildtimestamp)
-add_dependencies(BUILD_Microsoft.Z3 Z3_DOTNET_BUILD_DUMMY libz3)
+add_dependencies(BUILD_Microsoft.Z3 libz3)
 
 # Convenient top-level target
 add_custom_target(build_z3_dotnet_bindings ALL DEPENDS BUILD_Microsoft.Z3)
 
-#TODO install
+###############################################################################
+# Install: register a local nuget repo and install our package.
+#          the build step depends on the 'purge' target, making sure that
+#          a user will always restore the freshly-built package.
+###############################################################################
+option(INSTALL_DOTNET_BINDINGS "Install .NET bindings when invoking install target" ON)
+
+if(INSTALL_DOTNET_BINDINGS)
+    install(FILES "${CMAKE_BINARY_DIR}/Microsoft.Z3.${Z3_DOTNET_NUPKG_VERSION}.nupkg" DESTINATION "${CMAKE_INSTALL_LIBDIR}/z3.nuget")
+    install(CODE "include(${CMAKE_CURRENT_LIST_DIR}/../../../cmake/modules/FindDotnet.cmake)\n DOTNET_REGISTER_LOCAL_REPOSITORY(Microsoft.Z3.LocalBuild ${CMAKE_INSTALL_PREFIX}/${CMAKE_INSTALL_LIBDIR}/z3.nuget)")
+# TODO docs?
+#  install(FILES "${Z3_DOTNET_ASSEMBLY_DLL_DOC}" DESTINATION "${CMAKE_INSTALL_LIBDIR}")
+# TODO GAC?
+#  set(GAC_PKG_NAME "Microsoft.Z3.Sharp")
+#  set(PREFIX "${CMAKE_INSTALL_PREFIX}")
+#  set(VERSION "${Z3_VERSION}")
+endif()
+
diff --git a/src/api/dotnet/Microsoft.Z3.csproj.in b/src/api/dotnet/Microsoft.Z3.csproj.in
index b2fda27e4..cbbddc63f 100644
--- a/src/api/dotnet/Microsoft.Z3.csproj.in
+++ b/src/api/dotnet/Microsoft.Z3.csproj.in
@@ -1,4 +1,4 @@
-<Project Sdk="Microsoft.Net.Sdk">
+<Project Sdk="Microsoft.NET.Sdk">
 
   <!-- Package metadata properties -->
   <PropertyGroup>
@@ -58,11 +58,13 @@ ${Z3_DOTNET_COMPILE_ITEMS}
 
   <!-- Native binaries -->
   <ItemGroup>
-    <!-- FIXME configuration fixed to Release -->
-    <Content Include="${CMAKE_BINARY_DIR}/Release/libz3.dll" Condition="Exists('${CMAKE_BINARY_DIR}/Release/libz3.dll')">
+    <!--TODO detect if we're building x86.-->
+    <Content Include="${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libz3.dll" Condition="Exists('${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libz3.dll')">
       <PackagePath>runtimes\win-x64\native</PackagePath>
     </Content>
-    <!-- TODO XPlat support -->
+    <Content Include="${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libz3.so" Condition="Exists('${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libz3.so')">
+      <PackagePath>runtimes\linux-x64\native</PackagePath>
+    </Content>
   </ItemGroup>
 
   <!-- NuGet package references -->