Bindings escape ```proof_subshell```

[sauclovian-g]

Create foo.saw containing the following:

enable_experimental;

let foo () = do {
   prove_print do {
      proof_subshell ();
   } {{ True }};
};

let bar () = do {
   print {{ quack }};
};

foo ();
bar ();

Run it in saw, and when it starts the interactive proof subshell, do the following:

proof (1)> let quack = {{ 3 : [8] }}
proof (1)> trivial
proof (0)> ^D

It will then print

[22:42:44.165] 3

instead of failing on the theoretically unbound variable quack.

Note that print quack rather than print {{ quack }} fails, but that's because of saw's phase distinctions and not because the interpreter isn't also messing up the saw-script-level binding environment. If you call foo before declaring bar, then quack leaks into the environment before bar is typechecked and you can successfully do print quack as well.

I discovered this while investigating #2242, but it isn't (directly) related to it.

[sauclovian-g]

Note that we should try to figure out how to rig up a test case for this. It might be adequate to do something of the form (echo foo; echo bar) | saw test.saw, especially if we don't care about crosschecking the output.

If that works out, add a test case for #2242 as well.

[sauclovian-g]

The same thing happens with an "ordinary" subshell (the subshell command):

sawscript> enable_experimental 
sawscript> let f () = do { subshell (); print "(exit)"; return (); }
sawscript> let x = 3
sawscript> f ()
sawscript> let x = 5
sawscript> ^D
[02:09:56.331] (exit)
sawscript> return x
[02:09:59.548] 5
sawscript>