Reorganise build system to go via generating C

This has two main advantages: firstly, it actually makes the build slightly faster and less memory intensive, because Idris doesn't fork a new process and eat all the memory! Secondly, it means we can build a distribution with the C file, for building on machines which don't have Idris 1 available. Also includes a script for building such a distribution. I expect someone who is better a writing Makefiles than me can tidy this up. There are almost certainly problems on Windows too - please help if you can! There are new Make targets 'all-fromc' and 'install-fromc' which don't require building from Idris source, so that we can build with no Idris 1 available. A small consequence: make install-exec no longer builds the idris2 executable, just installs it.
2024-12-26 06:11:50 +03:00 · 2020-03-05 17:12:58 +00:00 · 2020-03-05 17:12:58 +00:00 · 2c2acdcfac
commit 2c2acdcfac
parent 1dd81ff10b
9 changed files with 120 additions and 155 deletions
--- a/INSTALL.md
+++ b/INSTALL.md
@ -1,8 +1,31 @@
 # Installation

-Idris 2 is built using Idris, and provides support for three default code
-generation targets: Chez, Chicken, and Racket.  It requires at least Idris
-version 1.3.2 (see https://www.idris-lang.org/download)
+Idris 2 is built using Idris, and provides support for two default code
+generation targets: Chez Scheme, and Racket. To build from source, it requires
+at least Idris version 1.3.2 (see https://www.idris-lang.org/download). You
+can also build from the generated C.
+
+## Quick summary:
+
+You need a C compiler (default is clang) and Chez Scheme, and optionally
+Idris 1.3.2 to build from source.
+
+* If you have Idris 1.3.2 installed:
+
+    make install
+
+* If not, and the generated C is available in `dist`, you can install directly
+  from the generated C:
+
+    make install-fromc
+
+The generated C is available in source distributions. It will not be available
+if you have cloned directly from https://github.com/edwinb/Idris2
+
+The above commands will build the executable, build the libraries, run the
+tests (if Idris 1 is available), then if all is well, install everything. The
+default installation directory is `$HOME/.idris2`. You can change this by
+setting the `PREFIX` variable in the `Makefile`.

 ## Idris

--- a/47
+++ b/47
@ -1,3 +1,13 @@
+##### Options which a user might set before building go here #####
+
+PREFIX ?= ${HOME}/.idris2
+
+# Add any optimisation/profiling flags for C here (e.g. -O2)
+export OPT=
+export CC=clang # clang compiles the output much faster than gcc!
+
+##################################################################
+
 # current Idris2 version components
 MAJOR=0
 MINOR=0
@ -17,7 +27,6 @@ endif
 IDRIS2_VERSION := ${MAJOR}.${MINOR}.${PATCH}
 IDRIS2_VERSION_TAG := ${IDRIS2_VERSION}${VER_TAG}

-PREFIX ?= ${HOME}/.idris2
 export IDRIS2_PATH = ${CURDIR}/libs/prelude/build/ttc:${CURDIR}/libs/base/build/ttc
 export IDRIS2_DATA = ${CURDIR}/support

@ -26,30 +35,42 @@ VALID_IDRIS_VERSION_REGEXP = "1.3.2.*"

 -include custom.mk

-.PHONY: ttimp idris2 prelude test base clean lib_clean check_version idris2c dist/idris2.c
+.PHONY: ttimp idris2 idris2-fromc prelude test base clean lib_clean check_version idris2c dist/idris2.c

 all: idris2 libs test

+# test requires an Idris install! Maybe we should do a version in Idris2?
+all-fromc: idris2-fromc libs
+
 check_version:
 	@echo "Using Idris 1 version: $(IDRIS_VERSION)"
 	@if [ $(shell expr $(IDRIS_VERSION) : $(VALID_IDRIS_VERSION_REGEXP)) -eq 0 ]; then echo "Wrong idris version, expected version matching $(VALID_IDRIS_VERSION_REGEXP)"; exit 1; fi

-idris2: src/YafflePaths.idr check_version
-	@echo "Building Idris 2 version: $(IDRIS2_VERSION_TAG)"
-	idris --build idris2.ipkg
+idris2: dist/idris2.c idris2-fromc

+# Just build the C, assuming already built from Idris source.
+# Separate rule to avoid having to build the C if Idris 1 isn't available.
+# (Also replaces the first line of the generated C with the proper prefix)
+#
+idris2-fromc:
+	sed -i '1 s|^.*$$|char* idris2_prefix = "${PREFIX}";|' dist/idris2.c
+	make -C dist
+	@cp dist/idris2 ./idris2
+
+# bit of a hack here, to get the prefix into the generated C!
 dist/idris2.c: src/YafflePaths.idr check_version
 	@echo "Building Idris 2 version: $(IDRIS2_VERSION_TAG)"
-	idris --build idris2-mkc.ipkg
-	@cat idris2.c dist/rts/idris_main.c > dist/idris2.c
-	@rm -f idris2.c
+	idris --build idris2.ipkg
+	@echo 'char* idris2_prefix = "${PREFIX}";' > idris2_prefix.c
+	@echo 'char* getIdris2_prefix() { return idris2_prefix; }' >> idris2_prefix.c
+	@cat idris2_prefix.c idris2.c dist/rts/idris_main.c > dist/idris2.c
+	@rm -f idris2.c idris2_prefix.c

 idris2c: dist/idris2.c
 	make -C dist

 src/YafflePaths.idr:
 	echo 'module YafflePaths; export yversion : ((Nat,Nat,Nat), String); yversion = ((${MAJOR},${MINOR},${PATCH}), "${GIT_SHA1}")' > src/YafflePaths.idr
-	echo 'export yprefix : String; yprefix = "${PREFIX}"' >> src/YafflePaths.idr

 prelude:
 	make -C libs/prelude IDRIS2=../../idris2
@ -83,7 +104,11 @@ test:
 	idris --build tests.ipkg
 	@make -C tests only=$(only)

-install: all install-exec install-support install-libs
+install-all: install-exec install-support install-libs
+
+install: all install-all
+
+install-fromc: all-fromc install-all

 install-support:
 	mkdir -p ${PREFIX}/idris2-${IDRIS2_VERSION}/support/chez
@ -93,7 +118,7 @@ install-support:
 	install support/chicken/* ${PREFIX}/idris2-${IDRIS2_VERSION}/support/chicken
 	install support/racket/* ${PREFIX}/idris2-${IDRIS2_VERSION}/support/racket

-install-exec: idris2
+install-exec:
 	mkdir -p ${PREFIX}/bin
 	mkdir -p ${PREFIX}/idris2-${IDRIS2_VERSION}/lib
 	install idris2 ${PREFIX}/bin
--- a/dist/Makefile
+++ b/dist/Makefile
@ -4,7 +4,7 @@ all: idris2

 idris2: idris2.c
 	make -C rts
-	$(CC) idris2.c -o idris2 -I rts -L rts -lidris_rts -lpthread -lgmp -lm
+	$(CC) $(OPT) idris2.c -o idris2 -I rts -L rts -lidris_rts -lpthread -lgmp -lm

 clean:
 	make -C rts clean
--- a/idris2-mkc.ipkg
+++ b/idris2-mkc.ipkg
@ -1,132 +0,0 @@
-package idris2
-
-modules =
-    Compiler.Common,
-    Compiler.CompileExpr,
-    Compiler.Inline,
-    Compiler.Scheme.Chez,
-    Compiler.Scheme.Chicken,
-    Compiler.Scheme.Racket,
-    Compiler.Scheme.Common,
-
-    Control.Delayed,
-
-    Core.AutoSearch,
-    Core.Binary,
-    Core.CaseBuilder,
-    Core.CaseTree,
-    Core.Context,
-    Core.CompileExpr,
-    Core.Core,
-    Core.Coverage,
-    Core.Directory,
-    Core.Env,
-    Core.FC,
-    Core.GetType,
-    Core.Hash,
-    Core.LinearCheck,
-    Core.Metadata,
-    Core.Name,
-    Core.Normalise,
-    Core.Options,
-    Core.Reflect,
-    Core.Termination,
-    Core.TT,
-    Core.TTC,
-    Core.Unify,
-    Core.UnifyState,
-    Core.Value,
-
-    Data.ANameMap,
-    Data.Bool.Extra,
-    Data.IntMap,
-    Data.IOArray,
-    Data.NameMap,
-    Data.StringMap,
-    Data.These,
-    Data.StringTrie,
-
-    Idris.CommandLine,
-    Idris.Desugar,
-    Idris.Elab.Implementation,
-    Idris.Elab.Interface,
-    Idris.Error,
-    Idris.IDEMode.CaseSplit,
-    Idris.IDEMode.Commands,
-    Idris.IDEMode.MakeClause,
-    Idris.IDEMode.Parser,
-    Idris.IDEMode.REPL,
-    Idris.IDEMode.TokenLine,
-    Idris.ModTree,
-    Idris.Package,
-    Idris.Parser,
-    Idris.ProcessIdr,
-    Idris.REPL,
-    Idris.REPLCommon,
-    Idris.REPLOpts,
-    Idris.Resugar,
-    Idris.SetOptions,
-    Idris.Socket,
-    Idris.Socket.Data,
-    Idris.Socket.Raw,
-    Idris.Syntax,
-
-    Parser.Lexer,
-    Parser.Support,
-
-    Text.Lexer,
-    Text.Lexer.Core,
-    Text.Parser,
-    Text.Parser.Core,
-    Text.Quantity,
-    Text.Token,
-
-    TTImp.BindImplicits,
-    TTImp.Elab,
-    TTImp.Elab.Ambiguity,
-    TTImp.Elab.App,
-    TTImp.Elab.As,
-    TTImp.Elab.Binders,
-    TTImp.Elab.Case,
-    TTImp.Elab.Check,
-    TTImp.Elab.Dot,
-    TTImp.Elab.Hole,
-    TTImp.Elab.ImplicitBind,
-    TTImp.Elab.Lazy,
-    TTImp.Elab.Local,
-    TTImp.Elab.Prim,
-    TTImp.Elab.Quote,
-    TTImp.Elab.Record,
-    TTImp.Elab.Rewrite,
-    TTImp.Elab.Term,
-    TTImp.Elab.Utils,
-    TTImp.Impossible,
-    TTImp.Interactive.CaseSplit,
-    TTImp.Interactive.ExprSearch,
-    TTImp.Interactive.GenerateDef,
-    TTImp.Interactive.MakeLemma,
-    TTImp.Parser,
-    TTImp.ProcessData,
-    TTImp.ProcessDecls,
-    TTImp.ProcessDef,
-    TTImp.ProcessParams,
-    TTImp.ProcessRecord,
-    TTImp.ProcessType,
-    TTImp.Reflect,
-    TTImp.TTImp,
-    TTImp.Unelab,
-    TTImp.Utils,
-    TTImp.WithClause,
-
-    Utils.Binary,
-    Utils.Hex,
-    Utils.Shunting,
-
-    Yaffle.Main,
-    Yaffle.REPL
-
-sourcedir = src
-executable = idris2.c
-opts = "--partial-eval -S"
-
-main = Idris.Main
--- a/idris2.ipkg
+++ b/idris2.ipkg
@ -126,11 +126,8 @@ modules =
    Yaffle.REPL

 sourcedir = src
-executable = idris2
-- opts = "--cg-opt -O2 --partial-eval"
-- opts = "--cg-opt -pg --partial-eval"
-opts = "--partial-eval"
-- opts = "--partial-eval --cg-opt -lws2_32" -- windows
+executable = idris2.c
+opts = "--partial-eval -S"

 main = Idris.Main

--- a/mkdist.sh
+++ b/mkdist.sh
@ -0,0 +1,30 @@
+#!/bin/sh
+
+if [ $# -eq 0 ]
+  then
+    echo "Usage: ./mkdist.sh [version]"
+    exit 1
+fi
+
+mkdir -p idris2-$1
+# Copy the source, but without build artefacts
+rsync -avm --include='*.idr' -f 'hide,! */' src idris2-$1
+rsync -avm --include-from='srcfiles' -f 'hide,! */' libs idris2-$1
+rsync -avm --include-from='srcfiles' -f 'hide,! */' samples idris2-$1
+rsync -avm --include-from='srcfiles' -f 'hide,! */' docs idris2-$1
+rsync -avm --include-from='srcfiles' -f 'hide,! */' tests idris2-$1
+# Copy run time support for Idris 1
+rsync -avm --include-from='srcfiles' -f 'hide,! */' dist idris2-$1
+# Copy run time support for Idris 2
+cp -r support idris2-$1/support
+# Copy top level files and docs
+cp *.md Makefile LICENSE idris2.ipkg idris2-$1
+
+tar zcvf idris2-$1.tgz idris2-$1
+
+echo "Did you remember to:"
+echo "\tmake dist/idris2.c?"
+echo "\ttag the release?"
+echo "\tset the -O2 flag?"
+
+
--- a/src/Core/Directory.idr
+++ b/src/Core/Directory.idr
@ -38,7 +38,8 @@ readDataFile fname
    = do d <- getDirs
         let fs = map (\p => p ++ dirSep ++ fname) (data_dirs d)
         Just f <- firstAvailable fs
-            | Nothing => throw (InternalError ("Can't find data file " ++ fname))
+            | Nothing => throw (InternalError ("Can't find data file " ++ fname ++
+                                               " in any of " ++ show fs))
         Right d <- coreLift $ readFile f
            | Left err => throw (FileErr f err)
         pure d
--- a/src/Idris/Main.idr
+++ b/src/Idris/Main.idr
@ -32,6 +32,9 @@ import YafflePaths
 %default covering
 %flag C "-g"

+yprefix : String
+yprefix = unsafePerformIO (foreign FFI_C "getIdris2_prefix" (IO String))
+
 findInput : List CLOpt -> Maybe String
 findInput [] = Nothing
 findInput (InputFile f :: fs) = Just f
@ -42,8 +45,10 @@ findInput (_ :: fs) = findInput fs
 updatePaths : {auto c : Ref Ctxt Defs} ->
              Core ()
 updatePaths
-    = do setPrefix yprefix
-         defs <- get Ctxt
+    = do bprefix <- coreLift $ getEnv "IDRIS2_PREFIX"
+         case bprefix of
+              Just p => setPrefix p
+              Nothing => setPrefix yprefix
         bpath <- coreLift $ getEnv "IDRIS2_PATH"
         case bpath of
              Just path => do traverse addExtraDir (map trim (split (==pathSep) path))
@ -63,6 +68,7 @@ updatePaths
         -- any conflicts. In particular, that means that setting IDRIS2_PATH
         -- for the tests means they test the local version not the installed
         -- version
+         defs <- get Ctxt
         addPkgDir "prelude"
         addPkgDir "base"
         addDataDir (dir_prefix (dirs (options defs)) ++ dirSep ++
--- a/15
+++ b/15
@ -0,0 +1,15 @@
+*.idr
+*.yaff
+*.ipkg
+Makefile
+config.mk
+lib-tests
+expected
+input
+run
+*.c
+*.h
+*.rst
+*.py
+*.md
+*.bat