johnw is currently certified at Master level.

Name: John Wiegley
Member since: 2000-09-20 05:20:40
Last Login: 2017-02-17 18:32:35

FOAF RDF Share This



My journal is now kept here.


Recent blog entries by johnw

Syndication: RSS 2.0

Putting lenses to work

Putting lenses to work

I gave a talk a couple of weeks ago at BayHac 2017 on “Putting lenses to work”, to show in a practical context how we use lenses at my workplace. I specifically avoided any theory about lenses, or the complex types, or the many operators, to show that at its core, lens is a truly invaluable library:

The videos are now available on YouTube, and the slides for this talk are on GitHub.

The code in the slides are taken directly (using Emacs) from a test file in that same repository, Lenses.hs, to serve as a way of preserving helpful examples, and to make it easy to cargo cult specific patterns into your code.

Syndicated 2017-04-22 00:00:00 from Lost in Technopolis

Submitting Haskell functions to Z3

Submitting Haskell functions to Z3

Conal Elliott has been working for several years now on using categories, specifically cartesian closed category, as a way to abstract Haskell functions at compile-time, so you can render the resulting “categorical term” into other categories.

Here’s an example Haskell function:

\x -> f x (g x)

And here’s its categorical rendering, just to give the flavor of the idea:

eval ∘ (f' △ g')

Where eval means uncurry ($), and f' and g' are the renderings of those two functions; and the operator is (&&&). I’m not using the typical Haskell names for these, by the way, in order to convince myself not to “think in Haskell” when working with these terms, but rather I’m choosing whatever symbols I find most often using in the literature on catgeory theory.

There are a few things to notice about these categorical terms:

  1. They must be point-free. There is no such thing as naming a term, only morphisms that use or produce objects. Hence Awodey calls category theory “the algebra of functions”.

  2. They quickly become very large and unreadable. All but the simplest terms are nearly impossible to understand just by looking at them. Think of it as the binary code for categories.

  3. Because they are just, in effect, chains of composition, without any name binding or scoping issue to consider, the nature of the computation is laid out in a very direct (albeit verbose) way, making rewrite rules available throughout the abstract term.

Although it seems a bit technical at first, the idea is quite simple: Discern the abstract, categorical meaning of a Haskell function, then realize that term in any other category that is cartesian (has products) and closed (has functions as objects, i.e., higher-order constructions). Nothing else needs to be known about the target category for the abstract term to have meaning there. That’s the beauty of using category theory as a universal language for expressing ideas: the meaning transports everywhere.

Here’s an equation meant for the solver, written in plain Haskell:

equation :: (Num a, Ord a) => a -> a -> Bool
equation x y =
    x < y &&
    y < 100 &&
    0 <= x - 3 + 7 * y &&
    (x == y || y + 20 == x + 30)

Here’s how I run the solver, using z3cat, which is built on top of Conal’s concat library:

mres <- liftIO $ runZ3 (ccc (uncurry (equation @Int))) $ do
    x <- mkFreshIntVar "x"
    y <- mkFreshIntVar "y"
    return $ PairE (PrimE x) (PrimE y)
case mres of
    Nothing  -> error "No solution found."
    Just sol -> putStrLn $ "Solution: " ++ show sol

And the result, also showing the equation submitted to Z3:

(let ((a!1 (ite (<= 0 (+ (- x!0 3) (* 7 y!1)))
                (ite (= x!0 y!1) true (= (+ y!1 20) (+ x!0 30)))
  (ite (< x!0 y!1) (ite (< y!1 100) a!1 false) false))
Solution: [-8,2]

Now with one function, I have either a predicate function I can use in Haskell, or an input for Z3 to find arguments for which it is true!

In addition to using Conal’s work in Haskell, I’m also working on a Coq rendering of his idea, which I hope will give me a more principled way to extract Coq programs into Haskell, by way of their categorical representation.

Syndicated 2017-04-18 00:00:00 from Lost in Technopolis

A case of reflection

A case of reflection

A while back, Edward Kmett wrote a library called reflection, based on a 2004 paper by Oleg Kiselyov and Chung-chieh Shan that describes a neat trick for reifying data into types (here the word “reify” can be understood as turning a value into something that can be referenced at the type level). There was also an article written by Austin Seipp on how to use the library, and some great answers on reddit and stackoverflow that go into detail about how it works.

And yet, in all these years, though I’ve been on the lookout for a way to make use of this library, I wasn’t able to fit it into my workflow – until today! So let’s look at my real world use for reflection, which solves a problem that maybe others have encountered as well.

As you may know, the QuickCheck library provides a facility for generating arbitrary data sets. The property testing features of QuickCheck make use of this generation to search for test data that might violate a set of properties.

However, the generation facility can also be used on its own, separate from the testing components, to randomly generate data for any purpose. The library for producing this random data offers lots of combinators, and is based around instances for a type class called Arbitrary. Here’s a basic example:

module Main where

import Test.QuickCheck.Arbitrary
import Test.QuickCheck.Gen

data Foo = Foo [Int] [String]
    deriving Show

instance Arbitrary Foo where
    arbitrary = do
        xs  <- listOf chooseAny
        len <- choose (1, 100)
        ys  <- vectorOf len (shuffle "Hello, world")
        return $ Foo xs ys

main :: IO ()
main = print =<< generate (arbitrary :: Gen Foo)

This creates a specifically shaped set of random data, where the list of integers may be of any length, and any value, but the list of strings will always be from 1 to 100 elements long, and the strings will only consist of random arrangements of the characters found in "Hello, world".

Now, what if you wanted to guide the generation process for Foo using external information? Such as picking the length of the list of strings from a value provided by the user? Since Arbitrary does not allow the use of Reader, how do we get that user-supplied value into the arbitrary function above? And without using global IORefs or unsafePerformIO?

The reflection library allows us to reify a runtime value into a type (whose name we’ll never know, requiring us to reference it through a type variable), and then communicate that type via a constraint, such that we can reflect the value back out as needed. If this sounds a bit confusing, maybe an example can make it clearer:

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}

module Main where

import Data.Proxy
import Data.Reflection
import Test.QuickCheck.Arbitrary
import Test.QuickCheck.Gen
import System.Environment

data Foo s = Foo [Int] [String]
    deriving Show

instance Reifies s Int => Arbitrary (Foo s) where
    arbitrary = do
        xs  <- listOf chooseAny
        len <- choose (1, reflect (Proxy :: Proxy s))
        ys  <- vectorOf len (shuffle "Hello, world")
        return $ Foo xs ys

main :: IO ()
main = do
    [len] <- getArgs
    reify (read len :: Int) $ \(Proxy :: Proxy s) ->
        print =<< generate (arbitrary :: Gen (Foo s))

There are a few additional things to note here:

  1. A phantom type variable has been added to Foo. This type variable associates the reified data to our type, so it can be reflected back out in the instance for this type.

  2. The Arbitrary instance for Foo s has incurred a new contraint, stating that the type represented by s somehow reifies an Int. How this happens is the magic of the reflection library, and uses a clever GHC trick representing Edward’s unique twist on Oleg and Chung-chieh’s work. This instance requires the UndecidableInstances extension.

  3. We now call reify with the data we want to pass along. This function takes a lambda whose first argument is a Proxy s, giving us a way to know which type variable to use in the type of the call to arbitrary. This requires the ScopedTypeVariables extension.

That’s it: reflection gives us a way to plumb extra data into instances at runtime, at the cost of adding a single phantom type.

If the phantom type seems excessive for one use case, or if adding the phantom would effect a large family of types, then an alternative is to enable the FlexibleInstances extension, and use Edward’s tagged library to carry the phantom instead:

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}

module Main where

import Data.Proxy
import Data.Tagged
import Data.Reflection
import Test.QuickCheck.Arbitrary
import Test.QuickCheck.Gen
import System.Environment

data Foo = Foo [Int] [String]
    deriving Show

instance Reifies s Int => Arbitrary (Tagged s Foo) where
    arbitrary = fmap Tagged $ do
        xs  <- listOf chooseAny
        len <- choose (1, reflect (Proxy :: Proxy s))
        ys  <- vectorOf len (shuffle "Hello, world")
        return $ Foo xs ys

main :: IO ()
main = do
    [len] <- getArgs
    reify (read len :: Int) $ \(Proxy :: Proxy s) ->
        print . unTagged =<< generate (arbitrary :: Gen (Tagged s Foo))

This way we leave the original type alone – which may be the only option if you’re generating arbitrary data for types from libraries. You’ll just have to wrap and unwrap the Tagged newtype wrapper as necessary.

Another benefit of using Tagged is that, because it can be wrapped and unwrapped as necessary, it becomes possible to change the refied information in cases where nested types are involved. In this last example, the user is allowed to specify the value that should be supplied to the Bar constructor during data generation.

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}

module Main where

import Data.Proxy
import Data.Tagged
import Data.Reflection
import Test.QuickCheck.Arbitrary
import Test.QuickCheck.Gen
import System.Environment

newtype Bar = Bar Int
    deriving Show

data Foo = Foo [Bar] [String]
    deriving Show

instance Reifies s Int => Arbitrary (Tagged s Bar) where
    arbitrary = return $ Tagged $ Bar $ reflect (Proxy :: Proxy s)

instance Reifies s (Int, Int) => Arbitrary (Tagged s Foo) where
    arbitrary = fmap Tagged $ do
        let (len, bar) = reflect (Proxy :: Proxy s)
        xs <- listOf (reify bar $ \(Proxy :: Proxy r) ->
                          unTagged <$> (arbitrary :: Gen (Tagged r Bar)))
        l  <- choose (1, len)
        ys <- vectorOf l (shuffle "Hello, world")
        return $ Foo xs ys

main :: IO ()
main = do
    [len, barValue] <- getArgs
    reify (read len :: Int, read barValue :: Int) $ \(Proxy :: Proxy s) ->
        print . unTagged =<< generate (arbitrary :: Gen (Tagged s Foo))

Syndicated 2017-02-23 00:00:00 from Lost in Technopolis

Using the FMap library in Coq

Using the FMap library in Coq

One of the most common structures used in programming are key/value maps, also called hash maps, dictionaries, association lists, or simply functions. These maps generally provide a way to add new values, lookup keys, iterate over the collection, etc. Yet in Coq, even though this facility exists in the standard library under the module FMap, it can be quite difficult to get started with. This post intends to clarify the typical patterns in a way that is easy to copy into your own project, based on the four different ways this library is typically used.

Using a known key type and map structure

Very often, one maps from a known, ordered type, like nat, to some other type, using one of the concrete structures offered by the FMap library. In that case, the code you want to start with looks like this:

Require Import

Module Import M := FMapList.Make(Nat_as_OT).

You can now create a map using M.t A, where A is your value type. You can prefix the map-related functions with M., or just call them directly. Some common function to use on maps are as follows:

  • empty
  • add
  • remove
  • find
  • mem
  • is_empty
  • map
  • mapi
  • map2
  • fold

There are also several relations you can use to phrase theorems about maps and map membership:

  • In
  • MapsTo
  • Equal
  • Equiv
  • Equivb
  • Empty

Additional functions and lemmas

In order to complete most proofs concerning maps, there are additional lemmas and functions you’ll want to include:

Require Import

Module P := WProperties_fun N_as_OT M.
Module F := P.F.

This provides two new prefixes, P. and F., which bring into scope many more helper functions and lemmas:

  • P.of_list
  • P.to_list
  • P.filter
  • P.for_all
  • P.exists_
  • P.partition
  • P.update
  • P.restrict
  • P.diff

Helper lemmas in the F module are generally best found using SearchAbout for the specific lemma you need. There are too many to list here, and they’re often quite specific in their use, such as F.find_mapsto_iff to reflect between the fact of a successful find operation, and its equivalent MapsTo relation.

Proofs involving maps

There are several induction principles you will need for completing inductive proofs over maps:

  • P.map_induction
  • P.map_induction_bis
  • P.fold_rec
  • P.fold_rec_bis
  • P.fold_rec_nodep
  • P.fold_rec_weak

The P.map_induction induction principle treats each intermediate map as an Add relation over a previous map, until it reaches the base Empty map. The _bis variant expresses the same information as successive calls to add down to an empty map.

P.fold_rec should be applied if the goal has the form of a call to M.fold over a map. If you use this, be sure to revert into the goal any hypotheses referring to the same map, since you’ll likely want to use those facts as part of the induction.

Note that these two sets of principles are used somewhat differently from each other:

-- Applies to any evidence in the context involving [m].
induction m using P.map_induction bis.

-- Applies only to evidence in the goal, thus sometimes
-- requiring use of [revert].
apply P.fold_rec.

Rewriting with maps

Since the internal structure of maps is not exposed by the FMap interface, rewriting can sometimes be a little confusing. Equality between maps is expressed by the equivalence Equal, which states that anything found in the first map is found at the same key in the second map. In other words:

forall k v, M.MapsTo k v m1 <-> M.MapsTo k v m2

This isn’t a problem if the terms you’re rewriting involve functions from the FMap modules, but if you create a new function that operates on maps, you’ll need to accompany it with a proof relating it to Equal. For example:

Definition map_operation `(m : M.t A) : M.t A := ...

Lemma map_operation_Proper :
  Proper (Equal ==> Equal) map_operation.

Now you can rewrite the arguments in a map_operation, provided you know they are Equal.

Also, if you find yourself facing difficulties using rewrite with folds, note that in addition to establishing a proof that the fold function is Proper for its arguments and result, you must also show that the final result is independent of the order of evaluation, since it’s not known from the FMap interface whether the contents of a map are reordered during insertion or not.

Abstracting the map implementation

Often when using maps, it’s not necessary to pick an implementation, you just need the map interface over a known key type. To do this, you just need to place your code in a module that itself requires and passes along the implementation module:

Require Import

Module MyModule (M : WSfun Nat_as_OT).

Module P := WProperties_fun Nat_as_OT M.
Module F := P.F.
End MyModule.

To later instantiate such a module functor using a map implementation, you’d write:

Require Import

Module Import M := FMapList.Make(Nat_as_OT).
Module Import MyMod := MyModule M.

Abstracting over both map and key

When implementing generic algorithms that are applicable to any map, you’ll also need to abstract over the key type. In this case, you have two choices: Do you need to know that the key type is ordered, or do you only need to know that it’s decidable? Often the latter suffices, making the algorithm even more general.

In both cases, you may refer to the key type as either E.key or M.key (since the M module re-exports key), and you can check for key equality using E.eq:

Require Import

Module MoreFacts (E : DecidableType) (M : WSfun E).

Global Program Instance filter_Proper {elt} : forall P,
  Proper (E.eq ==> eq ==> eq) P
    -> Proper (M.Equal (elt:=elt) ==> M.Equal) (@P.filter elt P).

End MoreFacts.

To require an ordered type, which makes available, use:

Require Import

Module MoreFacts (E : OrderedType) (M : WSfun E).
End MoreFacts.

Putting it all together

Since you probably came here just wondering how to construct a map, add stuff to it, and then search for what you added, here is a complete example you can cut and paste to start off with:

Require Import

Module Import M := FMapAVL.Make(Nat_as_OT).

Module P := WProperties_fun Nat_as_OT M.
Module F := P.F.

Compute M.find 1 (M.add 1 10 (M.empty _)).
Compute P.for_all (fun k _ => k <? 10) (M.add 1 10 (M.empty _)).

Also note that there is N_as_OT, which is much faster to compute with if you are using large constants, but it requires familiarity with the NArith library.

Syndicated 2016-10-27 00:00:00 from Lost in Technopolis

Emacs: Pattern Matching with pcase

Emacs: Pattern Matching with pcase

This is a tutorial on how to use the pcase macro in modern flavors of GNU Emacs.

Exact matches

All data fits into some kind of pattern. The most explicit pattern is a description of the data itself. Let’s consider the following value as a running example:

'(1 2 (4 . 5) "Hello")

Explicitly stated, this is a list of four elements, where the first two elements are the integers 1 and 2, the third is a cons consisting of a car of 4 and a cdr of 5, and the fourth is the string "Hello". This states an explicit pattern we can match against using an equality test:

(equal value '(1 2 (4 . 5) "Hello"))

Pattern matches

Where patterns become useful is when we want to generalize a bit. Let’s say we want to do a similar equality test, but we don’t care what the final string’s contents are, only that it’s a string. Even though it’s simply state, this becomes quite difficult using an equality test:

(and (equal (subseq value 0 3) '(1 2 (4 .5)))
     (stringp (nth 3 value)))

What we would prefer is a more direct language for encoding our description of the family of values we’d like to match against. The way we said in English was: the first three elements exactly so, and the last element, any string. This is how we’d phrase that using `pcase’:

(pcase value
  (`(1 2 (4 . 5) ,(pred stringp))
    (message "It matched!")))

Think of pcase as a form of cond, where instead of evaluating each test for non-nil, it compares a series of patterns against the value under consideration (often called the “scrutinee” in the literature). There can be many patterns, and the first one wins, as with cond.

Capturing matches

But pcase can go one step further: Not only can we compare a candidate value against a family of possible values described by their pattern, we can also “capture” sub-values from that pattern for later use. Continuing from the last example, let’s say we want to print the string that match, even though we didn’t care about the contents of the string for the sake of the match:

(pcase value
  (`(1 2 (4 . 5) ,(and (pred stringp) foo))
    (message "It matched, and the string was %s" foo)))

Whenever a naked symbol like foo occurs as a logical pattern (see next section), the part of the value being matched at that position is bound to a local variable of the same name.

Logical and literal patterns

To master pcase, there are two types of patterns you must know: Logical patterns, and literal, or quoted, patterns. Logical patterns describe the kind of data we’d like to match against, and other special actions to take when it matches; and quoted patterns are the “literal” aspect, stating the exact form of a particular match.

Literal patterns are by far the easiest to think about. To match against any atom, string, or list of the same, the corresponding literal pattern is that exact value. So the literal pattern "foo" matches the string "foo", 1 matches the atom 1, etc.

pcase matches against a list of logical patterns, so to use a literal pattern, we must quote it, unless it consists entirely of self-quoting atoms:

(pcase value
  ('sym (message "Matched the symbol `sym'"))
  ((1 2) (message "Matched the list (1 2)")))

Literal patterns may also be introduced using a backquote, in which case commas may be used to place logical patterns within them, in exactly the same way that quoting and anti-quoting works for macros. For example:

(pcase value
  (`(1 2 ,(or 3 4))
   (message "Matched either the list (1 2 3) or (1 2 4)")))

More on logical patterns

There are many special logical patterns. Let’s consider them one by one.

Underscore _

To match against anything whatsoever, no matter its type or value, use underscore. Thus to match against a list containing anything at all at its head, we’d use:

(pcase value
  (`(,_ 1 2)
   (message "Matched a list of anything followed by (1 2)")))


When performing a match, if a symbol occurs within a logical pattern, it binds whatever was found at that position to a local symbol of the same name. Some examples will help to make this clearer:

(pcase value
  (`(1 2 ,foo 3)
   (message "Matched 1, 2, something now bound to foo, and 3"))
   (message "Match anything at all, and bind it to foo!"))
  (`(,the-car . ,the-cdr))
   (message "Match any cons cell, binding the car and cdr locally"))

The reason for doing this is two-fold: Either to refer to a previous match later in the pattern (where it is compared using eq), or to make use of a matched value within the related code block:

(pcase value
  (`(1 2 ,foo ,foo 3)
   (message "Matched (1 2 %s %s 3)" foo)))

(or PAT ...) and (and PAT ...)

We can express boolean logic within a pattern match using the or and and Patterns:

(pcase value
  (`(1 2 ,(or 3 4)
     ,(and (pred stringp)
           (pred (string> "aaa"))
           (pred (lambda (x) (> (length x) 10)))))
   (message "Matched 1, 2, 3 or 4, and a long string "
            "that is lexically greater than 'aaa'")))

pred predicates

Arbitrary predicates can be applied to matched elements, where the predicate will be passed the object that matched. As in the previous example, lambdas can be used to form arbitrarily complex predicates, with their own logic. See above for examples.

guard expressions

At any point within a match, you may assert that something is true by inserting a guard. This might consult some other variable to confirm the validity of a pattern at a given time, or it might reference a local symbol that was earlier bound by the match itself, as described above:

(pcase value
  (`(1 2 ,foo ,(guard (and (not (numberp foo)) (/= foo 10)))
   (message "Matched 1, 2, anything, and then anything again, "
            "but only if the first anything wasn't the number 10"))))

Note that in this example, the guard occurs at a match position, so even though the guard doesn’t refer to what is being matched, if it passes, then whatever occurs at that position (the fourth element of the list), would be an unnamed successful matched. This is rather bad form, so we can be more explicit about the logic here:

(pcase value
  (`(1 2 ,(and foo (guard (and (not (numberp foo)) (/= foo 10)))) _)
   (message "Matched 1, 2, anything, and then anything again, "
            "but only if the first anything wasn't the number 10"))))

This means the same, but associates the guard with the value it tests, and makes it clear that we don’t care what the fourth element is, only that it exists.

Pattern let bindings

Within a pattern we can match sub-patterns, using a special form of let that has a meaning specific to `pcase’:

(pcase value
  (`(1 2 ,(and foo (let 3 foo)))
   (message "A weird way of matching (1 2 3)")))

This example is a bit contrived, but it allows us to build up complex guard patterns that might match against values captured elsewhere in the surrounding code:

(pcase value1
  (`(1 2 ,foo)
   (pcase value2
     (`(1 2 ,(and (let (or 3 4) foo) bar))
      (message "A nested pcase depends on the results of the first")))))

Here the third value of value2 – which must be a list of exactly three elements, starting with 1 and 2 – is being bound to the local variable bar, but only if foo was a 3 or 4. There are many other ways this logic could be expressed, but this gives you a test of how flexibly you can introduce arbitrary pattern matching of other values within any logical pattern.

pcase-let and pcase-let*

That’s all there is to know about pcase! The other two utilities you might like to use are pcase-let and pcase-let*, which do similar things to their logical pattern counter-part let, but as regular Lisp forms:

(pcase-let ((`(1 2 ,foo) value1)
            (`(3 4 ,bar) value2))
  (message "value1 is a list of (1 2 %s); value2 ends with %s"
           foo bar))

Note that pcase-let does not fail, and always executes the correspond forms unless there is a type error. That is, value1 above is not required to fit the form of the match exactly. Rather, every binding that can paired is bound to its corresponding element, but every binding that cannot is bound to nil:

(pcase-let ((`(1 2 ,foo) '(10)))
  (message "foo = %s" foo))   => prints "foo = nil"

(pcase-let ((`(1 2 ,foo) 10))
  (message "foo = %s" foo))   => Lisp error, 10 is not a list

(pcase-let ((`(1 2 ,foo) '(3 4 10)))
  (message "foo = %s" foo))   => prints "foo = 10"

Thus, pcase-let can be thought of as a more expressive form of destructuring-bind.

The pcase-let* variant, like let*, allows you to reference bound local symbols from prior matches.

(pcase-let* ((`(1 2 ,foo) '(1 2 3))
             (`(3 4 ,bar) (list 3 4 foo)))
  (message "foo = %s, bar = %s" foo bar))  => foo = 3, bar = 3

However, if you name a symbol with same name in a later logical pattern, it is not used as an eq test, but rather shadows that symbol:

(pcase-let* ((`(1 2 ,foo) '(1 2 3))
             (`(3 4 ,foo) '(3 4 5)))
  (message "1 2 %s" foo))

This prints out "1 2 5", rather than the current match.

Syndicated 2016-01-21 00:00:00 from Lost in Technopolis

76 older entries...


johnw certified others as follows:

  • johnw certified lerdsuwa as Journeyer
  • johnw certified Nafai77 as Apprentice
  • johnw certified rms as Master
  • johnw certified walters as Master
  • johnw certified rw as Apprentice

Others have certified johnw as follows:

  • aaronl certified johnw as Master
  • jtc certified johnw as Master
  • lerdsuwa certified johnw as Master
  • Ushakov certified johnw as Master
  • walters certified johnw as Master
  • cmm certified johnw as Master
  • rw certified johnw as Master
  • maragato certified johnw as Master
  • mishan certified johnw as Master
  • Nafai77 certified johnw as Master
  • lukeg certified johnw as Master
  • dgoel3 certified johnw as Master
  • deego certified johnw as Master
  • quarl certified johnw as Master
  • bpt certified johnw as Master
  • sachac certified johnw as Master
  • dhruva certified johnw as Master

[ Certification disabled because you're not logged in. ]

New Advogato Features

New HTML Parser: The long-awaited libxml2 based HTML parser code is live. It needs further work but already handles most markup better than the original parser.

Keep up with the latest Advogato features by reading the Advogato status blog.

If you're a C programmer with some spare time, take a look at the mod_virgule project page and help us with one of the tasks on the ToDo list!