reported by @nbraud reported in #1227.
Previously the CMake build system assumed that the `.git` file must
be a directory. This is not the case when the working directory
is a "git worktree". In this case the `.git` file is just a plain
file that points to a directory within the true `.git` directory.
This commit essentially implements the logic to traverse this extra
level of indirection and removes some assumptions that the `.git`
file is a directory.
Now that all include paths are relative to the `src/` trees (
one in source tree and one in the build tree) we can simplify
what the CMake build does significantly.
While I'm here I also removed some dead code that wasn't doing
anything useful.
to allow a new mode `SERIOUS_ONLY`.
Modes:
`ON` - All warnings are treated as errors (same as before)
`OFF` - Warnings are not treated as errors (same as before)
`SERIOUS_ONLY` - A subset of "serious" warnings are treated as errors.
Upgrade code is included to upgrade old CMake cache's to use the new
type of `WARNINGS_AS_ERRORS`. We should remove it eventually. The
user's previous setting is preserved when doing this.
Very few warnings are treated as errors for now. Developers can
add more later as they see fit.
Previously CMake was not aware of which headers files the generation
of `mem_initializer.cpp` depended on. Consequently this could result
in broken incremental builds if
* Existing headers that declare memory initializers/finalizers change.
* New headers are added that declare memory initializers/finalizer.
Now the `z3_add_component()` CMake function has been modifed so that
it now takes an optional `MEMORY_INIT_FINALIZER_HEADERS` argument
which allows the headers that declare memory initializers/finalizers
to be explicitly listed.
With this information CMake will now regenerate `mem_initializer.cpp`
correctly.
This required the `mk_mem_initializer_cpp_internal()` function to be
changed to take a list of header files rather than a list of component
source directories. The two consumers (CMake and Python/Makefile build
systems) of this function have been modified to work with this change.
This partially fixes#1030.
Previously CMake was not aware of which headers files the generation
of `gparams_register_modules.cpp` depended on. Consequently this could result
in broken incremental builds if
* Existing headers that declared module description/parameters change.
* New headers are added that declare module description/parameters.
* `.pyg` files that generate header files that declare module
description/parameters change
Now the `z3_add_component()` CMake function has been modifed so that
* All header files that are generated from `.pyg` files are added as
dependencies and are scanned from module description/parameter
declarations. This implicit dependency of `gparams_register_modules.cpp`
depending on other generated header files seems unnecessary complex. We
should revisit this design decision once the Python/Makefile build
system is deprecated.
* The function now takes an optional `EXTRA_REGISTER_MODULE_HEADERS`
argument which allows the headers that declare module
description/paramters to be explicitly listed.
With this information CMake will now regenerate `gparams_register_modules.cpp`
correctly.
This required the `mk_gparams_register_modules_internal()` function to be
changed to take a list of header files rather than a list of component
source directories. The two consumers (CMake and Python/Makefile build
systems) of this function have been modified to work with this change.
This partially fixes#1030.
Previously CMake was not aware of which headers files the generation
of `install_tactic.cpp` depended on. Consequently this could result
in broken incremental builds if
* Existing headers that declared tactics/probes changed.
* New tactics/probes were added to new header files.
Now the `z3_add_component()` CMake function has been modifed to take an
optional `TACTIC_HEADERS` argument which allows the headers that declare
tactics/probes to be explicitly listed. The necessary component
declarations have been modified to declare their tactic/probe header
files.
With this information CMake will now regenerate `install_tactic.cpp`
correctly.
This required the `mk_install_tactic_cpp_internal()` function to be
changed to take a list of header files rather than a list of component
source directories. The two consumers (CMake and Python/Makefile build
systems) of this function have been modified to work with this change.
This partially fixes#1030.
`contrib/cmake/bootstrap.py` script no longer needs to be executed.
The previous location of the CMake files was a compromise proposed
by @agurfinkel in #461. While this has served us well (allowing progress
to be made) over time limitations of this approach have appeared.
The main problem is that doing many git operations (e.g. pull, rebase)
means the CMake files don't get updated unless the user remembers to
run the script. This can lead to broken and confusing build system
behaviour.
This commit only does the file moving and necessary changes to
`.gitignore`. Other changes will be done in subsequent commits.
