haskell: simpler build setup, so we can use cabal sandboxes

haskell/.gitignore

+# generated doc files
+
+doc/refman.pdf
+doc/version.txt
+
+doc/figures/clientkernel.pdf
+doc/figures/clientserver.pdf
+doc/figures/derive.pdf
+doc/figures/ipctransfer.pdf
+doc/figures/truncation.pdf
+
+# generated build files
+
+**.lhs-boot
+dist
+
+# cabal dependencies 
+
+.cabal-sandbox/
+cabal.sandbox.config

haskell/build → haskell/Makefile

-#!/bin/bash
-#
 #
 # Copyright 2014, General Dynamics C4 Systems
 #
@@ -10,11 +8,26 @@
 # @TAG(GD_GPL)
 #
 
-#
-# If this script doesn't work, you may need to add --user or --global
-# to the "runhaskell Setup.hs configure" command below.
-# It depends on where cabal has installed your packages, whether that
-# was globally or just in your user home directory.
-#
-runhaskell Setup.hs configure --with-target=arm-qemu && \
-  runhaskell Setup.hs build
+
+BOOT_MODULES = Kernel/CSpace Kernel/Thread Kernel/FaultHandler \
+    Kernel/VSpace Kernel/Init Model/PSpace Object/TCB Object/CNode \
+    Object/ObjectType
+
+BOOT_FILES=$(BOOT_MODULES:%=src/SEL4/%.lhs-boot)
+
+all: build pdf
+	
+build: $(BOOT_FILES)
+	cabal sandbox init
+	cabal configure
+	cabal build
+
+pdf:
+	cd doc && make
+
+%.lhs-boot: %.lhs
+	perl mkhsboot.pl -l < $< > $@
+
+clean:
+	rm -f $(BOOT_FILES)
+	cabal clean

haskell/README.md

@@ -17,29 +17,17 @@ stand-alone; it must be integrated into a simulator that can run user-level
 binaries and generate events that the kernel model can process.
 
 To build it:
-  - install `GHC 7.8` or later
-  - install `Cabal 1.18` or later. This is included with GHC 7.8. 
-  - configure the sources:
-  
-        runhaskell Setup.hs configure --with-target=arm-qemu
-
-Further target options may be supported again in the future.
-
-  - build the library:
-  
-        runhaskell Setup.hs build
-
-  - install:
-  
-        runhaskell Setup.hs install --user
+  - install `GHC 7.8.x`
+  - install `Cabal 1.20.x`. This is usually included with GHC 7.8. 
+  - run `make`
 
 
 After that, you can compile Haskell programs using the simulator by adding
-`-package SEL4` to the `ghc` command line. Note that the qemu target requires
-some callback functions to be accessible via the FFI, so it is not possible to
-load a model compiled for those targets in GHCi.
+`-package SEL4-ARM` to the `ghc` command line. Note that the qemu target
+requires some callback functions to be accessible via the FFI, so it is not
+possible to load a model compiled for those targets in GHCi.
 
 Currently, the simulator interface is out of date, so this model is currently
 only useful as documentation and as intermediate artefact in the seL4
 correctness proof. The model itself is kept up to date with the C code, only
-the simulator interface is outdated.
\ No newline at end of file
+the simulator interface is outdated.

haskell/SEL4.cabal → haskell/SEL4-ARM.cabal

@@ -8,11 +8,11 @@
 -- @TAG(GD_GPL)
 --
 
-name:                   SEL4
+name:                   SEL4-ARM
 version:                1.4-pre
-cabal-version:          >= 1.18
+cabal-version:          >= 1.20
 build-type:             Simple
-license:                AllRightsReserved
+license:                GPL
 author:                 Philip Derrin et. al., NICTA
 synopsis:               Executable specification for the seL4 Kernel
 tested-with:            GHC == 7.8.3
@@ -71,7 +71,21 @@ Library
                             Data.BinaryTree
                             Data.Helpers
 
-    $TARGET-SPECIFIC-STUFF  -- will be inserted by the Setup.hs script
+                            SEL4.Machine.Hardware.ARM.QEmu
+
+                            SEL4.API.Types.ARM
+                            SEL4.API.Invocation.ARM
+                            SEL4.Kernel.VSpace.ARM
+                            SEL4.Kernel.Thread.ARM
+                            SEL4.Object.ObjectType.ARM
+                            SEL4.Object.Structures.ARM
+                            SEL4.Object.Interrupt.ARM
+                            SEL4.Object.Instances.ARM
+                            SEL4.Object.TCB.ARM
+                            SEL4.Model.StateData.ARM
+                            SEL4.Machine.RegisterSet.ARM
+                            SEL4.Machine.Hardware.ARM
+                           
 
     hs-source-dirs:         src
     ghc-prof-options:       -auto-all -fprof-auto
@@ -80,5 +94,12 @@ Library
                             -fno-spec-constr -fno-warn-name-shadowing
                             -fno-warn-unrecognised-pragmas
                             -fno-warn-unused-binds
+
+    cpp-options:
+                            -DTARGET=ARM
+                            -DTARGET_ARM
+                            -DPLATFORM=QEmu
+                            -DPLATFORM_QEmu
+                            
     Default-Language: Haskell98
 

haskell/Setup.hs

-#!/usr/bin/env runhaskell
-{-# LANGUAGE ViewPatterns #-}
---
--- Copyright 2014, General Dynamics C4 Systems
---
--- This software may be distributed and modified according to the terms of
--- the GNU General Public License version 2. Note that NO WARRANTY is provided.
--- See "LICENSE_GPLv2.txt" for details.
---
--- @TAG(GD_GPL)
---
-
-module Main where
-import Control.Applicative((<$>))
-import Distribution.Simple
-import Distribution.PackageDescription
-import System.Directory
-import Distribution.PackageDescription.Parse
-import Distribution.Verbosity
-import qualified Distribution.ModuleName
-import Distribution.Simple.Setup
-import System.Process
-import System.Exit
-import System.Environment(getArgs)
-import Data.List(isPrefixOf, find)
-import Control.Monad(unless, liftM)
-
-targets =
-    [ ("arm-qemu",     ("ARM", "QEmu")) ]
-
-bootModules =
-    [ "Kernel/CSpace"
-    , "Kernel/Thread"
-    , "Kernel/FaultHandler"
-    , "Kernel/VSpace"
-    , "Kernel/Init"
-    , "Model/PSpace"
-    , "Object/TCB"
-    , "Object/CNode"
-    , "Object/ObjectType"
-    ]
-
-platformModules =
-    [ "Machine.Hardware"
-    ]
-
-archModules =
-    [ "API.Types"
-    , "API.Invocation"
-    , "Kernel.VSpace"
-    , "Kernel.Thread"
-    , "Object.ObjectType"
-    , "Object.Structures"
-    , "Object.Interrupt"
-    , "Object.Instances"
-    , "Object.TCB"
-    , "Model.StateData"
-    , "Machine.RegisterSet"
-    , "Machine.Hardware"
-    ]
-
-targetModules arch platform =
-    (map (\a -> "SEL4." ++ a ++ "." ++ arch) archModules) ++
-    (map (\a -> "SEL4." ++ a ++ "." ++ arch_platform) platformModules)
-    where arch_platform = arch ++ "." ++ platform
-
-ghcOptions arch platform =
-    [ "-DTARGET=" ++ arch
-    , "-DTARGET_" ++ arch
-    , "-DPLATFORM=" ++ platform
-    , "-DPLATFORM_" ++ platform
-    ]
-
-bootFiles = map moduleToLHSName bootModules
-    where
-        moduleToLHSName f = "src/SEL4/" ++
-            (map (\a -> if a == '.' then '/' else a) f) ++ ".lhs"
-
-main :: IO ()
-main = do
-    args <- getArgs
-    let targetPrefix = "--with-target="
-    let targetArg = find (targetPrefix `isPrefixOf`) args
-    let targetName = liftM (drop (length targetPrefix)) targetArg
-    let args' = filter (not . isPrefixOf targetPrefix) args
-    let hooks = simpleUserHooks {
-                    preBuild = \args flags -> do
-                        generateHSBoot
-                        (preBuild simpleUserHooks) args flags,
-                    readDesc = do
-                      cabalfile <- generateTempCabalFile "SEL4.cabal" targetName
-                      v <- readPackageDescription normal $ cabalfile
-                      removeFile cabalfile
-                      return $ Just v
-                    }
-    defaultMainWithHooksArgs hooks args'
-
-printKnownTargets :: IO ()
-printKnownTargets = do
-    putStrLn "Recognised targets are:"
-    mapM_ (putStrLn.('\t':).fst) targets
-
-
-generateTempCabalFile :: String -> Maybe String -> IO String
-generateTempCabalFile fn targetName = do
-    case (do name <- targetName
-             (name, (arch, platform)) <- find ((==name).fst) targets
-             return (name, arch, platform)) of
-      Nothing -> do
-            putStrLn "Please specify a target: --with-target=<target>"
-            printKnownTargets
-            fail "No target"
-      Just (name, arch, platform) -> do
-         lns <- fmap lines $ readFile fn
-         writeFile (fn ++ "." ++ name) $ unlines (concatMap (f arch platform) lns)
-         return (fn ++ "." ++ name)
- where f arch platform (span (== ' ') -> (length -> indentation, str)) | "$TARGET-SPECIFIC-STUFF" `isPrefixOf` str = generateArchSpecificLines arch platform indentation
-       f _ _ x = [x]
-
-generateArchSpecificLines :: String -> String -> Int -> [String]
-generateArchSpecificLines arch platform indentation =
-    [replicate indentation ' ' ++ "other-modules:" ++ unwords (targetModules arch platform)
-    ,replicate indentation ' ' ++ "cpp-options:" ++ unwords (ghcOptions arch platform)]
-
-generateHSBoot :: IO ()
-generateHSBoot = mapM_ generateHSBoot' bootFiles
-        where
-                generateHSBoot' n = do
-                        putStrLn ("Generating boot file for " ++ n)
-                        r <- system ("perl mkhsboot.pl -l <" ++ n ++ " >"
-                                          ++ n ++ "-boot")
-                        unless (r == ExitSuccess) $ error "Couldn't generate boot file"
-
-