From 2e9c7fb8b587ea2734f0c62c64aa975c4cf95489 Mon Sep 17 00:00:00 2001 From: Mathew Polzin Date: Thu, 9 Feb 2023 16:49:49 -0600 Subject: [PATCH] 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 --- CHANGELOG.md | 7 +++++- INSTALL.md | 11 +++++----- Makefile | 28 ++++++------------------ support/Makefile | 56 ++++++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 74 insertions(+), 28 deletions(-) create mode 100644 support/Makefile diff --git a/CHANGELOG.md b/CHANGELOG.md index 7eef9f24c..5116b846a 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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-` and `clean-` naming. ## v0.6.0 diff --git a/INSTALL.md b/INSTALL.md index 2f8bf72e0..72e274e4d 100644 --- a/INSTALL.md +++ b/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 diff --git a/Makefile b/Makefile index c308b12b8..68bb27c99 100644 --- a/Makefile +++ b/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} diff --git a/support/Makefile b/support/Makefile new file mode 100644 index 000000000..ce43bd6c5 --- /dev/null +++ b/support/Makefile @@ -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