Printing tactics position info

[mtzguido]

Hey Clément!

Recently I added some ranges to the proofstate dumps pointing to where the call was made. It's in the JSON as .contents.position, could we make it display in emacs? I have a crappy local modification to print it, but it's a mess.

Best, Guido

[cpitclaudel]

Hey Guido!

Sure thing :) I remember we had chatted about this. It would be lovely to have it. It shouldn't be too hard, either. Before I start though, there's code at https://github.com/FStarLang/FStar/blob/master/src/fstar/FStar.Interactive.Ide.fs#L643-L668 to serialize ranges (instead of converting them to strings), and corresponding code to navigate to them on the Emacs side. Can you move these methods out of Ide.fs and use them for serialization?

Also, we should remember to update the protocol docs.

[mtzguido]

Done in guido_tactics and coming to master soon.

[mtzguido]

By the way, I'm sure you thought of it, but having some way of scrolling through these positions, and having them highlighted, would be awesome. Also using the depths in the proofstate the user could choose the granularity of the steps to take.

[cpitclaudel]

I actually haven't given it too too much thought, so your thoughts are very welcome indeed :)

[cpitclaudel]

Two more things: it would probably be good to add a new capability to the capability list ("features") in the protocol-info message, and I noticed that dump calls produce a dummy range (I think it'd be better if they just didn't include the location information at all, rather than a dummy)

[cpitclaudel]

Also, in the rest of the protocol, location arguments tend to be called "location", rather than "position". not sure how much this matters, but consistency might be nice

[mtzguido]

To make sure I understood the capability bit: you mean add a flag there, "tactic-range" or something, which would mean this version of F* will give you ranges on dumps? If so, sounds good.

They shouldn't print dummy ranges anymore, I fixed that recently (~1 day ago). If that was on a current master please send me a repro (I guess there could be some corner case, but most of them should have their range).

I can rename it to location. I'll do both things tonight.

[cpitclaudel]

To make sure I understood the capability bit: you mean add a flag there, "tactic-range" or something, which would mean this version of F* will give you ranges on dumps? If so, sounds good.

Yup

They shouldn't print dummy ranges anymore, I fixed that recently (~1 day ago). If that was on a current master please send me a repro (I guess there could be some corner case, but most of them should have their range).

Here's one:

let a =
  assert_by_tactic True
    (fun () -> (dump "A"))

I can rename it to location. I'll do both things tonight.

Thanks!

[cpitclaudel]

I pushed a prototype. It should "just work" once you rename .position to .location :)

[mtzguido]

I just tried it out, really cool! I made the changes, I'm trying to push to master now.

The ranges are not perfect as you noticed, tactics are annotated with ranges on let-bindings, so that standalone dump won't get anything meaningful. I don't yet know if I can add ranges to everything easily, but that'd be great.

[cpitclaudel]

Indeed, ranges on everything would be very nice :) I haven't implemented depth-related navigation yet, as you saw. How hard would it be to get a backtrace? Take the following example:

let tC () : Tac unit =
  idtac (); idtac ()

let tB () : Tac unit =
  idtac (); tC ()

let tA () : Tac unit =
  idtac (); tB()

let a' =
  assert_by_tactic True
    (fun () -> tA ())

(btw, I noticed that all messages have depth one in that example). It would be great for the first message to have stack: [assert_by_tactic], the second one stack: [assert_by_tactic, tA], the third one stack: [assert_by_tactic, tA, tB], etc.

[mtzguido]

I'm not sure how hard that is, I still need to give it some thought. It's tricky, since it means we're going to distinguish terms from their definitions, unlike this Tm_let trick which is completely static (and thus extractable!).

Same for the depth, it's also done via Tm_let. Those all have depth 1 since there's no left-nesting. If you had defined tB and tA with the sequence reversed you'd see it increasing.

[cpitclaudel]

Understood :)

[cpitclaudel]

This feature seems to work pretty well, so I'll close this. Please do open a new ticket if you get around to doing backtraces, though :)