Hi all, xtla begins to have a lot of features. Many are still missing, but it's also time to improve the existing.
Since some tla operations can be slow, we must do our possible to let the user continue working while running tla. This means two things : 1) Run tla asynchronously whenever possible 2) Allow several processes to be exectued at a time. The first is already done for most commands, and will be easy to apply to the other ones. The second is much more difficult to accomplish. I've tried writting my code in a way that wouldn't prevent this, but clearly, it's not possible currently since all process would share the output buffer ! I think we should forbid running commit while any other tla process is executing, but I'd really like to be able to update two local trees at a time for example. I currently find myself too often running tla from the command line because my Emacs is running another process ... Any ideas, remarks ? -- Matthieu
