Re: [Rodin-b-sharp-user] Unresolved problems with Rodin

[Laurent V. <lpv...@gm...>]

Dear Ken,

I'm sorry I didn't answer earlier.  I was on holiday last week and we  
had the Deploy project annual review with the European Commission this  
week.

I (and others at Systerel) tried to reproduce your problems with your  
projects, but we didn't succeed.  The log files you sent were  
unfortunately not tracing anything important and that could be related  
to your problems.

Le 4 mars 09 à 13:46, Ken Robinson a écrit :

> Your answer is interesting.  Laurent has agreed with me that the
> problem is almost certainly a problem with the tool itself and not
> with the projects under which it appears.

And I still agree.

>> I can only suggest tou  to do a refresh and clean, but I'm afraid it
>> won't be sufficient.
>> As a last resort, you may delete all files other than .bum and .buc
>> and do a projet/clean (but beware you'll lost all you proof work by
>> doing so).
>
> You will see that just before your mail arrived I sent an email
> describing an (unclear) sequence of actions that at least fix the
> explorer problem.
>
> That was achieved without changing any machine or conext, suggesting
> that the radical surgery you suggest is not necessary.  It shows that
> the explorer is quite flaky.  There are more extreme problem, probably
> connected with the errors that appear in the log that demonstrate more
> extreme problems with the explorer's display of PO status.  In some
> cases the display is simply incorrect.

Yes, it seems that the explorer can sometimes display proof  
obligations that have disappeared in the database since (this is the  
meaning of the last error messages in your log).

Shall this happen again, a workaround would be to restart the platform  
(as the explorer is not persisting any information between to launches  
of the platform).

> My main reason for writing to this forum is not to bombard you people
> with my problems, but to get some information on whether the problems
> are being addressed.
>
> There is nothing worse than teaching something like EventB using a
> toolkit that is buggy.
>
> If there is no plan to fix this problem I will simply have to explain
> the situation to the students, and unfortunately EventB will lose some
> of its shine.

Ken, we're definitely committed to have a very usable platform.  This  
is even more true for Systerel, where the Rodin platform is mission- 
critical in two system modelling projects, where it is used daily.

I've already put someone to work on this synchronisation problem  
between the database and the project explorer since yesterday.

Laurent.