extracting tactics and proof terms

Stream: new members

[Michael Jendrusch]

This is probably a question with a simple answer, but I'll ask it either way. Is there a way to programmatically extract the sequence of tactics used to prove a given lemma? I can get the proof term pretty easily by doing something like this:

import tactic
open tactic.interactive

namespace my_namespace

lemma my_lemma : Π n : ℕ, n + 1 > n :=
begin
  intros,
  rw gt,
  simp,
  comp_val,
end

#eval do
  env ← tactic.get_env,
  ml  ← env.get(mk_str_name "my_namespace" "my_lemma"),
  fmt ← tactic_format_expr ml.value,
  trace $ "type  : " ++ (to_string $ expr.to_raw_fmt ml.type) ++ "\n",
  trace $ "value : " ++ (to_string $ expr.to_raw_fmt ml.value) ++ "\n",
  return unit.star

end my_namespace

but I haven't had any luck extracting tactics yet. On another note, is there some function other than expr.to_raw_fmt for serializing expressions?

[Mario Carneiro]

No. It's not stored

[Keeley Hoek]

What do you mean "serializing"?

[Michael Jendrusch]

Serializing, as in generating some text (s-expression, JSON) or binary representation of expressions which can be read from another program. But I suppose expr.to_raw_fmtshould be enough for my purposes.