mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-12-25 22:06:33 +03:00
Some FFI documentation
Explaining how to write the most basic Idris bindings for readline, taking account of how to allocate Strings in the completion callback. Also adds the basic API as a sample, which can be used as a starting point for other packages containing C bindings.
This commit is contained in:
parent
10c70711f4
commit
1616879c3e
@ -138,6 +138,8 @@ use that instead:
|
||||
%foreign (libsmall "addWithMessage")
|
||||
prim_addWithMessage : String -> Int -> Int -> PrimIO Int
|
||||
|
||||
.. _sect-ffi-string:
|
||||
|
||||
Primitive FFI Types
|
||||
-------------------
|
||||
|
||||
@ -197,6 +199,8 @@ For an example, see the sample :ref:`sect-readline` bindings.
|
||||
Additionally, foreign functions can take *callbacks*, and take and return
|
||||
C ``struct`` pointers.
|
||||
|
||||
.. _sect-callbacks:
|
||||
|
||||
Callbacks
|
||||
---------
|
||||
|
||||
|
@ -4,5 +4,293 @@
|
||||
Example: Minimal Readline Bindings
|
||||
**********************************
|
||||
|
||||
[TODO]
|
||||
In this section, we'll see how to create bindings for a C library (the `GNU
|
||||
Readline <https://tiswww.case.edu/php/chet/readline/rltop.html>`_ library) in
|
||||
Idris, and make them available in a package. We'll only create the most minimal
|
||||
bindings, but nevertheless they demonstrate some of the trickier problems in
|
||||
creating bindings to a C library, in that they need to handle memory allocation
|
||||
of ``String``.
|
||||
|
||||
You can find the example in full in the Idris 2 source repository,
|
||||
in `samples/FFI-readline
|
||||
<https://github.com/edwinb/Idris2/tree/master/samples/FFI-readline>`_. As a
|
||||
minimal example, this can be used as a starting point for other C library
|
||||
bindings.
|
||||
|
||||
We are going to provide bindings to the following functions in the Readline
|
||||
API, available via ``#include <readline/readline.h>``:
|
||||
|
||||
::
|
||||
|
||||
char* readline (const char *prompt);
|
||||
void add_history(const char *string);
|
||||
|
||||
Additionally, we are going to support tab completion, which in the Readline
|
||||
API is achieved by setting a global variable to a callback function
|
||||
(see Section :ref:`sect-callbacks`) which explains how to handle the
|
||||
completion:
|
||||
|
||||
::
|
||||
|
||||
typedef char *rl_compentry_func_t (const char *, int);
|
||||
|
||||
rl_compentry_func_t * rl_completion_entry_function;
|
||||
|
||||
A completion function takes a ``String``, which is the text to complete, and
|
||||
an ``Int``, which is the number of times it has asked for a completion so far.
|
||||
In Idris, this could be a function ``complete : String -> Int -> IO String``.
|
||||
So, for example, if the text so far is ``"id"``, and the possible completions
|
||||
are ``idiomatic`` and ``idris``, then ``complete "id" 0`` would produce the
|
||||
string ``"idiomatic"`` and ``complete "id" 1`` would produce ``"idris"``.
|
||||
|
||||
We will define *glue* functions in a C file ``idris_readline.c``, which compiles
|
||||
to a shared object ``libidrisreadline``, so we write a function for locating
|
||||
the C functions:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
rlib : String -> String
|
||||
rlib fn = "C:" ++ fn ++ ",libidrisreadline"
|
||||
|
||||
Each of the foreign bindings will have a ``%foreign`` specifier which locates
|
||||
functions via ``rlib``.
|
||||
|
||||
Basic behaviour: Reading input, and history
|
||||
-------------------------------------------
|
||||
|
||||
We can start by writing a binding for ``readline`` directly. It's interactive,
|
||||
so needs to return a ``PrimIO``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
%foreign (rlib "readline")
|
||||
prim_readline : String -> PrimIO String
|
||||
|
||||
Then, we can write an ``IO`` wrapper:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
readline : String -> IO String
|
||||
readline prompt = primIO $ readline prompt
|
||||
|
||||
Unfortunately, this isn't quite good enough! The C ``readline`` function
|
||||
returns a ``NULL`` string if there is no input due to encountering an
|
||||
end of file. So, we need to handle that - if we don't, we'll get a crash
|
||||
on encountering end of file (remember: it's the Idris programmer's responsibility
|
||||
to give an appropriate type to the C binding!)
|
||||
|
||||
Instead, we need to use a ``Ptr`` to say that it might be a ``NULL``
|
||||
pointer (see Section :ref:`sect-ffi-string`):
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
%foreign (rlib "readline")
|
||||
prim_readline : String -> PrimIO (Ptr String)
|
||||
|
||||
We also need to provide a way to check whether the returned ``Ptr String`` is
|
||||
``NULL``. To do so, we'll write some glue code to convert back and forth
|
||||
between ``Ptr String`` and ``String, in a file ``idris_readline.c`` and a
|
||||
corresponding header ``idris_readline.h``. In ``idris_readline.h`` we have:
|
||||
|
||||
::
|
||||
|
||||
int isNullString(void* str); // return 0 if a string in NULL, non zero otherwise
|
||||
char* getString(void* str); // turn a non-NULL Ptr String into a String (assuming not NULL)
|
||||
void* mkString(char* str); // turn a String into a Ptr String
|
||||
void* nullString(); // create a new NULL String
|
||||
|
||||
Correspondingly, in ``idris_readline.c``:
|
||||
|
||||
::
|
||||
|
||||
int isNullString(void* str) {
|
||||
return str == NULL;
|
||||
}
|
||||
|
||||
char* getString(void* str) {
|
||||
return (char*)str;
|
||||
}
|
||||
|
||||
void* mkString(char* str) {
|
||||
return (void*)str;
|
||||
}
|
||||
|
||||
void* nullString() {
|
||||
return NULL;
|
||||
}
|
||||
|
||||
Now, we can use ``prim_readline`` as follows, with a safe API:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
export
|
||||
readline : String -> IO (Maybe String)
|
||||
readline s
|
||||
= do mstr <- primIO $ prim_readline s
|
||||
if isNullString mstr
|
||||
then pure $ Nothing
|
||||
else pure $ Just (getString mstr)
|
||||
|
||||
We'll need ``nullString`` and ``mkString`` later, for dealing with completions.
|
||||
|
||||
Once we've read a string, we'll want to add it to the input history. We can
|
||||
provide a binding to ``add_history`` as follows:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
%foreign (rlib "add_history")
|
||||
prim_add_history : String -> PrimIO ()
|
||||
|
||||
export
|
||||
addHistory : String -> IO ()
|
||||
addHistory s = primIO $ prim_add_history s
|
||||
|
||||
In this case, since Idris is in control of the ``String``, we know it's not
|
||||
going to be ``NULL``, so we can add it directly.
|
||||
|
||||
A small ``readline`` program that reads input, and echoes it, recording input
|
||||
history for non-empty inputs, can be written as follows:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
echoLoop : IO ()
|
||||
echoLoop
|
||||
= do Just x <- readline "> "
|
||||
| Nothing => putStrLn "EOF"
|
||||
putStrLn ("Read: " ++ x)
|
||||
when (x /= "") $ addHistory x
|
||||
if x /= "quit"
|
||||
then echoLoop
|
||||
else putStrLn "Done"
|
||||
|
||||
This gives us command history, and command line editing, but Readline becomes
|
||||
much more useful when we add tab completion. The default tab completion, which
|
||||
is available even in the small example above, is to tab complete file names
|
||||
in the current working directory. But for any realistic application, we probably
|
||||
want to tab complete other commands, such as function names, references to
|
||||
local data, or anything that is appropriate for the application.
|
||||
|
||||
Completions
|
||||
-----------
|
||||
|
||||
Readline has a large API, with several ways of supporting tab completion,
|
||||
typically involving setting a global variable to an appropriate completion
|
||||
function. We'll use the following:
|
||||
|
||||
::
|
||||
|
||||
typedef char *rl_compentry_func_t (const char *, int);
|
||||
rl_compentry_func_t * rl_completion_entry_function;
|
||||
|
||||
The completion function takes the prefix of the completion, and the number
|
||||
of times it has been called so far on this prefix, and returns the next
|
||||
completion, or ``NULL`` if there are no more completions. An Idris equivalent
|
||||
would therefore have the following type:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
setCompletionFn : (String -> Int -> IO (Maybe String)) -> IO ()
|
||||
|
||||
The function returns ``Nothing`` if there are no more completions, or
|
||||
``Just str`` for some ``str`` if there is another one for the current
|
||||
input.
|
||||
|
||||
We might hope that it's as simple as defining a function to assign the
|
||||
completion function...
|
||||
|
||||
::
|
||||
|
||||
void idrisrl_setCompletion(rl_compentry_func_t* fn) {
|
||||
rl_completion_entry_function = fn;
|
||||
}
|
||||
|
||||
...then defining the Idris binding, which needs to take into account that
|
||||
the Readline library expects ``NULL`` when there are no more completions:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
%foreign (rlib "idrisrl_setCompletion")
|
||||
prim_setCompletion : (String -> Int -> PrimIO (Ptr String)) -> PrimIO ()
|
||||
|
||||
export
|
||||
setCompletionFn : (String -> Int -> IO (Maybe String)) -> IO ()
|
||||
setCompletionFn fn
|
||||
= primIO $ prim_setCompletion $ \s, i => toPrim $
|
||||
do mstr <- fn s i
|
||||
case mstr of
|
||||
Nothing => pure nullString // need to return a Ptr String to readline!
|
||||
Just str => pure (mkString str)
|
||||
|
||||
So, we turn ``Nothing`` into ``nullString`` and ``Just str`` into ``mkString
|
||||
str``. Unfortunately, this doesn't quite work. Let's try it for the most basic
|
||||
completion function that returns one completion no matter what the input:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
testComplete : String -> Int -> IO (Maybe String)
|
||||
testComplete text 0 = pure $ Just "hamster"
|
||||
testComplete text st = pure Nothing
|
||||
|
||||
We'll try this in a small modification of ``echoLoop`` above, setting a
|
||||
completion function first:
|
||||
|
||||
.. code-block :: idris
|
||||
|
||||
main : IO ()
|
||||
main = do setCompletionFn testComplete
|
||||
echoLoop
|
||||
|
||||
Unfortunately, when we try running it, and hitting TAB before entering
|
||||
anything, things go wrong:
|
||||
|
||||
::
|
||||
|
||||
Main> :exec main
|
||||
> free(): invalid pointer
|
||||
|
||||
This problem arises because we haven't thought carefully enough about which
|
||||
parts of our program are responsible for allocating and freeing strings.
|
||||
When Idris calls a foreign function that returns a string, it copies the
|
||||
string to the Idris heap and frees it immediately. But, if the foreign
|
||||
library also frees the string, it ends up being freed twice. This is what's
|
||||
happening here: the callback passed to ``prim_setCompletion`` frees the string
|
||||
and puts it onto the Idris heap, but Readline also frees the string returned
|
||||
by ``prim_setCompletion`` once it has processed it. We can solve this
|
||||
problem by writing a wrapper for the completion function which reallocates
|
||||
the string, and using that in ``idrisrl_setCompletion`` instead.
|
||||
|
||||
::
|
||||
|
||||
rl_compentry_func_t* my_compentry;
|
||||
|
||||
char* compentry_wrapper(const char* text, int i) {
|
||||
char* res = my_compentry(text, i); // my_compentry is an Idris function, so res is on the Idris heap,
|
||||
// and freed on return
|
||||
if (res != NULL) {
|
||||
char* comp = malloc(strlen(res)+1); // comp is passed back to readline, which frees it when
|
||||
// it is finished with it
|
||||
strcpy(comp, res);
|
||||
return comp;
|
||||
}
|
||||
else {
|
||||
return NULL;
|
||||
}
|
||||
}
|
||||
|
||||
void idrisrl_setCompletion(rl_compentry_func_t* fn) {
|
||||
rl_completion_entry_function = compentry_wrapper;
|
||||
my_compentry = fn; // fn is an Idris function, called by compentry_wrapper
|
||||
}
|
||||
|
||||
So, we define the completion function in C, which calls the Idris completion
|
||||
function then makes sure the string returned by the Idris function is copied
|
||||
to the C heap.
|
||||
|
||||
We now have a primitive API that covers the most fundamental features of the
|
||||
readline API:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
readline : String -> IO (Maybe String)
|
||||
addHistory : String -> IO ()
|
||||
setCompletionFn : (String -> Int -> IO (Maybe String)) -> IO ()
|
||||
|
19
samples/FFI-readline/Test/ReadTab.idr
Normal file
19
samples/FFI-readline/Test/ReadTab.idr
Normal file
@ -0,0 +1,19 @@
|
||||
import Text.Readline
|
||||
|
||||
testComplete : String -> Int -> IO (Maybe String)
|
||||
testComplete text 0 = pure $ Just "hamster"
|
||||
testComplete text 1 = pure $ Just "bar"
|
||||
testComplete text st = pure Nothing
|
||||
|
||||
loop : IO ()
|
||||
loop = do Just x <- readline "> "
|
||||
| Nothing => putStrLn "EOF"
|
||||
putStrLn x
|
||||
when (x /= "") $ addHistory x
|
||||
if x /= "quit"
|
||||
then loop
|
||||
else putStrLn "Done"
|
||||
|
||||
main : IO ()
|
||||
main = do setCompletionFn testComplete
|
||||
loop
|
3
samples/FFI-readline/Test/test.ipkg
Normal file
3
samples/FFI-readline/Test/test.ipkg
Normal file
@ -0,0 +1,3 @@
|
||||
package test
|
||||
|
||||
opts = "-p readline"
|
10
samples/FFI-readline/readline.ipkg
Normal file
10
samples/FFI-readline/readline.ipkg
Normal file
@ -0,0 +1,10 @@
|
||||
package readline
|
||||
|
||||
sourcedir = "src"
|
||||
|
||||
modules = Text.Readline
|
||||
|
||||
prebuild = "make -C readline_glue"
|
||||
postinstall = "make -C readline_glue install"
|
||||
postclean = "make -C readline_glue clean"
|
||||
|
44
samples/FFI-readline/readline_glue/Makefile
Normal file
44
samples/FFI-readline/readline_glue/Makefile
Normal file
@ -0,0 +1,44 @@
|
||||
IDRIS := idris2
|
||||
MACHINE := $(shell $(CC) -dumpmachine)
|
||||
|
||||
ifneq (, $(findstring darwin, $(MACHINE)))
|
||||
OS :=darwin
|
||||
else ifneq (, $(findstring cygwin, $(MACHINE)))
|
||||
OS :=windows
|
||||
else ifneq (, $(findstring mingw, $(MACHINE)))
|
||||
OS :=windows
|
||||
else ifneq (, $(findstring windows, $(MACHINE)))
|
||||
OS :=windows
|
||||
else
|
||||
OS :=unix
|
||||
endif
|
||||
|
||||
ifeq ($(OS), darwin)
|
||||
SHLIB_SUFFIX :=dylib
|
||||
else ifeq ($(OS), windows)
|
||||
SHLIB_SUFFIX :=dll
|
||||
else
|
||||
SHLIB_SUFFIX :=so
|
||||
endif
|
||||
|
||||
LIBTARGET = libidrisreadline.$(SHLIB_SUFFIX)
|
||||
INSTALLDIR = `${IDRIS} --libdir`/readline/lib
|
||||
|
||||
HDRS = idris_readline.h
|
||||
OBJS = idris_readline.o
|
||||
|
||||
READLINE_LIBS := -lreadline
|
||||
READLINE_FLAGS := -fPIC
|
||||
|
||||
CFLAGS = $(READLINE_FLAGS)
|
||||
|
||||
$(LIBTARGET): $(OBJS)
|
||||
$(CC) -o $(LIBTARGET) -shared $(OBJS) $(READLINE_LIBS) $(READLINE_FLAGS)
|
||||
|
||||
install:
|
||||
@if ! [ -d $(INSTALLDIR) ]; then mkdir -p $(INSTALLDIR); fi
|
||||
install $(LIBTARGET) $(HDRS) $(INSTALLDIR)
|
||||
clean:
|
||||
rm $(OBJS) $(LIBTARGET)
|
||||
|
||||
.PHONY: install clean
|
37
samples/FFI-readline/readline_glue/idris_readline.c
Normal file
37
samples/FFI-readline/readline_glue/idris_readline.c
Normal file
@ -0,0 +1,37 @@
|
||||
#include <readline/readline.h>
|
||||
#include <stdlib.h>
|
||||
|
||||
rl_compentry_func_t* my_compentry;
|
||||
|
||||
char* compentry_wrapper(const char* text, int i) {
|
||||
char* res = my_compentry(text, i); // Idris frees this
|
||||
if (res != NULL) {
|
||||
char* comp = malloc(strlen(res)+1); // Readline frees this
|
||||
strcpy(comp, res);
|
||||
return comp;
|
||||
}
|
||||
else {
|
||||
return NULL;
|
||||
}
|
||||
}
|
||||
|
||||
void idrisrl_setCompletion(rl_compentry_func_t* fn) {
|
||||
rl_completion_entry_function = compentry_wrapper;
|
||||
my_compentry = fn;
|
||||
}
|
||||
|
||||
char* getString(void* str) {
|
||||
return (char*)str;
|
||||
}
|
||||
|
||||
void* mkString(char* str) {
|
||||
return (void*)str;
|
||||
}
|
||||
|
||||
void* nullString() {
|
||||
return NULL;
|
||||
}
|
||||
|
||||
int isNullString(void* str) {
|
||||
return str == NULL;
|
||||
}
|
11
samples/FFI-readline/readline_glue/idris_readline.h
Normal file
11
samples/FFI-readline/readline_glue/idris_readline.h
Normal file
@ -0,0 +1,11 @@
|
||||
#ifndef _IDRIS_READLINE_H
|
||||
#define _IDRIS_READLINE_H
|
||||
|
||||
void idrisrl_setCompletion(rl_completion_func_t* fn);
|
||||
|
||||
char* getString(void* str);
|
||||
void* mkString(char* str);
|
||||
void* nullString();
|
||||
int isNullString(void* str);
|
||||
|
||||
#endif
|
53
samples/FFI-readline/src/Text/Readline.idr
Normal file
53
samples/FFI-readline/src/Text/Readline.idr
Normal file
@ -0,0 +1,53 @@
|
||||
module Text.Readline
|
||||
|
||||
rlib : String -> String
|
||||
rlib fn = "C:" ++ fn ++ ",libidrisreadline"
|
||||
|
||||
%foreign (rlib "getString")
|
||||
export
|
||||
getString : Ptr String -> String
|
||||
|
||||
%foreign (rlib "mkString")
|
||||
export
|
||||
mkString : String -> Ptr String
|
||||
|
||||
%foreign (rlib "nullString")
|
||||
export
|
||||
nullString : Ptr String
|
||||
|
||||
%foreign (rlib "isNullString")
|
||||
prim_isNullString : Ptr String -> Int
|
||||
|
||||
export
|
||||
isNullString : Ptr String -> Bool
|
||||
isNullString str = if prim_isNullString str == 0 then False else True
|
||||
|
||||
%foreign (rlib "readline")
|
||||
prim_readline : String -> PrimIO (Ptr String)
|
||||
|
||||
export
|
||||
readline : String -> IO (Maybe String)
|
||||
readline s
|
||||
= do mstr <- primIO $ prim_readline s
|
||||
if isNullString mstr
|
||||
then pure $ Nothing
|
||||
else pure $ Just (getString mstr)
|
||||
|
||||
%foreign (rlib "add_history")
|
||||
prim_add_history : String -> PrimIO ()
|
||||
|
||||
export
|
||||
addHistory : String -> IO ()
|
||||
addHistory s = primIO $ prim_add_history s
|
||||
|
||||
%foreign (rlib "idrisrl_setCompletion")
|
||||
prim_setCompletion : (String -> Int -> PrimIO (Ptr String)) -> PrimIO ()
|
||||
|
||||
export
|
||||
setCompletionFn : (String -> Int -> IO (Maybe String)) -> IO ()
|
||||
setCompletionFn fn
|
||||
= primIO $ prim_setCompletion $ \s, i => toPrim $
|
||||
do mstr <- fn s i
|
||||
case mstr of
|
||||
Nothing => pure nullString
|
||||
Just str => pure (mkString str)
|
@ -49,6 +49,8 @@ record PkgDesc where
|
||||
postbuild : Maybe (FC, String) -- Script to run after building
|
||||
preinstall : Maybe (FC, String) -- Script to run after building, before installing
|
||||
postinstall : Maybe (FC, String) -- Script to run after installing
|
||||
preclean : Maybe (FC, String) -- Script to run before cleaning
|
||||
postclean : Maybe (FC, String) -- Script to run after cleaning
|
||||
|
||||
Show PkgDesc where
|
||||
show pkg = "Package: " ++ name pkg ++ "\n" ++
|
||||
@ -70,7 +72,9 @@ Show PkgDesc where
|
||||
maybe "" (\m => "Prebuild: " ++ snd m ++ "\n") (prebuild pkg) ++
|
||||
maybe "" (\m => "Postbuild: " ++ snd m ++ "\n") (postbuild pkg) ++
|
||||
maybe "" (\m => "Preinstall: " ++ snd m ++ "\n") (preinstall pkg) ++
|
||||
maybe "" (\m => "Postinstall: " ++ snd m ++ "\n") (postinstall pkg)
|
||||
maybe "" (\m => "Postinstall: " ++ snd m ++ "\n") (postinstall pkg) ++
|
||||
maybe "" (\m => "Preclean: " ++ snd m ++ "\n") (preclean pkg) ++
|
||||
maybe "" (\m => "Postclean: " ++ snd m ++ "\n") (postclean pkg)
|
||||
|
||||
initPkgDesc : String -> PkgDesc
|
||||
initPkgDesc pname
|
||||
@ -78,6 +82,7 @@ initPkgDesc pname
|
||||
Nothing Nothing Nothing Nothing Nothing
|
||||
[] []
|
||||
Nothing Nothing Nothing Nothing Nothing Nothing Nothing Nothing
|
||||
Nothing Nothing
|
||||
|
||||
data DescField : Type where
|
||||
PVersion : FC -> String -> DescField
|
||||
@ -99,6 +104,8 @@ data DescField : Type where
|
||||
PPostbuild : FC -> String -> DescField
|
||||
PPreinstall : FC -> String -> DescField
|
||||
PPostinstall : FC -> String -> DescField
|
||||
PPreclean : FC -> String -> DescField
|
||||
PPostclean : FC -> String -> DescField
|
||||
|
||||
field : String -> Rule DescField
|
||||
field fname
|
||||
@ -118,6 +125,8 @@ field fname
|
||||
<|> strField PPostbuild "postbuild"
|
||||
<|> strField PPreinstall "preinstall"
|
||||
<|> strField PPostinstall "postinstall"
|
||||
<|> strField PPreclean "preclean"
|
||||
<|> strField PPostclean "postclean"
|
||||
<|> do exactIdent "depends"; symbol "="
|
||||
ds <- sepBy1 (symbol ",") unqualifiedName
|
||||
pure (PDepends ds)
|
||||
@ -189,6 +198,8 @@ addField (PPrebuild fc e) pkg = pure $ record { prebuild = Just (fc, e) } pkg
|
||||
addField (PPostbuild fc e) pkg = pure $ record { postbuild = Just (fc, e) } pkg
|
||||
addField (PPreinstall fc e) pkg = pure $ record { preinstall = Just (fc, e) } pkg
|
||||
addField (PPostinstall fc e) pkg = pure $ record { postinstall = Just (fc, e) } pkg
|
||||
addField (PPreclean fc e) pkg = pure $ record { preclean = Just (fc, e) } pkg
|
||||
addField (PPostclean fc e) pkg = pure $ record { postclean = Just (fc, e) } pkg
|
||||
|
||||
addFields : {auto c : Ref Ctxt Defs} ->
|
||||
List DescField -> PkgDesc -> Core PkgDesc
|
||||
@ -343,6 +354,7 @@ clean : {auto c : Ref Ctxt Defs} ->
|
||||
clean pkg
|
||||
= do defs <- get Ctxt
|
||||
let build = build_dir (dirs (options defs))
|
||||
runScript (preclean pkg)
|
||||
let toClean = mapMaybe (\ks => [| MkPair (tail' ks) (head' ks) |]) $
|
||||
maybe (map fst (modules pkg))
|
||||
(\m => fst m :: map fst (modules pkg))
|
||||
@ -360,6 +372,7 @@ clean pkg
|
||||
(\ks => map concat . traverse (deleteBin builddir ks))
|
||||
pkgTrie
|
||||
deleteFolder builddir []
|
||||
runScript (postclean pkg)
|
||||
where
|
||||
delete : String -> Core ()
|
||||
delete path = do True <- coreLift $ fRemove path
|
||||
|
Loading…
Reference in New Issue
Block a user