Separate support derivation (and small related tweaks to the Makefile) (

#3172)

Makefile

@@ -43,8 +43,12 @@ else
 	SEP := :
 endif
 
+IDRIS2_SUPPORT_DIR ?= ${IDRIS2_CURDIR}/support/c
+
 TEST_PREFIX ?= ${IDRIS2_CURDIR}/build/env
 
+TEST_IDRIS2_SUPPORT_DIR ?= ${TEST_PREFIX}/${NAME_VERSION}
+
 # Library and data paths for bootstrap-test
 IDRIS2_BOOT_PREFIX := ${IDRIS2_CURDIR}/bootstrap-build
 
@@ -67,7 +71,7 @@ idris2-exec: ${TARGET}
 
 ${TARGET}: support src/IdrisPaths.idr
 	${IDRIS2_BOOT} --build ${IDRIS2_APP_IPKG}
-	cp ${IDRIS2_CURDIR}/support/c/${IDRIS2_SUPPORT} ${TARGETDIR}/${NAME}_app/${IDRIS2_SUPPORT}
+	cp ${IDRIS2_SUPPORT_DIR}/${IDRIS2_SUPPORT} ${TARGETDIR}/${NAME}_app/${IDRIS2_SUPPORT}
 
 # We use FORCE to always rebuild IdrisPath so that the git SHA1 info is always up to date
 src/IdrisPaths.idr: FORCE
@@ -113,7 +117,6 @@ libdocs:
 
 ifeq ($(OS), windows)
 ${TEST_PREFIX}/${NAME_VERSION} :
-	${MAKE} install-support PREFIX=${TEST_PREFIX}
 	cp -rf ${IDRIS2_CURDIR}/libs/prelude/build/ttc ${TEST_PREFIX}/${NAME_VERSION}/prelude-${IDRIS2_VERSION}
 	cp -rf ${IDRIS2_CURDIR}/libs/base/build/ttc    ${TEST_PREFIX}/${NAME_VERSION}/base-${IDRIS2_VERSION}
 	cp -rf ${IDRIS2_CURDIR}/libs/linear/build/ttc  ${TEST_PREFIX}/${NAME_VERSION}/linear-${IDRIS2_VERSION}
@@ -122,7 +125,6 @@ ${TEST_PREFIX}/${NAME_VERSION} :
 	cp -rf ${IDRIS2_CURDIR}/libs/test/build/ttc    ${TEST_PREFIX}/${NAME_VERSION}/test-${IDRIS2_VERSION}
 else
 ${TEST_PREFIX}/${NAME_VERSION} :
-	${MAKE} install-support PREFIX=${TEST_PREFIX}
 	ln -sf ${IDRIS2_CURDIR}/libs/prelude/build/ttc ${TEST_PREFIX}/${NAME_VERSION}/prelude-${IDRIS2_VERSION}
 	ln -sf ${IDRIS2_CURDIR}/libs/base/build/ttc    ${TEST_PREFIX}/${NAME_VERSION}/base-${IDRIS2_VERSION}
 	ln -sf ${IDRIS2_CURDIR}/libs/linear/build/ttc  ${TEST_PREFIX}/${NAME_VERSION}/linear-${IDRIS2_VERSION}
@@ -133,7 +135,13 @@ endif
 
 .PHONY: ${TEST_PREFIX}/${NAME_VERSION}
 
-testenv:
+${TEST_IDRIS2_SUPPORT_DIR}/${IDRIS2_SUPPORT}:
+	${MAKE} install-support PREFIX=${TEST_PREFIX}
+
+test-support: ${TEST_IDRIS2_SUPPORT_DIR}/${IDRIS2_SUPPORT}
+
+testenv: test-support
+	mkdir -p ${TEST_PREFIX}/${NAME_VERSION}
 	@${MAKE} ${TEST_PREFIX}/${NAME_VERSION}
 	@${MAKE} -C tests testbin IDRIS2=${TARGET} IDRIS2_PREFIX=${TEST_PREFIX}
 
@@ -164,9 +172,11 @@ test-installed:
 	@${MAKE} -C tests testbin      IDRIS2=$(IDRIS2_PREFIX)/bin/idris2 IDRIS2_PREFIX=${IDRIS2_PREFIX}
 	@${MAKE} -C tests only=$(only) IDRIS2=$(IDRIS2_PREFIX)/bin/idris2 IDRIS2_PREFIX=${IDRIS2_PREFIX}
 
-support:
+${IDRIS2_SUPPORT_DIR}/${IDRIS2_SUPPORT}:
 	@${MAKE} -C support
 
+support: ${IDRIS2_SUPPORT_DIR}/${IDRIS2_SUPPORT}
+
 clean-support:
 	@${MAKE} -C support clean
 
@@ -243,11 +253,15 @@ install-libdocs: libdocs
 .PHONY: bootstrap bootstrap-build bootstrap-racket bootstrap-racket-build bootstrap-test bootstrap-clean
 
 # Bootstrapping using SCHEME
+#
+# If you are bootstrapping using SCHEME _without building support_, support must have been explicitly
+# built previously and you must set the IDRIS2_SUPPORT_DIR and IDRIS2_DATA environment variables to the
+# locations of the lib and support folders (i.e. "/some/location/lib" and "/some/location/support").
 bootstrap: support
 	@if [ "$$(echo '(threaded?)' | $(SCHEME) --quiet)" = "#f" ] ; then \
 		echo "ERROR: Chez is missing threading support" ; exit 1 ; fi
 	mkdir -p bootstrap-build/idris2_app
-	cp support/c/${IDRIS2_SUPPORT} bootstrap-build/idris2_app/
+	cp ${IDRIS2_SUPPORT_DIR}/${IDRIS2_SUPPORT} bootstrap-build/idris2_app/
 	sed 's/libidris2_support.so/${IDRIS2_SUPPORT}/g; s|__PREFIX__|${IDRIS2_BOOT_PREFIX}|g' \
 		bootstrap/idris2_app/idris2.ss \
 		> bootstrap-build/idris2_app/idris2-boot.ss
@@ -257,7 +271,7 @@ bootstrap: support
 # Bootstrapping using racket
 bootstrap-racket: support
 	mkdir -p bootstrap-build/idris2_app
-	cp support/c/${IDRIS2_SUPPORT} bootstrap-build/idris2_app/
+	cp ${IDRIS2_SUPPORT_DIR}/${IDRIS2_SUPPORT} bootstrap-build/idris2_app/
 	sed 's|__PREFIX__|${IDRIS2_BOOT_PREFIX}|g' \
 		bootstrap/idris2_app/idris2.rkt \
 		> bootstrap-build/idris2_app/idris2-boot.rkt

bootstrap-stage1-chez.sh

@@ -20,5 +20,14 @@ ${SCHEME} --script ../bootstrap/compile.ss
 # Put the result in the usual place where the target goes
 mkdir -p ../build/exec
 mkdir -p ../build/exec/idris2_app
-install ../bootstrap/idris2-boot.sh ../build/exec/idris2
+
+# we "install" bootstrap/idris2-boot.sh as build/exec/idris2
+# but with the SCHEME var that we already know at this time
+# baked into it.
+echo '#!/bin/sh' >../build/exec/idris2
+echo "SCHEME=\"${SCHEME}\"" >>../build/exec/idris2
+cat ../bootstrap/idris2-boot.sh >>../build/exec/idris2
+chmod +x ../build/exec/idris2
+
 install idris2_app/* ../build/exec/idris2_app
+echo 'bootstrap stage 1 complete'

bootstrap-stage2.sh

@@ -8,16 +8,18 @@ IDRIS2_CG="${IDRIS2_CG-"chez"}"
 
 # BOOTSTRAP_PREFIX must be the "clean" build root, without cygpath -m
 # Otherwise, we get 'git: Bad address'
-echo "$BOOTSTRAP_PREFIX"
-DYLIB_PATH="$BOOTSTRAP_PREFIX/lib"
+echo "bootstrapping in: $BOOTSTRAP_PREFIX"
+export LD_LIBRARY_PATH="${LD_LIBRARY_PATH:-"${BOOTSTRAP_PREFIX}/lib"}"
+export DYLD_LIBRARY_PATH="${DYLD_LIBRARY_PATH:-"${BOOTSTRAP_PREFIX}/lib"}"
+export IDRIS2_DATA="${IDRIS2_DATA:-"${BOOTSTRAP_PREFIX}/support"}"
 
-$MAKE bootstrap-libs IDRIS2_CG="$IDRIS2_CG" LD_LIBRARY_PATH="$DYLIB_PATH" \
+$MAKE bootstrap-libs IDRIS2_CG="$IDRIS2_CG" \
     PREFIX="$BOOTSTRAP_PREFIX" SCHEME="$SCHEME"
-$MAKE bootstrap-install IDRIS2_CG="$IDRIS2_CG" LD_LIBRARY_PATH="$DYLIB_PATH" \
+$MAKE bootstrap-install IDRIS2_CG="$IDRIS2_CG" \
     PREFIX="$BOOTSTRAP_PREFIX" SCHEME="$SCHEME"
 
 # Now rebuild everything properly
 $MAKE clean-libs IDRIS2_BOOT="$BOOTSTRAP_PREFIX/bin/idris2"
 $MAKE all IDRIS2_BOOT="$BOOTSTRAP_PREFIX/bin/idris2" IDRIS2_CG="$IDRIS2_CG" \
-    LD_LIBRARY_PATH="$DYLIB_PATH" \
     SCHEME="$SCHEME"
+echo 'bootstrap stage 2 complete'

flake.nix

@@ -32,13 +32,16 @@
             pkgs.chez
           else
             pkgs.chez-racket; # TODO: Should this always be the default?
+          idris2Support = pkgs.callPackage ./nix/support.nix { inherit idris2-version; };
           idris2Bootstrap = pkgs.callPackage ./nix/package.nix {
             inherit idris2-version chez;
             idris2Bootstrap = null;
+            support = idris2Support;
             srcRev = self.shortRev or "dirty";
           };
           idris2Pkg = pkgs.callPackage ./nix/package.nix {
             inherit idris2-version chez idris2Bootstrap;
+            support = idris2Support;
             srcRev = self.shortRev or "dirty";
           };
           buildIdris = pkgs.callPackage ./nix/buildIdris.nix {
@@ -52,6 +55,7 @@
             idris = self;
           };
           packages = {
+            support = idris2Support;
             idris2 = idris2Pkg;
           } // (import ./nix/text-editor.nix {
             inherit pkgs idris-emacs-src idris2Pkg;

nix/package.nix

@@ -1,7 +1,12 @@
-{ stdenv, lib, chez, clang, gmp, fetchFromGitHub, makeWrapper, idris2-version
+{ stdenv, lib, chez, clang, gmp, fetchFromGitHub, makeWrapper, support, idris2-version
 , srcRev, gambit, nodejs, zsh, idris2Bootstrap ? null }:
 
 # Uses scheme to bootstrap the build of idris2
+let
+  bootstrap = idris2Bootstrap == null;
+  supportLibrariesPath = lib.makeLibraryPath [ support ];
+  supportSharePath = lib.makeSearchPath "share" [ support ];
+in
 stdenv.mkDerivation rec {
   pname = "idris2";
   version = idris2-version;
@@ -11,22 +16,40 @@ stdenv.mkDerivation rec {
   strictDeps = true;
   nativeBuildInputs = [ makeWrapper clang chez ]
     ++ lib.optional stdenv.isDarwin [ zsh ]
-    ++ lib.optional (!(idris2Bootstrap == null)) [ idris2Bootstrap ];
-  buildInputs = [ chez gmp ];
+    ++ lib.optional (! bootstrap) [ idris2Bootstrap ];
+  buildInputs = [ chez gmp support ];
 
   prePatch = ''
     patchShebangs --build tests
     sed 's/$(GIT_SHA1)/${srcRev}/' -i Makefile
   '';
 
-  makeFlags = [ "PREFIX=$(out)" ] ++ lib.optional stdenv.isDarwin "OS=";
+  makeFlags = [ "IDRIS2_SUPPORT_DIR=${supportLibrariesPath}" ]
+    ++ lib.optional stdenv.isDarwin "OS=";
 
   # The name of the main executable of pkgs.chez is `scheme`
-  buildFlags =
-    if idris2Bootstrap == null then [ "bootstrap" "SCHEME=scheme" ] else [ ];
+  buildFlags = [ "PREFIX=$(out)" ] ++
+    lib.optional bootstrap [
+      "bootstrap" "SCHEME=scheme"
+      "IDRIS2_DATA=${supportSharePath}"
+      "IDRIS2_LIBS=${supportLibrariesPath}"
+    ];
 
+  # checks happen against built compiler prior to the postInstall
+  # wrapper below so we must augment some paths to point at prebuilt
+  # support paths regardless of whether we are bootstrapping or not.
   checkInputs = [ gambit nodejs ]; # racket ];
-  checkFlags = [ "INTERACTIVE=" ];
+  checkFlags = [
+    "INTERACTIVE="
+    "IDRIS2_DATA=${supportSharePath}"
+    "IDRIS2_LIBS=${supportLibrariesPath}"
+    "TEST_IDRIS2_DATA=${supportSharePath}"
+    "TEST_IDRIS2_LIBS=${supportLibrariesPath}"
+    "TEST_IDRIS2_SUPPORT_DIR=${supportLibrariesPath}"
+  ];
+
+  installTargets = "install-idris2 install-libs";
+  installFlags = [ "PREFIX=$(out)" ];
 
   # TODO: Move this into its own derivation, such that this can be changed
   #       without having to recompile idris2 every time.
@@ -51,15 +74,13 @@ stdenv.mkDerivation rec {
     # idris2 installs packages with --install into the path given by
     #   IDRIS2_PREFIX. We set that to a default of ~/.idris2, to mirror the
     #   behaviour of the standard Makefile install.
-    # TODO: Make support libraries their own derivation such that
-    #       overriding LD_LIBRARY_PATH is unnecessary
     wrapProgram "$out/bin/idris2" \
       --set-default CHEZ "${chez}/bin/scheme" \
       --run 'export IDRIS2_PREFIX=''${IDRIS2_PREFIX-"$HOME/.idris2"}' \
-      --suffix IDRIS2_LIBS ':' "$out/${name}/lib" \
-      --suffix IDRIS2_DATA ':' "$out/${name}/support" \
+      --suffix IDRIS2_LIBS ':' "${supportLibrariesPath}" \
+      --suffix IDRIS2_DATA ':' "${supportSharePath}" \
       --suffix IDRIS2_PACKAGE_PATH ':' "${globalLibrariesPath}" \
-      --suffix DYLD_LIBRARY_PATH ':' "$out/${name}/lib" \
-      --suffix LD_LIBRARY_PATH ':' "$out/${name}/lib"
+      --suffix LD_LIBRARY_PATH ':' "${supportLibrariesPath}" \
+      --suffix DYLD_LIBRARY_PATH ':' "${supportLibrariesPath}" \
   '';
 }

nix/support.nix

@@ -0,0 +1,24 @@
+{ stdenv, lib, gmp, idris2-version }:
+stdenv.mkDerivation rec {
+  pname = "libidris2_support";
+  version = idris2-version;
+
+  src = ../.;
+
+  strictDeps = true;
+  buildInputs = [ gmp ];
+
+  makeFlags = [
+    "PREFIX=$(out)"
+  ] ++ lib.optional stdenv.isDarwin "OS=";
+
+  buildFlags = [ "support" ];
+
+  installTargets = "install-support";
+
+  postInstall = ''
+    mv $out/idris2-${version}/lib $out/lib
+    mv $out/idris2-${version}/support $out/share
+    rmdir $out/idris2-${version}
+  '';
+}

tests/Makefile

@@ -10,7 +10,7 @@ retest:
 	./build/exec/runtests $(IDRIS2) $(INTERACTIVE) --timing --failure-file failures --threads $(threads) --only-file failures --only $(only) --except $(except)
 
 testbin:
-	${IDRIS2} --build tests.ipkg
+	$(IDRIS2) --build tests.ipkg
 
 clean:
 	$(RM) failures

tests/testutils.sh

@@ -87,8 +87,10 @@ if [ -z "$PREFIX_CHANGED" ] && [ -n "$IDRIS2_PREFIX" ]; then
 
     # Set where to look to installed stuff
     export IDRIS2_PACKAGE_PATH="$OLD_PP$SEP$NEW_PP"
-    export IDRIS2_LIBS="$OLD_PP/libs$SEP$NEW_PP/libs"
-    export IDRIS2_DATA="$OLD_PP/support$SEP$NEW_PP/support"
+    # Use TEST_IDRIS2_LIBS and TEST_IDRIS2_DATA to pass locations for
+    # prebuilt libidris2_support and its DATA files.
+    export IDRIS2_LIBS="$OLD_PP/libs$SEP$NEW_PP/libs$SEP$TEST_IDRIS2_LIBS"
+    export IDRIS2_DATA="$OLD_PP/support$SEP$NEW_PP/support$SEP$TEST_IDRIS2_DATA"
 
     # Set where to install stuff
     export IDRIS2_PREFIX="$NEW_PREFIX"