Problem loading UC file in Proof General, UC DSL Interpreter mode

[uguryavuz]

There seems to a problem when UC DSL Interpreter is started by Proof General via "process the next proof command". When running uc-dsl/examples/smc2/testing.uci in Emacs, this is what I observe after processing the load line.

I cannot process the file further, getting a "parse error."

The issue is not present if the Interpreter has been launched beforehand, nor on the command line.

[alleystoughton]

Note that this user is running macOS on an M1 Mac, and using the GUI version of Emacs (just like me, and I'm not getting this behavior). Somehow the text *** no code running *** which should be in the *UC file frame is ending up in the *uc dsl interpreter* buffer after the initial load.

[alleystoughton]

OK, the user confirms that running open -a emacs testing.uci doesn't cause the problem. The problem occurs if one starts up emacs and then types C-x C-f RET and completes the path to testing.uci. Then the frame names are messed up. This weirdness doesn't occur with EasyCrypt's proof general code.

[alleystoughton]

This problem comes up for me if I first visit a .uc file, and then do C-x C-f RET and select a .uci file. The main frame is then called *UC file*. When the initial load is done, then the text *** no code running *** is put in the *uc dsl interpreter* buffer.

[alleystoughton]

Something is still not quite right here. If I start emacs, and then visit smc2/testing.uci, I get the following frames:

ucdsl-file-buffer has also been created, but I have to bring it manually up. Things then work, but this isn't ideal.

[alleystoughton]

Despite fix, still getting behavior in previous screenshots.