    -- | Machine-specific properties.
    --
    -- Many embedded computers have their own special configuration needed
    -- to use them. Rather than needing to hunt down documentation about the
    -- kernel, bootloader, etc for a given machine, if there's a property
    -- in here for your machine, you can simply use it.
    --
    -- Not all machine properties have been tested yet. If one flagged as
    -- untested and you find it works, please let us know.
    --
    -- You will need to configure the `Host` with the right `Architecture`
    -- for the machine. These properties do test at runtime that a supported
    -- Architecture was selected.
    --
    -- Sometimes non-free firmware is needed to use a board. If the board won't
    -- be functional at all without it, its property will include the non-free
    -- firmware, but if the non-free firmware is only needed for non-critical
    -- functionality, it won't be included.
    --
    -- Example: Building a disk image for a Marvell SheevaPlug
    --
    -- This defines a Host "sheeva" that is a Marvell SheevaPlug.
    -- A bootable disk image for "sheeva" is built on another machine
    -- "darkstar", which can be eg an Intel laptop running Debian.
    --
    -- > import Propellor.Property.Machine
    -- > import Propellor.Property.DiskImage
    -- >
    -- > sheeva :: Host
    -- > sheeva = host "sheeva.example.com" $ props
    -- > 	& osDebian Unstable ARMEL
    -- > 	& marvell_SheevaPlug Marvell_SheevaPlug_SDCard
    -- >	& hasPartition
    -- >		( partition EXT4
    -- > 		`mountedAt` "/"
    -- >		`addFreeSpace` MegaBytes 2048
    -- >		)
    -- >
    -- > darkstar :: Host
    -- > darkstar = host "darkstar.example.com" $ props
    -- >	& imageBuiltFor sheeva
    -- >		(RawDiskImage "/srv/sheeva-disk.img")
    -- >		(Debootstrapped mempty)

    module Propellor.Property.Machine (
    	-- * ARM boards
    	Marvell_SheevaPlug_BootDevice(..),
    	marvell_SheevaPlug,
    	cubietech_Cubietruck,
    	olimex_A10_OLinuXino_LIME,
    	lemaker_Banana_Pi,
    	-- * ARM boards (untested)
    	cubietech_Cubieboard,
    	cubietech_Cubieboard2,
    	lemaker_Banana_Pro,
    	olimex_A10s_OLinuXino_Micro,
    	olimex_A20_OLinuXino_LIME,
    	olimex_A20_OLinuXino_LIME2,
    	olimex_A20_OLinuXino_Micro,
    	olimex_A20_SOM_EVB,
    	linkSprite_pcDuino3_Nano,
    ) where

    import Propellor.Base
    import Propellor.Types.Core
    import qualified Propellor.Property.Apt as Apt
    import qualified Propellor.Property.FlashKernel as FlashKernel
    import qualified Propellor.Property.Uboot as Uboot
    import Propellor.Property.DiskImage.PartSpec

    data Marvell_SheevaPlug_BootDevice
    	= Marvell_SheevaPlug_SDCard
    	| Marvell_SheevaPlug_ESATA

    -- | Marvell SheevaPlug
    --
    -- This includes a small EXT2 formatted /boot partition.
    --
    -- Note that u-boot may need to be upgraded manually, and will need to be
    -- configured to boot from the SD card or eSATA. See
    -- https://www.cyrius.com/debian/kirkwood/sheevaplug/install/
    marvell_SheevaPlug :: Marvell_SheevaPlug_BootDevice -> Property (HasInfo + DebianLike)
    marvell_SheevaPlug :: Marvell_SheevaPlug_BootDevice -> Property (HasInfo + DebianLike)
    marvell_SheevaPlug bd :: Marvell_SheevaPlug_BootDevice
    bd = Property
      (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
    fk
    	Property
      (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
    -> Property DebianLike
    -> CombinedType
         (Property
            (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish]))
         (Property DebianLike)
    forall x y. Combines x y => x -> y -> CombinedType x y
    `requires` Property DebianLike
    marvell
    	Property
      (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
    -> Property
         (MetaTypes
            '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish,
               'Targeting 'OSArchLinux, 'Targeting 'OSFreeBSD])
    -> CombinedType
         (Property
            (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish]))
         (Property
            (MetaTypes
               '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish,
                  'Targeting 'OSArchLinux, 'Targeting 'OSFreeBSD]))
    forall x y. Combines x y => x -> y -> CombinedType x y
    `requires` PartSpec PartLocation -> Property (HasInfo + UnixLike)
    hasPartition PartSpec PartLocation
    bootpart
      where
    	fk :: Property
      (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
    fk = case Marvell_SheevaPlug_BootDevice
    bd of
    		Marvell_SheevaPlug_SDCard ->
    			Machine -> Property (HasInfo + DebianLike)
    FlashKernel.installed "Marvell SheevaPlug Reference Board"
    		Marvell_SheevaPlug_ESATA ->
    			Machine -> Property (HasInfo + DebianLike)
    FlashKernel.installed "Marvell eSATA SheevaPlug Reference Board"
    	-- The boot loader needs an EXT2 boot partition, which comes
    	-- first. Add some free space to allow for additional kernel images
    	-- and initrds.
    	bootpart :: PartSpec PartLocation
    	bootpart :: PartSpec PartLocation
    bootpart = Fs -> PartSpec PartLocation
    forall t. Monoid t => Fs -> PartSpec t
    partition Fs
    EXT2
    		PartSpec PartLocation -> Machine -> PartSpec PartLocation
    forall t. PartSpec t -> Machine -> PartSpec t
    `mountedAt` "/boot"
    		PartSpec PartLocation -> PartLocation -> PartSpec PartLocation
    `partLocation` PartLocation
    Beginning
    		PartSpec PartLocation -> PartSize -> PartSpec PartLocation
    forall t. PartSpec t -> PartSize -> PartSpec t
    `addFreeSpace` Integer -> PartSize
    MegaBytes 150

    -- | Cubietech Cubietruck
    --
    -- Wifi needs non-free firmware-brcm80211, which is not installed by
    -- this property. Also, see https://bugs.debian.org/844056
    cubietech_Cubietruck :: Property (HasInfo + DebianLike)
    cubietech_Cubietruck :: Property (HasInfo + DebianLike)
    cubietech_Cubietruck = Machine -> Property (HasInfo + DebianLike)
    FlashKernel.installed "Cubietech Cubietruck"
    	Property
      (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
    -> Property
         (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
    -> CombinedType
         (Property
            (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish]))
         (Property
            (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish]))
    forall x y. Combines x y => x -> y -> CombinedType x y
    `requires` Machine -> Property (HasInfo + DebianLike)
    sunixi "Cubietruck"
    	Property
      (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
    -> Property DebianLike
    -> CombinedType
         (Property
            (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish]))
         (Property DebianLike)
    forall x y. Combines x y => x -> y -> CombinedType x y
    `requires` Property DebianLike
    lpae

    -- | Cubietech Cubieboard (untested)
    cubietech_Cubieboard :: Property (HasInfo + DebianLike)
    cubietech_Cubieboard :: Property (HasInfo + DebianLike)
    cubietech_Cubieboard = Machine -> Property (HasInfo + DebianLike)
    FlashKernel.installed "Cubietech Cubieboard"
    	Property
      (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
    -> Property
         (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
    -> CombinedType
         (Property
            (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish]))
         (Property
            (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish]))
    forall x y. Combines x y => x -> y -> CombinedType x y
    `requires` Machine -> Property (HasInfo + DebianLike)
    sunixi "Cubieboard"
    	Property
      (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
    -> Property DebianLike
    -> CombinedType
         (Property
            (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish]))
         (Property DebianLike)
    forall x y. Combines x y => x -> y -> CombinedType x y
    `requires` Property DebianLike
    armmp

    -- | Cubietech Cubieboard2 (untested)
    cubietech_Cubieboard2 :: Property (HasInfo + DebianLike)
    cubietech_Cubieboard2 :: Property (HasInfo + DebianLike)
    cubietech_Cubieboard2 = Machine -> Property (HasInfo + DebianLike)
    FlashKernel.installed "Cubietech Cubieboard2"
    	Property
      (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
    -> Property
         (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
    -> CombinedType
         (Property
            (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish]))
         (Property
            (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish]))
    forall x y. Combines x y => x -> y -> CombinedType x y
    `requires` Machine -> Property (HasInfo + DebianLike)
    sunixi "Cubieboard2"
    	Property
      (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
    -> Property DebianLike
    -> CombinedType
         (Property
            (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish]))
         (Property DebianLike)
    forall x y. Combines x y => x -> y -> CombinedType x y
    `requires` Property DebianLike
    lpae

    -- | LeMaker Banana Pi
    lemaker_Banana_Pi :: Property (HasInfo + DebianLike)
    lemaker_Banana_Pi :: Property (HasInfo + DebianLike)
    lemaker_Banana_Pi = Machine -> Property (HasInfo + DebianLike)
    FlashKernel.installed "LeMaker Banana Pi"
    	Property
      (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
    -> Property
         (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
    -> CombinedType
         (Property
            (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish]))
         (Property
            (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish]))
    forall x y. Combines x y => x -> y -> CombinedType x y
    `requires` Machine -> Property (HasInfo + DebianLike)
    sunixi "Bananapi"
    	Property
      (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
    -> Property DebianLike
    -> CombinedType
         (Property
            (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish]))
         (Property DebianLike)
    forall x y. Combines x y => x -> y -> CombinedType x y
    `requires` Property DebianLike
    lpae

    -- | LeMaker Banana Pro (untested)
    lemaker_Banana_Pro :: Property (HasInfo + DebianLike)
    lemaker_Banana_Pro :: Property (HasInfo + DebianLike)
    lemaker_Banana_Pro = Machine -> Property (HasInfo + DebianLike)
    FlashKernel.installed "LeMaker Banana Pro"
    	Property
      (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
    -> Property
         (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
    -> CombinedType
         (Property
            (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish]))
         (Property
            (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish]))
    forall x y. Combines x y => x -> y -> CombinedType x y
    `requires` Machine -> Property (HasInfo + DebianLike)
    sunixi "Bananapro"
    	Property
      (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
    -> Property DebianLike
    -> CombinedType
         (Property
            (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish]))
         (Property DebianLike)
    forall x y. Combines x y => x -> y -> CombinedType x y
    `requires` Property DebianLike
    lpae

    -- | Olimex A10-OLinuXino-LIME
    olimex_A10_OLinuXino_LIME :: Property (HasInfo + DebianLike)
    olimex_A10_OLinuXino_LIME :: Property (HasInfo + DebianLike)
    olimex_A10_OLinuXino_LIME = Machine -> Property (HasInfo + DebianLike)
    FlashKernel.installed "Olimex A10-OLinuXino-LIME"
    	Property
      (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
    -> Property
         (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
    -> CombinedType
         (Property
            (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish]))
         (Property
            (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish]))
    forall x y. Combines x y => x -> y -> CombinedType x y
    `requires` Machine -> Property (HasInfo + DebianLike)
    sunixi "A10-OLinuXino-Lime"
    	Property
      (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
    -> Property DebianLike
    -> CombinedType
         (Property
            (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish]))
         (Property DebianLike)
    forall x y. Combines x y => x -> y -> CombinedType x y
    `requires` Property DebianLike
    armmp

    -- | Olimex A10s-Olinuxino Micro (untested)
    olimex_A10s_OLinuXino_Micro :: Property (HasInfo + DebianLike)
    olimex_A10s_OLinuXino_Micro :: Property (HasInfo + DebianLike)
    olimex_A10s_OLinuXino_Micro = Machine -> Property (HasInfo + DebianLike)
    FlashKernel.installed "Olimex A10s-Olinuxino Micro"
    	Property
      (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
    -> Property
         (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
    -> CombinedType
         (Property
            (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish]))
         (Property
            (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish]))
    forall x y. Combines x y => x -> y -> CombinedType x y
    `requires` Machine -> Property (HasInfo + DebianLike)
    sunixi "A10s-OLinuXino-M"
    	Property
      (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
    -> Property DebianLike
    -> CombinedType
         (Property
            (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish]))
         (Property DebianLike)
    forall x y. Combines x y => x -> y -> CombinedType x y
    `requires` Property DebianLike
    armmp

    -- | Olimex A20-OlinuXino-LIME (untested)
    olimex_A20_OLinuXino_LIME :: Property (HasInfo + DebianLike)
    olimex_A20_OLinuXino_LIME :: Property (HasInfo + DebianLike)
    olimex_A20_OLinuXino_LIME = Machine -> Property (HasInfo + DebianLike)
    FlashKernel.installed "Olimex A20-OLinuXino-LIME"
    	Property
      (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
    -> Property
         (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
    -> CombinedType
         (Property
            (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish]))
         (Property
            (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish]))
    forall x y. Combines x y => x -> y -> CombinedType x y
    `requires` Machine -> Property (HasInfo + DebianLike)
    sunixi "A20-OLinuXino-Lime"
    	Property
      (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
    -> Property DebianLike
    -> CombinedType
         (Property
            (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish]))
         (Property DebianLike)
    forall x y. Combines x y => x -> y -> CombinedType x y
    `requires` Property DebianLike
    lpae

    -- | Olimex A20-OlinuXino-LIME2 (untested)
    olimex_A20_OLinuXino_LIME2 :: Property (HasInfo + DebianLike)
    olimex_A20_OLinuXino_LIME2 :: Property (HasInfo + DebianLike)
    olimex_A20_OLinuXino_LIME2 = Machine -> Property (HasInfo + DebianLike)
    FlashKernel.installed "Olimex A20-OLinuXino-LIME2"
    	Property
      (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
    -> Property
         (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
    -> CombinedType
         (Property
            (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish]))
         (Property
            (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish]))
    forall x y. Combines x y => x -> y -> CombinedType x y
    `requires` Machine -> Property (HasInfo + DebianLike)
    sunixi "A20-OLinuXino-Lime2"
    	Property
      (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
    -> Property DebianLike
    -> CombinedType
         (Property
            (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish]))
         (Property DebianLike)
    forall x y. Combines x y => x -> y -> CombinedType x y
    `requires` Property DebianLike
    lpae

    -- | Olimex A20-Olinuxino Micro (untested)
    olimex_A20_OLinuXino_Micro :: Property (HasInfo + DebianLike)
    olimex_A20_OLinuXino_Micro :: Property (HasInfo + DebianLike)
    olimex_A20_OLinuXino_Micro = Machine -> Property (HasInfo + DebianLike)
    FlashKernel.installed "Olimex A20-Olinuxino Micro"
    	Property
      (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
    -> Property
         (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
    -> CombinedType
         (Property
            (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish]))
         (Property
            (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish]))
    forall x y. Combines x y => x -> y -> CombinedType x y
    `requires` Machine -> Property (HasInfo + DebianLike)
    sunixi "A20-OLinuXino-MICRO"
    	Property
      (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
    -> Property DebianLike
    -> CombinedType
         (Property
            (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish]))
         (Property DebianLike)
    forall x y. Combines x y => x -> y -> CombinedType x y
    `requires` Property DebianLike
    lpae

    -- | Olimex A20-SOM-EVB (untested)
    olimex_A20_SOM_EVB :: Property (HasInfo + DebianLike)
    olimex_A20_SOM_EVB :: Property (HasInfo + DebianLike)
    olimex_A20_SOM_EVB = Machine -> Property (HasInfo + DebianLike)
    FlashKernel.installed "Olimex A20-Olimex-SOM-EVB"
    	Property
      (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
    -> Property
         (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
    -> CombinedType
         (Property
            (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish]))
         (Property
            (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish]))
    forall x y. Combines x y => x -> y -> CombinedType x y
    `requires` Machine -> Property (HasInfo + DebianLike)
    sunixi "A20-Olimex-SOM-EVB"
    	Property
      (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
    -> Property DebianLike
    -> CombinedType
         (Property
            (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish]))
         (Property DebianLike)
    forall x y. Combines x y => x -> y -> CombinedType x y
    `requires` Property DebianLike
    lpae

    -- | LinkSprite pcDuino Nano (untested)
    --
    -- Needs non-free firmware, see
    -- https://wiki.debian.org/InstallingDebianOn/Allwinner
    linkSprite_pcDuino3_Nano :: Property (HasInfo + DebianLike)
    linkSprite_pcDuino3_Nano :: Property (HasInfo + DebianLike)
    linkSprite_pcDuino3_Nano = Machine -> Property (HasInfo + DebianLike)
    FlashKernel.installed "LinkSprite pcDuino3 Nano"
    	Property
      (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
    -> Property
         (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
    -> CombinedType
         (Property
            (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish]))
         (Property
            (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish]))
    forall x y. Combines x y => x -> y -> CombinedType x y
    `requires` Machine -> Property (HasInfo + DebianLike)
    sunixi "Linksprite_pcDuino3"
    	Property
      (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
    -> Property DebianLike
    -> CombinedType
         (Property
            (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish]))
         (Property DebianLike)
    forall x y. Combines x y => x -> y -> CombinedType x y
    `requires` Property DebianLike
    lpae

    sunixi :: Uboot.BoardName -> Property (HasInfo + DebianLike)
    sunixi :: Machine -> Property (HasInfo + DebianLike)
    sunixi boardname :: Machine
    boardname = Machine -> Property (HasInfo + DebianLike)
    Uboot.sunxi Machine
    boardname
    	Property
      (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
    -> Property DebianLike
    -> CombinedType
         (Property
            (Sing '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish]))
         (Property DebianLike)
    forall x y. Combines x y => x -> y -> CombinedType x y
    `requires` [Machine] -> Property DebianLike
    Apt.installed
    		[ "firmware-linux-free"
    		, "sunxi-tools"
    		]

    armmp :: Property DebianLike
    armmp :: Property DebianLike
    armmp = [Architecture] -> Property DebianLike -> Property DebianLike
    checkArchitecture [Architecture
    ARMHF, Architecture
    ARMEL] (Property DebianLike -> Property DebianLike)
    -> Property DebianLike -> Property DebianLike
    forall a b. (a -> b) -> a -> b
    $
    	[Machine] -> Property DebianLike
    Apt.installed ["linux-image-armmp"]

    lpae :: Property DebianLike
    lpae :: Property DebianLike
    lpae = [Architecture] -> Property DebianLike -> Property DebianLike
    checkArchitecture [Architecture
    ARMHF, Architecture
    ARMEL] (Property DebianLike -> Property DebianLike)
    -> Property DebianLike -> Property DebianLike
    forall a b. (a -> b) -> a -> b
    $
    	[Machine] -> Property DebianLike
    Apt.installed ["linux-image-armmp-lpae"]

    marvell :: Property DebianLike
    marvell :: Property DebianLike
    marvell = [Architecture] -> Property DebianLike -> Property DebianLike
    checkArchitecture [Architecture
    ARMEL] (Property DebianLike -> Property DebianLike)
    -> Property DebianLike -> Property DebianLike
    forall a b. (a -> b) -> a -> b
    $
    	[Machine] -> Property DebianLike
    Apt.installed ["linux-image-marvell"]

    checkArchitecture :: [Architecture] -> Property DebianLike -> Property DebianLike
    checkArchitecture :: [Architecture] -> Property DebianLike -> Property DebianLike
    checkArchitecture as :: [Architecture]
    as p :: Property DebianLike
    p = Machine
    -> (OuterMetaTypesWitness
          '[ 'Targeting 'OSDebian, 'Targeting 'OSBuntish]
        -> Maybe System -> Propellor Result)
    -> Property DebianLike
    forall k (metatypes :: k).
    SingI metatypes =>
    Machine
    -> (OuterMetaTypesWitness metatypes
        -> Maybe System -> Propellor Result)
    -> Property (MetaTypes metatypes)
    withOS (Property DebianLike -> Machine
    forall p. IsProp p => p -> Machine
    getDesc Property DebianLike
    p) ((OuterMetaTypesWitness
        '[ 'Targeting 'OSDebian, 'Targeting 'OSBuntish]
      -> Maybe System -> Propellor Result)
     -> Property DebianLike)
    -> (OuterMetaTypesWitness
          '[ 'Targeting 'OSDebian, 'Targeting 'OSBuntish]
        -> Maybe System -> Propellor Result)
    -> Property DebianLike
    forall a b. (a -> b) -> a -> b
    $ \w :: OuterMetaTypesWitness
      '[ 'Targeting 'OSDebian, 'Targeting 'OSBuntish]
    w o :: Maybe System
    o -> case Maybe System
    o of
    	(Just (System _ arch :: Architecture
    arch)) | Architecture
    arch Architecture -> [Architecture] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [Architecture]
    as -> OuterMetaTypesWitness
      '[ 'Targeting 'OSDebian, 'Targeting 'OSBuntish]
    -> Property DebianLike -> Propellor Result
    forall (inner :: [MetaType]) (outer :: [MetaType]).
    EnsurePropertyAllowed inner outer =>
    OuterMetaTypesWitness outer
    -> Property (MetaTypes inner) -> Propellor Result
    ensureProperty OuterMetaTypesWitness
      '[ 'Targeting 'OSDebian, 'Targeting 'OSBuntish]
    w Property DebianLike
    p
    	_ -> Machine -> Propellor Result
    forall a. HasCallStack => Machine -> a
    error (Machine -> Propellor Result) -> Machine -> Propellor Result
    forall a b. (a -> b) -> a -> b
    $ "Machine needs architecture to be one of: " Machine -> Machine -> Machine
    forall a. [a] -> [a] -> [a]
    ++ [Architecture] -> Machine
    forall a. Show a => a -> Machine
    show [Architecture]
    as