From 9e42eb1be16cc70b9504523df79a26ede8e390ce Mon Sep 17 00:00:00 2001 From: Kamil Shakirov <kamils80@gmail.com> Date: Thu, 18 Jun 2020 17:19:48 +0600 Subject: [PATCH] Fix 'install-api' makefile target When building from a clean state `src/IdrisPaths.idr` must be generated first before installing `idris2api.ipkg`. --- Makefile | 2 +- docs/source/backends/custom.rst | 17 ++++++++--------- 2 files changed, 9 insertions(+), 10 deletions(-) diff --git a/Makefile b/Makefile index aab3159ce..434646daf 100644 --- a/Makefile +++ b/Makefile @@ -101,7 +101,7 @@ clean: clean-libs support-clean install: install-idris2 install-support install-libs -install-api: +install-api: src/IdrisPaths.idr ${IDRIS2_BOOT} --install idris2api.ipkg install-idris2: diff --git a/docs/source/backends/custom.rst b/docs/source/backends/custom.rst index 877b2c2b5..699719a4d 100644 --- a/docs/source/backends/custom.rst +++ b/docs/source/backends/custom.rst @@ -10,13 +10,12 @@ starting idris with these codegens in addition to the built-in ones. Getting started =============== -To use Idris 2 as a library you need to install it with (the ipkg file -is at the top level of the Idris2 repo) +To use Idris 2 as a library you need to install it with (at the top level of the +Idris2 repo) :: - idris2 --build idris2api.ipkg - idris2 --install idris2api.ipkg + make install-api Now create a file containing @@ -53,11 +52,11 @@ Now you have an idris2 with an added backend. :: $ ./build/exec/lazy-idris2 - ____ __ _ ___ + ____ __ _ ___ / _/___/ /____(_)____ |__ \ - / // __ / ___/ / ___/ __/ / Version 0.2.0-d8c7f08bd - _/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org - /___/\__,_/_/ /_/____/ /____/ Type :? for help + / // __ / ___/ / ___/ __/ / Version 0.2.0-bd9498c00 + _/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org + /___/\__,_/_/ /_/____/ /____/ Type :? for help Welcome to Idris 2. Enjoy yourself! With codegen for: lazy @@ -67,6 +66,6 @@ It will not be overly eager to actually compile any code with the new backend th :: - $ ./build/exec/lazy --cg lazy Hello.idr -o hello + $ ./build/exec/lazy-idris2 --cg lazy Hello.idr -o hello I'd rather not. $