Add installation instructions

[joelberkeley]

trafficstars

Can we have installation instructions in the root README?

I'm not sure if this is the same problem or I need a separate issue, but make build gives

Error: While processing right hand side of cloneDep. Sorry, I can't find any elaboration which works. All errors:
If Prelude.::: When unifying:
    List ?a
and:
    String
Mismatch between: List ?a and String.

build:32:27--32:28
 28 | 
 29 | cloneDep : String -> String -> IO ()
 30 | cloneDep pkg url =
 31 |     unless !(exists $ "build" </> pkg)
 32 |         $ ignore $ system ["git", "clone", url, "build" </> pkg]
                                ^

If Prelude.Stream.::: When unifying:
    Stream ?a
and:
    String
Mismatch between: Stream ?a and String.

build:32:27--32:28
 28 | 
 29 | cloneDep : String -> String -> IO ()
 30 | cloneDep pkg url =
 31 |     unless !(exists $ "build" </> pkg)
 32 |         $ ignore $ system ["git", "clone", url, "build" </> pkg]
                                ^

Error: While processing right hand side of fetchDep. Sorry, I can't find any elaboration which works. All errors:
If Prelude.::: When unifying:
    List ?a
and:
    String
Mismatch between: List ?a and String.

build:39:31--39:32
 35 | fetchDep (pkg, url, commit) = do
 36 |     cloneDep pkg url
 37 |     whenJust commit
 38 |         $ \commit => ignore $ inDir ("build" </> pkg)
 39 |             $ ignore $ system ["git", "checkout", "--detach", commit]
                                    ^

If Prelude.Stream.::: When unifying:
    Stream ?a
and:
    String
Mismatch between: Stream ?a and String.

build:39:31--39:32
 35 | fetchDep (pkg, url, commit) = do
 36 |     cloneDep pkg url
 37 |     whenJust commit
 38 |         $ \commit => ignore $ inDir ("build" </> pkg)
 39 |             $ ignore $ system ["git", "checkout", "--detach", commit]
                                    ^

Error: While processing right hand side of buildDep. Sorry, I can't find any elaboration which works. All errors:
If Prelude.::: When unifying:
    List ?a
and:
    String
Mismatch between: List ?a and String.

build:45:16--45:17
 41 | buildDep : (String, String, Maybe String) -> IO ()
 42 | buildDep (pkg, url, _) = do
 43 |     Just 0 <- inDir ("build" </> pkg) $ do
 44 |         putStrLn "building \{pkg}"
 45 |         system ["idris2", "--build", pkg <.> "ipkg"]
                     ^

If Prelude.Stream.::: When unifying:
    Stream ?a
and:
    String
Mismatch between: Stream ?a and String.

build:45:16--45:17
 41 | buildDep : (String, String, Maybe String) -> IO ()
 42 | buildDep (pkg, url, _) = do
 43 |     Just 0 <- inDir ("build" </> pkg) $ do
 44 |         putStrLn "building \{pkg}"
 45 |         system ["idris2", "--build", pkg <.> "ipkg"]
                     ^

Warning: compiling hole Main.fetchDep
Warning: compiling hole Main.buildDep

[Z-snails]

Are you using an up to date version of idris2? That file build.idr requires the escaped form of the system function which was added to base, I think fairly recently.

[joelberkeley]

i'm using v0.5.1

[eayus]

Unfortunately to compile the current master you will need to download a newer version of the Idris2 compiler by building it from source. This is something I am in the process of rectifying on refactor