This gives the right location for finding libraries on the Mac, where
dirname has slightly different behaviour.
It does now require 'realpath' to be installed, which on the Mac is part
of 'coreutils' which can be installed via 'brew'
There was a lot of repeated work in packages, since it tried to build
the module tree starting from every listed module. Now, it skips the
ones where they're already in the tree.
It should be -O2 for the rts, but -O2 takes ages for idris2.c so should
be saved for releases (also OPT should be able to be edited easily for
e.g. adding profiling)
Also default to clang (perhaps it would be better if we could check
whether clang was available first, but it does a better job as the
default overall).
Surprisingly, this doesn't affect performance - it shows up as about the
same in the profile. But more importantly, it ports more directly to
Idris 2, which can't guarantee that 'strTail' doesn't allocate at
runtime, so using a List Char here is much more efficient.
This probably points to the need for better string primitives. Later...
Sorry, I should look more carefully... contrib is a space for incoming
experimental libraries that might get sorted into something better, so
it shouldn't be a place for things that are in the default library path
(this is consistent with Idris 1 behaviour)
Before compilation we need to decode all the relevant definitions from
the TTC, but the only bit we actually need is the compiled IR. So, put
that first, and leave a dummy definition for the rest, then replace it
when we're done.
Chasing all the definitions now takes about 20% of the time it did
before (at least on the program I'm most interested in)
This is instead of generating unique integer tags when generating IR to
pass to a back end. The reason is that this way requires whole program
compilation - to make sure the tags are unique - but it would be
beneficial to build the IR when checking a module, not all at once at
the end.
So, this is to support separate compilation.
It does mean the API for IRs has changed slightly - tags are now Maybe
Int rather than Int. If a tag is 'Nothing' you should generate something
to match on based on the name. The Scheme back ends currently do this
just by printing the string.
Matching on types is likely to be rare, but if this does turn out to be
a bottleneck, a backend can generate unique ids at that point, which is
a lot cheaper than doing it before building, inlining, optimising, etc.
Trying to keep both up to date - apologies if I'm missed anyone. I got
the list from the git logs, but feel free to edit yourself in or out as
you prefer.
Back ends can still shortcut these and use their own primitives, but
doing things this way gives consistent behaviour between the simple IO
primitives and file IO, and allow us to use stdin/stdout consistently
(e.g. to flush stdout).
This also fixes the behaviour of 'replWith' to be consistent with the
Idris 1 version.
