Merge pull request #1621 from edwinb/incremental-chez

Support for incremental compilation with Chez
This commit is contained in:
Edwin Brady 2021-06-27 19:29:56 +01:00 committed by GitHub
commit d88929ddd7
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
38 changed files with 739 additions and 141 deletions

37
.github/linters/.markdown-lint.yml vendored Normal file
View File

@ -0,0 +1,37 @@
---
###########################
###########################
## Markdown Linter rules ##
###########################
###########################
# Linter rules doc:
# - https://github.com/DavidAnson/markdownlint
#
# Note:
# To comment out a single error:
# <!-- markdownlint-disable -->
# any violations you want
# <!-- markdownlint-restore -->
#
###############
# Rules by id #
###############
MD004: false # Unordered list style
MD007:
indent: 2 # Unordered list indentation
MD013:
line_length: 400 # Line length 80 is far to short
MD024:
siblings_only: true # allow duplicate headings in CHANGELOG
MD026:
punctuation: ".,;:!。,;:" # List of not allowed
MD029: false # Ordered list item prefix
MD033: false # Allow inline HTML
MD036: false # Emphasis used instead of a heading
#################
# Rules by tags #
#################
blank_lines: false # Error on blank lines

View File

@ -1,5 +1,17 @@
# Changelog
## [Next version]
### Compiler changes
* Added incremental compilation, using either the `--inc` flag or the
`IDRIS2_INC_CGS` environment variable, which compiles modules incrementally.
In incremental mode, the final build step is much faster than in whole
program mode (the default), at the cost of runtime performance being about
half as good. The `--whole-program` flag overrides incremental compilation,
and reverts to whole program compilation. Incremental compilation is currently
supported only by the Chez Scheme back end.
## v0.4.0
### Syntax changes

View File

@ -88,7 +88,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`.
### 6: (Optional) Installing the Idris 2 API
### 6: (Optional) Enabling incremental compilation
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
`IDRIS2_INC_CGS=chez`, or set the `--inc chez` flag in `idris2.ipkg`.
### 7: (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:
@ -99,7 +106,7 @@ The API will only work if you've completed the self-hosting step, step 4, since
the intermediate code versions need to be consistent throughout. Otherwise, you
will get an `Error in TTC: TTC data is in an older format` error.
### 7: (Optional) Shell Auto-completion
### 8: (Optional) Shell Auto-completion
Idris2 supports tab auto-completion for Bash-like shells.

View File

@ -8,6 +8,10 @@ NAME = idris2
TARGETDIR = ${CURDIR}/build/exec
TARGET = ${TARGETDIR}/${NAME}
# Default code generator. This is passed to the libraries for incremental
# builds, but overridable via environment variables or arguments to make
IDRIS2_CG ?= chez
MAJOR=0
MINOR=4
PATCH=0
@ -68,19 +72,19 @@ src/IdrisPaths.idr: FORCE
FORCE:
prelude:
${MAKE} -C libs/prelude IDRIS2=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
${MAKE} -C libs/prelude IDRIS2=${TARGET} IDRIS2_INC_CGS=${IDRIS2_CG} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
base: prelude
${MAKE} -C libs/base IDRIS2=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
${MAKE} -C libs/base IDRIS2=${TARGET} IDRIS2_INC_CGS=${IDRIS2_CG} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
network: prelude
${MAKE} -C libs/network IDRIS2=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
${MAKE} -C libs/network IDRIS2=${TARGET} IDRIS2_INC_CGS=${IDRIS2_CG} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
contrib: base
${MAKE} -C libs/contrib IDRIS2=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
${MAKE} -C libs/contrib IDRIS2=${TARGET} IDRIS2_INC_CGS=${IDRIS2_CG} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
test-lib: contrib
${MAKE} -C libs/test IDRIS2=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
${MAKE} -C libs/test IDRIS2=${TARGET} IDRIS2_INC_CGS=${IDRIS2_CG} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
libs : prelude base contrib network test-lib

View File

@ -68,6 +68,6 @@ Chez Directives
%foreign "scheme:my-mul"
myMul : Int -> Int -> Int
.. code-block::
::
$ idris2 --codegen chez --directive extraRuntime=/path/to/extensions.scm -o main Main.idr

View File

@ -0,0 +1,73 @@
***************************
Incremental Code Generation
***************************
By default, Idris 2 is a whole program compiler - that is, it finds all the
necessary function definitions and compiles them only when you build an
executable. This gives plenty of optimisation opportunities, but can also
be slow for rebuilding. However, if the backend supports it, you can build
modules and executables *incrementally*. To do so, you can either:
1. Set the ``--inc <backend>`` flag at the command line, for each backend
you want to use incrementally.
2. Set the ``IDRIS2_INC_CGS`` environment variable with a comma separated list
of backends to use incrementally.
At the moment, only the Chez backend supports incremental builds.
Building modules incrementally
==============================
If either of the above are set, building a module will produce compiled binary
code for all of the definitions in the module, as well as the usual checked
TTC file. e.g.:
::
$ idris2 --inc chez Foo.idr
$ IDRIS2_INC_CGS=chez idris2 Foo.idr
On successful type checking, each of these will produce a Chez Scheme file
(``Foo.ss``) and compiled code for it (``Foo.so``) as well as the usual
``Foo.ttc``, in the same build directory as ``Foo.ttc``.
In incremental mode, you will see a warning for any holes in the module,
even if those holes will be defined in a different module.
Building executables incrementally
==================================
If either ``--inc`` is used or ``IDRIS2_INC_CGS`` is set, compiling to
an executable will attempt to link all of the compiled modules together,
rather than generating code for all of the functions at once. For this
to work, all the imported modules *must* have been built with incremental
compilation for the current back end (Idris will revert to whole program
compilation if any are missing, and you will see a warning.)
Therefore, all packages used by the executable must also have been built
incrementally for the current back end. The ``prelude``, ``base``,
``contrib``, ``network`` and ``test`` packages are all built with
incremental compilation support for Chez by default.
When switching between incremental and whole program compilation, it is
recommended that you remove the ``build`` directory first. This is
particularly important when switching to incremental compilation, since there
may be stale object files that Idris does not currently detect!
Overriding incremental compilation
==================================
The ``--whole-program`` flag overrides any incremental compilation settings
when building an executable.
Performance note
================
Incremental compilation means that executables are generated much quicker,
especially when only a small proportion of modules have changed. However,
it means that there are fewer optimisation opportunities, so the resulting
executable will not perform as well. For deployment, ``--whole-program``
compilation is recommended.

View File

@ -48,6 +48,17 @@ This will compile the expression ``Main.main``, generating an executable
``hello`` (with an extension depending on the code generator) in the
``build/exec`` directory.
By default, Idris 2 is a whole program compiler - that is, it finds all the
necessary function definitions and compiles them only when you build an
executable. This gives plenty of optimisation opportunities, but can also
be slow for rebuilding. However, if the backend supports it, you can build
modules and executables *incrementally*:
.. toctree::
:maxdepth: 1
incremental
If the backend supports it, you can generate profiling data by setting
the ``profile`` flag, either by starting Idris with ``--profile``, or
running ``:set profile`` at the REPL. The profile data generated will depend

View File

@ -8,5 +8,12 @@ sourcedir = "src"
-- (Currently supported by Racket and Chez back ends, others ignore it)
-- opts = "--profile"
-- Set if you want incremental builds. This is good for development, since
-- small changes compile faster, but bad for deployment since the resulting
-- executable runs at around half the speed.
-- (Alternatively: set the environment variable IDRIS2_INC_CGS=chez)
-- For this to work, you need to do the initial incremental build from clean.
-- opts = "--inc chez"
main = Idris.Main
executable = idris2

View File

@ -39,6 +39,17 @@ record Codegen where
ClosedTerm -> (outfile : String) -> Core (Maybe String)
||| Execute an Idris 2 expression directly.
executeExpr : Ref Ctxt Defs -> (tmpDir : String) -> ClosedTerm -> Core ()
||| Incrementally compile definitions in the current module (toIR defs)
||| if supported
||| Takes a source file name, returns the name of the generated object
||| file, if successful, plus any other backend specific data in a list
||| of strings. The generated object file should be placed in the same
||| directory as the associated TTC.
incCompileFile : Maybe (Ref Ctxt Defs ->
(sourcefile : String) ->
Core (Maybe (String, List String)))
||| If incremental compilation is supported, get the output file extension
incExt : Maybe String
-- Say which phase of compilation is the last one to use - it saves time if
-- you only ask for what you need.
@ -107,6 +118,14 @@ execute {c} cg tm
executeExpr cg c tmpDir tm
pure ()
export
incCompile : {auto c : Ref Ctxt Defs} ->
Codegen -> String -> Core (Maybe (String, List String))
incCompile {c} cg src
= do let Just inc = incCompileFile cg
| Nothing => pure Nothing
inc c src
-- If an entry isn't already decoded, get the minimal entry we need for
-- compilation, and record the Binary so that we can put it back when we're
-- done (so that we don't obliterate the definition)
@ -250,6 +269,15 @@ dumpVMCode fn lns
dumpDef : (Name, VMDef) -> String
dumpDef (n, d) = fullShow n ++ " = " ++ show d ++ "\n"
export
nonErased : {auto c : Ref Ctxt Defs} ->
Name -> Core Bool
nonErased n
= do defs <- get Ctxt
Just gdef <- lookupCtxtExact n (gamma defs)
| Nothing => pure True
pure (multiplicity gdef /= erased)
-- Find all the names which need compiling, from a given expression, and compile
-- them to CExp form (and update that in the Defs).
-- Return the names, the type tags, and a compiled version of the expression
@ -324,13 +352,40 @@ getCompileData doLazyAnnots phase tm_in
pure (MkCompileData compiledtm
(mapMaybe id namedefs)
lifted anf vmcode)
where
nonErased : Name -> Core Bool
nonErased n
= do defs <- get Ctxt
Just gdef <- lookupCtxtExact n (gamma defs)
| Nothing => pure True
pure (multiplicity gdef /= erased)
export
compileTerm : {auto c : Ref Ctxt Defs} ->
ClosedTerm -> Core (CExp [])
compileTerm tm_in
= do tm <- toFullNames tm_in
fixArityExp !(compileExp tm)
export
getIncCompileData : {auto c : Ref Ctxt Defs} -> (doLazyAnnots : Bool) ->
UsePhase -> Core CompileData
getIncCompileData doLazyAnnots phase
= do defs <- get Ctxt
-- Compile all the names in 'toIR', since those are the ones defined
-- in the current source file
let ns = keys (toIR defs)
cns <- traverse toFullNames ns
rcns <- filterM nonErased cns
traverse_ mkForgetDef rcns
namedefs <- traverse getNamedDef rcns
lifted_in <- if phase >= Lifted
then logTime "++ Lambda lift" $ traverse (lambdaLift doLazyAnnots) rcns
else pure []
let lifted = concat lifted_in
anf <- if phase >= ANF
then logTime "++ Get ANF" $ traverse (\ (n, d) => pure (n, !(toANF d))) lifted
else pure []
vmcode <- if phase >= VMCode
then logTime "++ Get VM Code" $ pure (allDefs anf)
else pure []
pure (MkCompileData (CErased emptyFC)
(mapMaybe id namedefs)
lifted anf vmcode)
-- Some things missing from Prelude.File

View File

@ -6,6 +6,7 @@ import Core.Context
import Core.Env
import Core.Name
import Core.Normalise
import Core.Options
import Core.TT
import Core.Value
@ -683,17 +684,53 @@ getCFTypes args (NBind fc _ (Pi _ _ _ ty) sc)
getCFTypes args t
= pure (reverse args, !(nfToCFType (getLoc t) False t))
lamRHSenv : Int -> FC -> (ns : List Name) -> SubstCEnv ns []
lamRHSenv i fc [] = []
lamRHSenv i fc (n :: ns)
= CRef fc (MN "x" i) :: lamRHSenv (i + 1) fc ns
mkBounds : (xs : _) -> Bounds xs
mkBounds [] = None
mkBounds (x :: xs) = Add x x (mkBounds xs)
getNewArgs : {done : _} ->
SubstCEnv done args -> List Name
getNewArgs [] = []
getNewArgs (CRef _ n :: xs) = n :: getNewArgs xs
getNewArgs {done = x :: xs} (_ :: sub) = x :: getNewArgs sub
-- If a name is declared in one module and defined in another,
-- we have to assume arity 0 for incremental compilation because
-- we have no idea how it's defined, and when we made calls to the
-- function, they had arity 0.
lamRHS : (ns : List Name) -> CExp ns -> CExp []
lamRHS ns tm
= let env = lamRHSenv 0 (getFC tm) ns
tmExp = substs env (rewrite appendNilRightNeutral ns in tm)
newArgs = reverse $ getNewArgs env
bounds = mkBounds newArgs
expLocs = mkLocals zero {vars = []} bounds tmExp in
lamBind (getFC tm) _ expLocs
where
lamBind : FC -> (ns : List Name) -> CExp ns -> CExp []
lamBind fc [] tm = tm
lamBind fc (n :: ns) tm = lamBind fc ns (CLam fc n tm)
toCDef : {auto c : Ref Ctxt Defs} ->
Name -> ClosedTerm -> List Nat -> Def ->
Core CDef
toCDef n ty _ None
= pure $ MkError $ CCrash emptyFC ("Encountered undefined name " ++ show !(getFullName n))
toCDef n ty erased (PMDef _ args _ tree _)
toCDef n ty erased (PMDef pi args _ tree _)
= do let (args' ** p) = mkSub 0 args erased
comptree <- toCExpTree n tree
if isNil erased
then pure $ MkFun args comptree
else pure $ MkFun args' (shrinkCExp p comptree)
pure $ toLam (externalDecl pi) $ if isNil erased
then MkFun args comptree
else MkFun args' (shrinkCExp p comptree)
where
toLam : Bool -> CDef -> CDef
toLam True (MkFun args rhs) = MkFun [] (lamRHS args rhs)
toLam _ d = d
toCDef n ty _ (ExternDef arity)
= let (ns ** args) = mkArgList 0 arity in
pure $ MkFun _ (CExtPrim emptyFC !(getFullName n) (map toArgExp (getVars args)))
@ -759,9 +796,22 @@ compileDef n
= do defs <- get Ctxt
Just gdef <- lookupCtxtExact n (gamma defs)
| Nothing => throw (InternalError ("Trying to compile unknown name " ++ show n))
ce <- toCDef n (type gdef) (eraseArgs gdef)
!(toFullNames (definition gdef))
setCompiled n ce
-- If we're incremental, and the name has no definition yet, it
-- might end up defined in another module, so leave it, but warn
if noDefYet (definition gdef) (incrementalCGs !getSession)
-- This won't be accurate if we have names declared in one module
-- and defined elsewhere. It's tricky to do the complete check that
-- we do for whole program compilation, though, since that involves
-- traversing everything from the main expression.
-- For now, consider it an incentive not to have cycles :).
then recordWarning (GenericWarn ("Compiling hole " ++ show n))
else do ce <- toCDef n (type gdef) (eraseArgs gdef)
!(toFullNames (definition gdef))
setCompiled n ce
where
noDefYet : Def -> List CG -> Bool
noDefYet None (_ :: _) = True
noDefYet _ _ = False
export
mkForgetDef : {auto c : Ref Ctxt Defs} ->

View File

@ -70,4 +70,4 @@ executeExpr c tmpDir tm =
||| Codegen wrapper for Javascript implementation.
export
codegenJavascript : Codegen
codegenJavascript = MkCG compileExpr executeExpr
codegenJavascript = MkCG compileExpr executeExpr Nothing Nothing

View File

@ -58,4 +58,4 @@ executeExpr c tmpDir tm =
||| Codegen wrapper for Node implementation.
export
codegenNode : Codegen
codegenNode = MkCG compileExpr executeExpr
codegenNode = MkCG compileExpr executeExpr Nothing Nothing

View File

@ -7,6 +7,7 @@ import Core.CompileExpr
import Core.Context
import Core.Context.Log
import Core.FC
import Core.Options
import Core.TT
import Libraries.Data.LengthMatch
@ -315,9 +316,9 @@ fixArityTm (CRef fc n) args
= do defs <- get Ctxt
Just gdef <- lookupCtxtExact n (gamma defs)
| Nothing => pure (unload args (CRef fc n))
let Just def = compexpr gdef
| Nothing => pure (unload args (CRef fc n))
let arity = getArity def
let arity = case compexpr gdef of
Just def => getArity def
_ => 0
pure $ expandToArity arity (CApp fc (CRef fc n) []) args
fixArityTm (CLam fc x sc) args
= pure $ expandToArity Z (CLam fc x !(fixArityTm sc [])) args
@ -501,9 +502,16 @@ mergeLamDef : {auto c : Ref Ctxt Defs} ->
Name -> Core ()
mergeLamDef n
= do defs <- get Ctxt
Just def <- lookupCtxtExact n (gamma defs) | Nothing => pure ()
let Just cexpr = compexpr def | Nothing => pure ()
setCompiled n !(mergeLam cexpr)
Just def <- lookupCtxtExact n (gamma defs)
| Nothing => pure ()
let PMDef pi _ _ _ _ = definition def
| _ => pure ()
if not (isNil (incrementalCGs !getSession)) &&
externalDecl pi -- better keep it at arity 0
then pure ()
else do let Just cexpr = compexpr def
| Nothing => pure ()
setCompiled n !(mergeLam cexpr)
export
compileAndInlineAll : {auto c : Ref Ctxt Defs} ->

View File

@ -1046,4 +1046,4 @@ compileExpr _ _ _ _ _ _ = pure Nothing
export
codegenRefC : Codegen
codegenRefC = MkCG (compileExpr ANF) executeExpr
codegenRefC = MkCG (compileExpr ANF) executeExpr Nothing Nothing

View File

@ -82,8 +82,8 @@ findLibs ds
then Just (trim (substr 3 (length d) d))
else Nothing
schHeader : String -> List String -> String
schHeader chez libs
schHeader : String -> List String -> Bool -> String
schHeader chez libs whole
= (if os /= "windows" then "#!" ++ chez ++ " --script\n\n" else "") ++
"; @generated\n" ++
"(import (chezscheme))\n" ++
@ -95,14 +95,18 @@ schHeader chez libs
" (load-shared-object \"ws2_32.dll\")]\n" ++
" [else (load-shared-object \"libc.so\")])\n\n" ++
showSep "\n" (map (\x => "(load-shared-object \"" ++ escapeStringChez x ++ "\")") libs) ++ "\n\n" ++
"(let ()\n"
if whole
then "(let ()\n"
else "(source-directories (cons (getenv \"IDRIS2_INC_SRC\") '()))\n"
schFooter : Bool -> String
schFooter prof
schFooter : Bool -> Bool -> String
schFooter prof whole
= "(collect 4)\n(blodwen-run-finalisers)\n" ++
if prof
then "(profile-dump-html))\n"
else ")\n"
(if prof
then "(profile-dump-html)"
else "") ++
(if whole
then ")\n" else "\n")
showChezChar : Char -> String -> String
showChezChar '\\' = ("\\\\" ++)
@ -156,7 +160,7 @@ mutual
= do structsc <- schExp chezExtPrim chezString 0 struct
pure $ "(ftype-ref " ++ s ++ " (" ++ fld ++ ") " ++ structsc ++ ")"
chezExtPrim i GetField [_,_,_,_,_,_]
= pure "(error \"bad getField\")"
= pure "(blodwen-error-quit \"bad getField\")"
chezExtPrim i SetField [NmPrimVal _ (Str s), _, _, struct,
NmPrimVal _ (Str fld), _, val, world]
= do structsc <- schExp chezExtPrim chezString 0 struct
@ -165,7 +169,7 @@ mutual
"(ftype-set! " ++ s ++ " (" ++ fld ++ ") " ++ structsc ++
" " ++ valsc ++ ")"
chezExtPrim i SetField [_,_,_,_,_,_,_,_]
= pure "(error \"bad setField\")"
= pure "(blodwen-error-quit \"bad setField\")"
chezExtPrim i SysCodegen []
= pure $ "\"chez\""
chezExtPrim i OnCollect [_, p, c, world]
@ -213,34 +217,55 @@ cftySpec fc (CFStruct n t) = pure $ "(* " ++ n ++ ")"
cftySpec fc t = throw (GenericMsg fc ("Can't pass argument of type " ++ show t ++
" to foreign function"))
export
loadLib : {auto c : Ref Ctxt Defs} ->
String -> String -> Core String
loadLib appdir clib
= do (fname, fullname) <- locate clib
copyLib (appdir </> fname, fullname)
pure $ "(load-shared-object \""
++ escapeStringChez fname
++ "\")\n"
loadSO : {auto c : Ref Ctxt Defs} ->
String -> String -> Core String
loadSO appdir "" = pure ""
loadSO appdir mod
= do d <- getDirs
let fs = map (\p => p </> mod)
((build_dir d </> "ttc") :: extra_dirs d)
Just fname <- firstAvailable fs
| Nothing => throw (InternalError ("Missing .so:" ++ mod))
-- Easier to put them all in the same directory, so we don't need
-- to traverse a directory tree when installing the executable. So,
-- separate with '-' rather than directory separators.
let modfname = fastConcat (intersperse "-" (splitPath mod))
copyLib (appdir </> modfname, fname)
pure $ "(load \"" ++ escapeStringChez modfname ++ "\")\n"
cCall : {auto c : Ref Ctxt Defs}
-> {auto l : Ref Loaded (List String)}
-> String
-> FC
-> (cfn : String)
-> (clib : String)
-> List (Name, CFType)
-> CFType
-> (collectSafe : Bool)
-> Core (String, String)
cCall appdir fc cfn clib args (CFIORes CFGCPtr) _
-> Core (Maybe String, String)
cCall fc cfn clib args (CFIORes CFGCPtr) _
= throw (GenericMsg fc "Can't return GCPtr from a foreign function")
cCall appdir fc cfn clib args CFGCPtr _
cCall fc cfn clib args CFGCPtr _
= throw (GenericMsg fc "Can't return GCPtr from a foreign function")
cCall appdir fc cfn clib args (CFIORes CFBuffer) _
cCall fc cfn clib args (CFIORes CFBuffer) _
= throw (GenericMsg fc "Can't return Buffer from a foreign function")
cCall appdir fc cfn clib args CFBuffer _
cCall fc cfn clib args CFBuffer _
= throw (GenericMsg fc "Can't return Buffer from a foreign function")
cCall appdir fc cfn clib args ret collectSafe
cCall fc cfn clib args ret collectSafe
= do loaded <- get Loaded
lib <- if clib `elem` loaded
then pure ""
else do (fname, fullname) <- locate clib
copyLib (appdir </> fname, fullname)
put Loaded (clib :: loaded)
pure $ "(load-shared-object \""
++ escapeStringChez fname
++ "\")\n"
then pure Nothing
else do put Loaded (clib :: loaded)
pure (Just clib)
argTypes <- traverse (cftySpec fc . snd) args
retType <- cftySpec fc ret
let callConv = if collectSafe then " __collect_safe" else ""
@ -305,22 +330,22 @@ schemeCall fc sfn argns ret
-- function call.
useCC : {auto c : Ref Ctxt Defs} ->
{auto l : Ref Loaded (List String)} ->
String -> FC -> List String -> List (Name, CFType) -> CFType ->
Maybe Version -> Core (String, String)
useCC appdir fc ccs args ret version
FC -> List String -> List (Name, CFType) -> CFType ->
Maybe Version -> Core (Maybe String, String)
useCC fc ccs args ret version
= case parseCC ["scheme,chez", "scheme", "C__collect_safe", "C"] ccs of
Just ("scheme,chez", [sfn]) =>
do body <- schemeCall fc sfn (map fst args) ret
pure ("", body)
pure (Nothing, body)
Just ("scheme", [sfn]) =>
do body <- schemeCall fc sfn (map fst args) ret
pure ("", body)
pure (Nothing, body)
Just ("C__collect_safe", (cfn :: clib :: _)) => do
if unsupportedCallingConvention version
then cCall appdir fc cfn clib args ret False
else cCall appdir fc cfn clib args ret True
then cCall fc cfn clib args ret False
else cCall fc cfn clib args ret True
Just ("C", (cfn :: clib :: _)) =>
cCall appdir fc cfn clib args ret False
cCall fc cfn clib args ret False
_ => throw (NoForeignCC fc ccs)
-- For every foreign arg type, return a name, and whether to pass it to the
@ -350,28 +375,30 @@ mkStruct _ = pure ""
schFgnDef : {auto c : Ref Ctxt Defs} ->
{auto l : Ref Loaded (List String)} ->
{auto s : Ref Structs (List String)} ->
String -> FC -> Name -> NamedDef -> Maybe Version -> Core (String, String)
schFgnDef appdir fc n (MkNmForeign cs args ret) version
FC -> Name -> NamedDef -> Maybe Version ->
Core (Maybe String, String)
schFgnDef fc n (MkNmForeign cs args ret) version
= do let argns = mkArgs 0 args
let allargns = map fst argns
let useargns = map fst (filter snd argns)
argStrs <- traverse mkStruct args
retStr <- mkStruct ret
(load, body) <- useCC appdir fc cs (zip useargns args) ret version
(load, body) <- useCC fc cs (zip useargns args) ret version
defs <- get Ctxt
pure (load,
concat argStrs ++ retStr ++
"(define " ++ schName !(full (gamma defs) n) ++
" (lambda (" ++ showSep " " (map schName allargns) ++ ") " ++
body ++ "))\n")
schFgnDef _ _ _ _ _ = pure ("", "")
schFgnDef _ _ _ _ = pure (Nothing, "")
export
getFgnCall : {auto c : Ref Ctxt Defs} ->
{auto l : Ref Loaded (List String)} ->
{auto s : Ref Structs (List String)} ->
String -> Maybe Version -> (Name, FC, NamedDef) -> Core (String, String)
getFgnCall appdir version (n, fc, d) = schFgnDef appdir fc n d version
Maybe Version -> (Name, FC, NamedDef) ->
Core (Maybe String, String)
getFgnCall version (n, fc, d) = schFgnDef fc n d version
export
startChezPreamble : String
@ -391,6 +418,7 @@ startChezPreamble = unlines
startChez : String -> String -> String
startChez appdir target = startChezPreamble ++ unlines
[ "export LD_LIBRARY_PATH=\"$DIR/" ++ appdir ++ "\":$LD_LIBRARY_PATH"
, "export IDRIS2_INC_SRC=\"$DIR/" ++ appdir ++ "\""
, "\"$DIR/" ++ target ++ "\" \"$@\""
]
@ -399,6 +427,7 @@ startChezCmd chez appdir target = unlines
[ "@echo off"
, "set APPDIR=%~dp0"
, "set PATH=%APPDIR%\\" ++ appdir ++ ";%PATH%"
, "set IDRIS2_INC_SRC=%APPDIR%\\"
, "\"" ++ chez ++ "\" --script \"%APPDIR%/" ++ target ++ "\" %*"
]
@ -411,12 +440,14 @@ startChezWinSh chez appdir target = unlines
, "DIR=$(dirname \"$(readlink -f -- \"$0\")\")"
, "CHEZ=$(cygpath \"" ++ chez ++"\")"
, "export PATH=\"$DIR/" ++ appdir ++ "\":$PATH"
, "export IDRIS2_INC_SRC=\"$DIR/" ++ appdir ++ "\""
, "\"$CHEZ\" --script \"$DIR/" ++ target ++ "\" \"$@\""
]
||| Compile a TT expression to Chez Scheme
compileToSS : Ref Ctxt Defs ->
Bool -> String -> ClosedTerm -> (outfile : String) -> Core ()
Bool -> -- profiling
String -> ClosedTerm -> (outfile : String) -> Core ()
compileToSS c prof appdir tm outfile
= do ds <- getDirectives Chez
libs <- findLibs ds
@ -430,17 +461,19 @@ compileToSS c prof appdir tm outfile
s <- newRef {t = List String} Structs []
chez <- coreLift findChez
version <- coreLift $ chezVersion chez
fgndefs <- traverse (getFgnCall appdir version) ndefs
fgndefs <- traverse (getFgnCall version) ndefs
loadlibs <- traverse (loadLib appdir) (mapMaybe fst fgndefs)
compdefs <- traverse (getScheme chezExtPrim chezString) ndefs
let code = fastAppend (map snd fgndefs ++ compdefs)
main <- schExp chezExtPrim chezString 0 ctm
support <- readDataFile "chez/support.ss"
extraRuntime <- getExtraRuntime ds
let scm = schHeader chez (map snd libs) ++
let scm = schHeader chez (map snd libs) True ++
support ++ extraRuntime ++ code ++
concat (map fst fgndefs) ++
concat loadlibs ++
"(collect-request-handler (lambda () (collect) (blodwen-run-finalisers)))\n" ++
main ++ schFooter prof
main ++ schFooter prof True
Right () <- coreLift $ writeFile outfile scm
| Left err => throw (FileErr outfile err)
coreLift_ $ chmodRaw outfile 0o755
@ -448,7 +481,8 @@ compileToSS c prof appdir tm outfile
||| Compile a Chez Scheme source file to an executable, daringly with runtime checks off.
compileToSO : {auto c : Ref Ctxt Defs} ->
Bool -> String -> (appDirRel : String) -> (outSsAbs : String) -> Core ()
Bool -> -- profiling
String -> (appDirRel : String) -> (outSsAbs : String) -> Core ()
compileToSO prof chez appDirRel outSsAbs
= do let tmpFileAbs = appDirRel </> "compileChez"
let build = "(parameterize ([optimize-level 3] "
@ -462,6 +496,35 @@ compileToSO prof chez appDirRel outSsAbs
coreLift_ $ system (chez ++ " --script \"" ++ tmpFileAbs ++ "\"")
pure ()
||| Compile a TT expression to Chez Scheme using incremental module builds
compileToSSInc : Ref Ctxt Defs ->
List String -> -- module so files
List String -> -- libraries to find and load
String -> ClosedTerm -> (outfile : String) -> Core ()
compileToSSInc c mods libs appdir tm outfile
= do chez <- coreLift findChez
tmcexp <- compileTerm tm
let ctm = forget tmcexp
loadlibs <- traverse (loadLib appdir) (nub libs)
loadsos <- traverse (loadSO appdir) (nub mods)
main <- schExp chezExtPrim chezString 0 ctm
support <- readDataFile "chez/support.ss"
let scm = schHeader chez [] False ++
support ++
concat loadlibs ++
concat loadsos ++
"(collect-request-handler (lambda () (collect) (blodwen-run-finalisers)))\n" ++
main ++ schFooter False False
Right () <- coreLift $ writeFile outfile scm
| Left err => throw (FileErr outfile err)
coreLift_ $ chmodRaw outfile 0o755
pure ()
makeSh : String -> String -> String -> Core ()
makeSh outShRel appdir outAbs
= do Right () <- coreLift $ writeFile outShRel (startChez appdir outAbs)
@ -478,10 +541,9 @@ makeShWindows chez outShRel appdir outAbs
| Left err => throw (FileErr outShRel err)
pure ()
||| Chez Scheme implementation of the `compileExpr` interface.
compileExpr : Bool -> Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String) ->
ClosedTerm -> (outfile : String) -> Core (Maybe String)
compileExpr makeitso c tmpDir outputDir tm outfile
compileExprWhole : Bool -> Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String) ->
ClosedTerm -> (outfile : String) -> Core (Maybe String)
compileExprWhole makeitso c tmpDir outputDir tm outfile
= do let appDirRel = outfile ++ "_app" -- relative to build dir
let appDirGen = outputDir </> appDirRel -- relative to here
coreLift_ $ mkdirAll appDirGen
@ -494,7 +556,8 @@ compileExpr makeitso c tmpDir outputDir tm outfile
chez <- coreLift $ findChez
let prof = profile !getSession
compileToSS c (makeitso && prof) appDirGen tm outSsAbs
logTime "++ Make SO" $ when makeitso $ compileToSO prof chez appDirGen outSsAbs
logTime "++ Make SO" $ when makeitso $
compileToSO prof chez appDirGen outSsAbs
let outShRel = outputDir </> outfile
if isWindows
then makeShWindows chez outShRel appDirRel (if makeitso then outSoFile else outSsFile)
@ -502,6 +565,41 @@ compileExpr makeitso c tmpDir outputDir tm outfile
coreLift_ $ chmodRaw outShRel 0o755
pure (Just outShRel)
compileExprInc : Bool -> Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String) ->
ClosedTerm -> (outfile : String) -> Core (Maybe String)
compileExprInc makeitso c tmpDir outputDir tm outfile
= do defs <- get Ctxt
let Just (mods, libs) = lookup Chez (allIncData defs)
| Nothing =>
do coreLift $ putStrLn $ "Missing incremental compile data, reverting to whole program compilation"
compileExprWhole makeitso c tmpDir outputDir tm outfile
let appDirRel = outfile ++ "_app" -- relative to build dir
let appDirGen = outputDir </> appDirRel -- relative to here
coreLift_ $ mkdirAll appDirGen
Just cwd <- coreLift currentDir
| Nothing => throw (InternalError "Can't get current directory")
let outSsFile = appDirRel </> outfile <.> "ss"
let outSoFile = appDirRel </> outfile <.> "so"
let outSsAbs = cwd </> outputDir </> outSsFile
let outSoAbs = cwd </> outputDir </> outSoFile
chez <- coreLift $ findChez
compileToSSInc c mods libs appDirGen tm outSsAbs
let outShRel = outputDir </> outfile
if isWindows
then makeShWindows chez outShRel appDirRel outSsFile
else makeSh outShRel appDirRel outSsFile
coreLift_ $ chmodRaw outShRel 0o755
pure (Just outShRel)
||| Chez Scheme implementation of the `compileExpr` interface.
compileExpr : Bool -> Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String) ->
ClosedTerm -> (outfile : String) -> Core (Maybe String)
compileExpr makeitso c tmpDir outputDir tm outfile
= do s <- getSession
if not (wholeProgram s) && (Chez `elem` incrementalCGs !getSession)
then compileExprInc makeitso c tmpDir outputDir tm outfile
else compileExprWhole makeitso c tmpDir outputDir tm outfile
||| Chez Scheme implementation of the `executeExpr` interface.
||| This implementation simply runs the usual compiler, saving it to a temp file, then interpreting it.
executeExpr : Ref Ctxt Defs -> (tmpDir : String) -> ClosedTerm -> Core ()
@ -511,7 +609,44 @@ executeExpr c tmpDir tm
coreLift_ $ system sh
pure ()
incCompile : Ref Ctxt Defs ->
(sourceFile : String) -> Core (Maybe (String, List String))
incCompile c sourceFile
= do ssFile <- getTTCFileName sourceFile "ss"
soFile <- getTTCFileName sourceFile "so"
soFilename <- getObjFileName sourceFile "so"
cdata <- getIncCompileData False Cases
d <- getDirs
let outputDir = build_dir d </> "ttc"
let ndefs = namedDefs cdata
if isNil ndefs
then pure (Just ("", []))
-- ^ no code to generate, but still recored that the
-- module has been compiled, with no output needed.
else do
l <- newRef {t = List String} Loaded ["libc", "libc 6"]
s <- newRef {t = List String} Structs []
chez <- coreLift findChez
version <- coreLift $ chezVersion chez
fgndefs <- traverse (getFgnCall version) ndefs
compdefs <- traverse (getScheme chezExtPrim chezString) ndefs
let code = fastAppend (map snd fgndefs ++ compdefs)
Right () <- coreLift $ writeFile ssFile code
| Left err => throw (FileErr ssFile err)
-- Compile to .so
let tmpFileAbs = outputDir </> "compileChez"
let build = "(parameterize ([optimize-level 3] " ++
"[compile-file-message #f]) (compile-file " ++
show ssFile ++ "))"
Right () <- coreLift $ writeFile tmpFileAbs build
| Left err => throw (FileErr tmpFileAbs err)
coreLift_ $ system (chez ++ " --script \"" ++ tmpFileAbs ++ "\"")
pure (Just (soFilename, mapMaybe fst fgndefs))
||| Codegen wrapper for Chez scheme implementation.
export
codegenChez : Codegen
codegenChez = MkCG (compileExpr True) executeExpr
codegenChez = MkCG (compileExpr True) executeExpr (Just incCompile) (Just "so")

View File

@ -217,8 +217,9 @@ compileToSS c chez appdir tm = do
++ " (import (chezscheme) (support) " ++ imports ++ ")\n\n"
let footer = ")"
fgndefs <- traverse (Chez.getFgnCall appdir version) cu.definitions
fgndefs <- traverse (Chez.getFgnCall version) cu.definitions
compdefs <- traverse (getScheme Chez.chezExtPrim Chez.chezString) cu.definitions
loadlibs <- traverse (loadLib appdir) (mapMaybe fst fgndefs)
-- write the files
log "compiler.scheme.chez" 3 $ "Generating code for " ++ chezLib
@ -226,7 +227,7 @@ compileToSS c chez appdir tm = do
[header]
++ map snd fgndefs -- definitions using foreign libs
++ compdefs
++ map fst fgndefs -- foreign library load statements
++ loadlibs -- foreign library load statements
++ [footer]
Core.writeFile (appdir </> chezLib <.> "hash") cuHash
@ -311,4 +312,4 @@ executeExpr c tmpDir tm
||| Codegen wrapper for Chez scheme implementation.
export
codegenChezSep : Codegen
codegenChezSep = MkCG (compileExpr True) executeExpr
codegenChezSep = MkCG (compileExpr True) executeExpr Nothing Nothing

View File

@ -423,4 +423,4 @@ executeExpr c tmpDir tm
export
codegenGambit : Codegen
codegenGambit = MkCG compileExpr executeExpr
codegenGambit = MkCG compileExpr executeExpr Nothing Nothing

View File

@ -456,4 +456,4 @@ executeExpr c tmpDir tm
export
codegenRacket : Codegen
codegenRacket = MkCG (compileExpr True) executeExpr
codegenRacket = MkCG (compileExpr True) executeExpr Nothing Nothing

View File

@ -31,7 +31,7 @@ import public Libraries.Utils.Binary
||| (Increment this when changing anything in the data format)
export
ttcVersion : Int
ttcVersion = 56
ttcVersion = 57
export
checkTTCVersion : String -> Int -> Int -> Core ()
@ -44,6 +44,7 @@ record TTCFile extra where
sourceHash : String
ifaceHash : Int
importHashes : List (Namespace, Int)
incData : List (CG, String, List String)
context : List (Name, Binary)
userHoles : List Name
autoHints : List (Name, Bool)
@ -92,14 +93,14 @@ HasNames (Name, Name, Bool) where
resolved c (n1, n2, b) = pure (!(resolved c n1), !(resolved c n2), b)
HasNames e => HasNames (TTCFile e) where
full gam (MkTTCFile version sourceHash ifaceHash iHashes
full gam (MkTTCFile version sourceHash ifaceHash iHashes incData
context userHoles
autoHints typeHints
imported nextVar currentNS nestedNS
pairnames rewritenames primnames
namedirectives cgdirectives trans
extra)
= pure $ MkTTCFile version sourceHash ifaceHash iHashes
= pure $ MkTTCFile version sourceHash ifaceHash iHashes incData
context userHoles
!(traverse (full gam) autoHints)
!(traverse (full gam) typeHints)
@ -130,14 +131,14 @@ HasNames e => HasNames (TTCFile e) where
-- I don't think we ever actually want to call this, because after we read
-- from the file we're going to add them to learn what the resolved names
-- are supposed to be! But for completeness, let's do it right.
resolved gam (MkTTCFile version sourceHash ifaceHash iHashes
resolved gam (MkTTCFile version sourceHash ifaceHash iHashes incData
context userHoles
autoHints typeHints
imported nextVar currentNS nestedNS
pairnames rewritenames primnames
namedirectives cgdirectives trans
extra)
= pure $ MkTTCFile version sourceHash ifaceHash iHashes
= pure $ MkTTCFile version sourceHash ifaceHash iHashes incData
context userHoles
!(traverse (resolved gam) autoHints)
!(traverse (resolved gam) typeHints)
@ -179,6 +180,7 @@ writeTTCFile b file_in
toBuf b (sourceHash file)
toBuf b (ifaceHash file)
toBuf b (importHashes file)
toBuf b (incData file)
toBuf b (imported file)
toBuf b (extraData file)
toBuf b (context file)
@ -208,10 +210,12 @@ readTTCFile readall file as b
sourceFileHash <- fromBuf b
ifaceHash <- fromBuf b
importHashes <- fromBuf b
incData <- fromBuf b
imp <- fromBuf b
ex <- fromBuf b
if not readall
then pure (MkTTCFile ver sourceFileHash ifaceHash importHashes [] [] [] [] []
then pure (MkTTCFile ver sourceFileHash ifaceHash importHashes
incData [] [] [] [] []
0 (mkNamespace "") [] Nothing
Nothing
(MkPrimNs Nothing Nothing Nothing Nothing)
@ -230,7 +234,7 @@ readTTCFile readall file as b
nds <- fromBuf b
cgds <- fromBuf b
trans <- fromBuf b
pure (MkTTCFile ver sourceFileHash ifaceHash importHashes
pure (MkTTCFile ver sourceFileHash ifaceHash importHashes incData
(map (replaceNS cns) defs) uholes
autohs typehs imp nextv cns nns
pns rws prims nds cgds trans ex)
@ -277,6 +281,7 @@ writeToTTC extradata sourceFileName ttcFileName
log "ttc.write" 5 $ "Writing " ++ ttcFileName ++ " with source hash " ++ sourceHash ++ " and interface hash " ++ show (ifaceHash defs)
writeTTCFile bin
(MkTTCFile ttcVersion (sourceHash) (ifaceHash defs) (importHashes defs)
(incData defs)
gdefs
(keys (userHoles defs))
(saveAutoHints defs)
@ -455,7 +460,7 @@ readFromTTC nestedns loc reexp fname modNS importAs
ttc <- readTTCFile True fname as bin
let ex = extraData ttc
traverse_ (addGlobalDef modNS (currentNS ttc) as) (context ttc)
traverse_ addUserHole (userHoles ttc)
traverse_ (addUserHole True) (userHoles ttc)
setNS (currentNS ttc)
when nestedns $ setNestedNS (nestedNS ttc)
-- Only do the next batch if the module hasn't been loaded
@ -464,6 +469,8 @@ readFromTTC nestedns loc reexp fname modNS importAs
-- Set up typeHints and autoHints based on the loaded data
do traverse_ (addTypeHint loc) (typeHints ttc)
traverse_ addAutoHint (autoHints ttc)
addImportedInc modNS (incData ttc)
defs <- get Ctxt
-- Set up pair/rewrite etc names
updatePair (pairnames ttc)
updateRewrite (rewritenames ttc)

View File

@ -40,10 +40,12 @@ record PMDefInfo where
holeInfo : HoleInfo -- data if it comes from a solved hole
alwaysReduce : Bool -- always reduce, even when quoting etc
-- typically for inlinable metavariable solutions
externalDecl : Bool -- declared in another module, which may affect how it
-- is compiled
export
defaultPI : PMDefInfo
defaultPI = MkPMDefInfo NotHole False
defaultPI = MkPMDefInfo NotHole False False
public export
record TypeFlags where
@ -1104,12 +1106,19 @@ record Defs where
-- be interpreted however the specific code generator requires
toCompileCase : List Name
-- ^ Names which need to be compiled to run time case trees
incData : List (CG, String, List String)
-- ^ What we've compiled incrementally for this module: codegen,
-- object file, any additional CG dependent data (e.g. linker flags)
allIncData : List (CG, List String, List String)
-- ^ Incrementally compiled files for all imports. Only lists CGs for
-- while all modules have associated incremental compile data
toIR : NameMap ()
-- ^ Names which need to be compiled to IR at the end of processing
-- the current module
userHoles : NameMap ()
userHoles : NameMap Bool
-- ^ Metavariables the user still has to fill in. In practice, that's
-- everything with a user accessible name and a definition of Hole
-- everything with a user accessible name and a definition of Hole.
-- The Bool says whether it was introduced in another module.
peFailures : NameMap ()
-- ^ Partial evaluation names which have failed, so don't bother trying
-- again
@ -1159,6 +1168,8 @@ initDefs
, allImported = []
, cgdirectives = []
, toCompileCase = []
, incData = []
, allIncData = []
, toIR = empty
, userHoles = empty
, peFailures = empty
@ -1288,10 +1299,12 @@ initHash
export
addUserHole : {auto c : Ref Ctxt Defs} ->
Name -> Core ()
addUserHole n
Bool -> -- defined in another module?
Name -> -- hole name
Core ()
addUserHole ext n
= do defs <- get Ctxt
put Ctxt (record { userHoles $= insert n () } defs)
put Ctxt (record { userHoles $= insert n ext } defs)
export
clearUserHole : {auto c : Ref Ctxt Defs} ->
@ -2639,3 +2652,47 @@ checkTimer
if (t > max)
then throw (Timeout action)
else pure ()
-- Update the list of imported incremental compile data, if we're in
-- incremental mode for the current CG
export
addImportedInc : {auto c : Ref Ctxt Defs} ->
ModuleIdent -> List (CG, String, List String) -> Core ()
addImportedInc modNS inc
= do s <- getSession
let cg = s.codegen
defs <- get Ctxt
when (cg `elem` s.incrementalCGs) $
case lookup cg inc of
Nothing =>
-- No incremental compile data for current CG, so we can't
-- compile incrementally
do recordWarning (GenericWarn ("No incremental compile data for " ++ show modNS))
defs <- get Ctxt
put Ctxt (record { allIncData $= drop cg } defs)
Just (mods, extra) =>
put Ctxt (record { allIncData $= addMod cg (mods, extra) }
defs)
where
addMod : CG -> (String, List String) ->
List (CG, (List String, List String)) ->
List (CG, (List String, List String))
addMod cg (mod, all) [] = [(cg, ([mod], all))]
addMod cg (mod, all) ((cg', (mods, libs)) :: xs)
= if cg == cg'
then ((cg, (mod :: mods, libs ++ all)) :: xs)
else ((cg', (mods, libs)) :: addMod cg (mod, all) xs)
drop : CG -> List (CG, a) -> List (CG, a)
drop cg [] = []
drop cg ((x, v) :: xs)
= if cg == x
then xs
else ((x, v) :: drop cg xs)
export
setIncData : {auto c : Ref Ctxt Defs} ->
CG -> (String, List String) -> Core ()
setIncData cg res
= do defs <- get Ctxt
put Ctxt (record { incData $= ((cg, res) :: )} defs)

View File

@ -65,6 +65,7 @@ data Warning : Type where
FC -> Env Term vars -> Term vars -> Warning
ShadowingGlobalDefs : FC -> List1 (String, List1 Name) -> Warning
Deprecated : String -> Warning
GenericWarn : String -> Warning
-- All possible errors, carrying a location
public export
@ -183,6 +184,7 @@ Show Warning where
show (UnreachableClause _ _ _) = ":Unreachable clause"
show (ShadowingGlobalDefs _ _) = ":Shadowing names"
show (Deprecated name) = ":Deprecated " ++ name
show (GenericWarn msg) = msg
export
@ -359,6 +361,7 @@ getWarningLoc : Warning -> Maybe FC
getWarningLoc (UnreachableClause fc _ _) = Just fc
getWarningLoc (ShadowingGlobalDefs fc _) = Just fc
getWarningLoc (Deprecated _) = Nothing
getWarningLoc (GenericWarn _) = Nothing
export
getErrorLoc : Error -> Maybe FC

View File

@ -207,6 +207,18 @@ getTTCFileName inp ext
let bdir = build_dir d
pure $ bdir </> "ttc" </> fname
-- Given a source file, return the name of the corresponding object file.
-- As above, but without the build directory
export
getObjFileName : {auto c : Ref Ctxt Defs} ->
String -> String -> Core String
getObjFileName inp ext
= do -- Get its namespace from the file relative to the working directory
-- and generate the ttc file from that
ns <- ctxtPathToNS inp
let fname = ModuleIdent.toPath ns <.> ext
pure $ fname
-- Given a root executable name, return the name in the build directory
export
getExecFileName : {auto c : Ref Ctxt Defs} -> String -> Core String

View File

@ -164,6 +164,11 @@ record Session where
showShadowingWarning : Bool
-- Experimental
checkHashesInsteadOfModTime : Bool
incrementalCGs : List CG
wholeProgram : Bool
-- Use whole program compilation for executables, no matter what
-- incremental CGs are set (intended for overriding any environment
-- variables that set incremental compilation)
public export
record PPrinter where
@ -212,7 +217,8 @@ export
defaultSession : Session
defaultSession = MkSessionOpts False False False Chez [] False defaultLogLevel
False False False Nothing Nothing
Nothing Nothing False 1000 False True False
Nothing Nothing False 1000 False True
False [] False
export
defaultElab : ElabDirectives

View File

@ -904,10 +904,12 @@ TTC PMDefInfo where
toBuf b l
= do toBuf b (holeInfo l)
toBuf b (alwaysReduce l)
toBuf b (externalDecl l)
fromBuf b
= do h <- fromBuf b
r <- fromBuf b
pure (MkPMDefInfo h r)
e <- fromBuf b
pure (MkPMDefInfo h r e)
export
TTC TypeFlags where

View File

@ -475,7 +475,7 @@ instantiate {newvars} loc mode env mname mref num mdef locs otm tm
rhs <- mkDef locs INil tm ty
logTerm "unify.instantiate" 5 "Definition" rhs
let simpleDef = MkPMDefInfo (SolvedHole num) (isSimple rhs)
let simpleDef = MkPMDefInfo (SolvedHole num) (isSimple rhs) False
let newdef = record { definition =
PMDef simpleDef [] (STerm 0 rhs) (STerm 0 rhs) []
} mdef
@ -1464,7 +1464,7 @@ retryGuess mode smode (hid, (loc, hname))
do ty <- getType [] tm
logTerm "unify.retry" 5 "Retry Delay" tm
pure $ delayMeta r envb !(getTerm ty) tm
let gdef = record { definition = PMDef (MkPMDefInfo NotHole True)
let gdef = record { definition = PMDef (MkPMDefInfo NotHole True False)
[] (STerm 0 tm') (STerm 0 tm') [] } def
logTerm "unify.retry" 5 ("Resolved " ++ show hname) tm'
ignore $ addDef (Resolved hid) gdef
@ -1490,7 +1490,7 @@ retryGuess mode smode (hid, (loc, hname))
-- All constraints resolved, so turn into a
-- proper definition and remove it from the
-- hole list
[] => do let gdef = record { definition = PMDef (MkPMDefInfo NotHole True)
[] => do let gdef = record { definition = PMDef (MkPMDefInfo NotHole True False)
[] (STerm 0 tm) (STerm 0 tm) [] } def
logTerm "unify.retry" 5 ("Resolved " ++ show hname) tm
ignore $ addDef (Resolved hid) gdef

View File

@ -139,6 +139,10 @@ data CLOpt
||| Use SHA256 hashes to determine if a source file needs rebuilding instead
||| of modification time.
HashesInsteadOfModTime |
||| Use incremental code generation, if the backend supports it
IncrementalCG String |
||| Use whole program compilation - overrides IncrementalCG if set
WholeProgram |
||| Generate bash completion info
BashCompletion String String |
||| Generate bash completion script
@ -209,6 +213,10 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
(Just "Don't implicitly import Prelude"),
MkOpt ["--codegen", "--cg"] [Required "backend"] (\f => [SetCG f])
(Just $ "Set code generator " ++ showDefault (codegen defaultSession)),
MkOpt ["--incremental-cg", "--inc"] [Required "backend"] (\f => [IncrementalCG f])
(Just "Incremental code generation on given backend"),
MkOpt ["--whole-program", "--wp"] [] [WholeProgram]
(Just "Use whole program compilation (overrides --inc)"),
MkOpt ["--directive"] [Required "directive"] (\d => [Directive d])
(Just $ "Pass a directive to the current code generator"),
MkOpt ["--package", "-p"] [Required "package"] (\f => [PkgPath f])

View File

@ -45,36 +45,42 @@ findInput (_ :: fs) = findInput fs
-- Add extra data from the "IDRIS2_x" environment variables
updateEnv : {auto c : Ref Ctxt Defs} ->
{auto o : Ref ROpts REPLOpts} ->
Core ()
updateEnv
= do defs <- get Ctxt
bprefix <- coreLift $ idrisGetEnv "IDRIS2_PREFIX"
the (Core ()) $ case bprefix of
case bprefix of
Just p => setPrefix p
Nothing => setPrefix yprefix
bpath <- coreLift $ idrisGetEnv "IDRIS2_PATH"
the (Core ()) $ case bpath of
case bpath of
Just path => do traverseList1_ addExtraDir (map trim (split (==pathSeparator) path))
Nothing => pure ()
bdata <- coreLift $ idrisGetEnv "IDRIS2_DATA"
the (Core ()) $ case bdata of
case bdata of
Just path => do traverseList1_ addDataDir (map trim (split (==pathSeparator) path))
Nothing => pure ()
blibs <- coreLift $ idrisGetEnv "IDRIS2_LIBS"
the (Core ()) $ case blibs of
case blibs of
Just path => do traverseList1_ addLibDir (map trim (split (==pathSeparator) path))
Nothing => pure ()
pdirs <- coreLift $ idrisGetEnv "IDRIS2_PACKAGE_PATH"
the (Core ()) $ case pdirs of
case pdirs of
Just path => do traverseList1_ addPackageDir (map trim (split (==pathSeparator) path))
Nothing => pure ()
cg <- coreLift $ idrisGetEnv "IDRIS2_CG"
the (Core ()) $ case cg of
case cg of
Just e => case getCG (options defs) e of
Just cg => setCG cg
Nothing => throw (InternalError ("Unknown code generator " ++ show e))
Nothing => pure ()
inccgs <- coreLift $ idrisGetEnv "IDRIS2_INC_CGS"
case inccgs of
Just cgs =>
traverse_ (setIncrementalCG False) $
map trim (toList (split (==',') cgs))
Nothing => pure ()
-- IDRIS2_PATH goes first so that it overrides this if there's
-- any conflicts. In particular, that means that setting IDRIS2_PATH
-- for the tests means they test the local version not the installed
@ -160,12 +166,12 @@ stMain cgs opts
when (ignoreMissingIpkg opts) $
setSession (record { ignoreMissingPkg = True } !getSession)
updateEnv
let ide = ideMode opts
let ideSocket = ideModeSocket opts
let outmode = if ide then IDEMode 0 stdin stdout else REPL False
let fname = findInput opts
o <- newRef ROpts (REPL.Opts.defaultOpts fname outmode cgs)
updateEnv
finish <- showInfo opts
when (not finish) $ do

View File

@ -27,6 +27,7 @@ envs = [
MkEnvDesc "IDRIS2_DATA" "Places Idris2 looks for data files",
MkEnvDesc "IDRIS2_LIBS" "Places Idris2 looks for libraries (for code generation)",
MkEnvDesc "IDRIS2_CG" "Codegen backend",
MkEnvDesc "IDRIS2_INC_CGS" "Code generators to use (comma separated) when compiling modules incrementally",
MkEnvDesc "CHEZ" "chez executable used in Chez codegen",
MkEnvDesc "RACKET" "racket executable used in Racket codegen",
MkEnvDesc "RACKET_RACO" "raco executable used in Racket codegen",

View File

@ -174,6 +174,8 @@ pwarning (ShadowingGlobalDefs _ ns)
pwarning (Deprecated s)
= pure $ pretty "Deprecation warning:" <++> pretty s
pwarning (GenericWarn s)
= pure $ pretty s
export
perror : {auto c : Ref Ctxt Defs} ->

View File

@ -341,11 +341,26 @@ copyFile src dest
| Left err => pure (Left err)
writeToFile dest buf
installFrom : {auto c : Ref Ctxt Defs} ->
installFrom : {auto o : Ref ROpts REPLOpts} ->
{auto c : Ref Ctxt Defs} ->
String -> String -> ModuleIdent -> Core ()
installFrom builddir destdir ns
= do let ttcfile = ModuleIdent.toPath ns
let ttcPath = builddir </> "ttc" </> ttcfile <.> "ttc"
objPaths_in <- traverse
(\cg =>
do Just cgdata <- getCG cg
| Nothing => pure Nothing
let Just ext = incExt cgdata
| Nothing => pure Nothing
let srcFile = builddir </> "ttc" </> ttcfile <.> ext
let destFile = destdir </> ttcfile <.> ext
let Just (dir, _) = splitParent destFile
| Nothing => pure Nothing
ensureDirectoryExists dir
pure $ Just (srcFile, destFile))
(incrementalCGs !getSession)
let objPaths = mapMaybe id objPaths_in
let modPath = reverse $ fromMaybe [] $ tail' $ unsafeUnfoldModuleIdent ns
let destNest = joinPath modPath
@ -361,6 +376,13 @@ installFrom builddir destdir ns
| Left err => throw $ InternalError $ unlines
[ "Can't copy file " ++ ttcPath ++ " to " ++ destPath
, show err ]
-- Copy object files, if any. They don't necessarily get created,
-- since some modules don't generate any code themselves.
traverse_ (\ (obj, dest) =>
do coreLift $ putStrLn $ "Installing " ++ obj ++ " to " ++ destPath
ignore $ coreLift $ copyFile obj dest)
objPaths
pure ()
installSrcFrom : {auto c : Ref Ctxt Defs} ->

View File

@ -1,5 +1,13 @@
module Idris.ProcessIdr
import Compiler.RefC.RefC
import Compiler.Scheme.Chez
import Compiler.Scheme.ChezSep
import Compiler.Scheme.Racket
import Compiler.Scheme.Gambit
import Compiler.ES.Node
import Compiler.ES.Javascript
import Compiler.Common
import Compiler.Inline
import Core.Binary
@ -29,7 +37,9 @@ import Idris.Pretty
import Data.List
import Libraries.Data.NameMap
import Libraries.Utils.Path
import System
import System.File
%default covering
@ -150,6 +160,7 @@ readAsMain fname
= do Just (syn, _, more) <- readFromTTC {extra = SyntaxInfo}
True EmptyFC True fname (nsAsModuleIdent emptyNS) emptyNS
| Nothing => throw (InternalError "Already loaded")
replNS <- getNS
replNestedNS <- getNestedNS
extendSyn syn
@ -225,6 +236,25 @@ unchangedHash sourceFileName ttcFileName
(storedSourceHash, _) <- readHashes ttcFileName
pure $ sourceCodeHash == storedSourceHash
export
getCG : {auto o : Ref ROpts REPLOpts} ->
{auto c : Ref Ctxt Defs} ->
CG -> Core (Maybe Codegen)
getCG Chez = pure $ Just codegenChez
getCG ChezSep = pure $ Just codegenChezSep
getCG Racket = pure $ Just codegenRacket
getCG Gambit = pure $ Just codegenGambit
getCG Node = pure $ Just codegenNode
getCG Javascript = pure $ Just codegenJavascript
getCG RefC = pure $ Just codegenRefC
getCG (Other s) = getCodegen s
export
findCG : {auto o : Ref ROpts REPLOpts} ->
{auto c : Ref Ctxt Defs} -> Core (Maybe Codegen)
findCG
= do defs <- get Ctxt
getCG (codegen (session (options defs)))
||| Process everything in the module; return the syntax information which
||| needs to be written to the TTC (e.g. exported infix operators)
@ -341,6 +371,17 @@ process buildmsg sourceFileName ident
do defs <- get Ctxt
ns <- ctxtPathToNS sourceFileName
makeBuildDirectory ns
traverse_
(\cg =>
do Just cgdata <- getCG cg
| Nothing =>
coreLift $ putStrLn $ "No incremental code generator for " ++ show cg
Just res <- incCompile cgdata sourceFileName
| Nothing => pure ()
setIncData cg res)
(incrementalCGs !getSession)
writeToTTC !(get Syn) sourceFileName ttcFileName
ttmFileName <- getTTCFileName sourceFileName "ttm"
writeToTTM ttmFileName

View File

@ -207,24 +207,6 @@ getOptions = do
, Editor (editor opts)
]
export
findCG : {auto o : Ref ROpts REPLOpts} ->
{auto c : Ref Ctxt Defs} -> Core Codegen
findCG
= do defs <- get Ctxt
case codegen (session (options defs)) of
Chez => pure codegenChez
ChezSep => pure codegenChezSep
Racket => pure codegenRacket
Gambit => pure codegenGambit
Node => pure codegenNode
Javascript => pure codegenJavascript
RefC => pure codegenRefC
Other s => case !(getCodegen s) of
Just cg => pure cg
Nothing => do coreLift_ $ putStrLn ("No such code generator: " ++ s)
coreLift $ exitWith (ExitFailure 1)
anyAt : (a -> Bool) -> a -> b -> Bool
anyAt p loc _ = p loc
@ -598,7 +580,11 @@ execExp : {auto c : Ref Ctxt Defs} ->
PTerm -> Core REPLResult
execExp ctm
= do tm_erased <- prepareExp ctm
execute !findCG tm_erased
Just cg <- findCG
| Nothing =>
do iputStrLn (reflow "No such code generator available")
pure CompilationFailed
execute cg tm_erased
pure $ Executed ctm
@ -628,7 +614,11 @@ compileExp : {auto c : Ref Ctxt Defs} ->
PTerm -> String -> Core REPLResult
compileExp ctm outfile
= do tm_erased <- prepareExp ctm
ok <- compile !findCG tm_erased outfile
Just cg <- findCG
| Nothing =>
do iputStrLn (reflow "No such code generator available")
pure CompilationFailed
ok <- compile cg tm_erased outfile
maybe (pure CompilationFailed)
(pure . Compiled)
ok

View File

@ -1,5 +1,7 @@
module Idris.SetOptions
import Compiler.Common
import Core.Context
import Core.Directory
import Core.Metadata
@ -10,6 +12,7 @@ import Libraries.Data.List.Extra
import Idris.CommandLine
import Idris.Package.Types
import Idris.ProcessIdr
import Idris.REPL
import Idris.Syntax
import Idris.Version
@ -241,6 +244,31 @@ completionScript fun =
-- Processing Options
--------------------------------------------------------------------------------
export
setIncrementalCG : {auto c : Ref Ctxt Defs} ->
{auto o : Ref ROpts REPLOpts} ->
Bool -> String -> Core ()
setIncrementalCG failOnError cgn
= do defs <- get Ctxt
case getCG (options defs) cgn of
Just cg =>
do Just cgd <- getCG cg
| Nothing => pure ()
let Just _ = incCompileFile cgd
| Nothing =>
if failOnError
then do coreLift $ putStrLn $ cgn ++ " does not support incremental builds"
coreLift $ exitWith (ExitFailure 1)
else pure ()
setSession (record { incrementalCGs $= (cg :: )} !getSession)
Nothing =>
if failOnError
then do coreLift $ putStrLn "No such code generator"
coreLift $ putStrLn $ "Code generators available: " ++
showSep ", " (map fst (availableCGs (options defs)))
coreLift $ exitWith (ExitFailure 1)
else pure ()
-- Options to be processed before type checking. Return whether to continue.
export
preOptions : {auto c : Ref Ctxt Defs} ->
@ -349,7 +377,14 @@ preOptions (IgnoreShadowingWarnings :: opts)
= do setSession (record { showShadowingWarning = False } !getSession)
preOptions opts
preOptions (HashesInsteadOfModTime :: opts)
= do setSession (record {checkHashesInsteadOfModTime = True} !getSession)
= do setSession (record { checkHashesInsteadOfModTime = True } !getSession)
preOptions opts
preOptions (IncrementalCG e :: opts)
= do defs <- get Ctxt
setIncrementalCG True e
preOptions opts
preOptions (WholeProgram :: opts)
= do setSession (record { wholeProgram = True } !getSession)
preOptions opts
preOptions (BashCompletion a b :: _)
= do os <- opts a b

View File

@ -253,7 +253,8 @@ retryDelayed' errmode acc (d@(_, i, hints, elab) :: ds)
let ds' = reverse (delayedElab ust) ++ ds
updateDef (Resolved i) (const (Just
(PMDef (MkPMDefInfo NotHole True) [] (STerm 0 tm) (STerm 0 tm) [])))
(PMDef (MkPMDefInfo NotHole True False)
[] (STerm 0 tm) (STerm 0 tm) [])))
logTerm "elab.update" 5 ("Resolved delayed hole " ++ show i) tm
logTermNF "elab.update" 5 ("Resolved delayed hole NF " ++ show i) [] tm
removeHole i

View File

@ -54,7 +54,7 @@ checkHole rig elabinfo nest env fc n_in (Just gexpty)
-- Record the LHS for this hole in the metadata
withCurrentLHS (Resolved idx)
addNameLoc fc nm
addUserHole nm
addUserHole False nm
saveHole nm
pure (metaval, gexpty)
checkHole rig elabinfo nest env fc n_in exp
@ -71,6 +71,6 @@ checkHole rig elabinfo nest env fc n_in exp
(idx, metaval) <- metaVarI fc rig env' nm ty
withCurrentLHS (Resolved idx)
addNameLoc fc nm
addUserHole nm
addUserHole False nm
saveHole nm
pure (metaval, gnf env ty)

View File

@ -871,11 +871,16 @@ processDef opts nest env fc n_in cs_in
do t <- toFullNames tree_ct
pure ("Case tree for " ++ show n ++ ": " ++ show t)
-- check whether the name was declared in a different source file
defs <- get Ctxt
let pi = case lookup n (userHoles defs) of
Nothing => defaultPI
Just e => record { externalDecl = e } defaultPI
-- Add compile time tree as a placeholder for the runtime tree,
-- but we'll rebuild that in a later pass once all the case
-- blocks etc are resolved
ignore $ addDef (Resolved nidx)
(record { definition = PMDef defaultPI cargs tree_ct tree_ct pats
(record { definition = PMDef pi cargs tree_ct tree_ct pats
} gdef)
when (visibility gdef == Public) $

View File

@ -203,7 +203,7 @@ initDef : {vars : _} ->
{auto u : Ref UST UState} ->
Name -> Env Term vars -> Term vars -> List FnOpt -> Core Def
initDef n env ty []
= do addUserHole n
= do addUserHole False n
pure None
initDef n env ty (ExternFn :: opts)
= do defs <- get Ctxt

View File

@ -13,7 +13,7 @@ execute : Ref Ctxt Defs -> (execDir : String) -> ClosedTerm -> Core ()
execute defs dir term = do coreLift $ putStrLn "Maybe in an hour."
lazyCodegen : Codegen
lazyCodegen = MkCG compile execute
lazyCodegen = MkCG compile execute Nothing Nothing
main : IO ()
main = mainWithCodegens [("lazy", lazyCodegen)]