mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-25 04:33:45 +03:00
Create a separate Makefile for the Idris 2 support libraries. (#2869)
* Create a separate Makefile for the Idris 2 support libraries. * Update INSTALL.md * satisfy natural language linter * Add to CHANGELOG * Update CHANGELOG.md
This commit is contained in:
parent
f76c4c4307
commit
2e9c7fb8b5
@ -107,7 +107,7 @@
|
||||
#### Papers
|
||||
|
||||
* In `Control.DivideAndConquer`: a port of the paper
|
||||
`A Type-Based Approach to Divide-And-Conquer Recursion in Coq'
|
||||
`A Type-Based Approach to Divide-And-Conquer Recursion in Coq`
|
||||
by Pedro Abreu, Benjamin Delaware, Alex Hubers, Christa Jenkins,
|
||||
J. Garret Morris, and Aaron Stump
|
||||
|
||||
@ -116,6 +116,11 @@
|
||||
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
|
||||
these installed library files.
|
||||
* Renamed `support-clean` Makefile target to `clean-support`. This is in line with most of the `install-<something>` and `clean-<something>` naming.
|
||||
|
||||
## v0.6.0
|
||||
|
||||
|
11
INSTALL.md
11
INSTALL.md
@ -9,13 +9,14 @@ The easiest way to install is via the existing generated Scheme code.
|
||||
The requirements are:
|
||||
|
||||
- A Scheme compiler; either Chez Scheme (default), or Racket.
|
||||
- `bash`, `GNU make`, `sha256sum` and `GMP`. On Linux, you probably already
|
||||
- `bash`, `GNU make`, `gcc` or `clang`, `sha256sum` and `GMP`. On Linux, you probably already
|
||||
have these. On macOS and major BSD flavours, you can install them using a
|
||||
package manager: for instance, on macOS, you can install with the
|
||||
`brew install coreutils gmp` and on OpenBSD, with the `pkg_add coreutils
|
||||
bash gmake gmp` command. You specifically need the dev GMP library, which
|
||||
means on some systems the package you need to install will be named
|
||||
something more like `libgmp3-dev`.
|
||||
something more like `libgmp3-dev`. macOS ships with `clang` whereas `gcc` is more
|
||||
common for other \*nix distributions.
|
||||
|
||||
On Windows, it has been reported that installing via `MSYS2` works
|
||||
[MSYS2](https://www.msys2.org/). On Windows older than Windows 8, you may need to
|
||||
@ -45,8 +46,6 @@ If you have an existing Idris 2, go to Step 3. Otherwise, read on...
|
||||
Make sure that:
|
||||
|
||||
- `$PREFIX/bin` is in your `PATH`
|
||||
- `$PREFIX/lib` is in your `LD_LIBRARY_PATH` or `DYLD_LIBRARY_PATH` if on
|
||||
`macOS` (so that the system knows where to look for library support code)
|
||||
|
||||
### 2: Installing without an existing Idris 2
|
||||
|
||||
@ -70,6 +69,8 @@ If all is well, to install, type:
|
||||
|
||||
- `make install`
|
||||
|
||||
If you are building with Racket, you'll need to run `IDRIS2_CG=racket make install`.
|
||||
|
||||
### 3: Installing with an existing Idris 2
|
||||
|
||||
If you have the latest *released* version of Idris 2
|
||||
@ -103,7 +104,7 @@ executable in `./build/exec`.
|
||||
|
||||
If you are working on Idris, incremental compilation means that rebuilds are
|
||||
much faster, at the cost of runtime performance being slower. To enable
|
||||
incremental compilation for the Chez back end, set the environment variable
|
||||
incremental compilation for the Chez backend, set the environment variable
|
||||
`IDRIS2_INC_CGS=chez`, or set the `--inc chez` flag in `idris2.ipkg`.
|
||||
|
||||
### 8: (Optional) Installing the Idris 2 API
|
||||
|
28
Makefile
28
Makefile
@ -57,7 +57,7 @@ export IDRIS2_BOOT_PATH := "$(IDRIS2_BOOT_PATH)"
|
||||
|
||||
export SCHEME
|
||||
|
||||
.PHONY: all idris2-exec libdocs testenv testenv-clean support support-clean clean FORCE
|
||||
.PHONY: all idris2-exec libdocs testenv testenv-clean support clean-support clean FORCE
|
||||
|
||||
all: support ${TARGET} libs
|
||||
|
||||
@ -162,14 +162,10 @@ test-installed:
|
||||
@${MAKE} -C tests only=$(only) IDRIS2=$(IDRIS2_PREFIX)/bin/idris2 IDRIS2_PREFIX=${IDRIS2_PREFIX}
|
||||
|
||||
support:
|
||||
@${MAKE} -C support/c
|
||||
@${MAKE} -C support/refc
|
||||
@${MAKE} -C support/chez
|
||||
@${MAKE} -C support
|
||||
|
||||
support-clean:
|
||||
@${MAKE} -C support/c cleandep
|
||||
@${MAKE} -C support/refc cleandep
|
||||
@${MAKE} -C support/chez clean
|
||||
clean-support:
|
||||
@${MAKE} -C support clean
|
||||
|
||||
clean-libs:
|
||||
${MAKE} -C libs/prelude clean
|
||||
@ -180,7 +176,7 @@ clean-libs:
|
||||
${MAKE} -C libs/linear clean
|
||||
${MAKE} -C libs/papers clean
|
||||
|
||||
clean: clean-libs support-clean testenv-clean
|
||||
clean: clean-libs clean-support testenv-clean
|
||||
-${IDRIS2_BOOT} --clean ${IDRIS2_APP_IPKG}
|
||||
$(RM) src/IdrisPaths.idr
|
||||
${MAKE} -C tests clean
|
||||
@ -201,23 +197,11 @@ install-idris2:
|
||||
ifeq ($(OS), windows)
|
||||
-install ${TARGET}.cmd ${PREFIX}/bin
|
||||
endif
|
||||
mkdir -p ${PREFIX}/lib/
|
||||
install support/c/${IDRIS2_SUPPORT} ${PREFIX}/lib
|
||||
mkdir -p ${PREFIX}/bin/${NAME}_app
|
||||
install ${TARGETDIR}/${NAME}_app/* ${PREFIX}/bin/${NAME}_app
|
||||
|
||||
install-support:
|
||||
mkdir -p ${PREFIX}/${NAME_VERSION}/support/docs
|
||||
mkdir -p ${PREFIX}/${NAME_VERSION}/support/racket
|
||||
mkdir -p ${PREFIX}/${NAME_VERSION}/support/gambit
|
||||
mkdir -p ${PREFIX}/${NAME_VERSION}/support/js
|
||||
install -m 644 support/docs/*.css ${PREFIX}/${NAME_VERSION}/support/docs
|
||||
install -m 644 support/racket/* ${PREFIX}/${NAME_VERSION}/support/racket
|
||||
install -m 644 support/gambit/* ${PREFIX}/${NAME_VERSION}/support/gambit
|
||||
install -m 644 support/js/* ${PREFIX}/${NAME_VERSION}/support/js
|
||||
@${MAKE} -C support/c install
|
||||
@${MAKE} -C support/refc install
|
||||
@${MAKE} -C support/chez install
|
||||
@${MAKE} -C support install
|
||||
|
||||
install-bootstrap-libs:
|
||||
${MAKE} -C libs/prelude install IDRIS2=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH} IDRIS2_INC_CGS=${IDRIS2_CG}
|
||||
|
56
support/Makefile
Normal file
56
support/Makefile
Normal file
@ -0,0 +1,56 @@
|
||||
include ../config.mk
|
||||
|
||||
.PHONY: build build-c build-refc build-chez
|
||||
|
||||
build: build-c build-refc build-chez
|
||||
|
||||
build-c:
|
||||
@${MAKE} -C c
|
||||
|
||||
build-refc:
|
||||
@${MAKE} -C refc
|
||||
|
||||
build-chez:
|
||||
@${MAKE} -C chez
|
||||
|
||||
.PHONY: clean clean-c clean-refc clean-chez
|
||||
|
||||
clean: clean-c clean-refc clean-chez
|
||||
|
||||
clean-c:
|
||||
@${MAKE} -C c cleandep
|
||||
|
||||
clean-refc:
|
||||
@${MAKE} -C refc cleandep
|
||||
|
||||
clean-chez:
|
||||
@${MAKE} -C chez clean
|
||||
|
||||
.PHONY: install install-docs install-racket install-gambit install-js install-c install-refc install-chez
|
||||
|
||||
install: install-docs install-racket install-gambit install-js install-c install-refc install-chez
|
||||
|
||||
install-docs:
|
||||
mkdir -p ${PREFIX}/${NAME_VERSION}/support/docs
|
||||
install -m 644 docs/*.css ${PREFIX}/${NAME_VERSION}/support/docs
|
||||
|
||||
install-racket:
|
||||
mkdir -p ${PREFIX}/${NAME_VERSION}/support/racket
|
||||
install -m 644 racket/* ${PREFIX}/${NAME_VERSION}/support/racket
|
||||
|
||||
install-gambit:
|
||||
mkdir -p ${PREFIX}/${NAME_VERSION}/support/gambit
|
||||
install -m 644 gambit/* ${PREFIX}/${NAME_VERSION}/support/gambit
|
||||
|
||||
install-js:
|
||||
mkdir -p ${PREFIX}/${NAME_VERSION}/support/js
|
||||
install -m 644 js/* ${PREFIX}/${NAME_VERSION}/support/js
|
||||
|
||||
install-c:
|
||||
@${MAKE} -C c install
|
||||
|
||||
install-refc:
|
||||
@${MAKE} -C refc install
|
||||
|
||||
install-chez:
|
||||
@${MAKE} -C chez install
|
Loading…
Reference in New Issue
Block a user