Idris' output has been updated to more accurately reflect its
progress through the compiler i.e. Type Checking; Totality Checking;
IBC Generation; Compiling; and Code Generation. To control the
loudness of the reporting three verbosity levels are introduced:
`--V0`, `--V1`, and `--V2`. The old aliases of `-V` and `--verbose`
have been retained.
I ran stylish-haskell over everything. The import grouping was
inconsistent so I just picked something: Idris.* and IRTS.*, then Util,
then autogenerated files, then modules from other packages.
+ Default location is `<getDataDir>/docs`.
+ Flag `--info` has been updated to show doc location.
+ New flag `--installdoc <ipkg>` provided to install documentation
+ New flag `--docdir` provided to show documentation installation location.
+ New environment variable `IDRIS_DOC_PATH` to allow alternate means of customisation.
+ Installation for Idris' std libraries has been augmented to install library documentation as well.
Introduction of a new module `Idris.Main` that contains the code
required to launch and run an interactive Idris session---compilation,
REPL et cetera. It has been spun out of `Idris.REPL`; common code has
been spun out from both into `Idris.ModeCommon`.
With `Idris.Main` comes a new entry point for Idris and presents
developers with a more unified API for running Idris programs. A side
affect of this approach is that the imports for codegens must be
changed to import `Idris.Main` and not `Idris.REPL`.
In anticipation of moving `idrisMain` out of `Idris.REPL` some
internal changes to Idris are made:
+ Move accessor methods for `Opt` to `AbsSyntax`.
+ Isolate and bring `Commond` under `Idris.REPL` module.
+ Fix some imports arising from changes.
+ Fix import and exports of `CmdOptions`.
This commit rehomes the code for package building and installation
under the Idris namespace, allowing for projects that use the code to
use a more meaningful import statement.
This commit also factors out the ipkg data type from the parser.
GCC on Windows will add .exe to the executable name. rawSystem needs
the exact name.
Add isWindows and put in the places that need special handling.
Conflicts:
main/Main.hs
For some inexplicable reason Haskell hardcodes latin1 as the encoding on
Windows. This stops the output when an unicode character is reached. It's better
all over to set the encoding to UTF8, if the user has a UTF8 terminal like
mintty it looks good. If the user has a terminal with latin1, there will
be some bad chars but they will see the entire text otherwise.
This is a quick and dirty solution for #1071.
I wish I were able to implement output of metadata, but since there is
no metadata saved (currently) alongside of a package, there is nothing
to display.
Displaying metadata in the output of this subcommand would mean that
there have to happen further improvements in the package-system of
idris.
Please see my proposal in #1126.
Eventually, this should be the only way to invoke code generators (by
invoking "idris-foo Main.ibc" for the code generator for backend foo.
For the moment, this serves as an example 'main' for any new code
generators, and *all* new code generators should be implemented this
way.
Add a new section to IPKG files called "tests". This section should be a
comma-separated list of fully qualified names of IO actions, the
sequence of which in some way test an Idris package.
When invoked as idris --testpkg IPKG, Idris will generate a module in a
temporary directory that imports every module from the package IPKG and
whose main function simply executes each specified test.
The intention is to keep test specifications as low-level as possible,
allowing user libraries to define a better mechanism on top of this.
continued the work on getting the parser to work
works now, still work to do though
done with the parser, removed reduntant code, added metavars
maybe fixes build error...
changed test that used --exec without arg, and added warnreach which i forgot
removed out-commented code, added last metavar
The command line option follows the convention from Perl. This causes
Idris to evaluate the provided expressions, pretty-printing them without
line breaks. Then, test results need not depend on terminal widths any
longer. If multiple -e options are provided, then the expressions are
evaluated in order.
