diff --git a/.gitignore b/.gitignore index 9b239a566..88ccbb56f 100644 --- a/.gitignore +++ b/.gitignore @@ -78,3 +78,4 @@ doc/api doc/code .vs examples/**/obj +CMakeSettings.json diff --git a/CMakeSettings.json b/CMakeSettings.json deleted file mode 100644 index f8c4fa7c6..000000000 --- a/CMakeSettings.json +++ /dev/null @@ -1,17 +0,0 @@ -{ - "configurations": [ - { - "name": "x64-Release", - "generator": "Visual Studio 15 2017 Win64", - "configurationType": "RelWithDebInfo", - "inheritEnvironments": [ - "msvc_x64_x64" - ], - "buildRoot": "F:\\b\\z3\\build\\${name}", - "installRoot": "F:\\b\\z3\\install\\${name}", - "cmakeCommandArgs": "", - "buildCommandArgs": "", - "ctestCommandArgs": "" - } - ] -} \ No newline at end of file diff --git a/cmake/modules/FindDotnet.cmake b/cmake/modules/FindDotnet.cmake index 4bcfe2215..bc53bf9df 100644 --- a/cmake/modules/FindDotnet.cmake +++ b/cmake/modules/FindDotnet.cmake @@ -95,7 +95,7 @@ # - DOTNET_PACKAGE_VERSION: a version string that can be referenced in the actual project file as $(DOTNET_PACKAGE_VERSION). # The version string value can be set with PACKAGE_VERSION argument, and defaults to '1.0.0'. # - XPLAT_LIB_DIR: points to the cmake build root directory. -# - OutputPath: Points to the cmake build root directory (overridden by OUTPUT_PATH). Therefore, projects built without cmake will consistently output +# - OutputPath: Points to the cmake binary directory (overridden by OUTPUT_PATH, relatively). Therefore, projects built without cmake will consistently output # to the cmake build directory. # - Custom properties can be injected with XML_INJECT argument, which injects an arbitrary string into the project XML file. # @@ -203,7 +203,7 @@ FUNCTION(DOTNET_GET_DEPS _DN_PROJECT arguments) ENDIF() IF(NOT _DN_CONFIG) - SET(_DN_CONFIG Release) + SET(_DN_CONFIG $,Debug,Release>) ENDIF() # If platform is not specified, do not pass the Platform property. @@ -226,7 +226,7 @@ FUNCTION(DOTNET_GET_DEPS _DN_PROJECT arguments) SET(_DN_VERSION "1.0.0") ENDIF() - # Set the output path to the current binary directory. + # Set the output path to the binary directory. # Build outputs in separated output directories prevent overwriting. # Later we then copy the outputs to the destination. @@ -234,7 +234,7 @@ FUNCTION(DOTNET_GET_DEPS _DN_PROJECT arguments) SET(_DN_OUTPUT_PATH ${_DN_projname_noext}) ENDIF() - GET_FILENAME_COMPONENT(_DN_OUTPUT_PATH ${CMAKE_CURRENT_BINARY_DIR}/${_DN_OUTPUT_PATH} ABSOLUTE) + GET_FILENAME_COMPONENT(_DN_OUTPUT_PATH ${CMAKE_BINARY_DIR}/${_DN_OUTPUT_PATH} ABSOLUTE) # In a cmake build, the XPLAT libraries are always copied over. # Set the proper directory for .NET projects. @@ -328,16 +328,11 @@ MACRO(DOTNET_BUILD_COMMANDS) LIST(APPEND build_dotnet_cmds COMMAND ${CMAKE_COMMAND} -E touch ${DOTNET_OUTPUTS}) IF(NOT "${DOTNET_PACKAGES}" STREQUAL "") MESSAGE("-- Adding ${build_dotnet_type} project ${DOTNET_PROJPATH} (version ${DOTNET_PACKAGE_VERSION})") - SET(_DN_OUTPUTS "") FOREACH(pkg ${DOTNET_PACKAGES}) - LIST(APPEND _DN_OUTPUTS ${DOTNET_OUTPUT_PATH}/${pkg}.${DOTNET_PACKAGE_VERSION}.nupkg) - LIST(APPEND DOTNET_OUTPUTS ${CMAKE_BINARY_DIR}/${pkg}.${DOTNET_PACKAGE_VERSION}.nupkg) - - LIST(APPEND _DN_OUTPUTS ${DOTNET_OUTPUT_PATH}/${pkg}.${DOTNET_PACKAGE_VERSION}.symbols.nupkg) - LIST(APPEND DOTNET_OUTPUTS ${CMAKE_BINARY_DIR}/${pkg}.${DOTNET_PACKAGE_VERSION}.symbols.nupkg) + LIST(APPEND DOTNET_OUTPUTS ${DOTNET_OUTPUT_PATH}/${pkg}.${DOTNET_PACKAGE_VERSION}.nupkg) + LIST(APPEND DOTNET_OUTPUTS ${DOTNET_OUTPUT_PATH}/${pkg}.${DOTNET_PACKAGE_VERSION}.symbols.nupkg) ENDFOREACH() LIST(APPEND build_dotnet_cmds COMMAND ${DOTNET_EXE} pack --no-build --no-restore ${DOTNET_PROJPATH} -c ${DOTNET_CONFIG} ${DOTNET_BUILD_PROPERTIES} ${DOTNET_PACK_OPTIONS}) - LIST(APPEND build_dotnet_cmds COMMAND ${CMAKE_COMMAND} -E copy ${_DN_OUTPUTS} ${CMAKE_BINARY_DIR}) ELSE() MESSAGE("-- Adding ${build_dotnet_type} project ${DOTNET_PROJPATH} (no nupkg)") ENDIF() diff --git a/src/api/dotnet/CMakeLists.txt b/src/api/dotnet/CMakeLists.txt index b9e26ec9e..26991bee7 100644 --- a/src/api/dotnet/CMakeLists.txt +++ b/src/api/dotnet/CMakeLists.txt @@ -139,8 +139,10 @@ endforeach() # And thus we can put the conditional properties in the project file. # Note, nuget package file names do not have the ${VER_REV} part. -# TODO how to receive "configuration" and "platform" from here? set(Z3_DOTNET_NUPKG_VERSION "${VER_MAJOR}.${VER_MINOR}.${VER_BUILD}") + +# TODO conditional for signing. we can then enable the ``Release_delaysign`` configuration + 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 VERSION ${Z3_DOTNET_NUPKG_VERSION} @@ -163,10 +165,9 @@ add_custom_target(build_z3_dotnet_bindings ALL DEPENDS BUILD_Microsoft.Z3) 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(FILES "${CMAKE_BINARY_DIR}/Microsoft.Z3/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}") + install(FILES "${CMAKE_BINARY_DIR}/Microsoft.Z3/Microsoft.Z3.xml" DESTINATION "${CMAKE_INSTALL_LIBDIR}/z3.nuget") # TODO GAC? # set(GAC_PKG_NAME "Microsoft.Z3.Sharp") # set(PREFIX "${CMAKE_INSTALL_PREFIX}") diff --git a/src/api/dotnet/Microsoft.Z3.csproj.in b/src/api/dotnet/Microsoft.Z3.csproj.in index 34321e90b..5af2ac5f3 100644 --- a/src/api/dotnet/Microsoft.Z3.csproj.in +++ b/src/api/dotnet/Microsoft.Z3.csproj.in @@ -12,7 +12,7 @@ Z3 - .NET Interface to the Z3 Theorem Prover + Z3 is a satisfiability modulo theories solver from Microsoft Research. .NET Interface to the Z3 Theorem Prover Copyright (C) 2006-2019 Microsoft Corporation @@ -28,17 +28,22 @@ @VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@ ${DOTNET_PACKAGE_VERSION} + smt constraint solver theorem prover + + Microsoft + Microsoft - + false - false DELAYSIGN + true + true