diff --git a/sledge/src/config.ml b/sledge/src/config.ml
index c4713de9d..3e149414e 100644
--- a/sledge/src/config.ml
+++ b/sledge/src/config.ml
@@ -39,7 +39,6 @@ end = struct
     let (Arg (trm, set)) = List.fold_right ~f:pair args ~init in
     Term.app (Term.const set) trm
 
-
   let args : arg list ref = ref []
 
   let mk ~default arg =
@@ -48,7 +47,6 @@ end = struct
     args := Arg (arg, set) :: !args ;
     var
 
-
   let parse info validate =
     match Term.eval (Term.(ret (const validate $ tuple !args)), info) with
     | `Ok () -> ()
@@ -58,28 +56,90 @@ end
 
 open Cmdliner
 
+let compile_only =
+  let default = false in
+  mk ~default Arg.(value & flag & info ["c"; "compile-only"])
+
 let input =
   mk ~default:""
     Arg.(required & pos ~rev:true 0 (some string) None & info [])
 
-
 let output =
   let default = None in
   mk ~default Arg.(value & opt (some string) default & info ["o"; "output"])
 
+let trace =
+  let default = Map.empty (module String) in
+  let parse s =
+    try
+      let index_from s i =
+        Option.merge ~f:min
+          (String.index_from s i '+')
+          (String.index_from s i '-')
+      in
+      let rec split s rev_parts i =
+        match index_from s (i + 1) with
+        | Some j when j = i -> split s rev_parts j
+        | Some j ->
+            split s (String.sub s ~pos:i ~len:(j - i) :: rev_parts) j
+        | _ -> List.rev (String.subo s ~pos:i :: rev_parts)
+      in
+      let parts = split s [] 0 in
+      List.fold parts ~init:default ~f:(fun m part ->
+          let parse_part part =
+            let sign, rest =
+              match part.[0] with
+              | '-' -> (false, String.subo part ~pos:1)
+              | '+' -> (true, String.subo part ~pos:1)
+              | _ -> (true, part)
+            in
+            assert (not (String.is_empty rest)) ;
+            assert (Char.is_uppercase rest.[0]) ;
+            match String.lsplit2 rest ~on:'.' with
+            | Some (mod_name, fun_name) ->
+                assert (Char.is_lowercase fun_name.[0]) ;
+                (mod_name, Some fun_name, sign)
+            | None -> (rest, None, sign)
+          in
+          match parse_part part with
+          | mod_name, Some fun_name, enabled ->
+              let {trace_mod; trace_funs} =
+                match Map.find m mod_name with
+                | Some c -> c
+                | None -> {trace_mod= None; trace_funs= default}
+              in
+              Map.set m ~key:mod_name
+                ~data:
+                  { trace_mod
+                  ; trace_funs=
+                      Map.set trace_funs ~key:fun_name ~data:enabled }
+          | mod_name, None, enabled ->
+              Map.set m ~key:mod_name
+                ~data:{trace_mod= Some enabled; trace_funs= default} )
+      |> fun x -> `Ok x
+    with _ -> `Error ("Invalid trace spec: " ^ s)
+  in
+  let print fs c =
+    let pf fmt = Format.fprintf fs fmt in
+    Map.iteri c ~f:(fun ~key:mod_name ~data:{trace_mod; trace_funs} ->
+        ( match trace_mod with
+        | Some true -> pf "+%s" mod_name
+        | Some false -> pf "-%s" mod_name
+        | None -> () ) ;
+        Map.iteri trace_funs ~f:(fun ~key:fun_name ~data:fun_enabled ->
+            if fun_enabled then pf "+%s.%s" mod_name fun_name
+            else pf "-%s.%s" mod_name fun_name ) )
+  in
+  mk ~default Arg.(value & opt (parse, print) default & info ["t"; "trace"])
 
 let trace_all =
   let default = false in
-  mk ~default Arg.(value & flag & info ["t"; "trace-all"])
-
+  mk ~default Arg.(value & flag & info ["v"; "trace-all"])
 
 let info = Term.info "sledge" ~version:Version.version
-
 let validate () = `Ok ()
 
-;;
-parse info validate
-
 let run main =
-  Trace.init ~trace_all:!trace_all ;
-  main ~input:!input ~output:!output
+  parse info validate ;
+  Trace.init ~config:{trace_all= !trace_all; trace_mods_funs= !trace} () ;
+  main ~input:!input ~output:!output ~compile_only:!compile_only
diff --git a/sledge/src/config.mli b/sledge/src/config.mli
index 5a0fa1518..e83501fe8 100644
--- a/sledge/src/config.mli
+++ b/sledge/src/config.mli
@@ -7,7 +7,8 @@
 
 (** Configuration options *)
 
-val run : (input:string -> output:string option -> 'a) -> 'a
+val run :
+  (input:string -> output:string option -> compile_only:bool -> 'a) -> 'a
 (** [run main] parses command line options, performs some imperative
     initialization, and then executes [main] passing the configuration
     options. *)
diff --git a/sledge/src/sledge.ml b/sledge/src/sledge.ml
index 6a0f345a9..5d717ca6b 100644
--- a/sledge/src/sledge.ml
+++ b/sledge/src/sledge.ml
@@ -7,16 +7,17 @@
 
 (** Sledge executable entry point *)
 
-let main ~input ~output =
+let main ~input ~output ~compile_only =
   try
     let program = Frontend.translate input in
     Trace.flush () ;
     Option.iter output ~f:(function
-      | "-" -> Format.printf "%a@." Llair.fmt program
+      | "-" -> Format.printf "%a@." Llair.pp program
       | filename ->
           Out_channel.with_file filename ~f:(fun oc ->
-              let ff = Format.formatter_of_out_channel oc in
-              Format.fprintf ff "%a@." Llair.fmt program ) ) ;
+              let fs = Format.formatter_of_out_channel oc in
+              Format.fprintf fs "%a@." Llair.pp program ) ) ;
+    if not compile_only then ( Control.exec_pgm program ; Trace.flush () ) ;
     Format.printf "@\nRESULT: Success@."
   with exn ->
     let bt = Caml.Printexc.get_raw_backtrace () in
@@ -32,6 +33,5 @@ let main ~input ~output =
           (Caml.Printexc.to_string exn) ) ;
     Caml.Printexc.raise_with_backtrace exn bt
 
-
 ;;
 Config.run main
diff --git a/sledge/src/version.ml.in b/sledge/src/version.ml.in
index fd5b79aef..cce512956 100644
--- a/sledge/src/version.ml.in
+++ b/sledge/src/version.ml.in
@@ -7,6 +7,5 @@
 
 (** Version information populated by build system *)
 
-let debug = [%debug ]
-
+let debug = [%debug]
 let version = "%%VERSION%%" ^ if debug then "-dbg" else "-opt"
diff --git a/sledge/src/version.mli b/sledge/src/version.mli
index 643480f6f..22b508509 100644
--- a/sledge/src/version.mli
+++ b/sledge/src/version.mli
@@ -8,5 +8,4 @@
 (** Version information populated by build system *)
 
 val debug : bool
-
 val version : string