diff --git a/CONTRIBUTORS b/CONTRIBUTORS index 364b4c035..472079878 100644 --- a/CONTRIBUTORS +++ b/CONTRIBUTORS @@ -5,6 +5,7 @@ Alex Gryzlov Alex Silva Andre Kuhlenschmidt André Videla +Andy Lok Arnaud Bailly Brian Wignall Christian Rasmussen diff --git a/INSTALL.md b/INSTALL.md index 9cc187c1a..45c2d1585 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -84,3 +84,14 @@ that everything has worked correctly. Assuming that `idris2` is in your After `make all`, type `make test` to check everything works. This uses the executable in `./build/exec`. + +5: (Optional) Installing the Idris 2 API +---------------------------------------- + +You'll only need this if you're developing support tools, such as an external +code generator. To do so, once everything is successfully installed, type: + +* `make install-api` + +The API will only work if you've completed the self-hosting step, step 3, since +the intermediate code versions need to be consistent throughout. diff --git a/Makefile b/Makefile index e1fd790f0..412be61fe 100644 --- a/Makefile +++ b/Makefile @@ -86,6 +86,9 @@ clean: clean-libs support-clean install: install-idris2 install-support install-libs +install-api: + ${IDRIS2_BOOT} --install idris2api.ipkg + install-idris2: mkdir -p ${PREFIX}/bin/ install ${TARGET} ${PREFIX}/bin diff --git a/idris2api.ipkg b/idris2api.ipkg new file mode 100644 index 000000000..88374b82b --- /dev/null +++ b/idris2api.ipkg @@ -0,0 +1,148 @@ +package idris2 + +modules = + Algebra, + Algebra.Preorder, + Algebra.Semiring, + Algebra.ZeroOneOmega, + + Compiler.ANF, + Compiler.Common, + Compiler.CompileExpr, + Compiler.Inline, + Compiler.LambdaLift, + Compiler.Scheme.Chez, + Compiler.Scheme.Racket, + Compiler.Scheme.Gambit, + Compiler.Scheme.Common, + Compiler.VMCode, + + 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.InitPrimitives, + Core.LinearCheck, + Core.Metadata, + Core.Name, + Core.Normalise, + Core.Options, + Core.Primitives, +-- Core.Reflect, + Core.Termination, + Core.Transform, + Core.TT, + Core.TTC, + Core.Unify, + Core.UnifyState, + Core.Value, + + Data.ANameMap, + Data.Bool.Extra, + Data.IntMap, + Data.LengthMatch, + Data.NameMap, + Data.StringMap, + Data.These, + Data.StringTrie, + + IdrisPaths, + + 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.Syntax, + Idris.Version, + + Parser.Lexer, + Parser.Support, + Parser.Unlit, + + Text.Lexer, + Text.Lexer.Core, + Text.Literate, + 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.Delayed, + 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.PartialEval, + TTImp.ProcessData, + TTImp.ProcessDecls, + TTImp.ProcessDef, + TTImp.ProcessParams, + TTImp.ProcessRecord, + TTImp.ProcessTransform, + TTImp.ProcessType, +-- TTImp.Reflect, + TTImp.TTImp, + TTImp.Unelab, + TTImp.Utils, + TTImp.WithClause, + + Utils.Binary, + Utils.Hex, + Utils.Octal, + Utils.Shunting, + Utils.String, + + Yaffle.Main, + Yaffle.REPL + +depends = contrib, network + +sourcedir = "src"