While the discussion about how to refactor test framework is not
finished (#1654), make this change: move `rm -rf build` in the
beginning of the test. For these reasons:
* it is useful to inspect the contents of the `build` directory
especially after the test failure
* if build crashes mid-test (e.g. process killed), next run should
not be affected by the `build` directory from the previous run
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.
On Unix-like operating systems stdio.h is usually line-buffered. As
putStr uses fputs(3) from stdio.h internally, output will be written to
standard out after a newline character is written to the buffer. Since
the prompt does not contain a newline, it will only be written to
standard output after the user presses return. I encountered this issue
on Alpine Linux which uses musl libc (instead of glibc). However, I
believe this issue is likely also reproducible with glibc. This commit
fixes this issue by flushing standard output after writing the prompt to
it. Surprisingly, `src/Idris/IDEMode/REPL.idr` already does this
correctly, `src/Idris/REPL.idr` does not though.
- Added initial implementations for terms and values
- Error messages converted to pretty printer
- Colorization for error messages
- Color and console width option both as command line and repl command
