Closed mtzguido closed 5 years ago
Made these changes and updated the PR. I also changed F*'s CLI output to more closely match fstar-mode (which was undoubtedly doing a better job). Here's the test file:
module Labels
open FStar.Tactics
let _ = assert (True /\ (True /\ True)) by (explode (); iseq [(fun () -> tlabel "Left"); (fun () -> tlabel "Right")]; dump "dump msg")
The CLI output
proof-state: State dump @ depth 0 (dump msg):
Location: Labels.fst(5,118-5,133)
Goal 1/3 (Left):
|- _ : Prims.squash Prims.l_True
Goal 2/3 (Right):
|- _ : Prims.squash Prims.l_True
Goal 3/3:
|- _ : Prims.squash Prims.l_True
Verified module: Labels (110 milliseconds)
All verification conditions discharged successfully
and emacs
Feel free to squash both commits into one, or I can do that too. Can you point me to the docs so I can update them?
Gentle ping. Did we merge this without closing the PR?
Hey Clément. Indeed, I messed up and pushed to master instead of to my branch. I had left a comment in a review, but I now see I didn't hit "submit" so you couldn't see them, sorry :(.
We're all good :)
Support for a new feature incoming in Meta-F*: goal labels. They're just a way for users to keep track of the goals by adding custom messages, and get displayed when a goal fails to be solved by SMT as well. I just copied the formatting from the witness, but please feel free to choose a better one!
(I haven't yet looked at those other issues again.. sorry)