Update all scripts and build system to call python3, given python2's
upcoming doom. Use sys.maxsize instead of sys.maxint in one script
(maxint does not exist in python3).
INTERNAL implies FORCE but in some versions of CMake if a config option
has been passed in via a -D option the INTERNAL set doesn't override the
value when it should.
See: https://gitlab.kitware.com/cmake/cmake/issues/19015
INTERNAL does not imply FORCE for CACHE
- Minimise calls to external_process as this is more expensive than
using built-in CMake file operations.
- Update check_outfile_stale to also save the list of files it checks
for stale checks so if a config changes the list of files then the
output file will still be stale even if the input list of files are
older than it.
Our upcoming cmake styling tool requires any custom functions you want
styled nicely to be lower case. We only need to style these two nicely,
as they have kwargs we would like aligned.
Add kernel_platforms_string and kernel_platforms_list to tools/helpers.cmake.
kernel_platforms_string: concatenates all platform strings together into a
newline separated string.
kernel_platforms_list: returns a list of all kernel platforms.
Modified the behaviour of the EXACT_INPUT option within the
CPPFile helper function. Now named EXACT_NAME, the option
copies the input file to a temporary file. The name of the
temporary file is also passed in by the caller. This
step in necessary in getting the CPP step to correctly
depend on the targets given by the caller
(through EXTRA_DEPS). Also updated the CPP generation of the
kernel_all.i file to reflect the change.
REALPATH was unnecessary and results in resolving symlinks in the target, although
the working directory will not have its symlink resolved. This results in very strange
paths from the base directory (which is the working directory) to the target.
This is a new version of GenCPPCommand that uses an OBJECT library intermediate to get
cmake to do 'arbitrary' compilation (by adding the -E flag) where the result does not
need to be linkable. The advantage of this over the GenCPPCommand version is there is
no need for trying to manually invoke GCC with all the correct arguments lists.
As a macro this helper would not operate as expected if output and input were defined
as the same variable. Making a function and explicitly writing into the PARENT_SCOPE
fixes this and also makes the code simpler
This change makes values take on more intuitive and expected defaults when gradually
configuring the kernel, either programatically or through the graphic interfaces
TOPLEVELTYPES is not intended to be configurable by the user, rather is a reflection
on the types defined by the source. This changes the TOPLEVELTYPES argument to be
a property, allowing it to be constructed as a generator expression when generating
BF files. By being a property, and not something like a global property, it removes
the need to ensure that additions to TOPLEVELTYPES are done prior to any bitfield
target definitions.
Uses the COMMAND_EXPAND_LISTS flag to allow for generator expressions in parameters
to GenBFCommand. As lists are now being expanded the 'args' variable must also be
quoted.
Previously if a variable had unmet dependencies and had been hidden, by being made
an internal variable, it would not have been unhidden by the use of `option`. This
emulates the behaviour of `option` that we were wanting, but additionally using `FORCE`
to override the `INTERNAL` setting
Uses file(GENERATE) to directly create the contents of generated configuration files instead of
awkwardly using custom commands to echo the contents of multi line strings into files.
Newer versions of cmake provide a COMMAND_EXPAND_LISTS option that allows a quoted string,
such as "a;b" to be given to a COMMAND parameter and have it expand into multiple arguments.
Using this we can much more nicely generate some of our COMMAND invocations, at the cost of
requiring a more recent cmake version
The config_option helper was previously using cmake_dependent_option, which supposedly took
a value to set the option to in the case where it was disabled. However, this only sets
the value in the current function context, and not the cache. I do not understand why this
is the case and it seems to make that functionality completely useless. This commit simply
does the dependency checking itself and correctly sets the disabled value.
Instead of explicitly depending on Kernel_C.thy prior to generating proofs, this removes
the dependency check and leaves isabelle to check the dependency upon import.
