This adds a new flag '--inc <backend>' which, if set, compiles all
modules incrementally, and for executables, links the incrementally
compiled modules rather than building the whole program.
Also, adds an environment variable IDRIS2_INC_CGS for providing a comma
separated list of backends to use for incremental builds.
Also, adds '--whole-program', which overrides incremental builds for an
executable.
Incremental builds are much faster if there's nothing to recompile, but
for the Chez backend, generate code which runs at about half the speed.
Currently only works for Chez - other backends ignore the flag.
Also, incremental building of an executable will only work if *all*
required modules have been built incrementally for the backend in use.
Set the maximum time when initialising the timer, which means we can
check in the middle of potentially expensive operations like
normalisation, rather than just at occasional points in expression
search.
If it's solved by unification, expression search should just print the
unified value. In fact it almost did this, but wasn't reducing the holes
so the result was being rendered incorrectly.
This is set to 1 second by default. Usually if it hasn't found a result
by then, it never will, but given that we find the first batch of
results then sort them, the timeout also stops us fruitlessly searching
for more solutions.
Hopefully 1s is more than enough for CI too. There is a mechanism to
change the timeout (%search_timeout) so if it turns out that CI needs
longer in some cases, we can increase it there.
I haven't documented this yet, but proof/definition search needs
documenting in general. I'll get to that.
The timer mechanism may also be useful elsewhere - I'm considering it
for ambiguity warnings, because the ambiguity depth limit isn't working
very well for that.
The Gentoo Chez package and some versions of the Ubuntu package
install Chez scheme as `/usr/bin/chezscheme' which requires manually
setting the CHEZ environment variable. Adding it to the search path
makes it easier for these users.
Closes: https://github.com/idris-lang/Idris2/issues/666
The option is hidden being a flag (`-Xcheck-hashes`) so that by default `touch`ing
a file is enough to get it recompiled.
Co-authored-by: Ben Hormann <benhormann@users.noreply.github.com>
