From: Andrew V. Jones Date: Tue, 9 Jun 2020 04:42:51 +0000 (+0100) Subject: Ensure correct CMake dependencies on Debug_tags.h/Trace_tags.h/git_versioninfo.cpp... X-Git-Tag: cvc5-1.0.0~3236 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=61734b41b7b96e7e7cbf46021a357d840d64b42e;p=cvc5.git Ensure correct CMake dependencies on Debug_tags.h/Trace_tags.h/git_versioninfo.cpp (#4570) ## Issue When building CVC4, and when there are no source code codes (a so-called "no op" build), it seems that some of CMake targets are still fired: ``` [avj@tempvm build]$ ninja -d explain -d stats ninja explain: output proofs/signatures/all of phony edge with no inputs doesn't exist ninja explain: proofs/signatures/all is dirty ninja explain: output doc/all of phony edge with no inputs doesn't exist ninja explain: doc/all is dirty ninja explain: output src/base/CMakeFiles/gen-gitinfo doesn't exist ninja explain: src/base/CMakeFiles/gen-gitinfo is dirty ninja explain: output src/base/CMakeFiles/gen-tags-debug doesn't exist ninja explain: src/base/Debug_tags.tmp is dirty ninja explain: src/base/CMakeFiles/gen-tags-debug is dirty ninja explain: src/base/Debug_tags.tmp is dirty ninja explain: output src/base/CMakeFiles/gen-tags-trace doesn't exist ninja explain: src/base/CMakeFiles/gen-tags-trace is dirty ninja explain: src/base/Trace_tags.tmp is dirty ninja explain: src/base/Debug_tags is dirty ninja explain: src/base/Debug_tags.h is dirty ninja explain: src/base/Trace_tags.tmp is dirty ninja explain: src/base/Trace_tags is dirty ninja explain: src/base/Trace_tags.h is dirty ninja explain: src/base/CMakeFiles/gen-tags is dirty ninja explain: src/base/Debug_tags.h is dirty ninja explain: src/base/Trace_tags.h is dirty ninja explain: src/base/Debug_tags is dirty ninja explain: src/base/Trace_tags is dirty ninja explain: src/base/gen-tags-debug is dirty ninja explain: src/base/gen-tags-trace is dirty ninja explain: output src/base/all of phony edge with no inputs doesn't exist ninja explain: src/base/all is dirty ninja explain: output src/expr/all of phony edge with no inputs doesn't exist ninja explain: src/expr/all is dirty ninja explain: output src/options/all of phony edge with no inputs doesn't exist ninja explain: src/options/all is dirty ninja explain: output src/theory/all of phony edge with no inputs doesn't exist ninja explain: src/theory/all is dirty ninja explain: output src/util/all of phony edge with no inputs doesn't exist ninja explain: src/util/all is dirty ninja explain: src/all is dirty ninja explain: output test/regress/all of phony edge with no inputs doesn't exist ninja explain: test/regress/all is dirty ninja explain: test/all is dirty [5/6] Generating Trace_tags metric count avg (us) total (ms) .ninja parse 2 7192.5 14.4 canonicalize str 3315 0.2 0.7 canonicalize path 3315 0.2 0.5 lookup node 5325 0.2 1.1 .ninja_log load 1 548.0 0.5 .ninja_deps load 1 3882.0 3.9 node stat 2234 1.4 3.0 StartEdge 12 76.8 0.9 FinishCommand 5 74.6 0.4 path->node hash load 0.77 (2468 entries / 3209 buckets) ``` This is mainly because `gen-tags-debug`, `gen-tags-trace` and `gen-gitinfo` are targets with no (stated) outputs and nothing that generates them. ## Solution This commit cleans-up the CMake inside of `src/base/CMakeLists.txt` such that, on an incremental build with no changes, no targets are fired: ``` [avj@tempvm build]$ ninja -d explain -d stats ninja explain: output proofs/signatures/all of phony edge with no inputs doesn't exist ninja explain: proofs/signatures/all is dirty ninja explain: output doc/all of phony edge with no inputs doesn't exist ninja explain: doc/all is dirty ninja explain: output src/base/all of phony edge with no inputs doesn't exist ninja explain: src/base/all is dirty ninja explain: output src/expr/all of phony edge with no inputs doesn't exist ninja explain: src/expr/all is dirty ninja explain: output src/options/all of phony edge with no inputs doesn't exist ninja explain: src/options/all is dirty ninja explain: output src/theory/all of phony edge with no inputs doesn't exist ninja explain: src/theory/all is dirty ninja explain: output src/util/all of phony edge with no inputs doesn't exist ninja explain: src/util/all is dirty ninja explain: src/all is dirty ninja explain: output test/regress/all of phony edge with no inputs doesn't exist ninja explain: test/regress/all is dirty ninja explain: test/all is dirty ninja: no work to do. metric count avg (us) total (ms) .ninja parse 2 9198.0 18.4 canonicalize str 5314 0.2 1.1 canonicalize path 5314 0.2 0.9 lookup node 7324 0.2 1.6 .ninja_log load 1 635.0 0.6 .ninja_deps load 1 4309.0 4.3 node stat 2240 1.3 3.0 path->node hash load 0.78 (2490 entries / 3209 buckets) ``` The important bit is `ninja: no work to do.` in the output. ### Notes I think the only thing to note is that I have changed the CMake around this comment: ``` # Note: gen-tags-{debug,trace} are targets since we always want to generate # the temporary tag files {Debug,Trace}_tags.tmp in order to check if tags # were added/modified/deleted. ``` I believe that the intention here was to ensure that the tags are **always** generated on a source file change. Given that the CVC4 CMake is passing in the files to be processed (`${source_files_list}`, which is a *string*), we can add a target dependency on this *list* (`${source_files}`) to ensure that `{Debug,Trace}_tags.tmp` always get regenerated on a change. So I believe I have captured the intent of the comment, without requiring the targets to be "unconditional". I have also added a dependency on `${gentmptags_script}`/`${gentags_script}`/`${genheader_script}` in some places because, without this, if you change one of `${gentmptags_script}`/`${gentags_script}`/`${genheader_script}` then the associated targets don't get fired. Signed-off-by: Andrew V. Jones --- diff --git a/src/base/CMakeLists.txt b/src/base/CMakeLists.txt index 000aa331c..96b188238 100644 --- a/src/base/CMakeLists.txt +++ b/src/base/CMakeLists.txt @@ -4,8 +4,17 @@ find_package(Git) configure_file(GitInfo.cmake.in GitInfo.cmake @ONLY) +add_custom_command( + OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/git_versioninfo.cpp + COMMAND ${CMAKE_COMMAND} -DGIT_FOUND=${GIT_FOUND} -P GitInfo.cmake +) +set_source_files_properties( + ${CMAKE_CURRENT_BINARY_DIR}/git_versioninfo.cpp + PROPERTIES GENERATED TRUE +) add_custom_target(gen-gitinfo - COMMAND ${CMAKE_COMMAND} -DGIT_FOUND=${GIT_FOUND} -P GitInfo.cmake) + DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/git_versioninfo.cpp +) #-----------------------------------------------------------------------------# @@ -40,47 +49,42 @@ file(GLOB_RECURSE source_files ${PROJECT_SOURCE_DIR}/src/*.g) string(REPLACE ";" " " source_files_list "${source_files}") -# Note: gen-tags-{debug,trace} are targets since we always want to generate -# the temporary tag files {Debug,Trace}_tags.tmp in order to check if tags -# were added/modified/deleted. -add_custom_target( - gen-tags-debug +add_custom_command( + OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/Debug_tags.tmp COMMAND ${gentmptags_script} ${CMAKE_CURRENT_LIST_DIR} Debug ${source_files_list} - DEPENDS mktags - BYPRODUCTS ${CMAKE_CURRENT_BINARY_DIR}/Debug_tags.tmp + DEPENDS mktags ${gentmptags_script} ${source_files} ) -add_custom_target( - gen-tags-trace +add_custom_command( + OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/Trace_tags.tmp COMMAND ${gentmptags_script} ${CMAKE_CURRENT_LIST_DIR} Trace ${source_files_list} - DEPENDS mktags - BYPRODUCTS ${CMAKE_CURRENT_BINARY_DIR}/Trace_tags.tmp + DEPENDS mktags ${gentmptags_script} ${source_files} ) add_custom_command( OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/Debug_tags COMMAND ${gentags_script} Debug - DEPENDS gen-tags-debug ${CMAKE_CURRENT_BINARY_DIR}/Debug_tags.tmp + DEPENDS ${gentags_script} ${CMAKE_CURRENT_BINARY_DIR}/Debug_tags.tmp ) add_custom_command( OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/Trace_tags COMMAND ${gentags_script} Trace - DEPENDS gen-tags-trace ${CMAKE_CURRENT_BINARY_DIR}/Trace_tags.tmp + DEPENDS ${gentags_script} ${CMAKE_CURRENT_BINARY_DIR}/Trace_tags.tmp ) add_custom_command( OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/Debug_tags.h COMMAND ${genheader_script} ${CMAKE_CURRENT_LIST_DIR} Debug - DEPENDS mktagheaders ${CMAKE_CURRENT_BINARY_DIR}/Debug_tags + DEPENDS mktagheaders ${genheader_script} ${CMAKE_CURRENT_BINARY_DIR}/Debug_tags ) add_custom_command( OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/Trace_tags.h COMMAND ${genheader_script} ${CMAKE_CURRENT_LIST_DIR} Trace - DEPENDS mktagheaders ${CMAKE_CURRENT_BINARY_DIR}/Trace_tags + DEPENDS mktagheaders ${genheader_script} ${CMAKE_CURRENT_BINARY_DIR}/Trace_tags ) add_custom_target(gen-tags @@ -88,3 +92,9 @@ add_custom_target(gen-tags ${CMAKE_CURRENT_BINARY_DIR}/Debug_tags.h ${CMAKE_CURRENT_BINARY_DIR}/Trace_tags.h ) + +set_source_files_properties( + ${CMAKE_CURRENT_BINARY_DIR}/Debug_tags.h + ${CMAKE_CURRENT_BINARY_DIR}/Trace_tags.h + PROPERTIES GENERATED TRUE +)