Weirdness with tactic failures and --trace_error

[mtzguido]

open FStar.Tactics.V2

[@@expect_failure]
let _ = assert True by begin
  fail "fail"
end

let _ = assert True by begin
  fail "fail"
end

This module rightly fails:

$ ./bin/fstar.exe Bug.fst 
proof-state: State dump @ depth 0 (at the time of failure):
Location: Bug.fst(7,2-7,13)
Goal 1/1:
 |- _ : Prims.squash Prims.l_True

proof-state: State dump @ depth 0 (at the time of failure):
Location: Bug.fst(11,2-11,13)
Goal 1/1:
 |- _ : Prims.squash Prims.l_True

* Error 228 at Bug.fst(10,8-10,14):
  - Tactic failed
  - fail
  - See also Bug.fst(11,2-11,13)

1 error was reported (see above)

But ends up claiming success if --trace_error is given...

$ ./bin/fstar.exe Bug.fst --trace_error 
proof-state: State dump @ depth 0 (at the time of failure):
Location: Bug.fst(7,2-7,13)
Goal 1/1:
 |- _ : Prims.squash Prims.l_True

Verified module: Bug
All verification conditions discharged successfully

Of course it didn't actually check the second tactic, but it's worrisome still. I think this may be stopping since we have logged an error in the first definition, so the second tactic is prevented from running. But in no case should we report success.

[mtzguido]

This is caused since when we run tactics to simplify a goal, we temporarily disable tactics by

    if Options.use_tactics() then begin
      Options.with_saved_options (fun () ->
        ignore <| Options.set_options "--no_tactics";
        ...
    )

And with_saved_options is defined like so, and will not pop the stack if an exception is raised with --trace_error, so the checking of the second let has tactics off, and rightfully succeeds since it's just an assert True essentially.

let with_saved_options f =
  // take some care to not mess up the stack on errors
  // (unless we're trying to track down an error)
  // TODO: This assumes `f` does not mess with the stack!
  if not (trace_error ()) then begin
      push ();
      let r = try Inr (f ()) with | ex -> Inl ex in
      pop ();
      match r with
      | Inr v  -> v
      | Inl ex -> raise ex
  end else begin
      push ();
      let retv = f () in
      pop ();
      retv
  end

The reason for this if is to not mess up the trace on the exception. It would be great to find a different way to do this, for instance maybe we can catch the exception and re-raise it with the same stack trace, if OCaml supports that. The raise_with_backtrace function here seems promising, but I don't see how to get the backtrace from an exception.