diff --git a/CHANGELOG.md b/CHANGELOG.md index 2a1315fa3..2ae31906e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -43,7 +43,8 @@ * Generated JavaScript files now include a shebang when using the Node.js backend * NodeJS now supports `popen`/`pclose` for the `Read` mode. -* `getChar` is now supported on Node.js and `putChar` is supported on both JavaScript backends. +* `getChar` is now supported on Node.js and `putChar` is supported on both + JavaScript backends. * Integer-indexed arrays are now supported. ### Compiler changes @@ -94,7 +95,8 @@ * Constant folding of trivial let statements and `believe_me`. -* Fixed a bug that caused holes to appear unexpectedly during quotation of dependent pairs. +* Fixed a bug that caused holes to appear unexpectedly during quotation of + dependent pairs. ### Library changes @@ -121,8 +123,8 @@ * Add `Show` instance to `Data.Vect.Quantifiers.All` and add a few helpers for listy computations on the `All` type. * Add an alias for `HVect` to `All id` in `Data.Vect.Quantifiers.All`. This is the - approach to getting a heterogeneous `Vect` of elements that is general preferred by - the community vs. a standalone type as seen in `contrib`. + approach to getting a heterogeneous `Vect` of elements that is general + preferred by the community vs. a standalone type as seen in `contrib`. * Add `Data.List.HasLength` from the compiler codebase slash contrib library but adopt the type signature from the compiler codebase and some of the naming from the contrib library. The type ended up being `HasLength n xs` rather than @@ -151,7 +153,8 @@ * Adds `Vect.allFins` for generating all the `Fin` elements as a `Vect` with matching length to the number of elements. -* Add `withRawMode`, `enableRawMode`, `resetRawMode` for character at a time input on stdin. +* Add `withRawMode`, `enableRawMode`, `resetRawMode` for character at a time + input on stdin. * Adds extraction functions to `Data.Singleton`. @@ -173,8 +176,8 @@ * `Eq` and `Ord` implementations for `Fin n` now run in constant time. -* Adds `getTermCols` and `getTermLines` to the base library. They return the size of the - terminal if either stdin or stdout is a tty. +* Adds `getTermCols` and `getTermLines` to the base library. They return the + size of the terminal if either stdin or stdout is a tty. #### System @@ -185,12 +188,13 @@ ### Contrib -* Adds `Data.List.Sufficient`, a small library defining a structurally inductive view of lists. +* Adds `Data.List.Sufficient`, a small library defining a structurally inductive + view of lists. -* Remove `Data.List.HasLength` from `contrib` library but add it to the `base` library - with the type signature from the compiler codebase and some of the naming - from the `contrib` library. The type ended up being `HasLength n xs` rather than - `HasLength xs n`. +* Remove `Data.List.HasLength` from `contrib` library but add it to the `base` + library with the type signature from the compiler codebase and some of the + naming from the `contrib` library. The type ended up being `HasLength n xs` + rather than `HasLength xs n`. * Adds an implementation for `Functor Text.Lexer.Tokenizer.Tokenizer`. @@ -217,11 +221,16 @@ recognized as a "data" directory by Idris 2. See the [documentation on Packages](https://idris2.readthedocs.io/en/latest/reference/packages.html) for details. -* The compiler no longer installs its own C support library into `${PREFIX}/lib`. This folder's - contents were always duplicates of files installed into `${PREFIX}/idris2-${IDRIS2_VERSION}/lib`. If you - need to adjust any tooling or scripts, point them to the latter location which still contains +* The compiler no longer installs its own C support library into + `${PREFIX}/lib`. This folder's contents were always duplicates of files + installed into `${PREFIX}/idris2-${IDRIS2_VERSION}/lib`. If you need to adjust + any tooling or scripts, point them to the latter location which still contains these installed library files. -* Renamed `support-clean` Makefile target to `clean-support`. This is in line with most of the `install-` and `clean-` naming. +* Renamed `support-clean` Makefile target to `clean-support`. This is in line + with most of the `install-` and `clean-` naming. +* Fixes an error in the `Makefile` where setting `IDRIS2_PREFIX` caused + bootstrapping to fail. +* Updates the docs for `envvars` to match the changes introduced in #2649. ## v0.6.0 diff --git a/Makefile b/Makefile index 68bb27c99..30aa8e29c 100644 --- a/Makefile +++ b/Makefile @@ -34,11 +34,11 @@ IDRIS2_LIB_IPKG := idris2api.ipkg ifeq ($(OS), windows) # This produces D:/../.. style paths - IDRIS2_PREFIX := $(shell cygpath -m ${PREFIX}) + IDRIS2_PREFIX ?= $(shell cygpath -m ${PREFIX}) IDRIS2_CURDIR := $(shell cygpath -m ${CURDIR}) SEP := ; else - IDRIS2_PREFIX := ${PREFIX} + IDRIS2_PREFIX ?= ${PREFIX} IDRIS2_CURDIR := ${CURDIR} SEP := : endif diff --git a/docs/source/reference/envvars.rst b/docs/source/reference/envvars.rst index d85cbe59b..6e7452869 100644 --- a/docs/source/reference/envvars.rst +++ b/docs/source/reference/envvars.rst @@ -8,25 +8,39 @@ Idris 2 recognises a number of environment variables, to decide where to look for packages, external libraries, code generators, etc. It currently recognises, in approximately the order you're likely to need them: -* ``EDITOR`` - Sets the editor used in REPL :e command -* ``IDRIS2_CG`` - Sets which code generator to use when compiling programs -* ``IDRIS2_PACKAGE_PATH`` - Lists the directories where Idris2 looks for packages, +* ``EDITOR`` - Editor used in REPL ``:e`` command. +* ``PREFIX`` - Default way to set the Idris2 installation prefix. +* ``IDRIS2_PREFIX`` - Alternative way to set the Idris2 installation prefix. +* ``IDRIS2_PATH`` - Directories where Idris2 looks for import files, in addition + to the imports in packages +* ``IDRIS2_PACKAGE_PATH`` - Directories where Idris2 looks for Idris 2 packages, in addition to the defaults (which are under the ``IDRIS2_PREFIX`` and in the ``depends`` subdirectory of the current working directory). - Directories are separated by a ``:``, or a ``;`` on Windows -* ``IDRIS2_PATH`` - Places Idris2 looks for import files, in addition to the - imports in packages -* ``IDRIS2_DATA`` - Places Idris2 looks for its data files. These are typically - support code for code generators. -* ``IDRIS2_LIBS`` - Places Idris2 looks for libraries used by code generators. -* ``IDRIS2_PREFIX`` - Gives the Idris2 installation prefix -* ``CHEZ`` - Sets the location of the ``chez`` executable used in Chez codegen -* ``RACKET`` - Sets the location of the ``racket`` executable used in Racket codegen -* ``RACKET_RACO`` - Sets the location of the ``raco`` executable used in Racket codegen -* ``GAMBIT_GSI`` - Sets the location of the ``gsi`` executable used in Gambit codegen -* ``GAMBIT_GSC`` - Sets the location of the ``gsc`` executable used in Gambit codegen -* ``GAMBIT_GSC_BACKEND`` - Sets the ``gsc`` executable backend argument -* ``IDRIS2_CC`` - Sets the location of the C compiler executable used in RefC codegen -* ``CC`` - Sets the location of the C compiler executable used in RefC codegen -* ``NODE`` - Sets the location of the ``node`` executable used in Node codegen -* ``PATH`` - used to search for executables in certain codegens + Directories are separated by a ``:`` on MacOS and *NIX systems, or a ``;`` on + Windows +* ``IDRIS2_DATA`` - Directories where Idris2 looks for data files. These are + typically support code for code generators. +* ``IDRIS2_LIBS`` - Directories where Idris2 looks for libraries (for code + generation). +* ``IDRIS2_CG`` - Codegen backend. +* ``IDRIS2_INC_CGS`` - Code generators to use (comma separated) when compiling modules incrementally. +* ``CHEZ`` - Chez backend: location of the ``chez`` executable. +* ``RACKET`` - Racket backend: location of the ``racket`` executable. +* ``RACKET_RACO`` - Racket backend: location of the ``raco`` executable. +* ``GAMBIT_GSI`` - Gambit backend: location of the ``gsi`` executable. +* ``GAMBIT_GSC`` - Gambit backend: location of the ``gsc`` executable. +* ``GAMBIT_GSC_BACKEND`` - Gambit backend: arguments passed to ``gsc``. +* ``IDRIS2_CC`` - RefC backend: location of the C compiler executable. +* ``IDRIS2_CFLAGS`` - RefC backend: C compiler flags. +* ``IDRIS2_CPPFLAGS`` - RefC backend: C preprocessor flags. +* ``IDRIS2_LDFLAGS`` - RefC backend: C linker flags. +* ``CC`` - RefC backend: C compiler executable (IDRIS2_CC takes precedence). +* ``CFLAGS`` - RefC backend: C compiler flags (IDRIS2_CFLAGS takes precedence). +* ``CPPFLAGS`` - RefC backend: C preprocessor flags (IDRIS2_CPPFLAGS takes precedence). +* ``LDFLAGS`` - RefC backend: C linker flags (IDRIS2_LDFLAGS takes precedence). +* ``NODE`` - NodeJS backend: ``node`` executable. +* ``PATH`` - PATH variable is used to search for executables in certain + codegens. +* ``NO_COLOR`` - Instruct Idris not to print colour to stdout. Passing the + --colour/--color option will supersede this environment variable. +