Misc debugging improvements

src/basic/FStar.Errors.Msg.fst

@@ -31,7 +31,7 @@ let renderdoc (d : document) : string =
 let backtrace_doc () : document =
   let s = stack_dump () in
   text "Stack trace:" ^/^
-  arbitrary_string s
+  arbitrary_string (trim_string s)
 
 let subdoc d =
   (* NOTE: slight hack here, using equality on Pprint documents. This works

src/basic/FStar.Errors.fst

@@ -464,7 +464,14 @@ let lookup err =
   | _ ->
     with_level level
 
+let maybe_add_backtrace (msg : error_message) : error_message =
+  if Options.trace_error () then
+    msg @ [backtrace_doc ()]
+  else
+    msg
+
 let log_issue_ctx r (e, msg) ctx =
+  let msg = maybe_add_backtrace msg in
   match lookup e with
   | (_, CAlwaysError, errno)
   | (_, CError, errno)  ->
@@ -517,10 +524,10 @@ let stop_if_err () =
     then raise Stop
 
 let raise_error_doc (e, msg) r =
-  raise (Error (e, msg, r, error_context.get ()))
+  raise (Error (e, maybe_add_backtrace msg, r, error_context.get ()))
 
 let raise_err_doc (e, msg) =
-  raise (Err (e, msg, error_context.get ()))
+  raise (Err (e, maybe_add_backtrace msg, error_context.get ()))
 
 let raise_error (e, msg) r =
   raise_error_doc (e, mkmsg msg) r

src/basic/FStar.Options.fst

@@ -1242,7 +1242,7 @@ let rec specs_with_types warn_unsafe : list (char * string * opt_type * Pprint.d
   ( noshort,
     "trace_error",
     Const (Bool true),
-    text "Don't print an error message; show an exception trace instead");
+    text "Attach stack traces on errors");
 
   ( noshort,
     "ugly",

src/syntax/FStar.Syntax.Print.fst

@@ -1007,3 +1007,4 @@ instance showable_binding = {
           | Binding_univ x -> "Binding_univ " ^ show x);
 }
 instance showable_pragma = { show = pragma_to_string; }
+instance showable_subst_elt = { show = subst_elt_to_string; }

src/syntax/FStar.Syntax.Print.fsti

@@ -105,3 +105,4 @@ instance val showable_uvar      : showable uvar
 instance val showable_ctxu      : showable ctx_uvar
 instance val showable_binding   : showable binding
 instance val showable_pragma    : showable pragma
+instance val showable_subst_elt : showable subst_elt