mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-11-12 21:41:32 +03:00
Adding support for Windows MingW32
This commit is contained in:
parent
50d93dcd5a
commit
fab5d73378
1
.gitattributes
vendored
Normal file
1
.gitattributes
vendored
Normal file
@ -0,0 +1 @@
|
||||
text=auto
|
1
.gitignore
vendored
1
.gitignore
vendored
@ -4,5 +4,6 @@ cabal-dev/
|
||||
*.o
|
||||
*.a
|
||||
*.swp
|
||||
*~
|
||||
test/output
|
||||
test/test???/output
|
||||
|
21
Setup.hs
21
Setup.hs
@ -1,3 +1,4 @@
|
||||
{-# LANGUAGE CPP #-}
|
||||
import Distribution.Simple
|
||||
import Distribution.Simple.InstallDirs as I
|
||||
import Distribution.Simple.LocalBuildInfo as L
|
||||
@ -13,23 +14,31 @@ import System.Process
|
||||
|
||||
make verbosity = P.runProgramInvocation verbosity . P.simpleProgramInvocation "make"
|
||||
|
||||
#ifdef mingw32_HOST_OS
|
||||
-- make on mingw32 exepects unix style separators
|
||||
idrisCmd local = "../dist/build/idris/idris"
|
||||
#else
|
||||
idrisCmd local = ".." </> buildDir local </> "idris" </> "idris"
|
||||
#endif
|
||||
|
||||
cleanStdLib verbosity
|
||||
= make verbosity [ "-C", "lib", "clean" ]
|
||||
|
||||
installStdLib pkg local verbosity copy
|
||||
= do let dirs = L.absoluteInstallDirs pkg local copy
|
||||
let idir = datadir dirs
|
||||
let icmd = ".." </> buildDir local </> "idris" </> "idris"
|
||||
let icmd = idrisCmd local
|
||||
putStrLn $ "Installing libraries in " ++ idir
|
||||
make verbosity
|
||||
[ "-C", "lib", "install"
|
||||
, "TARGET=" ++ idir
|
||||
, "IDRIS=" ++ icmd
|
||||
]
|
||||
putStrLn $ "Installing run time system in " ++ idir ++ "/rts"
|
||||
let idirRts = idir </> "rts"
|
||||
putStrLn $ "Installing run time system in " ++ idirRts
|
||||
make verbosity
|
||||
[ "-C", "rts", "install"
|
||||
, "TARGET=" ++ idir ++ "/rts"
|
||||
, "TARGET=" ++ idirRts
|
||||
, "IDRIS=" ++ icmd
|
||||
]
|
||||
|
||||
@ -39,14 +48,14 @@ installStdLib pkg local verbosity copy
|
||||
-- the file after configure.
|
||||
|
||||
removeLibIdris local verbosity
|
||||
= do let icmd = ".." </> buildDir local </> "idris" </> "idris"
|
||||
= do let icmd = idrisCmd local
|
||||
make verbosity
|
||||
[ "-C", "rts", "clean"
|
||||
, "IDRIS=" ++ icmd
|
||||
]
|
||||
|
||||
checkStdLib local verbosity
|
||||
= do let icmd = ".." </> buildDir local </> "idris" </> "idris"
|
||||
= do let icmd = idrisCmd local
|
||||
putStrLn $ "Building libraries..."
|
||||
make verbosity
|
||||
[ "-C", "lib", "check"
|
||||
@ -73,5 +82,3 @@ main = defaultMainWithHooks $ simpleUserHooks
|
||||
, postBuild = \ _ flags _ lbi -> do
|
||||
checkStdLib lbi (S.fromFlag $ S.buildVerbosity flags)
|
||||
}
|
||||
|
||||
|
||||
|
@ -89,7 +89,7 @@ Executable idris
|
||||
Paths_idris
|
||||
|
||||
Build-depends: base>=4 && <5, parsec, mtl, Cabal,
|
||||
haskeline>=0.7,
|
||||
haskeline>=0.7, split,
|
||||
containers, process, transformers, filepath,
|
||||
directory, binary, bytestring, pretty
|
||||
|
||||
|
@ -14,6 +14,7 @@ import System.Process
|
||||
import System.Exit
|
||||
import System.IO
|
||||
import System.Directory
|
||||
import System.FilePath ((</>), (<.>))
|
||||
import Control.Monad
|
||||
|
||||
codegenC :: [(Name, SDecl)] ->
|
||||
@ -30,7 +31,7 @@ codegenC defs out exec incs objs libs dbg
|
||||
let h = concatMap toDecl (map fst bc)
|
||||
let cc = concatMap (uncurry toC) bc
|
||||
d <- getDataDir
|
||||
mprog <- readFile (d ++ "/rts/idris_main.c")
|
||||
mprog <- readFile (d </> "rts" </> "idris_main" <.> "c")
|
||||
let cout = headers incs ++ debug dbg ++ h ++ cc ++
|
||||
(if (exec == Executable) then mprog else "")
|
||||
case exec of
|
||||
|
@ -23,6 +23,7 @@ import System.Process
|
||||
import System.IO
|
||||
import System.Directory
|
||||
import System.Environment
|
||||
import System.FilePath ((</>), addTrailingPathSeparator)
|
||||
|
||||
import Paths_idris
|
||||
|
||||
@ -72,7 +73,7 @@ compile target f tm
|
||||
case idris_metavars i \\ primDefs of
|
||||
[] -> return ()
|
||||
ms -> fail $ "There are undefined metavariables: " ++ show ms
|
||||
inDir d h = do let f = d ++ "/" ++ h
|
||||
inDir d h = do let f = d </> h
|
||||
ex <- doesFileExist f
|
||||
if ex then return f else return h
|
||||
mkObj f = f ++ " "
|
||||
|
@ -29,9 +29,9 @@ ibcPath :: FilePath -> Bool -> FilePath -> FilePath
|
||||
ibcPath ibcsd use_ibcsd fp = let (d_fp, n_fp) = splitFileName fp
|
||||
d = if (not use_ibcsd) || ibcsd == ""
|
||||
then d_fp
|
||||
else d_fp ++ ibcsd ++ "/"
|
||||
else d_fp </> ibcsd
|
||||
n = dropExtension n_fp
|
||||
in d ++ n ++ ".ibc"
|
||||
in d </> n <.> "ibc"
|
||||
|
||||
ibcPathWithFallback :: FilePath -> FilePath -> IO FilePath
|
||||
ibcPathWithFallback ibcsd fp = do let ibcp = ibcPath ibcsd True fp
|
||||
@ -45,7 +45,7 @@ ibcPathNoFallback ibcsd fp = ibcPath ibcsd True fp
|
||||
|
||||
findImport :: [FilePath] -> FilePath -> FilePath -> IO IFileType
|
||||
findImport [] ibcsd fp = fail $ "Can't find import " ++ fp
|
||||
findImport (d:ds) ibcsd fp = do let fp_full = d ++ "/" ++ fp
|
||||
findImport (d:ds) ibcsd fp = do let fp_full = d </> fp
|
||||
ibcp <- ibcPathWithFallback ibcsd fp_full
|
||||
let idrp = srcPath fp_full
|
||||
let lidrp = lsrcPath fp_full
|
||||
@ -68,7 +68,7 @@ findImport (d:ds) ibcsd fp = do let fp_full = d ++ "/" ++ fp
|
||||
|
||||
findInPath :: [FilePath] -> FilePath -> IO FilePath
|
||||
findInPath [] fp = fail $ "Can't find file " ++ fp
|
||||
findInPath (d:ds) fp = do let p = d ++ "/" ++ fp
|
||||
findInPath (d:ds) fp = do let p = d </> fp
|
||||
e <- doesFileExist p
|
||||
if e then return p else findInPath ds p
|
||||
|
||||
|
@ -25,6 +25,7 @@ import Text.Parsec.String
|
||||
import qualified Text.Parsec.Token as PTok
|
||||
|
||||
import Data.List
|
||||
import Data.List.Split(splitOn)
|
||||
import Control.Monad.State
|
||||
import Debug.Trace
|
||||
import Data.Maybe
|
||||
@ -255,16 +256,13 @@ notEndBlock = do ist <- getState
|
||||
pfc :: IParser FC
|
||||
pfc = do s <- getPosition
|
||||
let (dir, file) = splitFileName (sourceName s)
|
||||
let f = case dir of
|
||||
"./" -> file
|
||||
_ -> sourceName s
|
||||
let f = if dir == addTrailingPathSeparator "." then file else sourceName s
|
||||
return $ FC f (sourceLine s)
|
||||
|
||||
pImport :: IParser String
|
||||
pImport = do reserved "import"; f <- identifier; option ';' (lchar ';')
|
||||
return (map dot f)
|
||||
where dot '.' = '/'
|
||||
dot c = c
|
||||
return (toPath f)
|
||||
where toPath n = foldl1 (</>) $ splitOn "." n
|
||||
|
||||
-- a program is a list of declarations, possibly with associated
|
||||
-- documentation strings
|
||||
|
@ -548,7 +548,7 @@ idrisMain opts =
|
||||
|
||||
addPkgDir :: String -> Idris ()
|
||||
addPkgDir p = do ddir <- liftIO $ getDataDir
|
||||
addImportDir (ddir ++ "/" ++ p)
|
||||
addImportDir (ddir </> p)
|
||||
|
||||
getFile :: Opt -> Maybe String
|
||||
getFile (Filename str) = Just str
|
||||
|
@ -1,5 +1,7 @@
|
||||
module Idris.REPLParser(parseCmd) where
|
||||
|
||||
import System.FilePath ((</>))
|
||||
|
||||
import Idris.Parser
|
||||
import Idris.AbsSyntax
|
||||
import Core.TT
|
||||
@ -11,6 +13,7 @@ import qualified Text.ParserCombinators.Parsec.Token as PTok
|
||||
|
||||
import Debug.Trace
|
||||
import Data.List
|
||||
import Data.List.Split(splitOn)
|
||||
|
||||
parseCmd i = runParser pCmd i "(input)"
|
||||
|
||||
@ -24,7 +27,7 @@ pCmd = try (do cmd ["q", "quit"]; eof; return Quit)
|
||||
<|> try (do cmd ["h", "?", "help"]; eof; return Help)
|
||||
<|> try (do cmd ["r", "reload"]; eof; return Reload)
|
||||
<|> try (do cmd ["m", "module"]; f <- identifier; eof;
|
||||
return (ModImport (map dot f)))
|
||||
return (ModImport (toPath f)))
|
||||
<|> try (do cmd ["e", "edit"]; eof; return Edit)
|
||||
<|> try (do cmd ["exec", "execute"]; eof; return Execute)
|
||||
<|> try (do cmd ["ttshell"]; eof; return TTShell)
|
||||
@ -59,8 +62,7 @@ pCmd = try (do cmd ["q", "quit"]; eof; return Quit)
|
||||
<|> do t <- pFullExpr defaultSyntax; return (Eval t)
|
||||
<|> do eof; return NOP
|
||||
|
||||
where dot '.' = '/'
|
||||
dot c = c
|
||||
where toPath n = foldl1 (</>) $ splitOn "." n
|
||||
|
||||
pOption :: IParser Opt
|
||||
pOption = do discard (symbol "errorcontext"); return ErrContext
|
||||
|
@ -4,6 +4,7 @@ import System.Console.Haskeline
|
||||
import System.IO
|
||||
import System.Environment
|
||||
import System.Exit
|
||||
import System.FilePath ((</>), addTrailingPathSeparator)
|
||||
|
||||
import Data.Maybe
|
||||
import Data.Version
|
||||
@ -60,15 +61,15 @@ showver = do putStrLn $ "Idris version " ++ ver
|
||||
exitWith ExitSuccess
|
||||
|
||||
showLibs = do dir <- getDataDir
|
||||
putStrLn $ "-L" ++ dir ++ "/rts -lidris_rts -lgmp -lpthread"
|
||||
putStrLn $ "-L" ++ (dir </> "rts") ++ " -lidris_rts -lgmp -lpthread"
|
||||
exitWith ExitSuccess
|
||||
|
||||
showLibdir = do dir <- getDataDir
|
||||
putStrLn $ dir ++ "/"
|
||||
putStrLn $ addTrailingPathSeparator dir
|
||||
exitWith ExitSuccess
|
||||
|
||||
showIncs = do dir <- getDataDir
|
||||
putStrLn $ "-I" ++ dir ++ "/rts"
|
||||
putStrLn $ "-I" ++ dir </> "rts"
|
||||
exitWith ExitSuccess
|
||||
|
||||
usagemsg = "Idris version " ++ ver ++ "\n" ++
|
||||
|
@ -4,11 +4,13 @@ import System.Process
|
||||
import System.Directory
|
||||
import System.Exit
|
||||
import System.IO
|
||||
import System.FilePath ((</>), addTrailingPathSeparator)
|
||||
|
||||
import Util.System
|
||||
|
||||
import Control.Monad
|
||||
import Data.List
|
||||
import Data.List.Split(splitOn)
|
||||
|
||||
import Core.TT
|
||||
import Idris.REPL
|
||||
@ -32,14 +34,14 @@ buildPkg warnonly (install, fp)
|
||||
when (and ok) $
|
||||
do make (makefile pkgdesc)
|
||||
dir <- getCurrentDirectory
|
||||
setCurrentDirectory $ dir ++ "/" ++ sourcedir pkgdesc
|
||||
setCurrentDirectory $ dir </> sourcedir pkgdesc
|
||||
case (execout pkgdesc) of
|
||||
Nothing -> buildMods (NoREPL : Verbose : idris_opts pkgdesc)
|
||||
(modules pkgdesc)
|
||||
Just o -> do let exec = dir ++ "/" ++ o
|
||||
buildMod
|
||||
Just o -> do let exec = dir </> o
|
||||
buildMods
|
||||
(NoREPL : Verbose : Output exec : idris_opts pkgdesc)
|
||||
(idris_main pkgdesc)
|
||||
[idris_main pkgdesc]
|
||||
setCurrentDirectory dir
|
||||
when install $ installPkg pkgdesc
|
||||
|
||||
@ -48,11 +50,11 @@ cleanPkg fp
|
||||
= do pkgdesc <- parseDesc fp
|
||||
clean (makefile pkgdesc)
|
||||
dir <- getCurrentDirectory
|
||||
setCurrentDirectory $ dir ++ "/" ++ sourcedir pkgdesc
|
||||
setCurrentDirectory $ dir </> sourcedir pkgdesc
|
||||
mapM_ rmIBC (modules pkgdesc)
|
||||
case execout pkgdesc of
|
||||
Nothing -> return ()
|
||||
Just s -> do let exec = dir ++ "/" ++ s
|
||||
Just s -> do let exec = dir </> s
|
||||
putStrLn $ "Removing " ++ exec
|
||||
system $ "rm -f " ++ exec
|
||||
return ()
|
||||
@ -60,25 +62,17 @@ cleanPkg fp
|
||||
installPkg :: PkgDesc -> IO ()
|
||||
installPkg pkgdesc
|
||||
= do dir <- getCurrentDirectory
|
||||
setCurrentDirectory $ dir ++ "/" ++ sourcedir pkgdesc
|
||||
setCurrentDirectory $ dir </> sourcedir pkgdesc
|
||||
case (execout pkgdesc) of
|
||||
Nothing -> mapM_ (installIBC (pkgname pkgdesc)) (modules pkgdesc)
|
||||
Just o -> return () -- do nothing, keep executable locally, for noe
|
||||
mapM_ (installObj (pkgname pkgdesc)) (objs pkgdesc)
|
||||
|
||||
buildMod :: [Opt] -> Name -> IO ()
|
||||
buildMod opts n = do let f = map slash $ show n
|
||||
idris (Filename f : opts)
|
||||
return ()
|
||||
where slash '.' = '/'
|
||||
slash x = x
|
||||
|
||||
buildMods :: [Opt] -> [Name] -> IO ()
|
||||
buildMods opts ns = do let f = map ((map slash) . show) ns
|
||||
buildMods opts ns = do let f = map (toPath . show) ns
|
||||
idris (map Filename f ++ opts)
|
||||
return ()
|
||||
where slash '.' = '/'
|
||||
slash x = x
|
||||
where toPath n = foldl1 (</>) $ splitOn "." n
|
||||
|
||||
testLib :: Bool -> String -> String -> IO Bool
|
||||
testLib warn p f
|
||||
@ -86,7 +80,8 @@ testLib warn p f
|
||||
gcc <- getCC
|
||||
(tmpf, tmph) <- tempfile
|
||||
hClose tmph
|
||||
e <- system $ gcc ++ " " ++ d ++ "/rts/libtest.c -l" ++ f ++ " -o " ++ tmpf
|
||||
let libtest = d </> "rts" </> "libtest.c"
|
||||
e <- system $ gcc ++ " " ++ libtest ++ " -l" ++ f ++ " -o " ++ tmpf
|
||||
case e of
|
||||
ExitSuccess -> return True
|
||||
_ -> do if warn
|
||||
@ -102,22 +97,22 @@ rmIBC m = do let f = toIBCFile m
|
||||
return ()
|
||||
|
||||
toIBCFile (UN n) = n ++ ".ibc"
|
||||
toIBCFile (NS n ns) = concat (intersperse "/" (reverse ns)) ++ "/" ++ toIBCFile n
|
||||
toIBCFile (NS n ns) = foldl1 (</>) (reverse (toIBCFile n : ns))
|
||||
|
||||
installIBC :: String -> Name -> IO ()
|
||||
installIBC p m = do let f = toIBCFile m
|
||||
d <- getDataDir
|
||||
let destdir = d ++ "/" ++ p ++ "/" ++ getDest m
|
||||
let destdir = d </> p </> getDest m
|
||||
putStrLn $ "Installing " ++ f ++ " to " ++ destdir
|
||||
system $ "mkdir -p " ++ destdir
|
||||
system $ "install " ++ f ++ " " ++ destdir
|
||||
return ()
|
||||
where getDest (UN n) = ""
|
||||
getDest (NS n ns) = concat (intersperse "/" (reverse ns)) ++ "/" ++ getDest n
|
||||
getDest (NS n ns) = foldl1 (</>) (reverse (getDest n : ns))
|
||||
|
||||
installObj :: String -> String -> IO ()
|
||||
installObj p o = do d <- getDataDir
|
||||
let destdir = d ++ "/" ++ p ++ "/"
|
||||
let destdir = addTrailingPathSeparator (d </> p)
|
||||
putStrLn $ "Installing " ++ o ++ " to " ++ destdir
|
||||
system $ "mkdir -p " ++ destdir
|
||||
system $ "install " ++ o ++ " " ++ destdir
|
||||
@ -133,5 +128,3 @@ clean Nothing = return ()
|
||||
clean (Just s) = do system $ "make -f " ++ s ++ " clean"
|
||||
return ()
|
||||
|
||||
|
||||
|
||||
|
@ -17,6 +17,7 @@ import System.Process
|
||||
import System.IO
|
||||
import System.Directory
|
||||
import System.Environment
|
||||
import System.FilePath ((</>))
|
||||
import Debug.Trace
|
||||
|
||||
import Paths_idris
|
||||
@ -44,7 +45,7 @@ compileC f tm
|
||||
case idris_metavars i \\ primDefs of
|
||||
[] -> return ()
|
||||
ms -> fail $ "There are undefined metavariables: " ++ show ms
|
||||
inDir d h = do let f = d ++ "/" ++ h
|
||||
inDir d h = do let f = d </> h
|
||||
ex <- doesFileExist f
|
||||
if ex then return f else return h
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user