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>
I'm not sure how useful this is going to be, but I set it as the default
for evaluation at the REPL, since it can save duplicating work.
It's not a good choice for evaluation during type checking, since we
want to avoid evaluation when we don't need it. Also when we resume
suspended unification problems, the context may be different due to
solved metavariables, so even if we evaluate early we might still have
to evaluate again.
It's best if they don't use 'quote' (which actually is a potential
problem anyway, if quotes somehow end up nested).
applyToStack actually only worked properly for NTCon/NDCon/NPrim,
although in practice that was fine since it was only ever called in
those contexts. This fixes it so it properly continues evaluation, which
means we have a chance of caching results in more cases.
