diff --git a/Setup.hs b/Setup.hs index b9b568b849..3edfa379f8 100644 --- a/Setup.hs +++ b/Setup.hs @@ -20,158 +20,155 @@ import qualified Data.Text.IO as TIO -- After Idris is built, we need to check and install the prelude and other libs -make verbosity = P.runProgramInvocation verbosity . P.simpleProgramInvocation "make" +-- ----------------------------------------------------------------------------- +-- Idris Command Path -#ifdef mingw32_HOST_OS -- make on mingw32 exepects unix style separators +#ifdef mingw32_HOST_OS () = (Px.) -idrisCmd local = Px.joinPath $ splitDirectories $ - ".." buildDir local "idris" "idris" -rtsDir local = Px.joinPath $ splitDirectories $ - ".." buildDir local "rts" "libidris_rts" +idrisCmd local = Px.joinPath $ splitDirectories $ ".." buildDir local "idris" "idris" #else idrisCmd local = ".." buildDir local "idris" "idris" -rtsDir local = ".." buildDir local "rts" "libidris_rts" #endif -cleanStdLib verbosity - = do make verbosity [ "-C", "lib", "clean", "IDRIS=idris" ] - make verbosity [ "-C", "effects", "clean", "IDRIS=idris" ] - make verbosity [ "-C", "javascript", "clean", "IDRIS=idris" ] - -cleanJavaPom verbosity - = do execPomExists <- doesFileExist ("java" "executable_pom.xml") - when execPomExists $ removeFile ("java" "executable_pom.xml") - -cleanLLVMLib verbosity = make verbosity ["-C", "llvm", "clean"] - -installStdLib pkg local withoutEffects verbosity copy - = do let dirs = L.absoluteInstallDirs pkg local copy - let idir = datadir dirs - let icmd = idrisCmd local - putStrLn $ "Installing libraries in " ++ idir - make verbosity - [ "-C", "lib", "install" - , "TARGET=" ++ idir - , "IDRIS=" ++ icmd - ] - unless withoutEffects $ - make verbosity - [ "-C", "effects", "install" - , "TARGET=" ++ idir - , "IDRIS=" ++ icmd - ] - make verbosity - [ "-C", "javascript", "install" - , "TARGET=" ++ idir - , "IDRIS=" ++ icmd - ] - let idirRts = idir "rts" - putStrLn $ "Installing run time system in " ++ idirRts - make verbosity - [ "-C", "rts", "install" - , "TARGET=" ++ idirRts - , "IDRIS=" ++ icmd - ] - -installLLVMLib verbosity pkg local copy = - let idir = datadir $ L.absoluteInstallDirs pkg local copy in - make verbosity ["-C", "llvm", "install", "TARGET=" ++ idir "llvm"] - -buildLLVMLib verbosity = make verbosity ["-C", "llvm", "all"] - -installJavaPom pkg local verbosity copy version = do - putStrLn $ "Installing java pom template" - let dir = datadir $ L.absoluteInstallDirs pkg local copy - copyFile ("java" "executable_pom.xml") (dir "executable_pom.xml") - --- This is a hack. I don't know how to tell cabal that a data file needs --- installing but shouldn't be in the distribution. And it won't make the --- distribution if it's not there, so instead I just delete --- the file after configure. - -removeLibIdris local verbosity - = do let icmd = idrisCmd local - make verbosity - [ "-C", "rts", "clean" - , "IDRIS=" ++ icmd - ] - -checkStdLib local withoutEffects verbosity - = do let icmd = idrisCmd local - putStrLn $ "Building libraries..." - make verbosity - [ "-C", "lib", "check" - , "IDRIS=" ++ icmd - ] - unless withoutEffects $ - make verbosity - [ "-C", "effects", "check" - , "IDRIS=" ++ icmd - ] - make verbosity - [ "-C", "javascript", "check" - , "IDRIS=" ++ icmd - ] - make verbosity - [ "-C", "rts", "check" - , "IDRIS=" ++ icmd - ] - -llvmFlag flags = +-- ----------------------------------------------------------------------------- +-- Make Commands + +make verbosity = + P.runProgramInvocation verbosity . P.simpleProgramInvocation "make" + +-- ----------------------------------------------------------------------------- +-- Flags + +usesLLVM :: S.ConfigFlags -> Bool +usesLLVM flags = case lookup (FlagName "llvm") (S.configConfigurationsFlags flags) of Just True -> True Just False -> False Nothing -> True -noEffectsFlag flags = - case lookup (FlagName "noeffects") (S.configConfigurationsFlags flags) of +usesEffects :: S.ConfigFlags -> Bool +usesEffects flags = + case lookup (FlagName "effects") (S.configConfigurationsFlags flags) of Just True -> True Just False -> False - Nothing -> False - -preparePoms version - = do execPomTemplate <- TIO.readFile ("java" "executable_pom_template.xml") - TIO.writeFile ("java" "executable_pom.xml") (insertVersion execPomTemplate) - where - insertVersion template = - T.replace (T.pack "$RTS-VERSION$") (T.pack $ display version) template + Nothing -> True + +-- ----------------------------------------------------------------------------- +-- Clean + +idrisClean _ flags _ _ = do + cleanStdLib + cleanLLVM + cleanJava + where + verbosity = S.fromFlag $ S.cleanVerbosity flags + + cleanStdLib = do + makeClean "lib" + makeClean "effects" + makeClean "javascript" + + cleanJava = do + execPomExists <- doesFileExist ("java" "executable_pom.xml") + when execPomExists $ removeFile ("java" "executable_pom.xml") + + cleanLLVM = makeClean "llvm" + + makeClean dir = make verbosity [ "-C", dir, "clean", "IDRIS=idris" ] + + +-- ----------------------------------------------------------------------------- +-- Configure + +idrisConfigure _ flags _ local = do + configureRTS + configureJava + where + verbosity = S.fromFlag $ S.configVerbosity flags + version = pkgVersion . package $ localPkgDescr local + + -- This is a hack. I don't know how to tell cabal that a data file needs + -- installing but shouldn't be in the distribution. And it won't make the + -- distribution if it's not there, so instead I just delete + -- the file after configure. + configureRTS = make verbosity ["-C", "rts", "clean"] + + configureJava = do + execPomTemplate <- TIO.readFile ("java" "executable_pom_template.xml") + TIO.writeFile ("java" "executable_pom.xml") (insertVersion execPomTemplate) + where + insertVersion = T.replace (T.pack "$RTS-VERSION$") (T.pack $ display version) + +-- ----------------------------------------------------------------------------- +-- Build + +idrisBuild _ flags _ local = do + buildStdLib + buildRTS + when (usesLLVM $ configFlags local) buildLLVM + where + verbosity = S.fromFlag $ S.buildVerbosity flags + + buildStdLib = do + putStrLn "Building libraries..." + makeBuild "lib" + when (usesEffects $ configFlags local) $ makeBuild "effects" + makeBuild "javascript" + where + makeBuild dir = make verbosity [ "-C", dir, "build" , "IDRIS=" ++ idrisCmd local] + + buildRTS = make verbosity ["-C", "rts", "build"] + + buildLLVM = make verbosity ["-C", "llvm", "build"] + +-- ----------------------------------------------------------------------------- +-- Copy/Install + +idrisInstall verbosity copy pkg local = do + installStdLib + installRTS + installJava + when (usesLLVM $ configFlags local) installLLVM + where + target = datadir $ L.absoluteInstallDirs pkg local copy + + installStdLib = do + putStrLn $ "Installing libraries in " ++ target + makeInstall "lib" target + when (usesEffects $ configFlags local) $ makeInstall "effects" target + makeInstall "javascript" target + + installRTS = do + let target' = target "rts" + putStrLn $ "Installing run time system in " ++ target' + makeInstall "rts" target' + + installJava = do + putStrLn $ "Installing java pom template in " ++ target + copyFile ("java" "executable_pom.xml") (target "executable_pom.xml") + + installLLVM = do + let target' = target "llvm" + putStrLn $ "Installing LLVM library in " ++ target + makeInstall "llvm" target + + makeInstall src target = + make verbosity [ "-C", src, "install" , "TARGET=" ++ target, "IDRIS=" ++ idrisCmd local] + +-- ----------------------------------------------------------------------------- +-- Main -- Install libraries during both copy and install -- See http://hackage.haskell.org/trac/hackage/ticket/718 -main = do - defaultMainWithHooks $ simpleUserHooks - { postCopy = \ _ flags pkg lbi -> do - let verb = S.fromFlag $ S.copyVerbosity flags - let withoutEffects = noEffectsFlag $ configFlags lbi - installStdLib pkg lbi withoutEffects verb - (S.fromFlag $ S.copyDest flags) - installJavaPom pkg lbi verb - (S.fromFlag $ S.copyDest flags) - (pkgVersion . package $ localPkgDescr lbi) - when (llvmFlag $ configFlags lbi) - (installLLVMLib verb pkg lbi (S.fromFlag $ S.copyDest flags)) - , postInst = \ _ flags pkg lbi -> do - let verb = (S.fromFlag $ S.installVerbosity flags) - let withoutEffects = noEffectsFlag $ configFlags lbi - installStdLib pkg lbi withoutEffects verb - NoCopyDest - installJavaPom pkg lbi verb - NoCopyDest - (pkgVersion . package $ localPkgDescr lbi) - when (llvmFlag $ configFlags lbi) - (installLLVMLib verb pkg lbi NoCopyDest) - , postConf = \ _ flags _ lbi -> do - removeLibIdris lbi (S.fromFlag $ S.configVerbosity flags) - preparePoms . pkgVersion . package $ localPkgDescr lbi - , postClean = \ _ flags _ _ -> do - let verb = S.fromFlag $ S.cleanVerbosity flags - cleanStdLib verb - cleanLLVMLib verb - cleanJavaPom verb - , postBuild = \ _ flags _ lbi -> do - let verb = S.fromFlag $ S.buildVerbosity flags - when (llvmFlag $ configFlags lbi) (buildLLVMLib verb) - let withoutEffects = noEffectsFlag $ configFlags lbi - checkStdLib lbi withoutEffects verb - } +main = defaultMainWithHooks $ simpleUserHooks + { postClean = idrisClean + , postConf = idrisConfigure + , postBuild = idrisBuild + , postCopy = \_ flags pkg local -> + idrisInstall (S.fromFlag $ S.copyVerbosity flags) + (S.fromFlag $ S.copyDest flags) pkg local + , postInst = \_ flags pkg local -> + idrisInstall (S.fromFlag $ S.installVerbosity flags) + NoCopyDest pkg local + } diff --git a/effects/Makefile b/effects/Makefile index d398657c36..72811b3a25 100644 --- a/effects/Makefile +++ b/effects/Makefile @@ -1,13 +1,14 @@ +IDRIS := idris -check: .PHONY +build: .PHONY $(IDRIS) --build effects.ipkg -recheck: clean check +clean: .PHONY + $(IDRIS) --clean effects.ipkg install: $(IDRIS) --install effects.ipkg -clean: .PHONY - $(IDRIS) --clean effects.ipkg +rebuild: clean build .PHONY: diff --git a/idris.cabal b/idris.cabal index 211eddcd1d..e17ff8033e 100644 --- a/idris.cabal +++ b/idris.cabal @@ -14,7 +14,8 @@ Description: Idris is a general purpose language with full dependent types. Dependent types allow types to be predicated on values, meaning that some aspects of a program's behaviour can be specified precisely in the type. The language is closely - related to Epigram and Agda. There is a tutorial at . + related to Epigram and Agda. There is a tutorial at + . Features include: . * Full dependent types with dependent pattern matching @@ -43,38 +44,60 @@ Description: Idris is a general purpose language with full dependent types. Cabal-Version: >= 1.6 - Build-type: Custom - -Data-files: rts/idris_rts.h rts/idris_gc.h rts/idris_stdfgn.h - rts/idris_main.c rts/idris_gmp.h - rts/libtest.c +Data-files: js/Runtime-browser.js js/Runtime-common.js js/Runtime-node.js - js/Runtime-browser.js -Extra-source-files: lib/Makefile lib/*.idr lib/Prelude/*.idr - lib/Network/*.idr lib/Control/*.idr - lib/Control/Monad/*.idr lib/Language/*.idr - lib/Language/Reflection/*.idr - lib/System/Concurrency/*.idr - lib/Data/*.idr lib/Debug/*.idr + rts/idris_gc.h + rts/idris_gmp.h + rts/idris_main.c + rts/idris_rts.h + rts/idris_stdfgn.h + rts/libtest.c + +Extra-source-files: + Makefile + config.mk + + rts/*.c + rts/*.h + rts/Makefile + + lib/base.ipkg + lib/*.idr + lib/Control/*.idr + lib/Control/Monad/*.idr + lib/Data/*.idr lib/Data/Vect/*.idr + lib/Debug/*.idr lib/Decidable/*.idr - tutorial/examples/*.idr lib/base.ipkg - effects/Makefile effects/*.idr effects/Effect/*.idr + lib/Language/*.idr + lib/Language/Reflection/*.idr + lib/Makefile + lib/Network/*.idr + lib/Prelude/*.idr + lib/System/Concurrency/*.idr + + effects/Makefile effects/effects.ipkg - javascript/Makefile - javascript/JavaScript/*.idr + effects/Effect/*.idr + effects/*.idr + + java/*.xml + javascript/*.idr + javascript/JavaScript/*.idr + javascript/Makefile javascript/javascript.ipkg - config.mk - rts/*.c rts/*.h rts/Makefile - llvm/*.c llvm/Makefile + js/*.js - java/*.xml - Makefile + llvm/*.c + llvm/Makefile + + tutorial/examples/*.idr + test/Makefile test/runtest.pl test/reg001/run @@ -234,76 +257,140 @@ Extra-source-files: lib/Makefile lib/*.idr lib/Prelude/*.idr test/test030/*.idr test/test030/expected - source-repository head type: git location: git://github.com/edwinb/Idris-dev.git -Flag NoEffects - Description: Do not build the effects package - Default: False +Flag Effects + Description: Build the effects package + Default: True Flag LLVM Description: Build the LLVM backend Default: True manual: True -Executable idris - Main-is: Main.hs - hs-source-dirs: src - Other-modules: Core.TT, Core.Evaluate, Core.Execute, Core.Typecheck, - Core.ProofShell, Core.ProofState, Core.CoreParser, - Core.ShellParser, Core.Unify, Core.Elaborate, - Core.CaseTree, Core.Constraints, +Executable idris + Main-is: Main.hs + hs-source-dirs: src + Other-modules: + Core.CaseTree + , Core.Constraints + , Core.CoreParser + , Core.Elaborate + , Core.Evaluate + , Core.Execute + , Core.ProofShell + , Core.ProofState + , Core.ShellParser + , Core.TT + , Core.Typecheck + , Core.Unify + + , Idris.AbsSyntax + , Idris.AbsSyntaxTree + , Idris.Chaser + , Idris.Colours + , Idris.Completion + , Idris.Coverage + , Idris.DSL + , Idris.DataOpts + , Idris.Delaborate + , Idris.Docs + , Idris.ElabDecls + , Idris.ElabTerm + , Idris.Error + , Idris.Help + , Idris.IBC + , Idris.IdeSlave + , Idris.Imports + , Idris.Inliner + , Idris.Parser + , Idris.PartialEval + , Idris.Primitives + , Idris.Prover + , Idris.Providers + , Idris.REPL + , Idris.REPLParser + , Idris.Transforms + , Idris.Unlit + , Idris.UnusedArgs + + , IRTS.BCImp + , IRTS.Bytecode + , IRTS.CodegenC + , IRTS.CodegenCommon + , IRTS.CodegenJava + , IRTS.CodegenJavaScript + , IRTS.Compiler + , IRTS.Defunctionalise + , IRTS.DumpBC + , IRTS.Inliner + , IRTS.Java.ASTBuilding + , IRTS.Java.JTypes + , IRTS.Java.Mangling + , IRTS.LParser + , IRTS.Lang + , IRTS.Simplified + + , Util.Pretty + , Util.System + , Util.DynamicLinker - Idris.AbsSyntax, Idris.AbsSyntaxTree, Idris.Colours, - Idris.Parser, Idris.Help, Idris.IdeSlave, Idris.REPL, - Idris.REPLParser, Idris.ElabDecls, Idris.Error, - Idris.Delaborate, Idris.Primitives, Idris.Imports, - Idris.Prover, Idris.ElabTerm, - Idris.Coverage, Idris.IBC, Idris.Unlit, - Idris.DataOpts, Idris.Transforms, Idris.DSL, - Idris.UnusedArgs, Idris.Docs, Idris.Completion, - Idris.PartialEval, Idris.Providers, Idris.Chaser, - Idris.Inliner, + , Pkg.Package + , Pkg.PParser - Util.Pretty, Util.System, Util.DynamicLinker, - Pkg.Package, Pkg.PParser, + -- Auto Generated + Paths_idris - IRTS.Lang, IRTS.LParser, IRTS.Bytecode, IRTS.Simplified, - IRTS.CodegenC, IRTS.Defunctionalise, IRTS.Inliner, - IRTS.Compiler, IRTS.CodegenJava, IRTS.Java.ASTBuilding, - IRTS.Java.JTypes, IRTS.Java.Mangling, IRTS.BCImp, - IRTS.CodegenJavaScript, - IRTS.CodegenCommon, IRTS.DumpBC + Build-depends: base >=4 && <5 + , Cabal + , ansi-terminal + , binary + , bytestring + , containers + , directory + , directory >= 1.2 + , filepath + , haskeline >= 0.7 + , language-java >= 0.2.2 + , libffi + , mtl + , parsec >= 3 + , parsers >= 0.9 + , pretty + , process + , split + , text + , time >= 1.4 + , transformers + , trifecta >= 1.1 + , unordered-containers + , utf8-string + , vector + , vector-binary-instances - Paths_idris + Extensions: MultiParamTypeClasses + , FunctionalDependencies + , FlexibleInstances + , TemplateHaskell - Build-depends: base>=4 && <5, parsec>=3, mtl, Cabal, - haskeline>=0.7, split, directory>=1.2, - time>=1.4, - containers, process, transformers, filepath, - directory, binary, bytestring, text, pretty, - language-java>=0.2.2, libffi, - vector, vector-binary-instances, ansi-terminal, - utf8-string, unordered-containers, parsers>=0.9, trifecta>=1.1 + ghc-prof-options: -auto-all -caf-all + ghc-options: -rtsopts - Extensions: MultiParamTypeClasses, FunctionalDependencies, - FlexibleInstances, TemplateHaskell - ghc-prof-options: -auto-all -caf-all - ghc-options: -rtsopts - if os(linux) - cpp-options: -DLINUX - build-depends: unix - if os(darwin) - cpp-options: -DMACOSX - build-depends: unix - if os(windows) - cpp-options: -DWINDOWS - build-depends: Win32 - if flag(LLVM) - other-modules: IRTS.CodegenLLVM - cpp-options: -DIDRIS_LLVM - build-depends: llvm-general==3.3.8.*, llvm-general-pure==3.3.8.* - else - other-modules: Util.LLVMStubs + if os(linux) + cpp-options: -DLINUX + build-depends: unix + if os(darwin) + cpp-options: -DMACOSX + build-depends: unix + if os(windows) + cpp-options: -DWINDOWS + build-depends: Win32 + if flag(LLVM) + other-modules: IRTS.CodegenLLVM + cpp-options: -DIDRIS_LLVM + build-depends: llvm-general == 3.3.8.* + , llvm-general-pure == 3.3.8.* + else + other-modules: Util.LLVMStubs diff --git a/java/executable_pom_template.xml b/java/executable_pom_template.xml index 4edeb1d62d..5b51c88002 100644 --- a/java/executable_pom_template.xml +++ b/java/executable_pom_template.xml @@ -1,11 +1,12 @@ 4.0.0 - org.idris-lang + + $ARTIFACT-NAME$ + $ARTIFACT-NAME$ - jar + org.idris-lang 1.0 - $ARTIFACT-NAME$ UTF-8 @@ -14,13 +15,12 @@ org.idris-lang - idris - 0.9.10-alpha-1 + idris + $RTS-VERSION$ $DEPENDENCIES$ - $ARTIFACT-NAME$ diff --git a/javascript/Makefile b/javascript/Makefile index 336661e561..193e1f23f9 100644 --- a/javascript/Makefile +++ b/javascript/Makefile @@ -1,13 +1,14 @@ +IDRIS := idris -check: .PHONY +build: .PHONY $(IDRIS) --build javascript.ipkg -recheck: clean check - install: $(IDRIS) --install javascript.ipkg clean: .PHONY $(IDRIS) --clean javascript.ipkg +rebuild: clean build + .PHONY: diff --git a/lib/Makefile b/lib/Makefile index f512a71cf2..3e1bd4f0cf 100644 --- a/lib/Makefile +++ b/lib/Makefile @@ -1,16 +1,17 @@ +IDRIS := idris -check: .PHONY +build: .PHONY $(IDRIS) --build base.ipkg -recheck: clean check - install: $(IDRIS) --install base.ipkg clean: .PHONY $(IDRIS) --clean base.ipkg +rebuild: clean build + linecount: .PHONY - wc -l *.idr Network/*.idr Language/*.idr Prelude/*.idr Data/*.idr Control/Monad/*.idr Control/*.idr + find . -name '*.idr' | xargs wc -l .PHONY: diff --git a/llvm/Makefile b/llvm/Makefile index b0e40efb53..21be2a34e4 100644 --- a/llvm/Makefile +++ b/llvm/Makefile @@ -5,7 +5,7 @@ SOURCES=defs.c OBJECTS=$(SOURCES:.c=.o) LIB=libidris_rts.a -all: $(SOURCES) $(LIB) +build: $(SOURCES) $(LIB) $(LIB): $(OBJECTS) ar r $@ $(OBJECTS) diff --git a/rts/Makefile b/rts/Makefile index caca2ff6bd..4c52fe06bb 100644 --- a/rts/Makefile +++ b/rts/Makefile @@ -9,7 +9,7 @@ endif LIBTARGET = libidris_rts.a -check : $(LIBTARGET) $(DYLIBTARGET) +build: $(LIBTARGET) $(DYLIBTARGET) $(LIBTARGET) : $(OBJS) ar r $(LIBTARGET) $(OBJS)