May 2007 - xmonad - Haskell.org

Proofs of StackSet
by Neil Mitchell 08 May '07

08 May '07

Hi, {- ICFP referees look away now -} Dons asked me to check some of the StackSet code for potential pattern match errors, and indeed, there are some. I used Catch (http://www-users.cs.york.ac.uk/~ndm/catch/) to do all the testing. The first thing I had to do was apply a 2 line patch to get that module building with Yhc/nhc, to do with defaulting. Next I ran the program and found: 1) view related: * view calls error, this clearly makes it possible to crash. * raiseFocus calls view 2) head related: * promote calls head, in a potentially unsafe manner 3) tail related: * swap calls tail, again potentially unsafe. This one is easy to fix, simply use drop 1. This also means that promote could crash due to swap. 4) fromJust related: index calls fromJust, which means that it may crash. This means that all functions calling index are potentially unsafe, including: delete, insert, promote, push, shift, view, raiseFocus I took a look at delete, and it looks like the safety depends on the stacks and the cache all agreeing - plus possibly some other invariants. You could probably rewrite some of this code to be more rebust, and gain a proof of safety. 5) everything else: Everything else is safe, apart from (potentially) the Ord instances passed around - I abstracted them away for the testing of Data.Map. Realistically, I think you are fine on this point. This means you have a proof of pattern match safety for: screen, peekStack, empty, peek, member, rotate, workspace, visibleWorkspaces No changes were required for testing (other than the 2 line one for Yhc) - the test sits in a separate module and is very simple: main = screen ||| peekStack ||| index ||| empty ||| peek ||| push ||| delete ||| member ||| raiseFocus ||| rotate ||| promote ||| shift ||| view ||| workspace ||| insert ||| visibleWorkspaces ||| swap I hope some of that is useful to you. The testing is 100% automatic and pretty easy to run, once you have Yhc and Catch installed and configured. You have two choices related to pattern match failure: 1) Ignore it, guard against with QuickCheck 2) Prove it, using Catch You also have three options regarding Catch use: 1) Integrate the 2 line change, add the Catch module testing framework in so anyone with Catch installed can replicate these tests - and check you don't get worse. 2) Have a catch branch, which has the library driver and the patch. This would be a really small branch :-) 3) Don't do anything, I can continue to check things occasionally. I'm on #haskell as ndm, so let me know if you want any help running any of this. Thanks Neil

2 1

Haskell 98 compliance
by Neil Mitchell 08 May '07

08 May '07

Hi, This patch makes the StackSet file Haskell 98 once more, by using list comprehensions instead of pattern guards. This patch has not been tested, so please do the test script first. Use of Haskell 98 makes your lambdas sleep better at night, knowing they are more portable. Thanks Neil

1 0

darcs patch: keep focus stack.
by David Roundy 08 May '07

08 May '07

Hi all, Here's a cut at a focus stack. It's a bit crude, but seems to work. I had to tweak the rotate properties, since rotating the focus (obviously) changes the focus stack. I don't think this weakening of those checks is really a Bad Thing. And I'm a little puzzled how prop_delete_push ever passed. Maybe it failed, and noone noticed? Or maybe we aren't running enough tests with large enough stack sizes, so we never ran into the case where the focus wasn't on the master window to start with? I don't know, but it suggests something is wrong. David P.S. Sorry for my crude code. If we like this behavior, we can clean it up. Sat May 5 10:57:09 PDT 2007 David Roundy <droundy(a)darcs.net> * keep focus stack.

2 2

darcs patch: fix commend in RotView.
by David Roundy 06 May '07

06 May '07

This one is amended... Sat May 5 11:56:54 PDT 2007 David Roundy <droundy(a)darcs.net> * fix commend in RotView.

2 1

darcs patch: make quickcheck tests friendlier to read.
by David Roundy 06 May '07

06 May '07

Hi all, This is just a silly patch to make it easier to deal with failed quickcheck properties in ghci. Derives a read instance for StackSet, and makes windows T be Char, so they're easier to distinguish when a StackSet is printed. David Sat May 5 10:54:15 PDT 2007 David Roundy <droundy(a)darcs.net> * make quickcheck tests friendlier to read.

2 1

darcs patch: make Properties.hs exit with failure on test failure
by Jason Creighton 06 May '07

06 May '07

Sat May 5 11:43:57 MDT 2007 Jason Creighton <jcreigh(a)gmail.com> * make Properties.hs exit with failure on test failure

2 1

darcs patch: fix commend in RotView.
by David Roundy 05 May '07

05 May '07

Sat May 5 11:56:12 PDT 2007 David Roundy <droundy(a)darcs.net> * fix commend in RotView.

1 0

idea for float layer and extensible layout
by David Roundy 05 May '07

05 May '07

I had an idea. What if we implement the float layer via (an extended) extensible layout scheme? It seems pretty straightforward to write a higher order layout that partitions windows between two Layouts, in which case with a little bit of care we ought to be able to just write a layout that handles floating windows only, and then composit that together with any other layout. I doubt this would be the way to *start* implementing a floating layer, but it seems like doing this as a refactor afterwards would both maintain the cleanliness of the code, and ensure the extensible layout interface is sufficiently powerful and flexible to handle just about any window-managing interface. One feature we'd obviously need would be the ability to specify the stacking order of the windows independently of the focus--which would argue in favor of jcreigh's idea that we ought to pass the focussed window to doLayout. But, of course, there's a whole lot more than that which would need doing as well--most notably, the ability for the layout to draw window decorations and respond to mouse events. But these would also need doing by a tabbed interface, which is of much more interest to me than a floating layer. This idea would also have the benefit of keeping xmonad small, since the floating layer could (and would) be implemented outside of the core, as a module imported into Config.hs. -- David Roundy http://www.darcs.net

1 0

Constrained dynamically extensible layout events: a patch
by dons＠cse.unsw.edu.au 04 May '07

04 May '07

David, Spencer et al, are there any problems with restricting layoutMsg arguments to being members of the (open) Message class? I'd (strongly) prefer this over just Dynamic, since it restores most of the static checking we'd need. The only change for something like Mosaic would be to add the mosaic events to Message, with instance Message MyType, and to switch layoutMsg to sendMessage (its our 'throw' for dynamically extensible messages, in fact). The idea of constrained extensible messages is from SimonM's 06 HW paper on extensible exceptions. Comments? -- Don New patches: [Constrain layout messages to be members of a Message class Don Stewart <dons(a)cse.unsw.edu.au>**20070504075233 Using Typeables as the only constraint on layout messages is a bit scary, as a user can send arbitrary values to layoutMsg, whether they make sense or not: there's basically no type feedback on the values you supply to layoutMsg. Folloing Simon Marlow's dynamically extensible exceptions paper, we use an existential type, and a Message type class, to constrain valid arguments to layoutMsg to be valid members of Message. That is, a user writes some data type for messages their layout algorithm accepts: data MyLayoutEvent = Zoom | Explode | Flaming3DGlassEffect deriving (Typeable) and they then add this to the set of valid message types: instance Message MyLayoutEvent Done. We also reimplement the dynamic type check while we're here, to just directly use 'cast', rather than expose a raw fromDynamic/toDyn. With this, I'm much happier about out dynamically extensible layout event subsystem. ] { hunk ./Config.hs 157 - , ((modMask, xK_h ), layoutMsg Shrink) - , ((modMask, xK_l ), layoutMsg Expand) + , ((modMask, xK_h ), sendMessage Shrink) + , ((modMask, xK_l ), sendMessage Expand) hunk ./Operations.hs 19 -import Data.Dynamic ( Typeable, toDyn, fromDynamic ) hunk ./Operations.hs 77 +-- | Throw an (extensible) message value to the current Layout scheme, +-- possibly modifying how we layout the windows, then refresh. hunk ./Operations.hs 80 --- TODO, using Typeable for extensible stuff is a bit gunky. Check -- --- 'extensible exceptions' paper for other ideas. +-- TODO, this will refresh on Nothing. hunk ./Operations.hs 82 --- Basically this thing specifies the basic operations that vary between --- layouts. --- -data ShrinkOrExpand = Shrink | Expand deriving (Typeable, Eq) - -layoutMsg :: Typeable a => a -> X () -- FIXME: The below shouldn't refresh on Nothing -layoutMsg a = layout $ \x@(l:ls) -> maybe x (:ls) (modifyLayout l (toDyn a)) +sendMessage :: Message a => a -> X () +sendMessage m = layout $ \xs -> case xs of + [] -> [] + (l:ls) -> maybe xs (:ls) $ modifyLayout l (SomeMessage m) hunk ./Operations.hs 87 +------------------------------------------------------------------------ hunk ./Operations.hs 89 --- Standard layout algorithms: +-- Builtin layout algorithms: hunk ./Operations.hs 94 +-- +-- The latter algorithms support the following operations: hunk ./Operations.hs 97 -full :: Layout -tall, wide :: Rational -> Rational -> Layout +-- Shrink +-- Expand +-- + +data Resize = Shrink | Expand deriving (Typeable, Show) +instance Message Resize hunk ./Operations.hs 104 -full = Layout { doLayout = \sc ws -> [ (w,sc) | w <- ws ] - , modifyLayout = const Nothing } +full :: Layout +full = Layout { doLayout = \sc ws -> [ (w,sc) | w <- ws ] + , modifyLayout = const Nothing } -- no changes hunk ./Operations.hs 108 +tall, wide :: Rational -> Rational -> Layout hunk ./Operations.hs 112 - , modifyLayout = fmap f . fromDynamic } + , modifyLayout = fmap handler . fromMessage } hunk ./Operations.hs 114 - where f s = tall delta ((op s) frac delta) - op Shrink = (-) ; op Expand = (+) + where handler s = tall delta $ (case s of + Shrink -> (-) + Expand -> (+)) frac delta hunk ./XMonad.hs 20 + Typeable, Message, SomeMessage(..), fromMessage, hunk ./XMonad.hs 32 -import Data.Dynamic ( Dynamic ) +import Data.Typeable hunk ./XMonad.hs 40 - , layouts :: !(M.Map WorkspaceId [Layout]) -- ^ mapping of workspaces + , layouts :: !(M.Map WorkspaceId [Layout]) } -- ^ mapping of workspaces hunk ./XMonad.hs 42 - } hunk ./XMonad.hs 54 - , focusedBorder :: !Color -- ^ border color of the focused window - } + , focusedBorder :: !Color } -- ^ border color of the focused window hunk ./XMonad.hs 96 --- 'doLayout', a pure function to layout a Window set --- 'modifyLayout', +-- 'doLayout', a pure function to layout a Window set 'modifyLayout', +-- 'modifyLayout' can be considered a branch of an exception handler. +-- hunk ./XMonad.hs 100 - , modifyLayout :: Dynamic -> Maybe Layout } + , modifyLayout :: SomeMessage -> Maybe Layout } + +-- Based on ideas in /An Extensible Dynamically-Typed Hierarchy of Exceptions/, +-- Simon Marlow, 2006. Use extensible messages to the modifyLayout handler. +-- +-- User-extensible messages must be a member of this class: +-- +class (Typeable a, Show a) => Message a + +-- +-- A wrapped value of some type in the Message class. +-- +data SomeMessage = forall a. Message a => SomeMessage a + +-- +-- And now, unwrap a given, unknown Message type, performing a (dynamic) +-- type check on the result. +-- +fromMessage :: Message m => SomeMessage -> Maybe m +fromMessage (SomeMessage m) = cast m } Context: [refactoring, style, comments on new layout code Don Stewart <dons(a)cse.unsw.edu.au>**20070504023618] [use anyKey constant instead of magic number Jason Creighton <jcreigh(a)gmail.com>**20070504015043] [added mirrorLayout to mirror arbitrary layouts Jason Creighton <jcreigh(a)gmail.com>**20070504014653] [Fix layout switching order Spencer Janssen <sjanssen(a)cse.unl.edu>**20070503235632] [More Config.hs bugs Spencer Janssen <sjanssen(a)cse.unl.edu>**20070503234607] [Revert accidental change to Config.hs Spencer Janssen <sjanssen(a)cse.unl.edu>**20070503233148] [Add -fglasgow-exts for pattern guards. Properties.hs doesn't complain anymore Spencer Janssen <sjanssen(a)cse.unl.edu>**20070503214221] [Avoid the unsafe pattern match, in case Config.hs has no layouts Spencer Janssen <sjanssen(a)cse.unl.edu>**20070503214007] [add support for extensible layouts. David Roundy <droundy(a)darcs.net>**20070503144750] [comments. and stop tracing events to stderr Don Stewart <dons(a)cse.unsw.edu.au>**20070503075821] [-Wall police Don Stewart <dons(a)cse.unsw.edu.au>**20070503074937] [elaborate documentation in Config.hs Don Stewart <dons(a)cse.unsw.edu.au>**20070503074843] [Use updated refreshKeyboardMapping. Requires latest X11-extras Spencer Janssen <sjanssen(a)cse.unl.edu>**20070503032040] [run QC tests in addition to LOC test Jason Creighton <jcreigh(a)gmail.com>**20070503003202] [Add 'mod-n': refreshes current layout Spencer Janssen <sjanssen(a)cse.unl.edu>**20070503002252] [Fix tests after StackSet changes Spencer Janssen <sjanssen(a)cse.unl.edu>**20070502201622] [First steps to adding floating layer Spencer Janssen <sjanssen(a)cse.unl.edu>**20070502195917] [update motivational text using xmonad.org Don Stewart <dons(a)cse.unsw.edu.au>**20070502061859] [Sort dependencies in installation order Spencer Janssen <sjanssen(a)cse.unl.edu>**20070501204249] [Recommend X11-extras 0.1 Spencer Janssen <sjanssen(a)cse.unl.edu>**20070501204121] [elaborate description in .cabal Don Stewart <dons(a)cse.unsw.edu.au>**20070501035414] [use -fasm by default. Much faster Don Stewart <dons(a)cse.unsw.edu.au>**20070501031220] [Make border width configurable Spencer Janssen <sjanssen(a)cse.unl.edu>**20070430163515] [Add Config.hs-boot, remove defaultLayoutDesc from XConf Spencer Janssen <sjanssen(a)cse.unl.edu>**20070430162647] [Comment only Spencer Janssen <sjanssen(a)cse.unl.edu>**20070430161635] [Comment only Spencer Janssen <sjanssen(a)cse.unl.edu>**20070430161511] [check we never generate invalid stack sets Don Stewart <dons(a)cse.unsw.edu.au>**20070430065946] [view n . shift n . view i . shift i) x == x --> shift + view is invertible Don Stewart <dons(a)cse.unsw.edu.au>**20070430062901] [add rotate all and view idempotency tests Don Stewart <dons(a)cse.unsw.edu.au>**20070430055751] [Add XConf for values that don't change. Spencer Janssen <sjanssen(a)cse.unl.edu>**20070430054715] [Control.Arrow is suspicious, add an explicit import Spencer Janssen <sjanssen(a)cse.unl.edu>**20070430053623] [push is idempotent Don Stewart <dons(a)cse.unsw.edu.au>**20070430054345] [add two properties relating to empty window managers Don Stewart <dons(a)cse.unsw.edu.au>**20070430051016] [configurable border colors Jason Creighton <jcreigh(a)gmail.com>**20070430043859 This also fixes a bug where xmonad was assuming a 24-bit display, and just using, eg, 0xff0000 as an index into a colormap without querying the X server to determine the proper pixel value for "red". ] [new QC property: opening a window only affects the current screen Don Stewart <dons(a)cse.unsw.edu.au>**20070430050133] [a bit more precise about building non-empty stacksets for one test Don Stewart <dons(a)cse.unsw.edu.au>**20070430035729] [remove redundant call to 'delete' in 'shift' Don Stewart <dons(a)cse.unsw.edu.au>**20070430031151] [clean 'delete' a little Don Stewart <dons(a)cse.unsw.edu.au>**20070430025319] [shrink 'swap' Don Stewart <dons(a)cse.unsw.edu.au>**20070430024813] [shrink 'rotate' a little Don Stewart <dons(a)cse.unsw.edu.au>**20070430024525] [move size into Properties.hs Don Stewart <dons(a)cse.unsw.edu.au>**20070430021758] [don't need 'size' operation on StackSet Don Stewart <dons(a)cse.unsw.edu.au>**20070430015927] [avoid grabbing all keys when a keysym is undefined Jason Creighton <jcreigh(a)gmail.com>**20070428180046 XKeysymToKeycode() returns zero if the keysym is undefined. Zero also happens to be the value of AnyKey. ] [add homepage: field to .cabal file Don Stewart <dons(a)cse.unsw.edu.au>**20070429041011] [add fromList to Properties.hs Don Stewart <dons(a)cse.unsw.edu.au>**20070429035823] [move fromList into Properties.hs, -17 loc Don Stewart <dons(a)cse.unsw.edu.au>**20070429035804] [Further refactoring Spencer Janssen <sjanssen(a)cse.unl.edu>**20070426212257] [Refactor in Config.hs (no real changes) Spencer Janssen <sjanssen(a)cse.unl.edu>**20070426211407] [Add the manpage to extra-source-files Spencer Janssen <sjanssen(a)cse.unl.edu>**20070426014105] [add xmonad manpage David Lazar <davidlazar(a)styso.com>**20070426010812] [Remove toList Spencer Janssen <sjanssen(a)cse.unl.edu>**20070426005713] [Ignore numlock and capslock in keybindings Jason Creighton <jcreigh(a)gmail.com>**20070424013357] [Clear numlock bit Spencer Janssen <sjanssen(a)cse.unl.edu>**20070424010352] [force window border to 1px Jason Creighton <jcreigh(a)gmail.com>**20070423050824] [s/creigh// Don Stewart <dons(a)cse.unsw.edu.au>**20070423024026] [some other things to do Don Stewart <dons(a)cse.unsw.edu.au>**20070423023151] [Start TODOs for 0.2 Spencer Janssen <sjanssen(a)cse.unl.edu>**20070423021526] [update readme Don Stewart <dons(a)cse.unsw.edu.au>**20070422090507] [TAG 0.1 Spencer Janssen <sjanssen(a)cse.unl.edu>**20070422083033] Patch bundle hash: 58f3c7c9b1d98e93c2a0aa388fd91f7ee5567446

3 5

statically checked non-empty layout lists
by dons＠cse.unsw.edu.au 04 May '07

04 May '07

The new layout code introduces more chances for runtime errors than I'd like. In particular, the Dynamic type, and the possibility of users defining empty layout lists. Here's a cute approach, purely for instructive purposes, on statically checked non empty layout lists for Config.hs: Given a GADT for non-empty lists: data Empty data NonEmpty data List x y where Nil :: List Empty x Cons :: x -> List y x -> List NonEmpty x toList :: List t a -> [a] toList Nil = [] toList (Cons x y) = x : toList y infixr 5 .:. (.:.) :: x -> List t x -> List NonEmpty x (.:.) = Cons We can constrain: defaultLayouts :: List NonEmpty Layout meaning that this becomes a statically checked error: defaultLayouts = Nil resulting in: Config.hs:138:17: Couldn't match expected type `NonEmpty' against inferred type `Empty' Expected type: List NonEmpty Layout Inferred type: List Empty Layout While this is fine: defaultLayouts :: List NonEmpty Layout defaultLayouts = full .:. tall defaultDelta (1%2) .:. Nil Cute huh? -- Don

2 2