mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-28 02:23:44 +03:00
Add idris2api.ipkg
This is a small variation that installs all the modules as a library, which could be used by external tools, eg fancy REPLs, code generators, etcs.
This commit is contained in:
parent
d6cdef99e1
commit
0cd484fa09
@ -5,6 +5,7 @@ Alex Gryzlov
|
|||||||
Alex Silva
|
Alex Silva
|
||||||
Andre Kuhlenschmidt
|
Andre Kuhlenschmidt
|
||||||
André Videla
|
André Videla
|
||||||
|
Andy Lok
|
||||||
Arnaud Bailly
|
Arnaud Bailly
|
||||||
Brian Wignall
|
Brian Wignall
|
||||||
Christian Rasmussen
|
Christian Rasmussen
|
||||||
|
11
INSTALL.md
11
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
|
After `make all`, type `make test` to check everything works. This uses the
|
||||||
executable in `./build/exec`.
|
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.
|
||||||
|
3
Makefile
3
Makefile
@ -86,6 +86,9 @@ clean: clean-libs support-clean
|
|||||||
|
|
||||||
install: install-idris2 install-support install-libs
|
install: install-idris2 install-support install-libs
|
||||||
|
|
||||||
|
install-api:
|
||||||
|
${IDRIS2_BOOT} --install idris2api.ipkg
|
||||||
|
|
||||||
install-idris2:
|
install-idris2:
|
||||||
mkdir -p ${PREFIX}/bin/
|
mkdir -p ${PREFIX}/bin/
|
||||||
install ${TARGET} ${PREFIX}/bin
|
install ${TARGET} ${PREFIX}/bin
|
||||||
|
148
idris2api.ipkg
Normal file
148
idris2api.ipkg
Normal file
@ -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"
|
Loading…
Reference in New Issue
Block a user