search

easyuc / EasyUC

Experiments with Universal Composability in EasyCrypt
30 stars 1 forks source link

race condition when proof general starts up #29

Closed alleystoughton closed 11 months ago

alleystoughton commented 11 months ago

When proof general starts up, and a load is done, I sometimes find that the var command in

load SMC2.
functionality
  SMC2.SMC2Real
  (SMC.SMCReal(KeyExchange.KEReal),
  SMC.SMCReal(KeyExchange.KEReal)).
var text : text.

fails, saying text was already added. But when I redo the load, it works. I guess this is a proof general thing where the addition of the variable was run through the interpreter, but proof general doesn't know it should have advanced past it.

01tomislav commented 11 months ago

This only happens when opening the uci file for the second time in the same emacs session. I noticed that quitting emacs between opening uci files prevents this from happening.

01tomislav commented 11 months ago

I could not reproduce the race condition. However, same errors happen when uc-frame is deleted (red x button clicked). Somehow selecting a deleted frame does not result in exception, instead the code that fills current buffer, which should be the buffer shown in uc-frame, instead fills script buffer, and we get parsing exception from ucInterpreter. The ucInterpreter.el now checks if uc-frame is among the living frames before any buffer changes are made. Please see if this also solves race condition. Note that once uc-frame is deleted it will never be resurrected (we assume the user does not want to look at uc code).

alleystoughton commented 11 months ago

I still have the race condition, but I don't think this is a problem. The user will learn to let the first load bring up the UC file frame before continuing.