Can't find mutually recursive function in interactive mode

[catalin-hritcu]

I'm getting Identifier not found errors for mutually defined functions in the emacs mode (only):

To reproduce this take any mutual fixpoint let rec ... and ... (for instance examples/bug-reports/bug442.fst), feed the val declarations to F*, but not the let rec. Then feed the let rec. There might be more circumstances / steps to reproduce this, but I manage very often without even trying too hard :)

[cpitclaudel]

Running through bug 442 doesn't trigger the issue for me; I get a type error on "rights" instead:

Expected expression of type "(list (dList (?75497 'a 't rights l xs f)))"; got expression "rights" of type "(list (dList 't))" (see <input>(40,13-40,19))

Looks like you got that too? What's the trick to get the Identifier not found?

I tried this, too, but it worked just fine:

val f: nat -> nat
val g: nat -> nat

let rec f x = if x > 0 then g (x - 1) else 0
and g x = if x > 0 then f (x - 1) else 0

Can you run fstar-toggle-debug, reproduce the bug, and then paste the output of the *fstar-debug* buffer?

(Unrelated, but it might make debugging easier to update your fstar-mode. The errors in the Message buffer suggest it's outdated).

[cpitclaudel]

I think this may have been an issue with buffer segmentation. I rewrote this part a month or so ago, so assuming fixed. Please reopen if not :)