diff --git a/Dedukti/CodeGen/Exts.hs b/Dedukti/CodeGen/Exts.hs
--- a/Dedukti/CodeGen/Exts.hs
+++ b/Dedukti/CodeGen/Exts.hs
@@ -45,32 +45,32 @@
     emit rs@(RS x ty rules) =
         Rec x (length rules) (function rs : def_ty : def_box : zipWith defs_rule [0..] rules)
         where (tyname, boxname) = (varName (x .$ "ty"), varName (x .$ "box"))
-              def_ty  = [dec| ((tyname)) = $(code ty) |]
-              def_box = [dec| ((boxname)) = bbox $(term ty) $(Hs.var tyname) $(var x) |]
+              def_ty  = [$dec| ((tyname)) = $(code ty) |]
+              def_box = [$dec| ((boxname)) = bbox $(term ty) $(Hs.var tyname) $(var x) |]
               -- Checking rules involves much of the same work as checking all
               -- declarations at top-level, so let's just call the code
               -- generation functions recursively.
               defs_rule n (env :@ lhs :--> rhs) =
                   let f (x ::: ty) rs = (emit (RS x ty []) :: Record) : rs
                       ruleCheck = let rule_box = varName (qid "rule" .$ "box")
-                                  in Rec (qid "rule") 0 [[dec| ((rule_box)) = checkRule $(term lhs) $(term rhs) |]]
+                                  in Rec (qid "rule") 0 [[$dec| ((rule_box)) = checkRule $(term lhs) $(term rhs) |]]
                       Bundle decls = coalesce $ foldr f [ruleCheck] (env_bindings env)
                       rule = varName (x .$ "rule" .$ B.pack (show n))
-                      body = Hs.letE decls [hs| main |]
-                  in [dec| ((rule)) = $body |]
+                      body = Hs.letE decls [$hs| main |]
+                  in [$dec| ((rule)) = $body |]
 
     coalesce records = Bundle $ concatMap rec_code records ++ [main]
-        where main = [dec| main = $checks |]
+        where main = [$dec| main = $checks |]
               checks = Hs.Do (concatMap rules records ++ map declaration records)
               declaration r = let desc = Hs.strE $ show $ pretty $ unqualify $ rec_name r
-                                in Hs.qualStmt [hs| checkDeclaration $desc $(var (rec_name r .$ "box")) |]
+                                in Hs.qualStmt [$hs| checkDeclaration $desc $(var (rec_name r .$ "box")) |]
               rules (Rec _ 0 _) = []
               rules (Rec x nr _) =
                 let startmsg = Hs.strE $ "Starting rule " ++ show (pretty (unqualify x)) ++ "."
                     finishmsg = Hs.strE $ "Finished rule " ++ show (pretty (unqualify x)) ++ "."
-                in [Hs.qualStmt [hs| putStrLn $startmsg |]]
+                in [Hs.qualStmt [$hs| putStrLn $startmsg |]]
                     ++ map (\n -> Hs.qualStmt $ var (x .$ "rule" .$ B.pack (show n))) [0..nr-1]
-                    ++ [Hs.qualStmt [hs| putStrLn $finishmsg |]]
+                    ++ [Hs.qualStmt [$hs| putStrLn $finishmsg |]]
 
     serialize mod deps (Bundle decls) =
         B.pack $ prettyPrintWithMode defaultMode {layout = PPInLine} $
@@ -105,7 +105,7 @@
     where n = Rule.arity (head rs)
           occs = Stream.take n (Stream.map Hs.var variables)
           pats = Stream.take n variables
-          rhs = foldr (\x y -> [hs| Lam (\((x)) -> $y) |]) (Hs.metaFunction "__" occs) pats
+          rhs = foldr (\x y -> [$hs| Lam (\((x)) -> $y) |]) (Hs.metaFunction "__" occs) pats
           f | n > 0     = Hs.FunBind (map clause rs ++ [defaultClause x n])
             | otherwise = Hs.FunBind (map clause rs)
 
@@ -118,15 +118,15 @@
        else Hs.Match (*) (Hs.name "__") (map (pattern env) (Rule.patterns lrule))
             Nothing (Hs.GuardedRhss [Hs.GuardedRhs (*) (guards constraints) (code rhs)]) Hs.noBinds
     where guards = map (\(x, x') -> Hs.qualStmt $
-                                    [hs| convertible 0 $(var x) $(var x') |])
+                                    [$hs| convertible 0 $(var x) $(var x') |])
           qids = Stream.unfold (\i -> ((qid $ B.pack $ show i) .$ "fresh", i + 1)) 0
 
 defaultClause :: Id Record -> Int -> Hs.Match
 defaultClause x n =
     Hs.Match (*) (Hs.name "__") (Stream.take n (Stream.map Hs.pvar variables)) Nothing
-          (Hs.UnGuardedRhs (foldl' (\e x -> [hs| App $e $x |]) (constant x) (Stream.take n (Stream.map Hs.var variables)))) Hs.noBinds
+          (Hs.UnGuardedRhs (foldl' (\e x -> [$hs| App $e $x |]) (constant x) (Stream.take n (Stream.map Hs.var variables)))) Hs.noBinds
 
-constant c = [hs| Con $(Hs.strE $ show $ pretty c) |]
+constant c = [$hs| Con $(Hs.strE $ show $ pretty c) |]
 
 pattern :: Em Env -> Em Expr -> Hs.Pat
 pattern env (Var x _) | x `isin` env = Hs.pvar (varName x)
@@ -141,30 +141,30 @@
 -- | Turn an expression into object code with types erased.
 code :: Em Expr -> Hs.Exp
 code (Var x _)            = var x
-code (Lam (x ::: ty) t _) | n <- varName x = [hs| Lam (\((n)) -> $(code t)) |]
-code (Lam (Hole ty) t _)  = [hs| Lam (\_ -> $(code t)) |]
-code (Pi (x ::: ty) t _)  | n <- varName x = [hs| Pi $(code ty) (\((n)) -> $(code t)) |]
-code (Pi (Hole ty) t _)   = [hs| Pi $(code ty) (\_ -> $(code t)) |]
-code (App t1 t2 _)        = [hs| ap $(code t1) $(code t2) |]
-code Type                 = [hs| Type |]
+code (Lam (x ::: ty) t _) | n <- varName x = [$hs| Lam (\((n)) -> $(code t)) |]
+code (Lam (Hole ty) t _)  = [$hs| Lam (\_ -> $(code t)) |]
+code (Pi (x ::: ty) t _)  | n <- varName x = [$hs| Pi $(code ty) (\((n)) -> $(code t)) |]
+code (Pi (Hole ty) t _)   = [$hs| Pi $(code ty) (\_ -> $(code t)) |]
+code (App t1 t2 _)        = [$hs| ap $(code t1) $(code t2) |]
+code Type                 = [$hs| Type |]
 
 -- | Turn a term into its Haskell representation, including all types.
 term :: Em Expr -> Hs.Exp
 term (Var x _)     = var (x .$ "box")
-term (Lam b t _)   = typedAbstraction [hs| TLam |] b (term t)
-term (Pi b t _)    = typedAbstraction [hs| TPi |] b (term t)
-term (App t1 t2 _) = [hs| TApp $(term t1) (UBox $(term t2) $(code t2)) |]
-term Type          = [hs| TType |]
+term (Lam b t _)   = typedAbstraction [$hs| TLam |] b (term t)
+term (Pi b t _)    = typedAbstraction [$hs| TPi |] b (term t)
+term (App t1 t2 _) = [$hs| TApp $(term t1) (UBox $(term t2) $(code t2)) |]
+term Type          = [$hs| TType |]
 
 typedAbstraction c b t =
     case b of
-      x ::: ty -> [hs| $c $(dom ty) (\((box)) -> $ran) |]
+      x ::: ty -> [$hs| $c $(dom ty) (\((box)) -> $ran) |]
           where box = varName (x .$ "box")
                 ran = let n = varName x
-                      in [hs| let ((n)) = obj $(Hs.var box) in $t |]
-      Hole ty  -> [hs| $c $(dom ty) (\_ -> $t) |]
+                      in [$hs| let ((n)) = obj $(Hs.var box) in $t |]
+      Hole ty  -> [$hs| $c $(dom ty) (\_ -> $t) |]
     where dom ty = if isVariable ty
-                   then term ty else [hs| sbox $(term ty) Type $(code ty) |]
+                   then term ty else [$hs| sbox $(term ty) Type $(code ty) |]
 
 varName :: Id Record -> Hs.Name
 varName = Hs.name . xencode . unqualify
diff --git a/Dedukti/Parser/Interface.hs b/Dedukti/Parser/Interface.hs
new file mode 100644
--- /dev/null
+++ b/Dedukti/Parser/Interface.hs
@@ -0,0 +1,14 @@
+-- |
+-- Copyright : © 2009 CNRS - École Polytechnique - INRIA
+-- License   : GPL
+--
+-- Parser for interface files.
+
+module Dedukti.Parser.Interface (parse) where
+
+import Dedukti.Module
+import qualified Data.ByteString.Lazy.Char8 as B
+
+parse :: FilePath -> B.ByteString -> [Qid]
+parse _ = map qid . B.lines
+
diff --git a/Test.hs b/Test.hs
--- a/Test.hs
+++ b/Test.hs
@@ -84,7 +84,7 @@
 
 tests = [ testGroup "Smoke tests"
           [ check "nat" []
-          , check "logic" []
           , check "coc" []
+          , check "logic" ["coc"]
           , check "peano" ["logic", "coc"]
           , checkFailure "bug" [] ] ]
diff --git a/dedukti.cabal b/dedukti.cabal
--- a/dedukti.cabal
+++ b/dedukti.cabal
@@ -1,5 +1,5 @@
 name:           dedukti
-version:        1.1.0
+version:        1.1.1
 author:         Mathieu Boespflug
 maintainer:     Mathieu Boespflug <mboes@lix.polytechnique.fr>
 copyright:      © 2009 CNRS - École Polytechnique - INRIA
@@ -40,6 +40,10 @@
   description: Compile test harness (requires test-framework).
   default:     False
 
+source-repository head
+  type:     git
+  location: git://github.com/mboes/dedukti
+
 library
   exposed-modules:     Dedukti.Runtime
   build-depends:       time >= 1.1
@@ -52,6 +56,7 @@
                        Dedukti.Parser,
                        Dedukti.Parser.External,
                        Dedukti.Parser.Prefix,
+                       Dedukti.Parser.Interface,
                        Dedukti.Pretty,
                        Dedukti.Driver.Interactive,
                        Dedukti.Driver.Batch,
diff --git a/doc/manual.texi.in b/doc/manual.texi.in
--- a/doc/manual.texi.in
+++ b/doc/manual.texi.in
@@ -123,6 +123,7 @@
 * Local install::       Installing in your home directory.
 * Global install::      Installing in the system directories.
 * Building the documentation::     How to build the documentation.
+* Smoke tests::         Running smoke tests (for developers)
 @end menu
 
 @node Requirements
@@ -135,9 +136,11 @@
 of Dedukti to compile properly, so ulterior revisions in the 6.12 series
 are recommended.
 
-The PCRE library 7.0 or above, including the header files, must be
-present on the system before proceeding to @ref{Local install} or
-@ref{Global install}.
+The PCRE library version 7.0 or above, including the header files, must
+be present on the system before proceeding to @ref{Local install} or
+@ref{Global install}. Dedukti has an indirect dependency on @code{happy
+>= 1.17}. You should ensure that the @command{happy} command is in a
+location mentioned in your @env{PATH}.
 
 @node Local install
 @section Installing Dedukti locally
@@ -221,6 +224,24 @@
 folder, depending on the type of installation. You will also need a
 POSIX compatible environment to build the documentation, including the
 @command{m4} command to preprocess the texinfo source.
+
+@node Smoke tests
+@section Smoke tests
+
+The package description file for Dedukti declares a @code{test} flag.
+Enabling this flag instructs Cabal to build the test harness as well.
+The test harness currently contains a handful of smoke tests useful for
+sanity checking of new patches to Dedukti, for instance.
+
+In a Dedukti source directory, one can perform smoke tests as follows:
+
+@example
+$ cabal configure -f test
+$ cabal build
+$ cabal test
+@end example
+
+New changesets should not be submitted unless all tests pass.
 
 @node Dedukti syntax
 @chapter Dedukti syntax