From c77af6b75f5ae321d862b685b21d9d9af82efa23 Mon Sep 17 00:00:00 2001 From: Yatao Li Date: Mon, 10 Sep 2018 02:49:22 +0800 Subject: [PATCH 01/32] api: dotnet: switch to multi-targeting project and modern cmake-dotnet integration. --- cmake/modules/DotnetImports.props.in | 7 + cmake/modules/FindDotnet.cmake | 304 +++++++++++++ src/api/dotnet/CMakeLists.txt | 176 +------- src/api/dotnet/Microsoft.Z3.csproj | 417 ------------------ src/api/dotnet/Microsoft.Z3.csproj.in | 73 +++ src/api/dotnet/Microsoft.Z3.props | 22 + src/api/dotnet/Microsoft.Z3.targets | 11 + src/api/dotnet/Properties/AssemblyInfo.cs.in | 38 -- src/api/dotnet/core/DummyContracts.cs | 65 --- src/api/dotnet/core/README.txt | 9 - src/api/dotnet/core/project.json | 22 - src/api/dotnet/dotnet35/Example/App.config | 6 - .../dotnet/dotnet35/Example/Example.csproj | 78 ---- .../Example/Properties/AssemblyInfo.cs | 36 -- .../dotnet/dotnet35/Microsoft.Z3.NET35.csproj | 347 --------------- .../dotnet/dotnet35/Microsoft.Z3.NET35.sln | 48 -- .../dotnet35/Properties/AssemblyInfo.cs | 38 -- .../dotnet35/Properties/AssemblyInfo.cs.in | 38 -- src/api/dotnet/dotnet35/Readme.NET35 | 10 - src/api/dotnet/dotnet35/packages.config | 4 - 20 files changed, 438 insertions(+), 1311 deletions(-) create mode 100644 cmake/modules/DotnetImports.props.in create mode 100644 cmake/modules/FindDotnet.cmake delete mode 100644 src/api/dotnet/Microsoft.Z3.csproj create mode 100644 src/api/dotnet/Microsoft.Z3.csproj.in create mode 100644 src/api/dotnet/Microsoft.Z3.props create mode 100644 src/api/dotnet/Microsoft.Z3.targets delete mode 100644 src/api/dotnet/Properties/AssemblyInfo.cs.in delete mode 100644 src/api/dotnet/core/DummyContracts.cs delete mode 100644 src/api/dotnet/core/README.txt delete mode 100644 src/api/dotnet/core/project.json delete mode 100644 src/api/dotnet/dotnet35/Example/App.config delete mode 100644 src/api/dotnet/dotnet35/Example/Example.csproj delete mode 100644 src/api/dotnet/dotnet35/Example/Properties/AssemblyInfo.cs delete mode 100644 src/api/dotnet/dotnet35/Microsoft.Z3.NET35.csproj delete mode 100644 src/api/dotnet/dotnet35/Microsoft.Z3.NET35.sln delete mode 100644 src/api/dotnet/dotnet35/Properties/AssemblyInfo.cs delete mode 100644 src/api/dotnet/dotnet35/Properties/AssemblyInfo.cs.in delete mode 100644 src/api/dotnet/dotnet35/Readme.NET35 delete mode 100644 src/api/dotnet/dotnet35/packages.config diff --git a/cmake/modules/DotnetImports.props.in b/cmake/modules/DotnetImports.props.in new file mode 100644 index 000000000..fba9ae301 --- /dev/null +++ b/cmake/modules/DotnetImports.props.in @@ -0,0 +1,7 @@ + + + ${_DN_OUTPUT_PATH}/ + ${XPLAT_LIB_DIR}/ + ${_DN_VERSION} + + diff --git a/cmake/modules/FindDotnet.cmake b/cmake/modules/FindDotnet.cmake new file mode 100644 index 000000000..a3d0c2dd1 --- /dev/null +++ b/cmake/modules/FindDotnet.cmake @@ -0,0 +1,304 @@ +#.rst +# FindDotnet +# ---------- +# +# Find DotNet executable, and initialize functions for adding dotnet projects. +# +# Results are reported in the following variables:: +# +# DOTNET_FOUND - True if dotnet executable is found +# DOTNET_EXE - Dotnet executable +# DOTNET_VERSION - Dotnet version as reported by dotnet executable +# NUGET_EXE - Nuget executable (WIN32 only) +# NUGET_CACHE_PATH - Nuget package cache path +# +# The following functions are defined to add dotnet/msbuild projects: +# +# ADD_DOTNET -- add a project to be built by dotnet. +# +# ``` +# ADD_DOTNET( [RELEASE|DEBUG] [X86|X64|ANYCPU] [NETCOREAPP] +# [CONFIG configuration] +# [PLATFORM platform] +# [PACKAGE output_nuget_packages... ] +# [VERSION nuget_package_version] +# [DEPENDS depend_nuget_packages... ]) +# ``` +# +# RUN_DOTNET -- Run a project with `dotnet run`. The `OUTPUT` argument represents artifacts +# produced by running the .NET program, and can be consumed from other build steps. +# +# ``` +# RUN_DOTNET( +# [ARGUMENTS program_args...] +# [OUTPUT outputs...]) +# ``` +# +# ADD_MSBUILD -- add a project to be built by msbuild. Windows-only. When building in Unix systems, msbuild targets are skipped. +# +# ``` +# ADD_MSBUILD( [RELEASE|DEBUG] [X86|X64|ANYCPU] [NETCOREAPP] +# [CONFIG configuration] +# [PLATFORM platform] +# [PACKAGE output_nuget_packages... ] +# [DEPENDS depend_nuget_packages... ]) +# ``` +# +# DOTNET_REGISTER_LOCAL_REPOSITORY -- register a local NuGet package repository. +# +# ``` +# DOTNET_REGISTER_LOCAL_REPOSITORY(repo_name repo_path) +# ``` +# +# For all the above functions, `RELEASE|DEBUG` overrides `CONFIG`, `X86|X64|ANYCPU` overrides PLATFORM. +# For Unix systems, the target framework defaults to `netstandard2.0`, unless `NETCOREAPP` is specified. +# For Windows, the project is built as-is, allowing multi-targeting. +# +# Require 3.5 for batch copy multiple files + +CMAKE_MINIMUM_REQUIRED(VERSION 3.5.0) + +IF(DOTNET_FOUND) + RETURN() +ENDIF() + +SET(NUGET_CACHE_PATH "~/.nuget/packages") +FIND_PROGRAM(DOTNET_EXE dotnet) +SET(DOTNET_MODULE_DIR ${CMAKE_CURRENT_LIST_DIR}) + +IF(NOT DOTNET_EXE) + SET(DOTNET_FOUND FALSE) + RETURN() +ENDIF() + +EXECUTE_PROCESS( + COMMAND ${DOTNET_EXE} --version + OUTPUT_VARIABLE DOTNET_VERSION + OUTPUT_STRIP_TRAILING_WHITESPACE +) + +IF(WIN32) + FIND_PROGRAM(NUGET_EXE nuget PATHS ${CMAKE_BINARY_DIR}/tools) + IF(NUGET_EXE) + MESSAGE("-- Found nuget: ${NUGET_EXE}") + ELSE() + SET(NUGET_EXE ${CMAKE_BINARY_DIR}/tools/nuget.exe) + MESSAGE("-- Downloading nuget...") + FILE(DOWNLOAD https://dist.nuget.org/win-x86-commandline/latest/nuget.exe ${NUGET_EXE}) + MESSAGE("nuget.exe downloaded and saved to ${NUGET_EXE}") + ENDIF() +ENDIF() + +FUNCTION(DOTNET_REGISTER_LOCAL_REPOSITORY repo_name repo_path) + MESSAGE("-- Registering NuGet local repository '${repo_name}' at '${repo_path}'.") + GET_FILENAME_COMPONENT(repo_path ${repo_path} ABSOLUTE) + IF(WIN32) + STRING(REPLACE "/" "\\" repo_path ${repo_path}) + EXECUTE_PROCESS(COMMAND ${NUGET_EXE} sources list OUTPUT_QUIET) + EXECUTE_PROCESS(COMMAND ${NUGET_EXE} sources Remove -Name "${repo_name}" OUTPUT_QUIET ERROR_QUIET) + EXECUTE_PROCESS(COMMAND ${NUGET_EXE} sources Add -Name "${repo_name}" -Source "${repo_path}") + ELSE() + GET_FILENAME_COMPONENT(nuget_config ~/.nuget/NuGet/NuGet.Config ABSOLUTE) + EXECUTE_PROCESS(COMMAND ${DOTNET_EXE} nuget locals all --list OUTPUT_QUIET) + EXECUTE_PROCESS(COMMAND sed -i "/${repo_name}/d" "${nuget_config}") + EXECUTE_PROCESS(COMMAND sed -i "s## \\n #g" "${nuget_config}") + ENDIF() +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 + # options (flags) + "RELEASE;DEBUG;X86;X64;ANYCPU;NETCOREAPP" + # oneValueArgs + "CONFIG;PLATFORM;VERSION" + # multiValueArgs + "PACKAGE;DEPENDS;ARGUMENTS;OUTPUT" + # the input arguments + ${arguments}) + + 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) + STRING(REGEX REPLACE "\\.[^.]*$" "" _DN_projname_noext ${_DN_projname}) + + IF(_DN_RELEASE) + SET(_DN_CONFIG Release) + ELSEIF(_DN_DEBUG) + SET(_DN_CONFIG Debug) + ENDIF() + + IF(NOT _DN_CONFIG) + SET(_DN_CONFIG $) + IF(_DN_CONFIG STREQUAL "RelWithDebInfo" OR _DN_CONFIG STREQUAL "RelMinSize" OR NOT _DN_CONFIG) + SET(_DN_CONFIG "Release") + ENDIF() + ENDIF() + + # If platform is not specified, do not pass the Platform property. + # dotnet will pick the default Platform. + + IF(_DN_X86) + SET(_DN_PLATFORM x86) + ELSEIF(_DN_X64) + SET(_DN_PLATFORM x64) + ELSEIF(_DN_ANYCPU) + SET(_DN_PLATFORM "Any CPU") + ENDIF() + + # If package version is not set, first fallback to DOTNET_PACKAGE_VERSION + # If again not set, defaults to 1.0.0 + IF(NOT _DN_VERSION) + SET(_DN_VERSION ${DOTNET_PACKAGE_VERSION}) + ENDIF() + IF(NOT _DN_VERSION) + SET(_DN_VERSION "1.0.0") + ENDIF() + + GET_FILENAME_COMPONENT(_DN_OUTPUT_PATH ${CMAKE_CURRENT_BINARY_DIR}/bin ABSOLUTE) + + SET(DOTNET_PACKAGES ${_DN_PACKAGE} PARENT_SCOPE) + SET(DOTNET_CONFIG ${_DN_CONFIG} PARENT_SCOPE) + SET(DOTNET_PLATFORM ${_DN_PLATFORM} PARENT_SCOPE) + SET(DOTNET_DEPENDS ${_DN_DEPENDS} PARENT_SCOPE) + SET(DOTNET_PROJNAME ${_DN_projname_noext} PARENT_SCOPE) + SET(DOTNET_PROJPATH ${_DN_abs_proj} PARENT_SCOPE) + SET(DOTNET_PROJDIR ${_DN_proj_dir} PARENT_SCOPE) + SET(DOTNET_RUN_ARGUMENTS ${_DN_ARGUMENTS} PARENT_SCOPE) + SET(DOTNET_RUN_OUTPUT ${_DN_OUTPUT} PARENT_SCOPE) + SET(DOTNET_PACKAGE_VERSION ${_DN_VERSION} PARENT_SCOPE) + SET(DOTNET_OUTPUT_PATH ${_DN_OUTPUT_PATH} PARENT_SCOPE) + SET(DOTNET_deps ${DOTNET_deps} PARENT_SCOPE) + + IF(_DN_PLATFORM) + SET(_DN_PLATFORM_PROP "/p:Platform=${_DN_PLATFORM}") + ENDIF() + + IF(_DN_NETCOREAPP) + SET(_DN_BUILD_OPTIONS -f netcoreapp2.0) + SET(_DN_PACK_OPTIONS /p:TargetFrameworks=netcoreapp2.0) + ELSEIF(UNIX) + # Unix builds default to netstandard2.0 + SET(_DN_BUILD_OPTIONS -f netstandard2.0) + SET(_DN_PACK_OPTIONS /p:TargetFrameworks=netstandard2.0) + ENDIF() + + SET(_DN_IMPORT_PROP ${CMAKE_CURRENT_BINARY_DIR}/${_DN_projname}.imports.props) + CONFIGURE_FILE(${DOTNET_MODULE_DIR}/DotnetImports.props.in ${_DN_IMPORT_PROP}) + + SET(DOTNET_BUILD_PROPERTIES ${_DN_PLATFORM_PROP} ${_DN_TFMS_PROP} "/p:DirectoryBuildPropsPath=${_DN_IMPORT_PROP}" "/p:DOTNET_PACKAGE_VERSION=${_DN_VERSION}" PARENT_SCOPE) + SET(DOTNET_BUILD_OPTIONS ${_DN_BUILD_OPTIONS} PARENT_SCOPE) + SET(DOTNET_PACK_OPTIONS ${_DN_PACK_OPTIONS} PARENT_SCOPE) + +ENDFUNCTION() + +MACRO(ADD_DOTNET_DEPENDENCY_TARGETS) + FOREACH(pkg_dep ${DOTNET_DEPENDS}) + ADD_DEPENDENCIES(BUILD_${DOTNET_PROJNAME} PKG_${pkg_dep}) + MESSAGE(" ${DOTNET_PROJNAME} <- ${pkg_dep}") + ENDFOREACH() + + FOREACH(pkg ${DOTNET_PACKAGES}) + STRING(TOLOWER ${pkg} pkg_lowercase) + GET_FILENAME_COMPONENT(cache_path ${NUGET_CACHE_PATH}/${pkg_lowercase} ABSOLUTE) + IF(WIN32) + SET(rm_command powershell -NoLogo -NoProfile -NonInteractive -Command "Remove-Item -Recurse -Force -ErrorAction Ignore '${cache_path}'\; exit 0") + ELSE() + SET(rm_command rm -rf ${cache_path}) + ENDIF() + ADD_CUSTOM_TARGET( + DOTNET_PURGE_${pkg} + COMMAND ${CMAKE_COMMAND} -E echo "======= [x] Purging nuget package cache for ${pkg}" + COMMAND ${rm_command} + DEPENDS ${DOTNET_deps} + ) + ADD_DEPENDENCIES(BUILD_${DOTNET_PROJNAME} DOTNET_PURGE_${pkg}) + # Add a target for the built package -- this can be referenced in + # another project. + ADD_CUSTOM_TARGET(PKG_${pkg}) + ADD_DEPENDENCIES(PKG_${pkg} BUILD_${DOTNET_PROJNAME}) + MESSAGE("==== ${DOTNET_PROJNAME} -> ${pkg}") + ENDFOREACH() +ENDMACRO() + +MACRO(DOTNET_BUILD_COMMANDS) + IF(${DOTNET_IS_MSBUILD}) + SET(build_dotnet_cmds + COMMAND ${CMAKE_COMMAND} -E echo "=======> Building msbuild project ${DOTNET_PROJNAME} [${DOTNET_CONFIG} ${DOTNET_PLATFORM}]" + COMMAND ${NUGET_EXE} restore ${DOTNET_PROJPATH} + COMMAND ${DOTNET_EXE} msbuild ${DOTNET_PROJPATH} /t:Clean /p:Configuration="${DOTNET_CONFIG}" + COMMAND ${DOTNET_EXE} msbuild ${DOTNET_PROJPATH} /t:Build ${DOTNET_BUILD_PROPERTIES} /p:Configuration="${DOTNET_CONFIG}") + SET(build_dotnet_type "msbuild") + ELSE() + SET(build_dotnet_cmds + COMMAND ${CMAKE_COMMAND} -E echo "=======> Building .NET project ${DOTNET_PROJNAME} [${DOTNET_CONFIG} ${DOTNET_PLATFORM}]" + COMMAND ${DOTNET_EXE} restore ${DOTNET_PROJPATH} + COMMAND ${DOTNET_EXE} clean ${DOTNET_PROJPATH} ${DOTNET_BUILD_PROPERTIES} + COMMAND ${DOTNET_EXE} build --no-restore ${DOTNET_PROJPATH} -c ${DOTNET_CONFIG} ${DOTNET_BUILD_PROPERTIES} ${DOTNET_BUILD_OPTIONS}) + SET(build_dotnet_type "dotnet") + ENDIF() + + IF(NOT "${DOTNET_PACKAGES}" STREQUAL "") + MESSAGE("-- Adding ${build_dotnet_type} project ${DOTNET_PROJPATH} (version ${DOTNET_PACKAGE_VERSION})") + SET(_DOTNET_OUTPUTS "") + FOREACH(pkg ${DOTNET_PACKAGES}) + LIST(APPEND _DOTNET_OUTPUTS ${DOTNET_OUTPUT_PATH}/${pkg}.${DOTNET_PACKAGE_VERSION}.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 ${_DOTNET_OUTPUTS} ${CMAKE_BINARY_DIR}) + ELSE() + + MESSAGE("-- Adding ${build_dotnet_type} project ${DOTNET_PROJPATH} (no nupkg)") + SET(_DOTNET_OUTPUTS ${CMAKE_CURRENT_BINARY_DIR}/${DOTNET_PROJNAME}.buildtimestamp) + LIST(APPEND build_dotnet_cmds COMMAND ${CMAKE_COMMAND} -E touch ${_DOTNET_OUTPUTS}) + ENDIF() + + ADD_CUSTOM_COMMAND( + OUTPUT ${_DOTNET_OUTPUTS} + DEPENDS ${DOTNET_deps} + ${build_dotnet_cmds} + ) + ADD_CUSTOM_TARGET( + BUILD_${DOTNET_PROJNAME} ALL + DEPENDS ${_DOTNET_OUTPUTS}) + +ENDMACRO() + +FUNCTION(ADD_DOTNET DOTNET_PROJECT) + DOTNET_GET_DEPS(${DOTNET_PROJECT} "${ARGN}") + SET(DOTNET_IS_MSBUILD FALSE) + DOTNET_BUILD_COMMANDS() + ADD_DOTNET_DEPENDENCY_TARGETS() +ENDFUNCTION() + +FUNCTION(ADD_MSBUILD DOTNET_PROJECT) + IF(NOT WIN32) + MESSAGE("-- Building non-Win32, skipping ${DOTNET_PROJECT}") + RETURN() + ENDIF() + + DOTNET_GET_DEPS(${DOTNET_PROJECT} "${ARGN}") + SET(DOTNET_IS_MSBUILD TRUE) + DOTNET_BUILD_COMMANDS() + ADD_DOTNET_DEPENDENCY_TARGETS() +ENDFUNCTION() + +FUNCTION(RUN_DOTNET DOTNET_PROJECT) + DOTNET_GET_DEPS(${DOTNET_PROJECT} "${ARGN}") + ADD_CUSTOM_COMMAND( + OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/${DOTNET_PROJNAME}.runtimestamp ${DOTNET_RUN_OUTPUT} + DEPENDS ${DOTNET_deps} + COMMAND ${DOTNET_EXE} run ${DOTNET_RUN_ARGUMENTS} + COMMAND ${CMAKE_COMMAND} -E touch ${CMAKE_CURRENT_BINARY_DIR}/${DOTNET_PROJNAME}.runtimestamp + WORKING_DIRECTORY ${DOTNET_PROJDIR}) + ADD_CUSTOM_TARGET( + RUN_${DOTNET_PROJNAME} + DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/${DOTNET_PROJNAME}.runtimestamp ${DOTNET_RUN_OUTPUT}) + ADD_DEPENDENCIES(RUN_${DOTNET_PROJNAME} BUILD_${DOTNET_PROJNAME}) +ENDFUNCTION() + +MESSAGE("-- Found .NET toolchain: ${DOTNET_EXE} (version ${DOTNET_VERSION})") +SET(DOTNET_FOUND TRUE) diff --git a/src/api/dotnet/CMakeLists.txt b/src/api/dotnet/CMakeLists.txt index 50f643c8d..987ef3dff 100644 --- a/src/api/dotnet/CMakeLists.txt +++ b/src/api/dotnet/CMakeLists.txt @@ -1,12 +1,10 @@ -find_package(DotNetToolchain REQUIRED) +find_package(Dotnet REQUIRED) # Configure AssemblyInfo.cs set(VER_MAJOR "${Z3_VERSION_MAJOR}") set(VER_MINOR "${Z3_VERSION_MINOR}") set(VER_BUILD "${Z3_VERSION_PATCH}") set(VER_REVISION "${Z3_VERSION_TWEAK}") -set(Z3_DOTNET_ASSEMBLY_INFO_FILE "${CMAKE_CURRENT_BINARY_DIR}/Properties/AssemblyInfo.cs") -configure_file("Properties/AssemblyInfo.cs.in" "${Z3_DOTNET_ASSEMBLY_INFO_FILE}" @ONLY) # Generate Native.cs set(Z3_DOTNET_NATIVE_FILE "${CMAKE_CURRENT_BINARY_DIR}/Native.cs") @@ -127,165 +125,33 @@ endforeach() list(APPEND Z3_DOTNET_ASSEMBLY_SOURCES "${Z3_DOTNET_CONST_FILE}" "${Z3_DOTNET_NATIVE_FILE}" - "${Z3_DOTNET_ASSEMBLY_INFO_FILE}" ) -# ``csc.exe`` doesn't like UNIX style paths so convert them -# if necessary first to native paths. -set(Z3_DOTNET_ASSEMBLY_SOURCES_NATIVE_PATH "") -foreach (csfile_path ${Z3_DOTNET_ASSEMBLY_SOURCES}) - file(TO_NATIVE_PATH "${csfile_path}" csfile_path_native) - list(APPEND Z3_DOTNET_ASSEMBLY_SOURCES_NATIVE_PATH "${csfile_path_native}") + +# Generate items +set(Z3_DOTNET_COMPILE_ITEMS "") +foreach(csfile ${Z3_DOTNET_ASSEMBLY_SOURCES}) + set(Z3_DOTNET_COMPILE_ITEMS "${Z3_DOTNET_COMPILE_ITEMS}\n ") endforeach() -set(CSC_FLAGS "") -if (DOTNET_TOOLCHAIN_IS_WINDOWS) - # FIXME: Why use these flags? - # Note these flags have been copied from the Python build system. - list(APPEND CSC_FLAGS - "/noconfig" - "/nostdlib+" - "/reference:mscorlib.dll" - ) - # FIXME: This flag only works when the working directory of csc.exe is - # the directory containing the ``libz3`` target. I can't get this to work - # correctly with multi-configuration generators (i.e. Visual Studio) so - # just don't set the flag for now. - #list(APPEND CSC_FLAGS "/linkresource:$") -elseif (DOTNET_TOOLCHAIN_IS_MONO) - # We need to give the assembly a strong name so that it can be installed - # into the GAC. - list(APPEND CSC_FLAGS - "/keyfile:${CMAKE_CURRENT_SOURCE_DIR}/Microsoft.Z3.snk" - ) -else() - message(FATAL_ERROR "Unknown .NET toolchain") -endif() -# Common flags -list(APPEND CSC_FLAGS - "/unsafe+" - "/nowarn:1701,1702" - "/errorreport:prompt" - "/warn:4" - "/reference:System.Core.dll" - "/reference:System.dll" - "/reference:System.Numerics.dll" - "/filealign:512" # Why? - "/target:library" -) +# FindDotnet.cmake forwards CMake build type to MSBuild. +# And thus we can put the conditional properties in the project file. -# Set the build type flags. The build type for the assembly roughly corresponds -# with the native code build type. -list(APPEND CSC_FLAGS - # Debug flags, expands to nothing if we aren't doing a debug build - "$<$:/debug+>" - "$<$:/debug:full>" - "$<$:/optimize->" - # This has to be quoted otherwise the ``;`` is interpreted as a command separator - "$<$:\"/define:DEBUG$TRACE\">" - # Release flags, expands to nothing if we are doing a debug build - "$<$>:/optimize+>" -) +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}" + PACKAGE Microsoft.Z3) -# Mono's gacutil crashes when trying to install an assembly if we set the -# platform in some cases, so only set it on Windows. This bug has been -# reported at https://bugzilla.xamarin.com/show_bug.cgi?id=39955 . However mono -# ignores the platform of an assembly when running it ( -# http://lists.ximian.com/pipermail/mono-devel-list/2015-November/043370.html ) -# so this shouldn't matter in practice. -if (DOTNET_TOOLCHAIN_IS_WINDOWS) - # Set platform for assembly - if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64") - list(APPEND CSC_FLAGS "/platform:x64") - elseif ("${TARGET_ARCHITECTURE}" STREQUAL "i686") - list(APPEND CSC_FLAGS "/platform:x86") - endif() -endif() - -# FIXME: Ideally we should emit files into a configuration specific directory -# when using multi-configuration generators so that the files generated by each -# configuration don't clobber each other. Unfortunately the ``get_property()`` -# command only works correctly for single configuration generators so we can't -# use it. We also can't use ``$`` because the ``OUTPUT`` -# argument to ``add_custom_commands()`` won't accept it. -# See http://public.kitware.com/pipermail/cmake/2016-March/063101.html -# -# For now just output file to the root binary directory like the Python build -# system does and emit a warning when appropriate. -if (DEFINED CMAKE_CONFIGURATION_TYPES) - # Multi-configuration build (e.g. Visual Studio and Xcode). - message(WARNING "You are using a multi-configuration generator. The build rules for" - " the \".NET\" bindings currently do not emit files per configuration so previously" - " generated files for other configurations will be overwritten.") -endif() - -set(Z3_DOTNET_ASSEMBLY_OUTPUT_DIR "${CMAKE_BINARY_DIR}") -set(Z3_DOTNET_ASSEMBLY_NAME "Microsoft.Z3.dll") -set(Z3_DOTNET_ASSEMBLY_DLL "${Z3_DOTNET_ASSEMBLY_OUTPUT_DIR}/${Z3_DOTNET_ASSEMBLY_NAME}") -# csc.exe doesn't work with UNIX style paths so convert to native path -file(TO_NATIVE_PATH "${Z3_DOTNET_ASSEMBLY_DLL}" Z3_DOTNET_ASSEMBLY_DLL_NATIVE_PATH) -set(Z3_DOTNET_ASSEMBLY_DLL_DOC "${Z3_DOTNET_ASSEMBLY_OUTPUT_DIR}/Microsoft.Z3.xml") -file(TO_NATIVE_PATH "${Z3_DOTNET_ASSEMBLY_DLL_DOC}" Z3_DOTNET_ASSEMBLY_DLL_DOC_NATIVE_PATH) -add_custom_command(OUTPUT "${Z3_DOTNET_ASSEMBLY_DLL}" "${Z3_DOTNET_ASSEMBLY_DLL_DOC}" - COMMAND - "${DOTNET_CSC_EXECUTABLE}" - ${CSC_FLAGS} - "/out:${Z3_DOTNET_ASSEMBLY_DLL_NATIVE_PATH}" - "/doc:${Z3_DOTNET_ASSEMBLY_DLL_DOC_NATIVE_PATH}" - ${Z3_DOTNET_ASSEMBLY_SOURCES_NATIVE_PATH} - DEPENDS - ${Z3_DOTNET_ASSEMBLY_SOURCES} - libz3 - WORKING_DIRECTORY "${Z3_DOTNET_ASSEMBLY_OUTPUT_DIR}" - COMMENT "Building \"${Z3_DOTNET_ASSEMBLY_DLL}\"" -) +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) # Convenient top-level target -add_custom_target(build_z3_dotnet_bindings - ALL - DEPENDS - "${Z3_DOTNET_ASSEMBLY_DLL}" -) +add_custom_target(build_z3_dotnet_bindings ALL DEPENDS BUILD_Microsoft.Z3) -############################################################################### -# Install -############################################################################### -option(INSTALL_DOTNET_BINDINGS "Install .NET bindings when invoking install target" ON) -set(GAC_PKG_NAME "Microsoft.Z3.Sharp") -set(PREFIX "${CMAKE_INSTALL_PREFIX}") -set(VERSION "${Z3_VERSION}") -set(Z3_DOTNET_PKGCONFIG_FILE "${CMAKE_CURRENT_BINARY_DIR}/Microsoft.Z3.Sharp.pc") -configure_file("Microsoft.Z3.Sharp.pc.in" "${Z3_DOTNET_PKGCONFIG_FILE}" @ONLY) - -if (DOTNET_TOOLCHAIN_IS_MONO) - message(STATUS "Emitting install rules for .NET bindings") - # Install pkgconfig file for the assembly. This is needed by Monodevelop - # to find the assembly - install(FILES "${Z3_DOTNET_PKGCONFIG_FILE}" DESTINATION "${CMAKE_INSTALL_PKGCONFIGDIR}") - - # Configure the install and uninstall scripts. - # Note: If multi-configuration generator support is ever fixed then these - # scripts will be broken. - configure_file(cmake_install_gac.cmake.in cmake_install_gac.cmake @ONLY) - configure_file(cmake_uninstall_gac.cmake.in cmake_uninstall_gac.cmake @ONLY) - - # Tell CMake to Invoke a script to install assembly to the GAC during install - install(SCRIPT "${CMAKE_CURRENT_BINARY_DIR}/cmake_install_gac.cmake") - - # Add custom target to uninstall the assembly from the GAC - add_custom_target(remove_dotnet_dll_from_gac - COMMAND "${CMAKE_COMMAND}" "-P" "${CMAKE_CURRENT_BINARY_DIR}/cmake_uninstall_gac.cmake" - COMMENT "Uninstalling ${Z3_DOTNET_ASSEMBLY_NAME} from the GAC" - ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} - ) - add_dependencies(uninstall remove_dotnet_dll_from_gac) - -elseif(DOTNET_TOOLCHAIN_IS_WINDOWS) - # Don't install Z3_DOTNET_ASSEMBLY_DLL into the gac. Instead just copy into - # installation directory. - install(FILES "${Z3_DOTNET_ASSEMBLY_DLL}" DESTINATION "${CMAKE_INSTALL_LIBDIR}") - install(FILES "${Z3_DOTNET_ASSEMBLY_DLL_DOC}" DESTINATION "${CMAKE_INSTALL_LIBDIR}") -else() - message(FATAL_ERROR "Unknown .NET toolchain") -endif() +#TODO install diff --git a/src/api/dotnet/Microsoft.Z3.csproj b/src/api/dotnet/Microsoft.Z3.csproj deleted file mode 100644 index cde8b78c9..000000000 --- a/src/api/dotnet/Microsoft.Z3.csproj +++ /dev/null @@ -1,417 +0,0 @@ - - - - Debug - AnyCPU - 8.0.30703 - 2.0 - {EC3DB697-B734-42F7-9468-5B62821EEB5A} - Library - Properties - Microsoft.Z3 - Microsoft.Z3 - v4.0 - 512 - Client - 0 - - - true - full - false - ..\Debug\ - DEBUG;TRACE - prompt - 4 - true - ..\Debug\Microsoft.Z3.XML - False - False - True - False - False - True - False - True - True - False - False - False - True - False - False - False - True - False - False - True - True - True - False - False - - - - - - - True - Full - %28none%29 - 2 - - - pdbonly - true - ..\external\ - - - prompt - 4 - true - ..\external\Microsoft.Z3.xml - AnyCPU - - - ..\external\ - true - ..\external\Microsoft.Z3.xml - true - pdbonly - AnyCPU - bin\Release\Microsoft.Z3.dll.CodeAnalysisLog.xml - true - GlobalSuppressions.cs - prompt - MinimumRecommendedRules.ruleset - ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - true - ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - true - false - - - true - ..\x64\Debug\ - DEBUG;TRACE - true - full - x64 - ..\Debug\Microsoft.Z3.dll.CodeAnalysisLog.xml - true - GlobalSuppressions.cs - prompt - MinimumRecommendedRules.ruleset - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - true - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - true - True - False - True - False - False - False - False - False - False - False - False - False - False - False - False - False - True - False - False - True - False - False - False - - - - - - - False - Full - %28none%29 - 0 - ..\x64\Debug\Microsoft.Z3.XML - - - ..\x64\external_64\ - true - ..\x64\external_64\Microsoft.Z3.xml - true - pdbonly - x64 - ..\release\Microsoft.Z3.dll.CodeAnalysisLog.xml - true - GlobalSuppressions.cs - prompt - MinimumRecommendedRules.ruleset - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - true - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - True - False - True - False - False - True - True - True - False - False - False - True - True - False - False - False - True - False - False - True - True - False - False - - - - - -repro - - True - Full - %28none%29 - 2 - - - ..\x64\external\ - true - ..\x64\external\Microsoft.Z3.XML - true - pdbonly - x64 - bin\Release\Microsoft.Z3.dll.CodeAnalysisLog.xml - true - GlobalSuppressions.cs - prompt - MinimumRecommendedRules.ruleset - ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - true - ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - true - - - false - - - - - - - false - - - ..\Release_delaysign\ - true - ..\Release_delaysign\Microsoft.Z3.XML - true - pdbonly - AnyCPU - ..\release\Microsoft.Z3.dll.CodeAnalysisLog.xml - true - GlobalSuppressions.cs - prompt - MinimumRecommendedRules.ruleset - ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - true - ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - true - DELAYSIGN - - - bin\x64\Release_delaysign\ - true - bin\x64\Release_delaysign\Microsoft.Z3.XML - true - pdbonly - x64 - ..\release\Microsoft.Z3.dll.CodeAnalysisLog.xml - true - GlobalSuppressions.cs - prompt - MinimumRecommendedRules.ruleset - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - true - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - true - - - true - ..\x86\Debug\ - DEBUG;TRACE - true - full - x86 - ..\Debug\Microsoft.Z3.dll.CodeAnalysisLog.xml - true - GlobalSuppressions.cs - prompt - MinimumRecommendedRules.ruleset - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - ..\x86\Debug\Microsoft.Z3.XML - - - bin\x86\Release\ - true - bin\x86\Release\Microsoft.Z3.xml - true - pdbonly - x86 - ..\external\Microsoft.Z3.dll.CodeAnalysisLog.xml - true - GlobalSuppressions.cs - prompt - MinimumRecommendedRules.ruleset - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - - - bin\x86\external\ - true - bin\x86\external\Microsoft.Z3.XML - true - pdbonly - x86 - bin\Release\Microsoft.Z3.dll.CodeAnalysisLog.xml - true - GlobalSuppressions.cs - prompt - MinimumRecommendedRules.ruleset - ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - true - ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - true - - - bin\x86\Release_delaysign\ - DELAYSIGN - true - bin\x86\Release_delaysign\Microsoft.Z3.XML - true - pdbonly - x86 - ..\release\Microsoft.Z3.dll.CodeAnalysisLog.xml - true - GlobalSuppressions.cs - prompt - MinimumRecommendedRules.ruleset - ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - true - ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - true - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - \ No newline at end of file diff --git a/src/api/dotnet/Microsoft.Z3.csproj.in b/src/api/dotnet/Microsoft.Z3.csproj.in new file mode 100644 index 000000000..b2fda27e4 --- /dev/null +++ b/src/api/dotnet/Microsoft.Z3.csproj.in @@ -0,0 +1,73 @@ + + + + + + Microsoft.Z3 + Microsoft.Z3 + + Z3 .NET Interface + Z3 .NET Interface + + Z3 + + .NET Interface to the Z3 Theorem Prover + .NET Interface to the Z3 Theorem Prover + + Copyright (C) 2006-2015 Microsoft Corporation + Copyright (C) 2006-2015 Microsoft Corporation + + Microsoft Corporation + Microsoft Corporation + + @VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@ + @VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@ + + @VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@ + @VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@ + + ${DOTNET_PACKAGE_VERSION} + + + + + + + netstandard2.0;net461;net45 + library + True + 1701,1702 + 4 + FRAMEWORK_LT_4 + + + + +${Z3_DOTNET_COMPILE_ITEMS} + + + + + + build + + + build + + + + + + + + runtimes\win-x64\native + + + + + + + + + + diff --git a/src/api/dotnet/Microsoft.Z3.props b/src/api/dotnet/Microsoft.Z3.props new file mode 100644 index 000000000..67bb471ba --- /dev/null +++ b/src/api/dotnet/Microsoft.Z3.props @@ -0,0 +1,22 @@ + + + + + + true + true + true + + + $(MSBuildThisFileDirectory)..\..\ + $(Z3_PACKAGE_PATH)runtimes\win-x64\native\libz3.dll + $(Z3_PACKAGE_PATH)runtimes\linux-x64\native\libz3.so + + + + + + false + + + diff --git a/src/api/dotnet/Microsoft.Z3.targets b/src/api/dotnet/Microsoft.Z3.targets new file mode 100644 index 000000000..80179ce4c --- /dev/null +++ b/src/api/dotnet/Microsoft.Z3.targets @@ -0,0 +1,11 @@ + + + + + + %(RecursiveDir)%(FileName)%(Extension) + PreserveNewest + + + + diff --git a/src/api/dotnet/Properties/AssemblyInfo.cs.in b/src/api/dotnet/Properties/AssemblyInfo.cs.in deleted file mode 100644 index e5a85f16f..000000000 --- a/src/api/dotnet/Properties/AssemblyInfo.cs.in +++ /dev/null @@ -1,38 +0,0 @@ -using System; -using System.Reflection; -using System.Runtime.CompilerServices; -using System.Runtime.InteropServices; -using System.Security.Permissions; - -// General Information about an assembly is controlled through the following -// set of attributes. Change these attribute values to modify the information -// associated with an assembly. -[assembly: AssemblyTitle("Z3 .NET Interface")] -[assembly: AssemblyDescription(".NET Interface to the Z3 Theorem Prover")] -[assembly: AssemblyConfiguration("")] -[assembly: AssemblyCompany("Microsoft Corporation")] -[assembly: AssemblyProduct("Z3")] -[assembly: AssemblyCopyright("Copyright (C) 2006-2015 Microsoft Corporation")] -[assembly: AssemblyTrademark("")] -[assembly: AssemblyCulture("")] - -// Setting ComVisible to false makes the types in this assembly not visible -// to COM components. If you need to access a type in this assembly from -// COM, set the ComVisible attribute to true on that type. -[assembly: ComVisible(false)] - -// The following GUID is for the ID of the typelib if this project is exposed to COM -[assembly: Guid("4853ed71-2078-40f4-8117-bc46646bce0e")] - -// Version information for an assembly consists of the following four values: -// -// Major Version -// Minor Version -// Build Number -// Revision -// -// You can specify all the values or you can default the Build and Revision Numbers -// by using the '*' as shown below: -// [assembly: AssemblyVersion("4.2.0.0")] -[assembly: AssemblyVersion("@VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@")] -[assembly: AssemblyFileVersion("@VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@")] diff --git a/src/api/dotnet/core/DummyContracts.cs b/src/api/dotnet/core/DummyContracts.cs deleted file mode 100644 index 103cc1288..000000000 --- a/src/api/dotnet/core/DummyContracts.cs +++ /dev/null @@ -1,65 +0,0 @@ -/*++ -Copyright () 2016 Microsoft Corporation - -Module Name: - - Contracts.cs - -Abstract: - - Z3 Managed API: Dummy Code Contracts class for .NET - frameworks that don't support them (e.g., CoreCLR). - -Author: - - Christoph Wintersteiger (cwinter) 2016-10-06 - -Notes: - ---*/ - -namespace System.Diagnostics.Contracts -{ - public class ContractClass : Attribute - { - public ContractClass(Type t) { } - } - - public class ContractClassFor : Attribute - { - public ContractClassFor(Type t) { } - } - - public class ContractInvariantMethod : Attribute - { - public ContractInvariantMethod() { } - } - - public class ContractVerification : Attribute - { - public ContractVerification(bool b) { } - } - - public class Pure : Attribute { } - - public static class Contract - { - [Conditional("false")] - public static void Ensures(bool b) { } - [Conditional("false")] - public static void Requires(bool b) { } - [Conditional("false")] - public static void Assume(bool b, string msg) { } - [Conditional("false")] - public static void Assert(bool b) { } - public static bool ForAll(bool b) { return true; } - public static bool ForAll(Object c, Func p) { return true; } - public static bool ForAll(int from, int to, Predicate p) { return true; } - [Conditional("false")] - public static void Invariant(bool b) { } - public static T[] Result() { return new T[1]; } - [Conditional("false")] - public static void EndContractBlock() { } - public static T ValueAtReturn(out T v) { T[] t = new T[1]; v = t[0]; return v; } - } -} diff --git a/src/api/dotnet/core/README.txt b/src/api/dotnet/core/README.txt deleted file mode 100644 index 72331d7f9..000000000 --- a/src/api/dotnet/core/README.txt +++ /dev/null @@ -1,9 +0,0 @@ -Z3 API for .NET Core - -Z3's .NET API uses Code Contracts, which are not included in .NET Core. The -enclosed file called DummyContracts.cs provides stubs for the Code Contracts -functions, so that the API will compile, but not perform any contract -checking. To build this using .NET core, run (in this directory): - -dotnet restore -dotnet build project.json diff --git a/src/api/dotnet/core/project.json b/src/api/dotnet/core/project.json deleted file mode 100644 index d54b6877b..000000000 --- a/src/api/dotnet/core/project.json +++ /dev/null @@ -1,22 +0,0 @@ -{ - "version": "1.0.0-*", - "buildOptions": { - "debugType": "portable", - "emitEntryPoint": false, - "outputName": "Microsoft.Z3", - "compile": [ "../*.cs", "*.cs" ], - "define": ["DOTNET_CORE"] - }, - "dependencies": { }, - "frameworks": { - "netcoreapp1.0": { - "dependencies": { - "Microsoft.NETCore.App": { - "type": "platform", - "version": "1.0.1" - } - }, - "imports": "dnxcore50" - } - } -} diff --git a/src/api/dotnet/dotnet35/Example/App.config b/src/api/dotnet/dotnet35/Example/App.config deleted file mode 100644 index 737ed23f2..000000000 --- a/src/api/dotnet/dotnet35/Example/App.config +++ /dev/null @@ -1,6 +0,0 @@ - - - - - - diff --git a/src/api/dotnet/dotnet35/Example/Example.csproj b/src/api/dotnet/dotnet35/Example/Example.csproj deleted file mode 100644 index 842fbac41..000000000 --- a/src/api/dotnet/dotnet35/Example/Example.csproj +++ /dev/null @@ -1,78 +0,0 @@ - - - - - Debug - AnyCPU - {2A8E577B-7B6D-4CA9-832A-CA2EEC314812} - Exe - Properties - Example - Example - v4.5.2 - 512 - true - - - AnyCPU - true - full - false - bin\Debug\ - TRACE;DEBUG;FRAMEWORK_LT_4 - prompt - 4 - - - AnyCPU - pdbonly - true - bin\Release\ - TRACE;FRAMEWORK_LT_4 - prompt - 4 - - - true - bin\x64\Debug\ - TRACE;DEBUG;FRAMEWORK_LT_4 - full - x64 - prompt - MinimumRecommendedRules.ruleset - true - - - bin\x64\Release\ - TRACE;FRAMEWORK_LT_4 - true - pdbonly - x64 - prompt - MinimumRecommendedRules.ruleset - true - - - - Program.cs - - - - - - - - - {ec3db697-b734-42f7-9468-5b62821eeb5a} - Microsoft.Z3.NET35 - - - - - diff --git a/src/api/dotnet/dotnet35/Example/Properties/AssemblyInfo.cs b/src/api/dotnet/dotnet35/Example/Properties/AssemblyInfo.cs deleted file mode 100644 index ed0d8454f..000000000 --- a/src/api/dotnet/dotnet35/Example/Properties/AssemblyInfo.cs +++ /dev/null @@ -1,36 +0,0 @@ -using System.Reflection; -using System.Runtime.CompilerServices; -using System.Runtime.InteropServices; - -// General Information about an assembly is controlled through the following -// set of attributes. Change these attribute values to modify the information -// associated with an assembly. -[assembly: AssemblyTitle("Example")] -[assembly: AssemblyDescription("")] -[assembly: AssemblyConfiguration("")] -[assembly: AssemblyCompany("")] -[assembly: AssemblyProduct("Example")] -[assembly: AssemblyCopyright("Copyright © 2017")] -[assembly: AssemblyTrademark("")] -[assembly: AssemblyCulture("")] - -// Setting ComVisible to false makes the types in this assembly not visible -// to COM components. If you need to access a type in this assembly from -// COM, set the ComVisible attribute to true on that type. -[assembly: ComVisible(false)] - -// The following GUID is for the ID of the typelib if this project is exposed to COM -[assembly: Guid("2a8e577b-7b6d-4ca9-832a-ca2eec314812")] - -// Version information for an assembly consists of the following four values: -// -// Major Version -// Minor Version -// Build Number -// Revision -// -// You can specify all the values or you can default the Build and Revision Numbers -// by using the '*' as shown below: -// [assembly: AssemblyVersion("1.0.*")] -[assembly: AssemblyVersion("1.0.0.0")] -[assembly: AssemblyFileVersion("1.0.0.0")] diff --git a/src/api/dotnet/dotnet35/Microsoft.Z3.NET35.csproj b/src/api/dotnet/dotnet35/Microsoft.Z3.NET35.csproj deleted file mode 100644 index 15eaac445..000000000 --- a/src/api/dotnet/dotnet35/Microsoft.Z3.NET35.csproj +++ /dev/null @@ -1,347 +0,0 @@ - - - - Debug - AnyCPU - 8.0.30703 - 2.0 - {EC3DB697-B734-42F7-9468-5B62821EEB5A} - Library - Properties - Microsoft.Z3 - Microsoft.Z3 - v3.5 - 512 - - - 0 - - - true - full - false - Debug\ - TRACE;DEBUG;FRAMEWORK_LT_4 - prompt - 4 - true - Debug\Microsoft.Z3.XML - False - False - True - False - False - True - False - True - True - False - False - False - True - False - False - False - True - False - False - True - True - True - False - False - - - - - - - True - Full - %28none%29 - 2 - - - pdbonly - true - Release\ - FRAMEWORK_LT_4 - prompt - 4 - true - Release\Microsoft.Z3.xml - x86 - - - true - - - - - - - false - - - true - bin\x64\Debug\ - TRACE;DEBUG;FRAMEWORK_LT_4 - true - Debug\Microsoft.Z3.XML - full - x64 - prompt - MinimumRecommendedRules.ruleset - - - bin\x64\Release\ - FRAMEWORK_LT_4 - true - Release\Microsoft.Z3.xml - true - pdbonly - x64 - prompt - MinimumRecommendedRules.ruleset - - - - packages\Code.Contract.1.0.0\lib\net35\Microsoft.Contracts.dll - True - - - - - - - AlgebraicNum.cs - - - ApplyResult.cs - - - ArithExpr.cs - - - ArithSort.cs - - - ArrayExpr.cs - - - ArraySort.cs - - - AST.cs - - - ASTMap.cs - - - ASTVector.cs - - - BitVecExpr.cs - - - BitVecNum.cs - - - BitVecSort.cs - - - BoolExpr.cs - - - BoolSort.cs - - - Constructor.cs - - - ConstructorList.cs - - - Context.cs - - - DatatypeExpr.cs - - - DatatypeSort.cs - - - Deprecated.cs - - - Enumerations.cs - - - EnumSort.cs - - - Expr.cs - - - FiniteDomainExpr.cs - - - FiniteDomainNum.cs - - - FiniteDomainSort.cs - - - Fixedpoint.cs - - - FPExpr.cs - - - FPNum.cs - - - FPRMExpr.cs - - - FPRMNum.cs - - - FPRMSort.cs - - - FPSort.cs - - - FuncDecl.cs - - - FuncInterp.cs - - - Global.cs - - - Goal.cs - - - IDecRefQueue.cs - - - InterpolationContext.cs - - - IntExpr.cs - - - IntNum.cs - - - IntSort.cs - - - IntSymbol.cs - - - ListSort.cs - - - Log.cs - - - Model.cs - - - Native.cs - - - Optimize.cs - - - ParamDescrs.cs - - - Params.cs - - - Pattern.cs - - - Probe.cs - - - Quantifier.cs - - - RatNum.cs - - - RealExpr.cs - - - RealSort.cs - - - ReExpr.cs - - - RelationSort.cs - - - ReSort.cs - - - SeqExpr.cs - - - SeqSort.cs - - - SetSort.cs - - - Solver.cs - - - Sort.cs - - - Statistics.cs - - - Status.cs - - - StringSymbol.cs - - - Symbol.cs - - - Tactic.cs - - - TupleSort.cs - - - UninterpretedSort.cs - - - Version.cs - - - Z3Exception.cs - - - Z3Object.cs - - - - - - - - - - - diff --git a/src/api/dotnet/dotnet35/Microsoft.Z3.NET35.sln b/src/api/dotnet/dotnet35/Microsoft.Z3.NET35.sln deleted file mode 100644 index 1e33f136e..000000000 --- a/src/api/dotnet/dotnet35/Microsoft.Z3.NET35.sln +++ /dev/null @@ -1,48 +0,0 @@ - -Microsoft Visual Studio Solution File, Format Version 12.00 -# Visual Studio 14 -VisualStudioVersion = 14.0.25420.1 -MinimumVisualStudioVersion = 10.0.40219.1 -Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Microsoft.Z3.NET35", "Microsoft.Z3.NET35.csproj", "{EC3DB697-B734-42F7-9468-5B62821EEB5A}" -EndProject -Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Example", "Example\Example.csproj", "{2A8E577B-7B6D-4CA9-832A-CA2EEC314812}" -EndProject -Global - GlobalSection(SolutionConfigurationPlatforms) = preSolution - Debug|Any CPU = Debug|Any CPU - Debug|x64 = Debug|x64 - Debug|x86 = Debug|x86 - Release|Any CPU = Release|Any CPU - Release|x64 = Release|x64 - Release|x86 = Release|x86 - EndGlobalSection - GlobalSection(ProjectConfigurationPlatforms) = postSolution - {EC3DB697-B734-42F7-9468-5B62821EEB5A}.Debug|Any CPU.ActiveCfg = Debug|Any CPU - {EC3DB697-B734-42F7-9468-5B62821EEB5A}.Debug|Any CPU.Build.0 = Debug|Any CPU - {EC3DB697-B734-42F7-9468-5B62821EEB5A}.Debug|x64.ActiveCfg = Debug|Any CPU - {EC3DB697-B734-42F7-9468-5B62821EEB5A}.Debug|x64.Build.0 = Debug|Any CPU - {EC3DB697-B734-42F7-9468-5B62821EEB5A}.Debug|x86.ActiveCfg = Debug|Any CPU - {EC3DB697-B734-42F7-9468-5B62821EEB5A}.Debug|x86.Build.0 = Debug|Any CPU - {EC3DB697-B734-42F7-9468-5B62821EEB5A}.Release|Any CPU.ActiveCfg = Release|Any CPU - {EC3DB697-B734-42F7-9468-5B62821EEB5A}.Release|Any CPU.Build.0 = Release|Any CPU - {EC3DB697-B734-42F7-9468-5B62821EEB5A}.Release|x64.ActiveCfg = Release|x64 - {EC3DB697-B734-42F7-9468-5B62821EEB5A}.Release|x64.Build.0 = Release|x64 - {EC3DB697-B734-42F7-9468-5B62821EEB5A}.Release|x86.ActiveCfg = Release|Any CPU - {EC3DB697-B734-42F7-9468-5B62821EEB5A}.Release|x86.Build.0 = Release|Any CPU - {2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Debug|Any CPU.ActiveCfg = Debug|Any CPU - {2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Debug|Any CPU.Build.0 = Debug|Any CPU - {2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Debug|x64.ActiveCfg = Debug|Any CPU - {2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Debug|x64.Build.0 = Debug|Any CPU - {2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Debug|x86.ActiveCfg = Debug|Any CPU - {2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Debug|x86.Build.0 = Debug|Any CPU - {2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Release|Any CPU.ActiveCfg = Release|Any CPU - {2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Release|Any CPU.Build.0 = Release|Any CPU - {2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Release|x64.ActiveCfg = Release|x64 - {2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Release|x64.Build.0 = Release|x64 - {2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Release|x86.ActiveCfg = Release|Any CPU - {2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Release|x86.Build.0 = Release|Any CPU - EndGlobalSection - GlobalSection(SolutionProperties) = preSolution - HideSolutionNode = FALSE - EndGlobalSection -EndGlobal diff --git a/src/api/dotnet/dotnet35/Properties/AssemblyInfo.cs b/src/api/dotnet/dotnet35/Properties/AssemblyInfo.cs deleted file mode 100644 index fb4319002..000000000 --- a/src/api/dotnet/dotnet35/Properties/AssemblyInfo.cs +++ /dev/null @@ -1,38 +0,0 @@ -using System; -using System.Reflection; -using System.Runtime.CompilerServices; -using System.Runtime.InteropServices; -using System.Security.Permissions; - -// General Information about an assembly is controlled through the following -// set of attributes. Change these attribute values to modify the information -// associated with an assembly. -[assembly: AssemblyTitle("Z3 .NET Interface")] -[assembly: AssemblyDescription(".NET Interface to the Z3 Theorem Prover")] -[assembly: AssemblyConfiguration("")] -[assembly: AssemblyCompany("Microsoft Corporation")] -[assembly: AssemblyProduct("Z3")] -[assembly: AssemblyCopyright("Copyright (C) 2006-2015 Microsoft Corporation")] -[assembly: AssemblyTrademark("")] -[assembly: AssemblyCulture("")] - -// Setting ComVisible to false makes the types in this assembly not visible -// to COM components. If you need to access a type in this assembly from -// COM, set the ComVisible attribute to true on that type. -[assembly: ComVisible(false)] - -// The following GUID is for the ID of the typelib if this project is exposed to COM -[assembly: Guid("4853ed71-2078-40f4-8117-bc46646bce0e")] - -// Version information for an assembly consists of the following four values: -// -// Major Version -// Minor Version -// Build Number -// Revision -// -// You can specify all the values or you can default the Build and Revision Numbers -// by using the '*' as shown below: -// [assembly: AssemblyVersion("4.2.0.0")] -[assembly: AssemblyVersion("4.5.1.6031")] -[assembly: AssemblyFileVersion("4.5.1.6031")] diff --git a/src/api/dotnet/dotnet35/Properties/AssemblyInfo.cs.in b/src/api/dotnet/dotnet35/Properties/AssemblyInfo.cs.in deleted file mode 100644 index e5a85f16f..000000000 --- a/src/api/dotnet/dotnet35/Properties/AssemblyInfo.cs.in +++ /dev/null @@ -1,38 +0,0 @@ -using System; -using System.Reflection; -using System.Runtime.CompilerServices; -using System.Runtime.InteropServices; -using System.Security.Permissions; - -// General Information about an assembly is controlled through the following -// set of attributes. Change these attribute values to modify the information -// associated with an assembly. -[assembly: AssemblyTitle("Z3 .NET Interface")] -[assembly: AssemblyDescription(".NET Interface to the Z3 Theorem Prover")] -[assembly: AssemblyConfiguration("")] -[assembly: AssemblyCompany("Microsoft Corporation")] -[assembly: AssemblyProduct("Z3")] -[assembly: AssemblyCopyright("Copyright (C) 2006-2015 Microsoft Corporation")] -[assembly: AssemblyTrademark("")] -[assembly: AssemblyCulture("")] - -// Setting ComVisible to false makes the types in this assembly not visible -// to COM components. If you need to access a type in this assembly from -// COM, set the ComVisible attribute to true on that type. -[assembly: ComVisible(false)] - -// The following GUID is for the ID of the typelib if this project is exposed to COM -[assembly: Guid("4853ed71-2078-40f4-8117-bc46646bce0e")] - -// Version information for an assembly consists of the following four values: -// -// Major Version -// Minor Version -// Build Number -// Revision -// -// You can specify all the values or you can default the Build and Revision Numbers -// by using the '*' as shown below: -// [assembly: AssemblyVersion("4.2.0.0")] -[assembly: AssemblyVersion("@VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@")] -[assembly: AssemblyFileVersion("@VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@")] diff --git a/src/api/dotnet/dotnet35/Readme.NET35 b/src/api/dotnet/dotnet35/Readme.NET35 deleted file mode 100644 index f8c2958ee..000000000 --- a/src/api/dotnet/dotnet35/Readme.NET35 +++ /dev/null @@ -1,10 +0,0 @@ -The default Z3 bindings for .NET are built for the .NET framework version 4. -Should the need arise, it is also possible to build them for .NET 3.5; the -instructions are as follows: - -In the project properties of Microsoft.Z3.csproj: -- Under 'Application': Change Target framework to .NET Framework 3.5 -- Under 'Build': Add FRAMEWORK_LT_4 to the condidional compilation symbols -- Remove the reference to System.Numerics -- Install the NuGet Package "Microsoft Code Contracts for Net3.5": - In the Package Manager Console enter Install-Package Code.Contract diff --git a/src/api/dotnet/dotnet35/packages.config b/src/api/dotnet/dotnet35/packages.config deleted file mode 100644 index bc9f365bc..000000000 --- a/src/api/dotnet/dotnet35/packages.config +++ /dev/null @@ -1,4 +0,0 @@ - - - - From 232a88101bf6a5867f0e038746decefee86fd47b Mon Sep 17 00:00:00 2001 From: Yatao Li Date: Mon, 10 Sep 2018 08:57:28 +0800 Subject: [PATCH 02/32] api: dotnet: ADD_DOTNET should be uppercased. --- src/api/dotnet/CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/dotnet/CMakeLists.txt b/src/api/dotnet/CMakeLists.txt index 987ef3dff..2d9b32a2f 100644 --- a/src/api/dotnet/CMakeLists.txt +++ b/src/api/dotnet/CMakeLists.txt @@ -139,7 +139,7 @@ endforeach() # And thus we can put the conditional properties in the project file. 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 +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}" PACKAGE Microsoft.Z3) From 90890e46a95a66660035f926b6713e558091a017 Mon Sep 17 00:00:00 2001 From: Yatao Li Date: Mon, 10 Sep 2018 09:34:28 +0800 Subject: [PATCH 03/32] api: dotnet: FindDotnet.cmake now handles 'REQUIRED' option. --- cmake/modules/FindDotnet.cmake | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/cmake/modules/FindDotnet.cmake b/cmake/modules/FindDotnet.cmake index a3d0c2dd1..4ca792ed6 100644 --- a/cmake/modules/FindDotnet.cmake +++ b/cmake/modules/FindDotnet.cmake @@ -56,7 +56,7 @@ # # Require 3.5 for batch copy multiple files -CMAKE_MINIMUM_REQUIRED(VERSION 3.5.0) +cmake_minimum_required(VERSION 3.5.0) IF(DOTNET_FOUND) RETURN() @@ -68,6 +68,9 @@ SET(DOTNET_MODULE_DIR ${CMAKE_CURRENT_LIST_DIR}) IF(NOT DOTNET_EXE) SET(DOTNET_FOUND FALSE) + IF(Dotnet_FIND_REQUIRED) + MESSAGE(SEND_ERROR "Command 'dotnet' is not found.") + ENDIF() RETURN() ENDIF() From 969a922145e3f7a96298143ac03cd31fb61ab5b9 Mon Sep 17 00:00:00 2001 From: Yatao Li Date: Mon, 10 Sep 2018 13:19:48 +0800 Subject: [PATCH 04/32] 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 @@ - + @@ -58,11 +58,13 @@ ${Z3_DOTNET_COMPILE_ITEMS} - - + + runtimes\win-x64\native - + + runtimes\linux-x64\native + From 534de98ff36a89613ecdfefaf83faf204983f4b6 Mon Sep 17 00:00:00 2001 From: Yatao Li Date: Mon, 10 Sep 2018 15:05:22 +0800 Subject: [PATCH 05/32] fine-tune native assembly packing --- src/api/dotnet/CMakeLists.txt | 2 +- src/api/dotnet/Microsoft.Z3.csproj.in | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/dotnet/CMakeLists.txt b/src/api/dotnet/CMakeLists.txt index 6a70f43b5..07091cab9 100644 --- a/src/api/dotnet/CMakeLists.txt +++ b/src/api/dotnet/CMakeLists.txt @@ -142,7 +142,7 @@ 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 VERSION ${Z3_DOTNET_NUPKG_VERSION} - SOURCES ${CMAKE_CURRENT_SOURCE_DIR}/Microsoft.Z3.csproj.in + SOURCES ${CMAKE_CURRENT_SOURCE_DIR}/Microsoft.Z3.csproj.in ${Z3_DOTNET_ASSEMBLY_SOURCES} PACKAGE Microsoft.Z3) add_dependencies(BUILD_Microsoft.Z3 libz3) diff --git a/src/api/dotnet/Microsoft.Z3.csproj.in b/src/api/dotnet/Microsoft.Z3.csproj.in index cbbddc63f..01d18def9 100644 --- a/src/api/dotnet/Microsoft.Z3.csproj.in +++ b/src/api/dotnet/Microsoft.Z3.csproj.in @@ -59,7 +59,7 @@ ${Z3_DOTNET_COMPILE_ITEMS} - + runtimes\win-x64\native From 5c81559f71c5278284cad64e4037a55feafd304c Mon Sep 17 00:00:00 2001 From: Yatao Li Date: Mon, 10 Sep 2018 16:02:09 +0800 Subject: [PATCH 06/32] api: dotnet: copy native binary to output folder only for non-netstandard, non-netcoreapp TFMs. --- src/api/dotnet/Microsoft.Z3.targets | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/dotnet/Microsoft.Z3.targets b/src/api/dotnet/Microsoft.Z3.targets index 80179ce4c..9eba049c6 100644 --- a/src/api/dotnet/Microsoft.Z3.targets +++ b/src/api/dotnet/Microsoft.Z3.targets @@ -1,7 +1,7 @@ - + %(RecursiveDir)%(FileName)%(Extension) PreserveNewest From e787c01d4128056870539353e2c7d84fc51a92e1 Mon Sep 17 00:00:00 2001 From: Yatao Li Date: Mon, 10 Sep 2018 16:40:22 +0800 Subject: [PATCH 07/32] ... --- src/api/dotnet/CMakeLists.txt | 5 ++++- src/api/dotnet/Microsoft.Z3.targets | 2 +- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/api/dotnet/CMakeLists.txt b/src/api/dotnet/CMakeLists.txt index 07091cab9..b2909f03c 100644 --- a/src/api/dotnet/CMakeLists.txt +++ b/src/api/dotnet/CMakeLists.txt @@ -142,7 +142,10 @@ 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 VERSION ${Z3_DOTNET_NUPKG_VERSION} - SOURCES ${CMAKE_CURRENT_SOURCE_DIR}/Microsoft.Z3.csproj.in ${Z3_DOTNET_ASSEMBLY_SOURCES} + SOURCES ${CMAKE_CURRENT_SOURCE_DIR}/Microsoft.Z3.csproj.in + ${CMAKE_CURRENT_SOURCE_DIR}/Microsoft.Z3.props + ${CMAKE_CURRENT_SOURCE_DIR}/Microsoft.Z3.targets + ${Z3_DOTNET_ASSEMBLY_SOURCES} PACKAGE Microsoft.Z3) add_dependencies(BUILD_Microsoft.Z3 libz3) diff --git a/src/api/dotnet/Microsoft.Z3.targets b/src/api/dotnet/Microsoft.Z3.targets index 9eba049c6..38e56b350 100644 --- a/src/api/dotnet/Microsoft.Z3.targets +++ b/src/api/dotnet/Microsoft.Z3.targets @@ -1,7 +1,7 @@ - + %(RecursiveDir)%(FileName)%(Extension) PreserveNewest From a162a60d9ce372da826d65eb2e637011ff3f48d7 Mon Sep 17 00:00:00 2001 From: Yatao Li Date: Tue, 11 Sep 2018 23:16:45 +0800 Subject: [PATCH 08/32] CI: trying to incorporate .net sdk into travis build --- .travis.yml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.travis.yml b/.travis.yml index 9ec6132b6..7776c3f58 100644 --- a/.travis.yml +++ b/.travis.yml @@ -74,6 +74,8 @@ env: - LINUX_BASE=ubuntu_14.04 C_COMPILER=/usr/bin/gcc-4.8 CXX_COMPILER=/usr/bin/g++-4.8 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=RelWithDebInfo # 64-bit GCC 4.8 Debug - LINUX_BASE=ubuntu_14.04 C_COMPILER=/usr/bin/gcc-4.8 CXX_COMPILER=/usr/bin/g++-4.8 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug RUN_UNIT_TESTS=BUILD_ONLY + include: + - dotnet: 2.1.4 # macOS (a.k.a OSX) support matrix: @@ -85,6 +87,7 @@ matrix: osx_image: xcode8.3 # Note: Apple Clang does not support OpenMP env: Z3_BUILD_TYPE=RelWithDebInfo USE_OPENMP=0 DOTNET_BINDINGS=0 + - dotnet: 2.1.4 script: # Use `travis_wait` when doing LTO builds because this configuration will # have long link times during which it will not show any output which From 538272d2d5526f19853e5d801889c2d332e76212 Mon Sep 17 00:00:00 2001 From: Yatao Li Date: Tue, 11 Sep 2018 23:32:29 +0800 Subject: [PATCH 09/32] CI: 2nd attempt: trying to incorporate .net sdk into travis build --- .travis.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.travis.yml b/.travis.yml index 7776c3f58..51e08a703 100644 --- a/.travis.yml +++ b/.travis.yml @@ -5,6 +5,7 @@ cache: - $DOCKER_TRAVIS_CI_CACHE_DIR sudo: required language: cpp +dotnet: 2.1.4 services: - docker env: @@ -74,8 +75,6 @@ env: - LINUX_BASE=ubuntu_14.04 C_COMPILER=/usr/bin/gcc-4.8 CXX_COMPILER=/usr/bin/g++-4.8 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=RelWithDebInfo # 64-bit GCC 4.8 Debug - LINUX_BASE=ubuntu_14.04 C_COMPILER=/usr/bin/gcc-4.8 CXX_COMPILER=/usr/bin/g++-4.8 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug RUN_UNIT_TESTS=BUILD_ONLY - include: - - dotnet: 2.1.4 # macOS (a.k.a OSX) support matrix: @@ -87,8 +86,9 @@ matrix: osx_image: xcode8.3 # Note: Apple Clang does not support OpenMP env: Z3_BUILD_TYPE=RelWithDebInfo USE_OPENMP=0 DOTNET_BINDINGS=0 - - dotnet: 2.1.4 script: + # Add at least one dotnet command invocation to activate the build env. + - dotnet restore # Use `travis_wait` when doing LTO builds because this configuration will # have long link times during which it will not show any output which # TravisCI might kill due to perceived inactivity. From 44e21d99489a6a12d020ad890bb952fda8d41ec2 Mon Sep 17 00:00:00 2001 From: Yatao Li Date: Tue, 11 Sep 2018 23:37:26 +0800 Subject: [PATCH 10/32] CI: 3rd attempt: trying to incorporate .net sdk into travis build --- .travis.yml | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/.travis.yml b/.travis.yml index 51e08a703..038874c0d 100644 --- a/.travis.yml +++ b/.travis.yml @@ -5,7 +5,6 @@ cache: - $DOCKER_TRAVIS_CI_CACHE_DIR sudo: required language: cpp -dotnet: 2.1.4 services: - docker env: @@ -86,9 +85,15 @@ matrix: osx_image: xcode8.3 # Note: Apple Clang does not support OpenMP env: Z3_BUILD_TYPE=RelWithDebInfo USE_OPENMP=0 DOTNET_BINDINGS=0 + +matrix: + include: + - language: csharp + dotnet: 2.1.4 + script: + # Add at least one dotnet command invocation to activate the build env. + - dotnet restore script: - # Add at least one dotnet command invocation to activate the build env. - - dotnet restore # Use `travis_wait` when doing LTO builds because this configuration will # have long link times during which it will not show any output which # TravisCI might kill due to perceived inactivity. From 5bc7a5d67324c14059ec9edaaf778f6f7fddcf44 Mon Sep 17 00:00:00 2001 From: Yatao Li Date: Wed, 12 Sep 2018 00:29:58 +0800 Subject: [PATCH 11/32] CI: configure dotnet via docker --- .travis.yml | 7 ------- contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile | 5 +++-- contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile | 8 ++++++-- contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile | 8 ++++++-- 4 files changed, 15 insertions(+), 13 deletions(-) diff --git a/.travis.yml b/.travis.yml index 038874c0d..076b3a554 100644 --- a/.travis.yml +++ b/.travis.yml @@ -86,13 +86,6 @@ matrix: # Note: Apple Clang does not support OpenMP env: Z3_BUILD_TYPE=RelWithDebInfo USE_OPENMP=0 DOTNET_BINDINGS=0 -matrix: - include: - - language: csharp - dotnet: 2.1.4 - script: - # Add at least one dotnet command invocation to activate the build env. - - dotnet restore script: # Use `travis_wait` when doing LTO builds because this configuration will # have long link times during which it will not show any output which diff --git a/contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile b/contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile index 87e3c8d67..6012bb25f 100644 --- a/contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile +++ b/contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile @@ -32,7 +32,6 @@ RUN apt-get update && \ libomp-dev \ llvm-3.9 \ make \ - mono-devel \ ninja-build \ python3 \ python3-setuptools \ @@ -48,4 +47,6 @@ RUN useradd -m user && \ echo 'user ALL=(root) NOPASSWD: ALL' >> /etc/sudoers USER user WORKDIR /home/user -ENV ASAN_SYMBOLIZER_PATH=/usr/lib/llvm-3.9/bin/llvm-symbolizer +# TODO .NET core does not support Linux x86 yet, disable it for now. +# see: https://github.com/dotnet/coreclr/issues/9265 +ENV ASAN_SYMBOLIZER_PATH=/usr/lib/llvm-3.9/bin/llvm-symbolizer DOTNET_BINDINGS=0 diff --git a/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile b/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile index c963ce255..15144fa8e 100644 --- a/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile +++ b/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile @@ -1,5 +1,9 @@ FROM ubuntu:14.04 +RUN wget -q https://packages.microsoft.com/config/ubuntu/16.04/packages-microsoft-prod.deb && \ + dpkg -i packages-microsoft-prod.deb && \ + apt-get install apt-transport-https + RUN apt-get update && \ apt-get -y --no-install-recommends install \ binutils \ @@ -18,12 +22,12 @@ RUN apt-get update && \ lib32gomp1 \ llvm-3.9 \ make \ - mono-devel \ ninja-build \ python3 \ python3-setuptools \ python2.7 \ - python-setuptools + python-setuptools \ + dotnet-sdk-2.1 # Create `user` user for container with password `user`. and give it # password-less sudo access diff --git a/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile b/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile index 08686e275..1963a4ad3 100644 --- a/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile +++ b/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile @@ -1,5 +1,9 @@ FROM ubuntu:16.04 +RUN wget -q https://packages.microsoft.com/config/ubuntu/16.04/packages-microsoft-prod.deb && \ + dpkg -i packages-microsoft-prod.deb && \ + apt-get install apt-transport-https + RUN apt-get update && \ apt-get -y --no-install-recommends install \ binutils \ @@ -20,13 +24,13 @@ RUN apt-get update && \ libomp-dev \ llvm-3.9 \ make \ - mono-devel \ ninja-build \ python3 \ python3-setuptools \ python2.7 \ python-setuptools \ - sudo + sudo \ + dotnet-sdk-2.1 # Create `user` user for container with password `user`. and give it # password-less sudo access From 5fdf3ff7996a9ce7e58f4990a21dca3f3e735597 Mon Sep 17 00:00:00 2001 From: Yatao Li Date: Wed, 12 Sep 2018 00:37:06 +0800 Subject: [PATCH 12/32] CI: Dockerfile: use curl instead of wget --- contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile | 2 +- contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile b/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile index 15144fa8e..ce78e7fb9 100644 --- a/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile +++ b/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile @@ -1,6 +1,6 @@ FROM ubuntu:14.04 -RUN wget -q https://packages.microsoft.com/config/ubuntu/16.04/packages-microsoft-prod.deb && \ +RUN curl -SL https://packages.microsoft.com/config/ubuntu/16.04/packages-microsoft-prod.deb --output packages-microsoft-prod.deb && \ dpkg -i packages-microsoft-prod.deb && \ apt-get install apt-transport-https diff --git a/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile b/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile index 1963a4ad3..efa1d5600 100644 --- a/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile +++ b/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile @@ -1,6 +1,6 @@ FROM ubuntu:16.04 -RUN wget -q https://packages.microsoft.com/config/ubuntu/16.04/packages-microsoft-prod.deb && \ +RUN curl -SL https://packages.microsoft.com/config/ubuntu/16.04/packages-microsoft-prod.deb --output packages-microsoft-prod.deb && \ dpkg -i packages-microsoft-prod.deb && \ apt-get install apt-transport-https From 5474e1675a8b75f4e01ae3620c27f435d6466c77 Mon Sep 17 00:00:00 2001 From: Yatao Li Date: Wed, 12 Sep 2018 00:53:10 +0800 Subject: [PATCH 13/32] CI: Dockerfile: install curl before dotnet --- .../ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile | 14 ++++++++------ .../ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile | 14 ++++++++------ 2 files changed, 16 insertions(+), 12 deletions(-) diff --git a/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile b/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile index ce78e7fb9..f6541a2c9 100644 --- a/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile +++ b/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile @@ -1,14 +1,12 @@ FROM ubuntu:14.04 -RUN curl -SL https://packages.microsoft.com/config/ubuntu/16.04/packages-microsoft-prod.deb --output packages-microsoft-prod.deb && \ - dpkg -i packages-microsoft-prod.deb && \ - apt-get install apt-transport-https - RUN apt-get update && \ apt-get -y --no-install-recommends install \ + apt-transport-https \ binutils \ clang-3.9 \ cmake \ + curl \ doxygen \ default-jdk \ gcc-multilib \ @@ -26,8 +24,12 @@ RUN apt-get update && \ python3 \ python3-setuptools \ python2.7 \ - python-setuptools \ - dotnet-sdk-2.1 + python-setuptools + +RUN curl -SL https://packages.microsoft.com/config/ubuntu/16.04/packages-microsoft-prod.deb --output packages-microsoft-prod.deb && \ + dpkg -i packages-microsoft-prod.deb && \ + apt-get update && \ + apt-get -y --no-install-recommends install dotnet-sdk-2.1 # Create `user` user for container with password `user`. and give it # password-less sudo access diff --git a/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile b/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile index efa1d5600..f4d9c873a 100644 --- a/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile +++ b/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile @@ -1,15 +1,13 @@ FROM ubuntu:16.04 -RUN curl -SL https://packages.microsoft.com/config/ubuntu/16.04/packages-microsoft-prod.deb --output packages-microsoft-prod.deb && \ - dpkg -i packages-microsoft-prod.deb && \ - apt-get install apt-transport-https - RUN apt-get update && \ apt-get -y --no-install-recommends install \ + apt-transport-https \ binutils \ clang \ clang-3.9 \ cmake \ + curl \ doxygen \ default-jdk \ gcc-multilib \ @@ -29,8 +27,12 @@ RUN apt-get update && \ python3-setuptools \ python2.7 \ python-setuptools \ - sudo \ - dotnet-sdk-2.1 + sudo + +RUN curl -SL https://packages.microsoft.com/config/ubuntu/16.04/packages-microsoft-prod.deb --output packages-microsoft-prod.deb && \ + dpkg -i packages-microsoft-prod.deb && \ + apt-get update && \ + apt-get -y --no-install-recommends install dotnet-sdk-2.1 # Create `user` user for container with password `user`. and give it # password-less sudo access From 20c128d3fa2212fa937a6de7d6b4a5317526aa6e Mon Sep 17 00:00:00 2001 From: Yatao Li Date: Wed, 12 Sep 2018 01:28:42 +0800 Subject: [PATCH 14/32] replace LIST FILTER with handrolled implementation to cancel cmake v3.6+ dependency --- cmake/modules/FindDotnet.cmake | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/cmake/modules/FindDotnet.cmake b/cmake/modules/FindDotnet.cmake index ed1186999..625317a41 100644 --- a/cmake/modules/FindDotnet.cmake +++ b/cmake/modules/FindDotnet.cmake @@ -125,7 +125,12 @@ FUNCTION(DOTNET_GET_DEPS _DN_PROJECT arguments) ${arguments}) LIST(APPEND DOTNET_deps ${_DN_SOURCES}) - LIST(FILTER DOTNET_deps EXCLUDE REGEX /obj/) + SET(_DN_deps "") + FOREACH(dep ${DOTNET_deps}) + IF(NOT dep MATCHES /obj/) + LIST(APPEND _DN_deps ${dep}) + ENDIF() + ENDFOREACH() GET_FILENAME_COMPONENT(_DN_abs_proj "${_DN_PROJECT}" ABSOLUTE) GET_FILENAME_COMPONENT(_DN_proj_dir "${_DN_PROJECT}" DIRECTORY) @@ -178,7 +183,7 @@ FUNCTION(DOTNET_GET_DEPS _DN_PROJECT arguments) SET(DOTNET_RUN_OUTPUT ${_DN_OUTPUT} PARENT_SCOPE) SET(DOTNET_PACKAGE_VERSION ${_DN_VERSION} PARENT_SCOPE) SET(DOTNET_OUTPUT_PATH ${_DN_OUTPUT_PATH} PARENT_SCOPE) - SET(DOTNET_deps ${DOTNET_deps} PARENT_SCOPE) + SET(DOTNET_deps ${_DN_deps} PARENT_SCOPE) IF(_DN_PLATFORM) SET(_DN_PLATFORM_PROP "/p:Platform=${_DN_PLATFORM}") From aae28bd0eb6f2b2be9107ec59ad650c87690f8b7 Mon Sep 17 00:00:00 2001 From: Yatao Li Date: Wed, 12 Sep 2018 14:26:21 +0800 Subject: [PATCH 15/32] CI: update dotnet example to coreclr 2.0 --- contrib/ci/scripts/test_z3_examples_cmake.sh | 4 ++-- examples/dotnet/dotnet.csproj | 12 ++++++++++++ 2 files changed, 14 insertions(+), 2 deletions(-) create mode 100644 examples/dotnet/dotnet.csproj diff --git a/contrib/ci/scripts/test_z3_examples_cmake.sh b/contrib/ci/scripts/test_z3_examples_cmake.sh index 687efebb4..a1de9f375 100755 --- a/contrib/ci/scripts/test_z3_examples_cmake.sh +++ b/contrib/ci/scripts/test_z3_examples_cmake.sh @@ -91,8 +91,8 @@ if [ "X${DOTNET_BINDINGS}" = "X1" ]; then # Build .NET example # FIXME: Move compliation step into CMake target mcs ${Z3_SRC_DIR}/examples/dotnet/Program.cs /target:exe /out:dotnet_test.exe /reference:Microsoft.Z3.dll /r:System.Numerics.dll - # Run .NET example - run_quiet run_non_native_binding mono ./dotnet_test.exe + # Build & Run .NET example + run_quiet run_non_native_binding dotnet run -p ${Z3_SRC_DIR}/examples/dotnet/dotnet.csproj fi if [ "X${JAVA_BINDINGS}" = "X1" ]; then diff --git a/examples/dotnet/dotnet.csproj b/examples/dotnet/dotnet.csproj new file mode 100644 index 000000000..0dc4ee2ec --- /dev/null +++ b/examples/dotnet/dotnet.csproj @@ -0,0 +1,12 @@ + + + + Exe + netcoreapp2.0 + + + + + + + From 461c32e11e5fa529475962f830664fcd0a1d9bea Mon Sep 17 00:00:00 2001 From: Yatao Li Date: Wed, 12 Sep 2018 16:07:45 +0800 Subject: [PATCH 16/32] ... --- contrib/ci/scripts/test_z3_examples_cmake.sh | 3 --- 1 file changed, 3 deletions(-) diff --git a/contrib/ci/scripts/test_z3_examples_cmake.sh b/contrib/ci/scripts/test_z3_examples_cmake.sh index a1de9f375..679fc4a69 100755 --- a/contrib/ci/scripts/test_z3_examples_cmake.sh +++ b/contrib/ci/scripts/test_z3_examples_cmake.sh @@ -88,9 +88,6 @@ if [ "X${PYTHON_BINDINGS}" = "X1" ]; then fi if [ "X${DOTNET_BINDINGS}" = "X1" ]; then - # Build .NET example - # FIXME: Move compliation step into CMake target - mcs ${Z3_SRC_DIR}/examples/dotnet/Program.cs /target:exe /out:dotnet_test.exe /reference:Microsoft.Z3.dll /r:System.Numerics.dll # Build & Run .NET example run_quiet run_non_native_binding dotnet run -p ${Z3_SRC_DIR}/examples/dotnet/dotnet.csproj fi From 519098b73d5f555dc833b861fb3fed96734a4cbd Mon Sep 17 00:00:00 2001 From: Yatao Li Date: Wed, 17 Oct 2018 11:27:20 +0800 Subject: [PATCH 17/32] fix nuget props package path detection --- src/api/dotnet/Microsoft.Z3.props | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/dotnet/Microsoft.Z3.props b/src/api/dotnet/Microsoft.Z3.props index 67bb471ba..290cc5f86 100644 --- a/src/api/dotnet/Microsoft.Z3.props +++ b/src/api/dotnet/Microsoft.Z3.props @@ -7,8 +7,8 @@ true true - - $(MSBuildThisFileDirectory)..\..\ + + $(MSBuildThisFileDirectory)..\ $(Z3_PACKAGE_PATH)runtimes\win-x64\native\libz3.dll $(Z3_PACKAGE_PATH)runtimes\linux-x64\native\libz3.so From b72cb96ee3a94d8a9402b2f87a499c975ce828f0 Mon Sep 17 00:00:00 2001 From: Yatao Li Date: Sat, 29 Dec 2018 16:43:08 +0800 Subject: [PATCH 18/32] update dotnet cmake module --- cmake/modules/FindDotnet.cmake | 179 ++++++++++++++++++++++++++++----- src/api/dotnet/CMakeLists.txt | 2 + 2 files changed, 158 insertions(+), 23 deletions(-) diff --git a/cmake/modules/FindDotnet.cmake b/cmake/modules/FindDotnet.cmake index 625317a41..f424d3f23 100644 --- a/cmake/modules/FindDotnet.cmake +++ b/cmake/modules/FindDotnet.cmake @@ -23,6 +23,8 @@ # [PACKAGE output_nuget_packages... ] # [VERSION nuget_package_version] # [DEPENDS depend_nuget_packages... ] +# [OUTPUT_PATH output_path relative to cmake binary output dir] +# [CUSTOM_BUILDPROPS value....] # [SOURCES additional_file_dependencies... ]) # ``` # @@ -43,18 +45,58 @@ # [PLATFORM platform] # [PACKAGE output_nuget_packages... ] # [DEPENDS depend_nuget_packages... ] +# [CUSTOM_BUILDPROPS value....] # [SOURCES additional_file_dependencies... ]) # ``` # +# SMOKETEST_DOTNET -- add a dotnet smoke test project to the build. The project will be run during a build, +# and if the program fails to build or run, the build fails. Currently only .NET Core App framework is supported. +# Multiple smoke tests will be run one-by-one to avoid global resource conflicts. +# +# SMOKETEST_DOTNET( [RELEASE|DEBUG] [X86|X64|ANYCPU] [NETCOREAPP] +# [CONFIG configuration] +# [PLATFORM platform] +# [PACKAGE output_nuget_packages... ] +# [VERSION nuget_package_version] +# [DEPENDS depend_nuget_packages... ] +# [CUSTOM_BUILDPROPS value....] +# [SOURCES additional_file_dependencies... ]) +# +# For all the above functions, `RELEASE|DEBUG` overrides `CONFIG`, `X86|X64|ANYCPU` overrides PLATFORM. +# For Unix systems, the target framework defaults to `netstandard2.0`, unless `NETCOREAPP` is specified. +# For Windows, the project is built as-is, allowing multi-targeting. +# +# # DOTNET_REGISTER_LOCAL_REPOSITORY -- register a local NuGet package repository. # # ``` # DOTNET_REGISTER_LOCAL_REPOSITORY(repo_name repo_path) # ``` +# +# TEST_DOTNET -- add a dotnet test project to ctest. The project will be run with `dotnet test`, +# and trx test reports will be generated in the build directory. For Windows, all target frameworks +# are tested against. For other platforms, only .NET Core App is tested against. +# Test failures will not fail the build. +# Tests are only run with `ctest -C `, not with `cmake --build ...` +# +# ``` +# TEST_DOTNET( +# [ARGUMENTS additional_dotnet_test_args...]) +# ``` # -# For all the above functions, `RELEASE|DEBUG` overrides `CONFIG`, `X86|X64|ANYCPU` overrides PLATFORM. -# For Unix systems, the target framework defaults to `netstandard2.0`, unless `NETCOREAPP` is specified. -# For Windows, the project is built as-is, allowing multi-targeting. +# GEN_DOTNET_PROPS -- Generates a Directory.Build.props file. The created file is populated with MSBuild properties: +# - 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 +# to the cmake build directory. +# - Custom properties can be injected with XML_INJECT argument, which injects an arbitrary string into the project XML file. +# +# ``` +# GEN_DOTNET_PROPS( +# [PACKAGE_VERSION version] +# [XML_INJECT xml_injection]) +# ``` # # Require 3.5 for batch copy multiple files @@ -118,9 +160,9 @@ FUNCTION(DOTNET_GET_DEPS _DN_PROJECT arguments) # options (flags) "RELEASE;DEBUG;X86;X64;ANYCPU;NETCOREAPP" # oneValueArgs - "CONFIG;PLATFORM;VERSION" + "CONFIG;PLATFORM;VERSION;OUTPUT_PATH" # multiValueArgs - "PACKAGE;DEPENDS;ARGUMENTS;OUTPUT;SOURCES" + "PACKAGE;DEPENDS;ARGUMENTS;OUTPUT;SOURCES;CUSTOM_BUILDPROPS" # the input arguments ${arguments}) @@ -170,7 +212,19 @@ FUNCTION(DOTNET_GET_DEPS _DN_PROJECT arguments) SET(_DN_VERSION "1.0.0") ENDIF() - GET_FILENAME_COMPONENT(_DN_OUTPUT_PATH ${CMAKE_CURRENT_BINARY_DIR}/bin ABSOLUTE) + # Set the output path to the current binary directory. + # Build outputs in separated output directories prevent overwriting. + # Later we then copy the outputs to the destination. + + IF(NOT _DN_OUTPUT_PATH) + SET(_DN_OUTPUT_PATH "bin") + ENDIF() + + GET_FILENAME_COMPONENT(_DN_OUTPUT_PATH ${CMAKE_CURRENT_BINARY_DIR}/${_DN_OUTPUT_PATH} ABSOLUTE) + + # In a cmake build, the XPLAT libraries are always copied over. + # Set the proper directory for .NET projects. + SET(_DN_XPLAT_LIB_DIR ${CMAKE_BINARY_DIR}) SET(DOTNET_PACKAGES ${_DN_PACKAGE} PARENT_SCOPE) SET(DOTNET_CONFIG ${_DN_CONFIG} PARENT_SCOPE) @@ -200,16 +254,18 @@ FUNCTION(DOTNET_GET_DEPS _DN_PROJECT arguments) SET(_DN_IMPORT_PROP ${CMAKE_CURRENT_BINARY_DIR}/${_DN_projname}.imports.props) CONFIGURE_FILE(${DOTNET_MODULE_DIR}/DotnetImports.props.in ${_DN_IMPORT_PROP}) + SET(_DN_IMPORT_ARGS "/p:DirectoryBuildPropsPath=${_DN_IMPORT_PROP}") - SET(DOTNET_BUILD_PROPERTIES ${_DN_PLATFORM_PROP} ${_DN_TFMS_PROP} "/p:DirectoryBuildPropsPath=${_DN_IMPORT_PROP}" "/p:DOTNET_PACKAGE_VERSION=${_DN_VERSION}" PARENT_SCOPE) + SET(DOTNET_IMPORT_PROPERTIES ${_DN_IMPORT_ARGS} PARENT_SCOPE) + SET(DOTNET_BUILD_PROPERTIES ${_DN_PLATFORM_PROP} ${_DN_IMPORT_ARGS} PARENT_SCOPE) SET(DOTNET_BUILD_OPTIONS ${_DN_BUILD_OPTIONS} PARENT_SCOPE) - SET(DOTNET_PACK_OPTIONS ${_DN_PACK_OPTIONS} PARENT_SCOPE) + SET(DOTNET_PACK_OPTIONS --include-symbols ${_DN_PACK_OPTIONS} PARENT_SCOPE) ENDFUNCTION() -MACRO(ADD_DOTNET_DEPENDENCY_TARGETS) +MACRO(ADD_DOTNET_DEPENDENCY_TARGETS tgt) FOREACH(pkg_dep ${DOTNET_DEPENDS}) - ADD_DEPENDENCIES(BUILD_${DOTNET_PROJNAME} PKG_${pkg_dep}) + ADD_DEPENDENCIES(${tgt}_${DOTNET_PROJNAME} PKG_${pkg_dep}) MESSAGE(" ${DOTNET_PROJNAME} <- ${pkg_dep}") ENDFOREACH() @@ -227,11 +283,11 @@ MACRO(ADD_DOTNET_DEPENDENCY_TARGETS) COMMAND ${rm_command} DEPENDS ${DOTNET_deps} ) - ADD_DEPENDENCIES(BUILD_${DOTNET_PROJNAME} DOTNET_PURGE_${pkg}) + ADD_DEPENDENCIES(${tgt}_${DOTNET_PROJNAME} DOTNET_PURGE_${pkg}) # Add a target for the built package -- this can be referenced in # another project. ADD_CUSTOM_TARGET(PKG_${pkg}) - ADD_DEPENDENCIES(PKG_${pkg} BUILD_${DOTNET_PROJNAME}) + ADD_DEPENDENCIES(PKG_${pkg} ${tgt}_${DOTNET_PROJNAME}) MESSAGE("==== ${DOTNET_PROJNAME} -> ${pkg}") ENDFOREACH() ENDMACRO() @@ -240,42 +296,45 @@ MACRO(DOTNET_BUILD_COMMANDS) IF(${DOTNET_IS_MSBUILD}) SET(build_dotnet_cmds COMMAND ${CMAKE_COMMAND} -E echo "=======> Building msbuild project ${DOTNET_PROJNAME} [${DOTNET_CONFIG} ${DOTNET_PLATFORM}]" - COMMAND ${NUGET_EXE} restore ${DOTNET_PROJPATH} + COMMAND ${NUGET_EXE} restore ${DOTNET_PROJPATH} -PackagesDirectory packages COMMAND ${DOTNET_EXE} msbuild ${DOTNET_PROJPATH} /t:Clean /p:Configuration="${DOTNET_CONFIG}" COMMAND ${DOTNET_EXE} msbuild ${DOTNET_PROJPATH} /t:Build ${DOTNET_BUILD_PROPERTIES} /p:Configuration="${DOTNET_CONFIG}") SET(build_dotnet_type "msbuild") ELSE() SET(build_dotnet_cmds COMMAND ${CMAKE_COMMAND} -E echo "=======> Building .NET project ${DOTNET_PROJNAME} [${DOTNET_CONFIG} ${DOTNET_PLATFORM}]" - COMMAND ${DOTNET_EXE} restore ${DOTNET_PROJPATH} + COMMAND ${DOTNET_EXE} restore ${DOTNET_PROJPATH} ${DOTNET_IMPORT_PROPERTIES} COMMAND ${DOTNET_EXE} clean ${DOTNET_PROJPATH} ${DOTNET_BUILD_PROPERTIES} COMMAND ${DOTNET_EXE} build --no-restore ${DOTNET_PROJPATH} -c ${DOTNET_CONFIG} ${DOTNET_BUILD_PROPERTIES} ${DOTNET_BUILD_OPTIONS}) SET(build_dotnet_type "dotnet") ENDIF() + # DOTNET_OUTPUTS refer to artifacts produced, that the BUILD_proj_name target depends on. + SET(DOTNET_OUTPUTS "") IF(NOT "${DOTNET_PACKAGES}" STREQUAL "") MESSAGE("-- Adding ${build_dotnet_type} project ${DOTNET_PROJPATH} (version ${DOTNET_PACKAGE_VERSION})") - SET(_DOTNET_OUTPUTS "") + SET(_DN_OUTPUTS "") FOREACH(pkg ${DOTNET_PACKAGES}) - LIST(APPEND _DOTNET_OUTPUTS ${DOTNET_OUTPUT_PATH}/${pkg}.${DOTNET_PACKAGE_VERSION}.nupkg) + LIST(APPEND _DN_OUTPUTS ${DOTNET_OUTPUT_PATH}/${pkg}.${DOTNET_PACKAGE_VERSION}.nupkg) + LIST(APPEND DOTNET_OUTPUTS ${CMAKE_BINARY_DIR}/${pkg}.${DOTNET_PACKAGE_VERSION}.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 ${_DOTNET_OUTPUTS} ${CMAKE_BINARY_DIR}) + 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)") - SET(_DOTNET_OUTPUTS ${CMAKE_CURRENT_BINARY_DIR}/${DOTNET_PROJNAME}.buildtimestamp) - LIST(APPEND build_dotnet_cmds COMMAND ${CMAKE_COMMAND} -E touch ${_DOTNET_OUTPUTS}) + SET(DOTNET_OUTPUTS ${CMAKE_CURRENT_BINARY_DIR}/${DOTNET_PROJNAME}.buildtimestamp) + LIST(APPEND build_dotnet_cmds COMMAND ${CMAKE_COMMAND} -E touch ${DOTNET_OUTPUTS}) ENDIF() ADD_CUSTOM_COMMAND( - OUTPUT ${_DOTNET_OUTPUTS} + OUTPUT ${DOTNET_OUTPUTS} DEPENDS ${DOTNET_deps} ${build_dotnet_cmds} ) ADD_CUSTOM_TARGET( BUILD_${DOTNET_PROJNAME} ALL - DEPENDS ${_DOTNET_OUTPUTS}) + DEPENDS ${DOTNET_OUTPUTS}) ENDMACRO() @@ -283,7 +342,7 @@ FUNCTION(ADD_DOTNET DOTNET_PROJECT) DOTNET_GET_DEPS(${DOTNET_PROJECT} "${ARGN}") SET(DOTNET_IS_MSBUILD FALSE) DOTNET_BUILD_COMMANDS() - ADD_DOTNET_DEPENDENCY_TARGETS() + ADD_DOTNET_DEPENDENCY_TARGETS(BUILD) ENDFUNCTION() FUNCTION(ADD_MSBUILD DOTNET_PROJECT) @@ -295,7 +354,7 @@ FUNCTION(ADD_MSBUILD DOTNET_PROJECT) DOTNET_GET_DEPS(${DOTNET_PROJECT} "${ARGN}") SET(DOTNET_IS_MSBUILD TRUE) DOTNET_BUILD_COMMANDS() - ADD_DOTNET_DEPENDENCY_TARGETS() + ADD_DOTNET_DEPENDENCY_TARGETS(BUILD) ENDFUNCTION() FUNCTION(RUN_DOTNET DOTNET_PROJECT) @@ -312,5 +371,79 @@ FUNCTION(RUN_DOTNET DOTNET_PROJECT) ADD_DEPENDENCIES(RUN_${DOTNET_PROJNAME} BUILD_${DOTNET_PROJNAME}) ENDFUNCTION() +FUNCTION(TEST_DOTNET DOTNET_PROJECT) + DOTNET_GET_DEPS(${DOTNET_PROJECT} "${ARGN}") + MESSAGE("-- Adding dotnet test project ${DOTNET_PROJECT}") + IF(WIN32) + SET(test_framework_args "") + ELSE() + SET(test_framework_args -f netcoreapp2.0) + ENDIF() + + ADD_TEST(NAME ${DOTNET_PROJNAME} + COMMAND ${DOTNET_EXE} test ${test_framework_args} --results-directory "${CMAKE_BINARY_DIR}" --logger trx ${DOTNET_RUN_ARGUMENTS} + WORKING_DIRECTORY ${DOTNET_PROJDIR}) + +ENDFUNCTION() + +SET(DOTNET_LAST_SMOKETEST "") + +FUNCTION(SMOKETEST_DOTNET DOTNET_PROJECT) + IF(WIN32) + ADD_DOTNET(${DOTNET_PROJECT} "${ARGN}") + # TODO should run on all targeted frameworks + RUN_DOTNET(${DOTNET_PROJECT} "${ARGN}" ARGUMENTS -f netcoreapp2.0) + ELSE() + ADD_DOTNET(${DOTNET_PROJECT} "${ARGN}" NETCOREAPP) + RUN_DOTNET(${DOTNET_PROJECT} "${ARGN}" ARGUMENTS -f netcoreapp2.0) + ENDIF() + + DOTNET_GET_DEPS(${DOTNET_PROJECT} "${ARGN}") + ADD_CUSTOM_TARGET( + SMOKETEST_${DOTNET_PROJNAME} + ALL + DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/${DOTNET_PROJNAME}.runtimestamp) + ADD_DOTNET_DEPENDENCY_TARGETS(SMOKETEST) + IF(DOTNET_LAST_SMOKETEST) + ADD_DEPENDENCIES(SMOKETEST_${DOTNET_PROJNAME} ${DOTNET_LAST_SMOKETEST}) + ENDIF() + # Chain the smoke tests together so they are executed sequentially + SET(DOTNET_LAST_SMOKETEST SMOKETEST_${DOTNET_PROJNAME}) + +ENDFUNCTION() + +SET(DOTNET_IMPORTS_TEMPLATE ${CMAKE_CURRENT_LIST_DIR}/DotnetImports.props.in) + +FUNCTION(GEN_DOTNET_PROPS target_props_file) + CMAKE_PARSE_ARGUMENTS( + # prefix + _DNP + # options (flags) + "" + # oneValueArgs + "PACKAGE_VERSION;XML_INJECT" + # multiValueArgs + "" + # the input arguments + ${ARGN}) + + IF(NOT _DNP_PACKAGE_VERSION) + SET(_DNP_PACKAGE_VERSION 1.0.0) + ENDIF() + + IF(_DNP_XML_INJECT) + SET(_DN_CUSTOM_BUILDPROPS ${_DNP_XML_INJECT}) + ENDIF() + + SET(_DN_OUTPUT_PATH ${CMAKE_BINARY_DIR}) + SET(_DN_XPLAT_LIB_DIR ${CMAKE_BINARY_DIR}) + SET(_DN_VERSION ${_DNP_PACKAGE_VERSION}) + CONFIGURE_FILE(${DOTNET_IMPORTS_TEMPLATE} ${target_props_file}) + UNSET(_DN_OUTPUT_PATH) + UNSET(_DN_XPLAT_LIB_DIR) + UNSET(_DN_VERSION) +ENDFUNCTION() + + MESSAGE("-- Found .NET toolchain: ${DOTNET_EXE} (version ${DOTNET_VERSION})") SET(DOTNET_FOUND TRUE) diff --git a/src/api/dotnet/CMakeLists.txt b/src/api/dotnet/CMakeLists.txt index b2909f03c..b9e26ec9e 100644 --- a/src/api/dotnet/CMakeLists.txt +++ b/src/api/dotnet/CMakeLists.txt @@ -138,6 +138,8 @@ 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. + +# TODO how to receive "configuration" and "platform" from here? 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 From ffd26e5a563aa2c464014261c5774435a3e9bcc6 Mon Sep 17 00:00:00 2001 From: Yatao Li Date: Sat, 12 Jan 2019 15:01:05 +0800 Subject: [PATCH 19/32] .net: remove net35 related build props; drop src/api/dotnet/core --- .gitignore | 2 + CMakeSettings.json | 17 +++ cmake/modules/DotnetImports.props.in | 3 +- cmake/modules/FindDotnet.cmake | 97 +++++++++------ src/api/dotnet/Microsoft.Z3.csproj.in | 165 +------------------------- src/api/dotnet/core/README.txt | 15 --- src/api/dotnet/core/core.csproj | 18 --- src/api/dotnet/dotnet35/Readme.NET35 | 10 -- 8 files changed, 86 insertions(+), 241 deletions(-) create mode 100644 CMakeSettings.json delete mode 100644 src/api/dotnet/core/README.txt delete mode 100644 src/api/dotnet/core/core.csproj delete mode 100644 src/api/dotnet/dotnet35/Readme.NET35 diff --git a/.gitignore b/.gitignore index e189a9569..9b239a566 100644 --- a/.gitignore +++ b/.gitignore @@ -76,3 +76,5 @@ src/api/ml/z3.mllib *.bak doc/api doc/code +.vs +examples/**/obj diff --git a/CMakeSettings.json b/CMakeSettings.json new file mode 100644 index 000000000..f8c4fa7c6 --- /dev/null +++ b/CMakeSettings.json @@ -0,0 +1,17 @@ +{ + "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/DotnetImports.props.in b/cmake/modules/DotnetImports.props.in index fba9ae301..090d46502 100644 --- a/cmake/modules/DotnetImports.props.in +++ b/cmake/modules/DotnetImports.props.in @@ -1,7 +1,8 @@ ${_DN_OUTPUT_PATH}/ - ${XPLAT_LIB_DIR}/ + ${_DN_XPLAT_LIB_DIR}/ ${_DN_VERSION} + ${_DN_CUSTOM_BUILDPROPS} diff --git a/cmake/modules/FindDotnet.cmake b/cmake/modules/FindDotnet.cmake index f424d3f23..4bcfe2215 100644 --- a/cmake/modules/FindDotnet.cmake +++ b/cmake/modules/FindDotnet.cmake @@ -32,9 +32,15 @@ # produced by running the .NET program, and can be consumed from other build steps. # # ``` -# RUN_DOTNET( +# RUN_DOTNET( [RELEASE|DEBUG] [X86|X64|ANYCPU] [NETCOREAPP] # [ARGUMENTS program_args...] -# [OUTPUT outputs...]) +# [OUTPUT outputs...] +# [CONFIG configuration] +# [PLATFORM platform] +# [DEPENDS depend_nuget_packages... ] +# [OUTPUT_PATH output_path relative to cmake binary output dir] +# [CUSTOM_BUILDPROPS value....] +# [SOURCES additional_file_dependencies... ]) # ``` # # ADD_MSBUILD -- add a project to be built by msbuild. Windows-only. When building in Unix systems, msbuild targets are skipped. @@ -54,11 +60,11 @@ # Multiple smoke tests will be run one-by-one to avoid global resource conflicts. # # SMOKETEST_DOTNET( [RELEASE|DEBUG] [X86|X64|ANYCPU] [NETCOREAPP] +# [ARGUMENTS program_args...] # [CONFIG configuration] # [PLATFORM platform] -# [PACKAGE output_nuget_packages... ] -# [VERSION nuget_package_version] # [DEPENDS depend_nuget_packages... ] +# [OUTPUT_PATH output_path relative to cmake binary output dir] # [CUSTOM_BUILDPROPS value....] # [SOURCES additional_file_dependencies... ]) # @@ -81,7 +87,8 @@ # # ``` # TEST_DOTNET( -# [ARGUMENTS additional_dotnet_test_args...]) +# [ARGUMENTS additional_dotnet_test_args...] +# [OUTPUT_PATH output_path relative to cmake binary output dir]) # ``` # # GEN_DOTNET_PROPS -- Generates a Directory.Build.props file. The created file is populated with MSBuild properties: @@ -153,7 +160,6 @@ FUNCTION(DOTNET_REGISTER_LOCAL_REPOSITORY repo_name repo_path) ENDFUNCTION() FUNCTION(DOTNET_GET_DEPS _DN_PROJECT arguments) - FILE(GLOB_RECURSE DOTNET_deps *.cs *.fs *.xaml *.csproj *.fsproj *.tsl) CMAKE_PARSE_ARGUMENTS( # prefix _DN @@ -166,18 +172,29 @@ FUNCTION(DOTNET_GET_DEPS _DN_PROJECT arguments) # the input arguments ${arguments}) + GET_FILENAME_COMPONENT(_DN_abs_proj "${_DN_PROJECT}" ABSOLUTE) + GET_FILENAME_COMPONENT(_DN_proj_dir "${_DN_abs_proj}" DIRECTORY) + GET_FILENAME_COMPONENT(_DN_projname "${_DN_PROJECT}" NAME) + STRING(REGEX REPLACE "\\.[^.]*$" "" _DN_projname_noext ${_DN_projname}) + + FILE(GLOB_RECURSE DOTNET_deps + ${_DN_proj_dir}/*.cs + ${_DN_proj_dir}/*.fs + ${_DN_proj_dir}/*.vb + ${_DN_proj_dir}/*.xaml + ${_DN_proj_dir}/*.resx + ${_DN_proj_dir}/*.xml + ${_DN_proj_dir}/*.*proj + ${_DN_proj_dir}/*.cs + ${_DN_proj_dir}/*.config) LIST(APPEND DOTNET_deps ${_DN_SOURCES}) SET(_DN_deps "") FOREACH(dep ${DOTNET_deps}) - IF(NOT dep MATCHES /obj/) + IF(NOT dep MATCHES /obj/ AND NOT dep MATCHES /bin/) LIST(APPEND _DN_deps ${dep}) ENDIF() ENDFOREACH() - 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) - STRING(REGEX REPLACE "\\.[^.]*$" "" _DN_projname_noext ${_DN_projname}) IF(_DN_RELEASE) SET(_DN_CONFIG Release) @@ -186,10 +203,7 @@ FUNCTION(DOTNET_GET_DEPS _DN_PROJECT arguments) ENDIF() IF(NOT _DN_CONFIG) - SET(_DN_CONFIG $) - IF(_DN_CONFIG STREQUAL "RelWithDebInfo" OR _DN_CONFIG STREQUAL "RelMinSize" OR NOT _DN_CONFIG) - SET(_DN_CONFIG "Release") - ENDIF() + SET(_DN_CONFIG Release) ENDIF() # If platform is not specified, do not pass the Platform property. @@ -217,7 +231,7 @@ FUNCTION(DOTNET_GET_DEPS _DN_PROJECT arguments) # Later we then copy the outputs to the destination. IF(NOT _DN_OUTPUT_PATH) - SET(_DN_OUTPUT_PATH "bin") + SET(_DN_OUTPUT_PATH ${_DN_projname_noext}) ENDIF() GET_FILENAME_COMPONENT(_DN_OUTPUT_PATH ${CMAKE_CURRENT_BINARY_DIR}/${_DN_OUTPUT_PATH} ABSOLUTE) @@ -295,14 +309,14 @@ ENDMACRO() MACRO(DOTNET_BUILD_COMMANDS) IF(${DOTNET_IS_MSBUILD}) SET(build_dotnet_cmds - COMMAND ${CMAKE_COMMAND} -E echo "=======> Building msbuild project ${DOTNET_PROJNAME} [${DOTNET_CONFIG} ${DOTNET_PLATFORM}]" - COMMAND ${NUGET_EXE} restore ${DOTNET_PROJPATH} -PackagesDirectory packages - COMMAND ${DOTNET_EXE} msbuild ${DOTNET_PROJPATH} /t:Clean /p:Configuration="${DOTNET_CONFIG}" + COMMAND ${CMAKE_COMMAND} -E echo "======= Building msbuild project ${DOTNET_PROJNAME} [${DOTNET_CONFIG} ${DOTNET_PLATFORM}]" + COMMAND ${NUGET_EXE} restore -Force ${DOTNET_PROJPATH} + COMMAND ${DOTNET_EXE} msbuild ${DOTNET_PROJPATH} /t:Clean ${DOTNET_BUILD_PROPERTIES} /p:Configuration="${DOTNET_CONFIG}" COMMAND ${DOTNET_EXE} msbuild ${DOTNET_PROJPATH} /t:Build ${DOTNET_BUILD_PROPERTIES} /p:Configuration="${DOTNET_CONFIG}") SET(build_dotnet_type "msbuild") ELSE() SET(build_dotnet_cmds - COMMAND ${CMAKE_COMMAND} -E echo "=======> Building .NET project ${DOTNET_PROJNAME} [${DOTNET_CONFIG} ${DOTNET_PLATFORM}]" + COMMAND ${CMAKE_COMMAND} -E echo "======= Building .NET project ${DOTNET_PROJNAME} [${DOTNET_CONFIG} ${DOTNET_PLATFORM}]" COMMAND ${DOTNET_EXE} restore ${DOTNET_PROJPATH} ${DOTNET_IMPORT_PROPERTIES} COMMAND ${DOTNET_EXE} clean ${DOTNET_PROJPATH} ${DOTNET_BUILD_PROPERTIES} COMMAND ${DOTNET_EXE} build --no-restore ${DOTNET_PROJPATH} -c ${DOTNET_CONFIG} ${DOTNET_BUILD_PROPERTIES} ${DOTNET_BUILD_OPTIONS}) @@ -310,21 +324,22 @@ MACRO(DOTNET_BUILD_COMMANDS) ENDIF() # DOTNET_OUTPUTS refer to artifacts produced, that the BUILD_proj_name target depends on. - SET(DOTNET_OUTPUTS "") + SET(DOTNET_OUTPUTS ${CMAKE_CURRENT_BINARY_DIR}/${DOTNET_PROJNAME}.buildtimestamp) + 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) 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)") - SET(DOTNET_OUTPUTS ${CMAKE_CURRENT_BINARY_DIR}/${DOTNET_PROJNAME}.buildtimestamp) - LIST(APPEND build_dotnet_cmds COMMAND ${CMAKE_COMMAND} -E touch ${DOTNET_OUTPUTS}) ENDIF() ADD_CUSTOM_COMMAND( @@ -358,17 +373,23 @@ FUNCTION(ADD_MSBUILD DOTNET_PROJECT) ENDFUNCTION() FUNCTION(RUN_DOTNET DOTNET_PROJECT) - DOTNET_GET_DEPS(${DOTNET_PROJECT} "${ARGN}") + DOTNET_GET_DEPS(${DOTNET_PROJECT} "${ARGN};NETCOREAPP") + MESSAGE("-- Adding dotnet run project ${DOTNET_PROJECT}") + FILE(MAKE_DIRECTORY ${DOTNET_OUTPUT_PATH}) ADD_CUSTOM_COMMAND( OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/${DOTNET_PROJNAME}.runtimestamp ${DOTNET_RUN_OUTPUT} DEPENDS ${DOTNET_deps} - COMMAND ${DOTNET_EXE} run ${DOTNET_RUN_ARGUMENTS} + COMMAND ${DOTNET_EXE} restore ${DOTNET_PROJPATH} ${DOTNET_IMPORT_PROPERTIES} + COMMAND ${DOTNET_EXE} clean ${DOTNET_PROJPATH} ${DOTNET_BUILD_PROPERTIES} + COMMAND ${DOTNET_EXE} build --no-restore ${DOTNET_PROJPATH} -c ${DOTNET_CONFIG} ${DOTNET_BUILD_PROPERTIES} ${DOTNET_BUILD_OPTIONS} + # XXX tfm + COMMAND ${DOTNET_EXE} ${DOTNET_OUTPUT_PATH}/netcoreapp2.0/${DOTNET_PROJNAME}.dll ${DOTNET_RUN_ARGUMENTS} COMMAND ${CMAKE_COMMAND} -E touch ${CMAKE_CURRENT_BINARY_DIR}/${DOTNET_PROJNAME}.runtimestamp - WORKING_DIRECTORY ${DOTNET_PROJDIR}) + WORKING_DIRECTORY ${DOTNET_OUTPUT_PATH}) ADD_CUSTOM_TARGET( RUN_${DOTNET_PROJNAME} DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/${DOTNET_PROJNAME}.runtimestamp ${DOTNET_RUN_OUTPUT}) - ADD_DEPENDENCIES(RUN_${DOTNET_PROJNAME} BUILD_${DOTNET_PROJNAME}) + ADD_DOTNET_DEPENDENCY_TARGETS(RUN) ENDFUNCTION() FUNCTION(TEST_DOTNET DOTNET_PROJECT) @@ -382,20 +403,18 @@ FUNCTION(TEST_DOTNET DOTNET_PROJECT) ADD_TEST(NAME ${DOTNET_PROJNAME} COMMAND ${DOTNET_EXE} test ${test_framework_args} --results-directory "${CMAKE_BINARY_DIR}" --logger trx ${DOTNET_RUN_ARGUMENTS} - WORKING_DIRECTORY ${DOTNET_PROJDIR}) + WORKING_DIRECTORY ${DOTNET_OUTPUT_PATH}) ENDFUNCTION() -SET(DOTNET_LAST_SMOKETEST "") +SET_PROPERTY(GLOBAL PROPERTY DOTNET_LAST_SMOKETEST "") FUNCTION(SMOKETEST_DOTNET DOTNET_PROJECT) + MESSAGE("-- Adding dotnet smoke test project ${DOTNET_PROJECT}") IF(WIN32) - ADD_DOTNET(${DOTNET_PROJECT} "${ARGN}") - # TODO should run on all targeted frameworks - RUN_DOTNET(${DOTNET_PROJECT} "${ARGN}" ARGUMENTS -f netcoreapp2.0) + RUN_DOTNET(${DOTNET_PROJECT} "${ARGN}") ELSE() - ADD_DOTNET(${DOTNET_PROJECT} "${ARGN}" NETCOREAPP) - RUN_DOTNET(${DOTNET_PROJECT} "${ARGN}" ARGUMENTS -f netcoreapp2.0) + RUN_DOTNET(${DOTNET_PROJECT} "${ARGN}") ENDIF() DOTNET_GET_DEPS(${DOTNET_PROJECT} "${ARGN}") @@ -404,11 +423,13 @@ FUNCTION(SMOKETEST_DOTNET DOTNET_PROJECT) ALL DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/${DOTNET_PROJNAME}.runtimestamp) ADD_DOTNET_DEPENDENCY_TARGETS(SMOKETEST) - IF(DOTNET_LAST_SMOKETEST) - ADD_DEPENDENCIES(SMOKETEST_${DOTNET_PROJNAME} ${DOTNET_LAST_SMOKETEST}) + GET_PROPERTY(_dn_last_smoketest GLOBAL PROPERTY DOTNET_LAST_SMOKETEST) + IF(_dn_last_smoketest) + MESSAGE("${_dn_last_smoketest} -> SMOKETEST_${DOTNET_PROJNAME}") + ADD_DEPENDENCIES(SMOKETEST_${DOTNET_PROJNAME} ${_dn_last_smoketest}) ENDIF() # Chain the smoke tests together so they are executed sequentially - SET(DOTNET_LAST_SMOKETEST SMOKETEST_${DOTNET_PROJNAME}) + SET_PROPERTY(GLOBAL PROPERTY DOTNET_LAST_SMOKETEST SMOKETEST_${DOTNET_PROJNAME}) ENDFUNCTION() diff --git a/src/api/dotnet/Microsoft.Z3.csproj.in b/src/api/dotnet/Microsoft.Z3.csproj.in index ee7b9237d..34321e90b 100644 --- a/src/api/dotnet/Microsoft.Z3.csproj.in +++ b/src/api/dotnet/Microsoft.Z3.csproj.in @@ -15,8 +15,8 @@ .NET Interface to the Z3 Theorem Prover .NET Interface to the Z3 Theorem Prover - Copyright (C) 2006-2015 Microsoft Corporation - Copyright (C) 2006-2015 Microsoft Corporation + Copyright (C) 2006-2019 Microsoft Corporation + Copyright (C) 2006-2019 Microsoft Corporation Microsoft Corporation Microsoft Corporation @@ -36,163 +36,19 @@ false - - False - False - True - False - False - True - False - True - True - False - False - False - True - False - False - False - True - False - False - True - True - True - False - False - - - - - - - True - Full - %28none%29 - 2 - - - true - GlobalSuppressions.cs - MinimumRecommendedRules.ruleset - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - true - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - true - True - False - True - False - False - False - False - False - False - False - False - False - False - False - False - False - True - False - False - True - False - False - False - - - - - - - False - Full - %28none%29 - 0 - - - true - GlobalSuppressions.cs - MinimumRecommendedRules.ruleset - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - true - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - True - False - True - False - False - True - True - True - False - False - False - True - True - False - False - False - True - False - False - True - True - False - False - - - - - -repro - - True - Full - %28none%29 - 2 - + - true - GlobalSuppressions.cs - MinimumRecommendedRules.ruleset - ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - true - ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - true DELAYSIGN - - true - GlobalSuppressions.cs - MinimumRecommendedRules.ruleset - ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - true - ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - true - false - - - true - GlobalSuppressions.cs - MinimumRecommendedRules.ruleset - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - - - + netstandard2.0;net461;net45 library True 1701,1702 4 - FRAMEWORK_LT_4 true $(OutputPath)\Microsoft.Z3.xml @@ -224,20 +80,11 @@ ${Z3_DOTNET_COMPILE_ITEMS} - - + + runtimes\win-x86\native - - runtimes\linux-x86\native - - - - - - - diff --git a/src/api/dotnet/core/README.txt b/src/api/dotnet/core/README.txt deleted file mode 100644 index fa274f72b..000000000 --- a/src/api/dotnet/core/README.txt +++ /dev/null @@ -1,15 +0,0 @@ -Z3 API for .NET Core - -Z3's .NET API uses Code Contracts, which are not included in .NET Core. The -enclosed file called DummyContracts.cs provides stubs for the Code Contracts -functions, so that the API will compile, but not perform any contract -checking. To build this using .NET core, run (in this directory): - -dotnet restore -dotnet build core.csproj -c Release - -If you are building with the cmake system, you should first -copy over files that are produced by the compiler into -this directory. You need to copy over Native.cs and Enumeration.cs - --- good luck! diff --git a/src/api/dotnet/core/core.csproj b/src/api/dotnet/core/core.csproj deleted file mode 100644 index 5fa3275cf..000000000 --- a/src/api/dotnet/core/core.csproj +++ /dev/null @@ -1,18 +0,0 @@ - - - - netcoreapp1.0 - $(DefineConstants);DOTNET_CORE - portable - Microsoft.Z3 - Library - core - $(PackageTargetFallback);dnxcore50 - 1.0.4 - - - - - - - diff --git a/src/api/dotnet/dotnet35/Readme.NET35 b/src/api/dotnet/dotnet35/Readme.NET35 deleted file mode 100644 index 75210f8b6..000000000 --- a/src/api/dotnet/dotnet35/Readme.NET35 +++ /dev/null @@ -1,10 +0,0 @@ -The default Z3 bindings for .NET are built for the .NET framework version 4. -Should the need arise, it is also possible to build them for .NET 3.5; the -instructions are as follows: - -In the project properties of Microsoft.Z3.csproj: -- Under 'Application': Change Target framework to .NET Framework 3.5 -- Under 'Build': Add FRAMEWORK_LT_4 to the conditional compilation symbols -- Remove the reference to System.Numerics -- Install the NuGet Package "Microsoft Code Contracts for Net3.5": - In the Package Manager Console enter Install-Package Code.Contract From 53eaab4709b4402951030bbcde9a5b49d35aa3d1 Mon Sep 17 00:00:00 2001 From: Yatao Li Date: Sat, 12 Jan 2019 17:38:24 +0800 Subject: [PATCH 20/32] dotnet: update build scripts --- .gitignore | 1 + CMakeSettings.json | 17 ----------------- cmake/modules/FindDotnet.cmake | 17 ++++++----------- src/api/dotnet/CMakeLists.txt | 9 +++++---- src/api/dotnet/Microsoft.Z3.csproj.in | 11 ++++++++--- 5 files changed, 20 insertions(+), 35 deletions(-) delete mode 100644 CMakeSettings.json 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 From e5f65263bb4989773f9b5b3d370cce1d557aaba1 Mon Sep 17 00:00:00 2001 From: Yatao Li Date: Sat, 12 Jan 2019 19:22:38 +0800 Subject: [PATCH 21/32] dotnet: reigster local repo for nupkg --- src/api/dotnet/CMakeLists.txt | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/api/dotnet/CMakeLists.txt b/src/api/dotnet/CMakeLists.txt index 26991bee7..77f5bbc16 100644 --- a/src/api/dotnet/CMakeLists.txt +++ b/src/api/dotnet/CMakeLists.txt @@ -157,6 +157,10 @@ add_dependencies(BUILD_Microsoft.Z3 libz3) # Convenient top-level target add_custom_target(build_z3_dotnet_bindings ALL DEPENDS BUILD_Microsoft.Z3) +# Register the local nupkg repo +set(Z3_DOTNET_LOCALREPO_NAME "Microsoft Z3 Local Repository") +DOTNET_REGISTER_LOCAL_REPOSITORY(${Z3_DOTNET_LOCALREPO_NAME} ${CMAKE_BINARY_DIR}) + ############################################################################### # Install: register a local nuget repo and install our package. # the build step depends on the 'purge' target, making sure that @@ -166,7 +170,8 @@ option(INSTALL_DOTNET_BINDINGS "Install .NET bindings when invoking install targ if(INSTALL_DOTNET_BINDINGS) 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)") + # move the local repo to the installation directory (cancel the build-time repo) + install(CODE "include(${CMAKE_CURRENT_LIST_DIR}/../../../cmake/modules/FindDotnet.cmake)\n DOTNET_REGISTER_LOCAL_REPOSITORY(\"${Z3_DOTNET_LOCALREPO_NAME}\" ${CMAKE_INSTALL_PREFIX}/${CMAKE_INSTALL_LIBDIR}/z3.nuget)") 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") From 3767c311aa58c0d6c17d75f823abff93544ebd90 Mon Sep 17 00:00:00 2001 From: Yatao Li Date: Sat, 12 Jan 2019 19:35:08 +0800 Subject: [PATCH 22/32] FindDotnet: generator expression IF is not available for older cmake versions --- cmake/modules/FindDotnet.cmake | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cmake/modules/FindDotnet.cmake b/cmake/modules/FindDotnet.cmake index bc53bf9df..615962f19 100644 --- a/cmake/modules/FindDotnet.cmake +++ b/cmake/modules/FindDotnet.cmake @@ -203,7 +203,7 @@ FUNCTION(DOTNET_GET_DEPS _DN_PROJECT arguments) ENDIF() IF(NOT _DN_CONFIG) - SET(_DN_CONFIG $,Debug,Release>) + SET(_DN_CONFIG "$<$:Debug>$<$>:Release>") ENDIF() # If platform is not specified, do not pass the Platform property. From 4b3189f3e2094a71c63e4204083c5e9258088e19 Mon Sep 17 00:00:00 2001 From: Yatao Li Date: Sat, 12 Jan 2019 20:04:44 +0800 Subject: [PATCH 23/32] dotnet: identifies arch-specific native libraries --- src/api/dotnet/CMakeLists.txt | 5 +++++ src/api/dotnet/Microsoft.Z3.csproj.in | 2 +- src/api/dotnet/Microsoft.Z3.props | 3 ++- 3 files changed, 8 insertions(+), 2 deletions(-) diff --git a/src/api/dotnet/CMakeLists.txt b/src/api/dotnet/CMakeLists.txt index 77f5bbc16..cf40170cd 100644 --- a/src/api/dotnet/CMakeLists.txt +++ b/src/api/dotnet/CMakeLists.txt @@ -140,6 +140,11 @@ endforeach() # Note, nuget package file names do not have the ${VER_REV} part. set(Z3_DOTNET_NUPKG_VERSION "${VER_MAJOR}.${VER_MINOR}.${VER_BUILD}") +if("${TARGET_ARCHITECTURE}" STREQUAL "i686") + set(Z3_DOTNET_PLATFORM "x86") +else() + set(Z3_DOTNET_PLATFORM "Any CPU") +endif() # TODO conditional for signing. we can then enable the ``Release_delaysign`` configuration diff --git a/src/api/dotnet/Microsoft.Z3.csproj.in b/src/api/dotnet/Microsoft.Z3.csproj.in index 5af2ac5f3..ecae050d7 100644 --- a/src/api/dotnet/Microsoft.Z3.csproj.in +++ b/src/api/dotnet/Microsoft.Z3.csproj.in @@ -76,7 +76,7 @@ ${Z3_DOTNET_COMPILE_ITEMS} - + runtimes\win-x64\native diff --git a/src/api/dotnet/Microsoft.Z3.props b/src/api/dotnet/Microsoft.Z3.props index 290cc5f86..a5db71359 100644 --- a/src/api/dotnet/Microsoft.Z3.props +++ b/src/api/dotnet/Microsoft.Z3.props @@ -9,7 +9,8 @@ $(MSBuildThisFileDirectory)..\ - $(Z3_PACKAGE_PATH)runtimes\win-x64\native\libz3.dll + $(Z3_PACKAGE_PATH)runtimes\win-x64\native\libz3.dll + $(Z3_PACKAGE_PATH)runtimes\win-x86\native\libz3.dll $(Z3_PACKAGE_PATH)runtimes\linux-x64\native\libz3.so From 55f92f3658ce01be3f6b21a2297dd85dcf4b3112 Mon Sep 17 00:00:00 2001 From: Yatao Li Date: Sat, 12 Jan 2019 21:33:09 +0800 Subject: [PATCH 24/32] dotnet: remove stale packages before pack; relay cmake config generator expression into msbuild property.. --- cmake/modules/FindDotnet.cmake | 24 +++++++++++++++--------- src/api/dotnet/CMakeLists.txt | 5 ++++- src/api/dotnet/Microsoft.Z3.csproj.in | 6 +++--- 3 files changed, 22 insertions(+), 13 deletions(-) diff --git a/cmake/modules/FindDotnet.cmake b/cmake/modules/FindDotnet.cmake index 615962f19..191364858 100644 --- a/cmake/modules/FindDotnet.cmake +++ b/cmake/modules/FindDotnet.cmake @@ -25,7 +25,9 @@ # [DEPENDS depend_nuget_packages... ] # [OUTPUT_PATH output_path relative to cmake binary output dir] # [CUSTOM_BUILDPROPS value....] -# [SOURCES additional_file_dependencies... ]) +# [SOURCES additional_file_dependencies... ] +# [ARGUMENTS additional_build_args...] +# [PACK_ARGUMENTS additional_pack_args...]) # ``` # # RUN_DOTNET -- Run a project with `dotnet run`. The `OUTPUT` argument represents artifacts @@ -52,7 +54,9 @@ # [PACKAGE output_nuget_packages... ] # [DEPENDS depend_nuget_packages... ] # [CUSTOM_BUILDPROPS value....] -# [SOURCES additional_file_dependencies... ]) +# [SOURCES additional_file_dependencies... ] +# [ARGUMENTS additional_build_args...] +# [PACK_ARGUMENTS additional_pack_args...]) # ``` # # SMOKETEST_DOTNET -- add a dotnet smoke test project to the build. The project will be run during a build, @@ -168,7 +172,7 @@ FUNCTION(DOTNET_GET_DEPS _DN_PROJECT arguments) # oneValueArgs "CONFIG;PLATFORM;VERSION;OUTPUT_PATH" # multiValueArgs - "PACKAGE;DEPENDS;ARGUMENTS;OUTPUT;SOURCES;CUSTOM_BUILDPROPS" + "PACKAGE;DEPENDS;ARGUMENTS;PACK_ARGUMENTS;OUTPUT;SOURCES;CUSTOM_BUILDPROPS" # the input arguments ${arguments}) @@ -247,7 +251,7 @@ FUNCTION(DOTNET_GET_DEPS _DN_PROJECT arguments) SET(DOTNET_PROJNAME ${_DN_projname_noext} PARENT_SCOPE) SET(DOTNET_PROJPATH ${_DN_abs_proj} PARENT_SCOPE) SET(DOTNET_PROJDIR ${_DN_proj_dir} PARENT_SCOPE) - SET(DOTNET_RUN_ARGUMENTS ${_DN_ARGUMENTS} PARENT_SCOPE) + SET(DOTNET_ARGUMENTS ${_DN_ARGUMENTS} PARENT_SCOPE) SET(DOTNET_RUN_OUTPUT ${_DN_OUTPUT} PARENT_SCOPE) SET(DOTNET_PACKAGE_VERSION ${_DN_VERSION} PARENT_SCOPE) SET(DOTNET_OUTPUT_PATH ${_DN_OUTPUT_PATH} PARENT_SCOPE) @@ -273,7 +277,7 @@ FUNCTION(DOTNET_GET_DEPS _DN_PROJECT arguments) SET(DOTNET_IMPORT_PROPERTIES ${_DN_IMPORT_ARGS} PARENT_SCOPE) SET(DOTNET_BUILD_PROPERTIES ${_DN_PLATFORM_PROP} ${_DN_IMPORT_ARGS} PARENT_SCOPE) SET(DOTNET_BUILD_OPTIONS ${_DN_BUILD_OPTIONS} PARENT_SCOPE) - SET(DOTNET_PACK_OPTIONS --include-symbols ${_DN_PACK_OPTIONS} PARENT_SCOPE) + SET(DOTNET_PACK_OPTIONS --include-symbols ${_DN_PACK_OPTIONS} ${_DN_PACK_ARGUMENTS} PARENT_SCOPE) ENDFUNCTION() @@ -312,14 +316,14 @@ MACRO(DOTNET_BUILD_COMMANDS) COMMAND ${CMAKE_COMMAND} -E echo "======= Building msbuild project ${DOTNET_PROJNAME} [${DOTNET_CONFIG} ${DOTNET_PLATFORM}]" COMMAND ${NUGET_EXE} restore -Force ${DOTNET_PROJPATH} COMMAND ${DOTNET_EXE} msbuild ${DOTNET_PROJPATH} /t:Clean ${DOTNET_BUILD_PROPERTIES} /p:Configuration="${DOTNET_CONFIG}" - COMMAND ${DOTNET_EXE} msbuild ${DOTNET_PROJPATH} /t:Build ${DOTNET_BUILD_PROPERTIES} /p:Configuration="${DOTNET_CONFIG}") + COMMAND ${DOTNET_EXE} msbuild ${DOTNET_PROJPATH} /t:Build ${DOTNET_BUILD_PROPERTIES} /p:Configuration="${DOTNET_CONFIG}" ${DOTNET_ARGUMENTS}) SET(build_dotnet_type "msbuild") ELSE() SET(build_dotnet_cmds COMMAND ${CMAKE_COMMAND} -E echo "======= Building .NET project ${DOTNET_PROJNAME} [${DOTNET_CONFIG} ${DOTNET_PLATFORM}]" COMMAND ${DOTNET_EXE} restore ${DOTNET_PROJPATH} ${DOTNET_IMPORT_PROPERTIES} COMMAND ${DOTNET_EXE} clean ${DOTNET_PROJPATH} ${DOTNET_BUILD_PROPERTIES} - COMMAND ${DOTNET_EXE} build --no-restore ${DOTNET_PROJPATH} -c ${DOTNET_CONFIG} ${DOTNET_BUILD_PROPERTIES} ${DOTNET_BUILD_OPTIONS}) + COMMAND ${DOTNET_EXE} build --no-restore ${DOTNET_PROJPATH} -c ${DOTNET_CONFIG} ${DOTNET_BUILD_PROPERTIES} ${DOTNET_BUILD_OPTIONS} ${DOTNET_ARGUMENTS}) SET(build_dotnet_type "dotnet") ENDIF() @@ -331,6 +335,8 @@ MACRO(DOTNET_BUILD_COMMANDS) FOREACH(pkg ${DOTNET_PACKAGES}) 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) + LIST(APPEND build_dotnet_cmds COMMAND ${CMAKE_COMMAND} -E remove ${DOTNET_OUTPUT_PATH}/${pkg}.${DOTNET_PACKAGE_VERSION}.nupkg) + LIST(APPEND build_dotnet_cmds COMMAND ${CMAKE_COMMAND} -E remove ${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}) ELSE() @@ -378,7 +384,7 @@ FUNCTION(RUN_DOTNET DOTNET_PROJECT) COMMAND ${DOTNET_EXE} clean ${DOTNET_PROJPATH} ${DOTNET_BUILD_PROPERTIES} COMMAND ${DOTNET_EXE} build --no-restore ${DOTNET_PROJPATH} -c ${DOTNET_CONFIG} ${DOTNET_BUILD_PROPERTIES} ${DOTNET_BUILD_OPTIONS} # XXX tfm - COMMAND ${DOTNET_EXE} ${DOTNET_OUTPUT_PATH}/netcoreapp2.0/${DOTNET_PROJNAME}.dll ${DOTNET_RUN_ARGUMENTS} + COMMAND ${DOTNET_EXE} ${DOTNET_OUTPUT_PATH}/netcoreapp2.0/${DOTNET_PROJNAME}.dll ${DOTNET_ARGUMENTS} COMMAND ${CMAKE_COMMAND} -E touch ${CMAKE_CURRENT_BINARY_DIR}/${DOTNET_PROJNAME}.runtimestamp WORKING_DIRECTORY ${DOTNET_OUTPUT_PATH}) ADD_CUSTOM_TARGET( @@ -397,7 +403,7 @@ FUNCTION(TEST_DOTNET DOTNET_PROJECT) ENDIF() ADD_TEST(NAME ${DOTNET_PROJNAME} - COMMAND ${DOTNET_EXE} test ${test_framework_args} --results-directory "${CMAKE_BINARY_DIR}" --logger trx ${DOTNET_RUN_ARGUMENTS} + COMMAND ${DOTNET_EXE} test ${test_framework_args} --results-directory "${CMAKE_BINARY_DIR}" --logger trx ${DOTNET_ARGUMENTS} WORKING_DIRECTORY ${DOTNET_OUTPUT_PATH}) ENDFUNCTION() diff --git a/src/api/dotnet/CMakeLists.txt b/src/api/dotnet/CMakeLists.txt index cf40170cd..68f7b9335 100644 --- a/src/api/dotnet/CMakeLists.txt +++ b/src/api/dotnet/CMakeLists.txt @@ -151,11 +151,14 @@ endif() 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} + PLATFORM ${Z3_DOTNET_PLATFORM} SOURCES ${CMAKE_CURRENT_SOURCE_DIR}/Microsoft.Z3.csproj.in ${CMAKE_CURRENT_SOURCE_DIR}/Microsoft.Z3.props ${CMAKE_CURRENT_SOURCE_DIR}/Microsoft.Z3.targets ${Z3_DOTNET_ASSEMBLY_SOURCES} - PACKAGE Microsoft.Z3) + PACKAGE Microsoft.Z3 + PACK_ARGUMENTS "/p:_DN_CMAKE_CONFIG=$" + ) add_dependencies(BUILD_Microsoft.Z3 libz3) diff --git a/src/api/dotnet/Microsoft.Z3.csproj.in b/src/api/dotnet/Microsoft.Z3.csproj.in index ecae050d7..fc6d6a978 100644 --- a/src/api/dotnet/Microsoft.Z3.csproj.in +++ b/src/api/dotnet/Microsoft.Z3.csproj.in @@ -49,7 +49,7 @@ - netstandard2.0;net461;net45 + netstandard2.0;net45 library True 1701,1702 @@ -77,7 +77,7 @@ ${Z3_DOTNET_COMPILE_ITEMS} - + runtimes\win-x64\native @@ -87,7 +87,7 @@ ${Z3_DOTNET_COMPILE_ITEMS} - + runtimes\win-x86\native From 5e79dba3d6d1fe1bdc7486f9e9d2c4dd9f485675 Mon Sep 17 00:00:00 2001 From: Yatao Li Date: Sun, 13 Jan 2019 00:03:37 +0800 Subject: [PATCH 25/32] dotnet: move example project build to cmake --- contrib/ci/scripts/test_z3_examples_cmake.sh | 4 ++-- examples/dotnet/dotnet.csproj | 2 +- src/api/dotnet/CMakeLists.txt | 4 ++++ 3 files changed, 7 insertions(+), 3 deletions(-) diff --git a/contrib/ci/scripts/test_z3_examples_cmake.sh b/contrib/ci/scripts/test_z3_examples_cmake.sh index 679fc4a69..1e75a5701 100755 --- a/contrib/ci/scripts/test_z3_examples_cmake.sh +++ b/contrib/ci/scripts/test_z3_examples_cmake.sh @@ -88,8 +88,8 @@ if [ "X${PYTHON_BINDINGS}" = "X1" ]; then fi if [ "X${DOTNET_BINDINGS}" = "X1" ]; then - # Build & Run .NET example - run_quiet run_non_native_binding dotnet run -p ${Z3_SRC_DIR}/examples/dotnet/dotnet.csproj + # Run .NET example + run_quiet run_non_native_binding dotnet ${Z3_BUILD_DIR}/dotnet/netcoreapp2.0/dotnet.dll fi if [ "X${JAVA_BINDINGS}" = "X1" ]; then diff --git a/examples/dotnet/dotnet.csproj b/examples/dotnet/dotnet.csproj index 0dc4ee2ec..7776259ea 100644 --- a/examples/dotnet/dotnet.csproj +++ b/examples/dotnet/dotnet.csproj @@ -6,7 +6,7 @@ - + diff --git a/src/api/dotnet/CMakeLists.txt b/src/api/dotnet/CMakeLists.txt index 68f7b9335..db5a53259 100644 --- a/src/api/dotnet/CMakeLists.txt +++ b/src/api/dotnet/CMakeLists.txt @@ -159,6 +159,10 @@ ADD_DOTNET(${CMAKE_CURRENT_BINARY_DIR}/build/Microsoft.Z3.csproj PACKAGE Microsoft.Z3 PACK_ARGUMENTS "/p:_DN_CMAKE_CONFIG=$" ) +ADD_DOTNET(${CMAKE_SOURCE_DIR}/examples/dotnet/dotnet.csproj + PLATFORM ${Z3_DOTNET_PLATFORM} + CUSTOM_BUILDPROPS "${VER_MAJOR}.${VER_MINOR}.${VER_BUILD}" + DEPENDS Microsoft.Z3) add_dependencies(BUILD_Microsoft.Z3 libz3) From 0a6a76734a8321a73e00d1ee0c8078da2c8138c6 Mon Sep 17 00:00:00 2001 From: Yatao Li Date: Sun, 13 Jan 2019 00:08:32 +0800 Subject: [PATCH 26/32] docker: ubuntu 14.04 dotnet source fix --- contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile b/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile index f6541a2c9..8a4812de2 100644 --- a/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile +++ b/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile @@ -26,7 +26,7 @@ RUN apt-get update && \ python2.7 \ python-setuptools -RUN curl -SL https://packages.microsoft.com/config/ubuntu/16.04/packages-microsoft-prod.deb --output packages-microsoft-prod.deb && \ +RUN curl -SL https://packages.microsoft.com/config/ubuntu/14.04/packages-microsoft-prod.deb --output packages-microsoft-prod.deb && \ dpkg -i packages-microsoft-prod.deb && \ apt-get update && \ apt-get -y --no-install-recommends install dotnet-sdk-2.1 From 8ebde41f3581287c8ea556bf3cccca1c7f505b1b Mon Sep 17 00:00:00 2001 From: Yatao Li Date: Sun, 13 Jan 2019 22:45:05 +0800 Subject: [PATCH 27/32] dotnet: example: copy to binary dir before build --- examples/CMakeLists.txt | 7 +++++++ examples/dotnet/CMakeLists.txt | 15 +++++++++++++++ examples/dotnet/README | 3 +-- src/api/dotnet/CMakeLists.txt | 5 ----- 4 files changed, 23 insertions(+), 7 deletions(-) create mode 100644 examples/dotnet/CMakeLists.txt diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt index 6c50320ed..5d06029f9 100644 --- a/examples/CMakeLists.txt +++ b/examples/CMakeLists.txt @@ -112,3 +112,10 @@ set_target_properties(z3_tptp5 PROPERTIES EXCLUDE_FROM_ALL TRUE) if (BUILD_PYTHON_BINDINGS) add_subdirectory(python) endif() + +################################################################################ +# Build dotnet examples +################################################################################ +if (BUILD_DOTNET_BINDINGS) + add_subdirectory(dotnet) +endif() \ No newline at end of file diff --git a/examples/dotnet/CMakeLists.txt b/examples/dotnet/CMakeLists.txt new file mode 100644 index 000000000..d0cd2bb15 --- /dev/null +++ b/examples/dotnet/CMakeLists.txt @@ -0,0 +1,15 @@ +find_package(Dotnet REQUIRED) + +if("${TARGET_ARCHITECTURE}" STREQUAL "i686") + set(Z3_DOTNET_PLATFORM "x86") +else() + set(Z3_DOTNET_PLATFORM "Any CPU") +endif() + +configure_file(dotnet.csproj dotnet.csproj COPYONLY) +configure_file(program.cs program.cs COPYONLY) + +ADD_DOTNET(${CMAKE_CURRENT_BINARY_DIR}/dotnet.csproj + PLATFORM ${Z3_DOTNET_PLATFORM} + CUSTOM_BUILDPROPS "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}" + DEPENDS Microsoft.Z3) diff --git a/examples/dotnet/README b/examples/dotnet/README index 3f7e989df..b42156761 100644 --- a/examples/dotnet/README +++ b/examples/dotnet/README @@ -1,7 +1,6 @@ Small example using the .Net bindings. -This example is only built if you have Visual Studio. To build the example execute make examples in the build directory. -It will create the executable dotnet_example.exe +It will create a .net core 2.0 app. diff --git a/src/api/dotnet/CMakeLists.txt b/src/api/dotnet/CMakeLists.txt index db5a53259..4f4230ff2 100644 --- a/src/api/dotnet/CMakeLists.txt +++ b/src/api/dotnet/CMakeLists.txt @@ -159,11 +159,6 @@ ADD_DOTNET(${CMAKE_CURRENT_BINARY_DIR}/build/Microsoft.Z3.csproj PACKAGE Microsoft.Z3 PACK_ARGUMENTS "/p:_DN_CMAKE_CONFIG=$" ) -ADD_DOTNET(${CMAKE_SOURCE_DIR}/examples/dotnet/dotnet.csproj - PLATFORM ${Z3_DOTNET_PLATFORM} - CUSTOM_BUILDPROPS "${VER_MAJOR}.${VER_MINOR}.${VER_BUILD}" - DEPENDS Microsoft.Z3) - add_dependencies(BUILD_Microsoft.Z3 libz3) # Convenient top-level target From 08adc1bf97bc825452c9311f9bdcf0c29453c79e Mon Sep 17 00:00:00 2001 From: Yatao Li Date: Sun, 13 Jan 2019 23:15:40 +0800 Subject: [PATCH 28/32] ... --- examples/dotnet/CMakeLists.txt | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/examples/dotnet/CMakeLists.txt b/examples/dotnet/CMakeLists.txt index d0cd2bb15..57a1ba7ac 100644 --- a/examples/dotnet/CMakeLists.txt +++ b/examples/dotnet/CMakeLists.txt @@ -6,8 +6,8 @@ else() set(Z3_DOTNET_PLATFORM "Any CPU") endif() -configure_file(dotnet.csproj dotnet.csproj COPYONLY) -configure_file(program.cs program.cs COPYONLY) +configure_file(${CMAKE_CURRENT_SOURCE_DIR}/dotnet.csproj dotnet.csproj COPYONLY) +configure_file(${CMAKE_CURRENT_SOURCE_DIR}/program.cs program.cs COPYONLY) ADD_DOTNET(${CMAKE_CURRENT_BINARY_DIR}/dotnet.csproj PLATFORM ${Z3_DOTNET_PLATFORM} From f0f9a16f85ecddc13f16d48247c3f2adf57a97f1 Mon Sep 17 00:00:00 2001 From: Yatao Li Date: Mon, 14 Jan 2019 00:22:51 +0800 Subject: [PATCH 29/32] cmake: dotnet: example: program -> Program --- examples/dotnet/CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/dotnet/CMakeLists.txt b/examples/dotnet/CMakeLists.txt index 57a1ba7ac..c89c90f2f 100644 --- a/examples/dotnet/CMakeLists.txt +++ b/examples/dotnet/CMakeLists.txt @@ -7,7 +7,7 @@ else() endif() configure_file(${CMAKE_CURRENT_SOURCE_DIR}/dotnet.csproj dotnet.csproj COPYONLY) -configure_file(${CMAKE_CURRENT_SOURCE_DIR}/program.cs program.cs COPYONLY) +configure_file(${CMAKE_CURRENT_SOURCE_DIR}/Program.cs Program.cs COPYONLY) ADD_DOTNET(${CMAKE_CURRENT_BINARY_DIR}/dotnet.csproj PLATFORM ${Z3_DOTNET_PLATFORM} From 209ebecb867013519ade81445146438fe710ccb4 Mon Sep 17 00:00:00 2001 From: Yatao Li Date: Mon, 14 Jan 2019 00:51:44 +0800 Subject: [PATCH 30/32] cmake: dotnet: example: dotnet.csproj is NETCOREAPP --- examples/dotnet/CMakeLists.txt | 1 + 1 file changed, 1 insertion(+) diff --git a/examples/dotnet/CMakeLists.txt b/examples/dotnet/CMakeLists.txt index c89c90f2f..d145a2269 100644 --- a/examples/dotnet/CMakeLists.txt +++ b/examples/dotnet/CMakeLists.txt @@ -11,5 +11,6 @@ configure_file(${CMAKE_CURRENT_SOURCE_DIR}/Program.cs Program.cs COPYONLY) ADD_DOTNET(${CMAKE_CURRENT_BINARY_DIR}/dotnet.csproj PLATFORM ${Z3_DOTNET_PLATFORM} + NETCOREAPP CUSTOM_BUILDPROPS "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}" DEPENDS Microsoft.Z3) From 58e8b2b8d57c217b02f1a9e9da000902b4c7f9c2 Mon Sep 17 00:00:00 2001 From: Yatao Li Date: Mon, 14 Jan 2019 14:02:58 +0800 Subject: [PATCH 31/32] Dockerfile: update ubuntu 14.04 image with cmake 3.12 --- .travis.yml | 2 +- contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile | 4 +++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/.travis.yml b/.travis.yml index 076b3a554..bdd572852 100644 --- a/.travis.yml +++ b/.travis.yml @@ -20,7 +20,7 @@ env: # 64-bit UBSan Debug build - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/clang-3.9 CXX_COMPILER=/usr/bin/clang++-3.9 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug UBSAN_BUILD=1 RUN_UNIT_TESTS=SKIP # 64-bit ASan Debug build - - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/clang-3.9 CXX_COMPILER=/usr/bin/clang++-3.9 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug ASAN_BUILD=1 RUN_UNIT_TESTS=SKIP ASAN_DSO=/usr/lib/clang/3.9/lib/linux/libclang_rt.asan-x86_64.so + - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/clang-3.9 CXX_COMPILER=/usr/bin/clang++-3.9 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug ASAN_BUILD=1 RUN_UNIT_TESTS=SKIP ASAN_DSO=/usr/lib/clang/3.9/lib/linux/libclang_rt.asan-x86_64.so DOTNET_BINDINGS=0 # Build for running unit tests under ASan/UBSan # FIXME: We should really be doing a debug build but the unit tests run too # slowly when we do that. diff --git a/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile b/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile index 8a4812de2..9c6bdc054 100644 --- a/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile +++ b/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile @@ -5,7 +5,6 @@ RUN apt-get update && \ apt-transport-https \ binutils \ clang-3.9 \ - cmake \ curl \ doxygen \ default-jdk \ @@ -31,6 +30,9 @@ RUN curl -SL https://packages.microsoft.com/config/ubuntu/14.04/packages-microso apt-get update && \ apt-get -y --no-install-recommends install dotnet-sdk-2.1 +RUN curl -SL https://cmake.org/files/v3.12/cmake-3.12.0-Linux-x86_64.sh --output cmake-3.12.0-Linux-x86_64.sh && \ + sh cmake-3.12.0-Linux-x86_64.sh --prefix=/usr/local --exclude-subdir + # Create `user` user for container with password `user`. and give it # password-less sudo access RUN useradd -m user && \ From 43ee345f01e2ecb7b3d93fa90c0a8cc639afde97 Mon Sep 17 00:00:00 2001 From: Yatao Li Date: Tue, 15 Jan 2019 03:06:36 +0900 Subject: [PATCH 32/32] dotnet deps hack for test --- .travis.yml | 2 +- cmake/modules/FindDotnet.cmake | 2 +- contrib/ci/scripts/test_z3_examples_cmake.sh | 8 +++++++- examples/dotnet/CMakeLists.txt | 20 +++++++++++++++++++- src/api/dotnet/CMakeLists.txt | 2 +- 5 files changed, 29 insertions(+), 5 deletions(-) diff --git a/.travis.yml b/.travis.yml index bdd572852..12e62ed3d 100644 --- a/.travis.yml +++ b/.travis.yml @@ -20,7 +20,7 @@ env: # 64-bit UBSan Debug build - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/clang-3.9 CXX_COMPILER=/usr/bin/clang++-3.9 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug UBSAN_BUILD=1 RUN_UNIT_TESTS=SKIP # 64-bit ASan Debug build - - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/clang-3.9 CXX_COMPILER=/usr/bin/clang++-3.9 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug ASAN_BUILD=1 RUN_UNIT_TESTS=SKIP ASAN_DSO=/usr/lib/clang/3.9/lib/linux/libclang_rt.asan-x86_64.so DOTNET_BINDINGS=0 + - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/clang-3.9 CXX_COMPILER=/usr/bin/clang++-3.9 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug ASAN_BUILD=1 RUN_UNIT_TESTS=SKIP ASAN_DSO=/usr/lib/clang/3.9/lib/linux/libclang_rt.asan-x86_64.so # Build for running unit tests under ASan/UBSan # FIXME: We should really be doing a debug build but the unit tests run too # slowly when we do that. diff --git a/cmake/modules/FindDotnet.cmake b/cmake/modules/FindDotnet.cmake index 191364858..98c5f2079 100644 --- a/cmake/modules/FindDotnet.cmake +++ b/cmake/modules/FindDotnet.cmake @@ -218,7 +218,7 @@ FUNCTION(DOTNET_GET_DEPS _DN_PROJECT arguments) ELSEIF(_DN_X64) SET(_DN_PLATFORM x64) ELSEIF(_DN_ANYCPU) - SET(_DN_PLATFORM "Any CPU") + SET(_DN_PLATFORM "AnyCPU") ENDIF() # If package version is not set, first fallback to DOTNET_PACKAGE_VERSION diff --git a/contrib/ci/scripts/test_z3_examples_cmake.sh b/contrib/ci/scripts/test_z3_examples_cmake.sh index 1e75a5701..a149a1d83 100755 --- a/contrib/ci/scripts/test_z3_examples_cmake.sh +++ b/contrib/ci/scripts/test_z3_examples_cmake.sh @@ -89,7 +89,13 @@ fi if [ "X${DOTNET_BINDINGS}" = "X1" ]; then # Run .NET example - run_quiet run_non_native_binding dotnet ${Z3_BUILD_DIR}/dotnet/netcoreapp2.0/dotnet.dll + if [ "X${ASAN_BUILD}" = "X1" ]; then + # The dotnet test get stuck on ASAN + # so don't run it for now. + echo "Skipping .NET example under ASan build" + else + run_quiet run_non_native_binding dotnet ${Z3_BUILD_DIR}/dotnet/netcoreapp2.0/dotnet.dll + fi fi if [ "X${JAVA_BINDINGS}" = "X1" ]; then diff --git a/examples/dotnet/CMakeLists.txt b/examples/dotnet/CMakeLists.txt index d145a2269..108326f83 100644 --- a/examples/dotnet/CMakeLists.txt +++ b/examples/dotnet/CMakeLists.txt @@ -3,7 +3,7 @@ find_package(Dotnet REQUIRED) if("${TARGET_ARCHITECTURE}" STREQUAL "i686") set(Z3_DOTNET_PLATFORM "x86") else() - set(Z3_DOTNET_PLATFORM "Any CPU") + set(Z3_DOTNET_PLATFORM "AnyCPU") endif() configure_file(${CMAKE_CURRENT_SOURCE_DIR}/dotnet.csproj dotnet.csproj COPYONLY) @@ -14,3 +14,21 @@ ADD_DOTNET(${CMAKE_CURRENT_BINARY_DIR}/dotnet.csproj NETCOREAPP CUSTOM_BUILDPROPS "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}" DEPENDS Microsoft.Z3) + +if(UNIX AND NOT APPLE) + set(z3_dotnet_native_lib ${CMAKE_BINARY_DIR}/libz3.so) + set(z3_dotnet_test_manual_copy_deps + ${CMAKE_BINARY_DIR}/Microsoft.Z3/netstandard2.0/Microsoft.Z3.dll + ${z3_dotnet_native_lib} + ) + + add_custom_target( + z3_dotnet_test_manual_copy_assembly_hack ALL + COMMAND ${CMAKE_COMMAND} -E copy ${z3_dotnet_test_manual_copy_deps} ${CMAKE_BINARY_DIR}/dotnet/netcoreapp2.0/ + # hack the libz3 entry in deps so it's easy enough for dotnet to reach it... + COMMAND sed \"s/runtimes\\/.*libz3\\.so/libz3.so/\" -i ${CMAKE_BINARY_DIR}/dotnet/netcoreapp2.0/dotnet.deps.json + ) + + add_dependencies(z3_dotnet_test_manual_copy_assembly_hack BUILD_dotnet) +endif() + diff --git a/src/api/dotnet/CMakeLists.txt b/src/api/dotnet/CMakeLists.txt index 4f4230ff2..3ff1a484a 100644 --- a/src/api/dotnet/CMakeLists.txt +++ b/src/api/dotnet/CMakeLists.txt @@ -143,7 +143,7 @@ set(Z3_DOTNET_NUPKG_VERSION "${VER_MAJOR}.${VER_MINOR}.${VER_BUILD}") if("${TARGET_ARCHITECTURE}" STREQUAL "i686") set(Z3_DOTNET_PLATFORM "x86") else() - set(Z3_DOTNET_PLATFORM "Any CPU") + set(Z3_DOTNET_PLATFORM "AnyCPU") endif() # TODO conditional for signing. we can then enable the ``Release_delaysign`` configuration