From ffd26e5a563aa2c464014261c5774435a3e9bcc6 Mon Sep 17 00:00:00 2001 From: Yatao Li Date: Sat, 12 Jan 2019 15:01:05 +0800 Subject: [PATCH] .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