Can only evaluate once?

[catalin-hritcu]

It seems that I can only evaluate once? If I do it again I get this:

Evaluation of [run_tm (as_arith_expr (expr_to_term (Neg (Lit 42))))] failed: <input>(0,4-0,21): (Error 47) Duplicate top-level names [CanonDeep.__compute_dummy__]; previously declared at <input>(0,4-0,21)

Is this a known issue?

[cpitclaudel]

Nope, and since all the tests interactive mode tests seem to pass, it'd help to have a repro :)

[s-zanella]

I can reproduce by just evaluating () twice:

;;; Started F* interactive: ("***/everest/FStar/bin/fstar.exe" "***/M.fst" "--ide" "--smt" "***/everest/z3-4.5.1.1f29cebd4df6-x64-osx-10.11.6/bin/z3")
{"kind":"protocol-info","version":2,"features":["autocomplete","autocomplete/context","compute","compute/reify","compute/pure-subterms","describe-protocol","describe-repl","exit","lookup","lookup/context","lookup/documentation","lookup/definition","peek","pop","push","search","segment","vfs-add"]}
;;; Complete message received: (status: nil; message: ((kind . "protocol-info") (version . 2) (features "autocomplete" "autocomplete/context" "compute" "compute/reify" "compute/pure-subterms" "describe-protocol" "describe-repl" "exit" "lookup" "lookup/context" "lookup/documentation" "lookup/definition" "peek" "pop" "push" "search" "segment" "vfs-add")))
;;; [23.15ms] Feature list received
;;; Processing queue
>>> {"query-id":"1","query":"vfs-add","args":{"filename":null,"contents":"module M\n\n"}}
>>> {"query-id":"2","query":"push","args":{"kind":"full","code":"module M\n","line":1,"column":0}}
{"kind":"response","query-id":"1","status":"success","response":null}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "1") (status . "success") (response . :json-null)))
{"kind":"response","query-id":"2","status":"success","response":[]}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "2") (status . "success") (response)))
;;; Queue is empty (1 overlays)
>>> {"query-id":"3","query":"compute","args":{"term":"()","rules":["beta","delta","iota","zeta","reify","pure-subterms"]}}
{"kind":"response","query-id":"3","status":"success","response":"()"}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "3") (status . "success") (response . "()")))
;;; Queue is empty (1 overlays)
>>> {"query-id":"4","query":"compute","args":{"term":"()","rules":["beta","delta","iota","zeta","reify","pure-subterms"]}}
{"kind":"response","query-id":"4","status":"failure","response":"<input>(0,4-0,21): (Error 47) Duplicate top-level names [M.__compute_dummy__]; previously declared at <input>(0,4-0,21)\n"}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "4") (status . "failure") (response . "<input>(0,4-0,21): (Error 47) Duplicate top-level names [M.__compute_dummy__]; previously declared at <input>(0,4-0,21)
;;; ")))
;;; Queue is empty (1 overlays)

[cpitclaudel]

Oh, I misunderstood "evaluate". Thanks. The bug is likely in the implementation of

let run_and_rewind st task =
  let env' = push st.repl_env "#compute" in
  let results = try Inl <| task st with e -> Inr e in
  pop env' "#compute";
  match results with
  | Inl results -> (results, Inl st)
  | Inr e -> raise e

But I can't quite spot what's wrong with that. @nikswamy?

[cpitclaudel]

Looks like the sigmap isn't being rolled back

[cpitclaudel]

Fixes in https://github.com/FStarLang/FStar/pull/1399, thanks.