Ensure correct CMake dependencies on Debug_tags.h/Trace_tags.h/git_versioninfo.cpp...

## 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 <andrew.jones@vector.com>

diff --git a/src/base/CMakeLists.txt b/src/base/CMakeLists.txt
index 000aa331c7f0ac5db1b55cc4ecdf2fb1230bd97d..96b18823826195d691550167630ec8396790b212 100644 (file)
--- 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
+)