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 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>
We already did this, but missed a few cases due to the way arguments are
elaborated. So now, when checking an LHS, we don't allow LHS argument
types to be inferred from the pattern, but rather they must be inferred
from elsewhere. To do this, we keep track of the constraints which would
be solved when inferring the type, and make sure they don't solve any
new metavariables. Fixes#1510, and also now gets the error location
right as a bonus!
Because it relies on the source file that I've just fixed for the
linter. I think I've now spent more time pleasing the linter than fixing
the actual bug...
We need to fully evaluate, not just the public export names, otherwise
we don't pattern match properly and potentially generate catch all
patterns we don't mean.
Fixes#1537
Why:
* To implement robust cross-project go-to-definition in LSP
i.e you can jump to definition of any global name coming
from library dependencies, as well as from the local project files.
What it does:
* Modify `FC`s to carry `ModuleIdent` for .idr sources,
file name for .ipkg sources or nothing for interactive runs.
* Add `--install-with-src` to install the source code alongside
the ttc binaries. The source is installed into the same directory
as the corresponding ttc file. Installed sources are made read-only.
* As we install the sources pinned to the related ttc files we gain
the versioning of sources for free.
Need to use the 8 byte version of Ints for the shortcut version of
reading TTCs too, otherwise we'll read the wrong hash and build things
unnecessarily.
* Add utility functions to treat All as a heterogeneous container
* Distinguish RefC Int and Bits types
* Change RefC Integers to be arbitrary precision
* Add RefC Bits maths operations
* Make RefC div and mod Euclidean
* Add RefC bit-ops tests
* Add RefC integer comparison tests
* Add RefC IntN support
This saves a lot of unnecessary exploring of size change graphs, which
can get over the top quite quickly if there's complex mutual
definitions, or even just a single function with an interesting variety
of recursive calls.
Fixes#1365Fixes#1277Fixes#645
- Fix off-by-one error in String reverse
- Correct order of arguments in strSubstr
- Actually use start index of strSubstr
- Reduce memory usage of strSubstr in case of overrunning string end
- Add fastPack/fastUnpack/fastConcat
- Use unsigned chars for character comparisons
- Fix generated C character encodings
We do this during desugaring because elaboration may insert valid
`?` values on the LHS (e.g. when elaborating things that cannot be
pattern-matched on and should be checked to be forced).
Where 'small' means they don't refer to other metavariables, except
right at the top level, and they don't go beyond a certain small depth,
arrived at by experimenting.
We already did a bit of this, but only for depth 0. The effect of this
is that we don't need to save out lots of metavariables, so ttc loading
is faster. This takes about 8s off the Idris build time!
We stored them as equations between terms, I think because terms are
easy to re-evaluate with new information, and because I thought we might
want to save them out. It's not usually a problem to do that. However...
Going back and forth between terms and values can be expensive if
we're stuck in the middle of a complicated unification problem, the like
of which can turn up a lot if your types are complicated. So, we need to
be able to handle this.
Now store the postponed problems as NF, rather than Term, and add a
fuction to resume evaluating a NF with an updated context.
* Banners for test pools
* Summary with the list of failing tests at the end
* Option to write the list of failing tests to a file
* Option to read the list of tests to run from a file
* Using these two latest features to add a new make target to rerun precisely the tests that failed last time
It has always bothered me that 'False' got mapped to tag 1 and 'True'
got mapped to tag 0. This doesn't change much in practice (except that
perhaps a code generator might notice some useful things in intToBool)
but I'm changing it now anyway. Also added a couple of inlinings of
boolean operations.
This saves a small amount of allocation, especially since we never
actually look at the tag in a record. We can use null? for Nothing just
like for Nil.
This also involves adding a flag to constructors and case alternatives
in CExp which say whether it's a NIL or CONS. Currently, we only do this
for Prelude.List, which already has an effect, but soon I'll extend this
to work for all list-shaped things and rather than being hard coded. We
could also imagine spotting other shapes (enumerations especially) for
code generators to spot as they see fit.
This will require code generators to be fixed to recognise the new
ConInfo flag, but you can just ignore it.
Bootstrap code also updated, because we don't currently have a way of
having separate support.ss/rkt for the bootstrap and normal builds!
