Re: [Rodin-b-sharp-user] Running Rodin in a Virtual Machine

[Andy <ae...@ec...>]

Hi Jason,

it might not be obvious, especially if you haven't installed Rodin 
(often) before; Make sure you remember to install the Atelier-B provers 
in the VM (from the update-site, available through the help/install new 
software menu). They are not installed by default, and this would 
certainly explain the behaviour you describe in the VM.

regards,
Andy

On 13/08/14 20:29, Jason Keltz wrote:
> Hi.
> I've been asked to create a virtual image for a software engineering
> course which includes various software including Rodin.  The virtual
> machine O/S is Linux/CentOS 6.5.  As I'm not a Rodin user, I've been
> given a very basic project example to use to test that Rodin is working
> in the VM.  While the software seems to be mostly working in the VM,
> testing has turned up 1 issue that I cannot seem to resolve.  When I
> import the sample project that I've been given, go into the "Proving"
> perspective, prune the proof, then click on the "robot"  ("Run auto
> provers"), I get back a sad face and "loopOnAllPending: All tactics
> failed".  If I run the identical test on our non-VM CentOS system, it
> works perfectly.  I've tried the 32 bit version of Rodin and the 64 bit
> version with the identical problem in the VM.  I've ensured that both
> the VM and the standard CentOS 6.5 system have the same
> dependencies/libraries.  I've removed the "workspace" directory, and
> started fresh on both systems.  I checked for a .log file in the
> workspace .metadata directory, but can't find one.   I was hoping this
> might help debug the issue.  I've tried to "clean" the project, which
> doesn't help. I've looked at the binaries to see if there are any
> missing system libraries, and there are not.  I've searched the list
> archives, though I can't seem to find anything related to this problem.
> I've tried the IRC channel, #rodin, but unfortunately, there was nobody
> there.
>
> In all fairness, it's entirely possible that there's a bug in
> VirtualBox, but if this is the case, I'd really like to be able to get
> more details on the bug so that I could submit it to the VirtualBox bug
> system.  On the other hand, if there's any easy solution, I'd love to be
> able to implement it.    This is difficult for me to debug since I don't
> know anything about Rodin.  I wonder if, as a start, someone might be
> able to tell me how to get Rodin to produce more debugging output so
> that I can see where the process is really failing when the "All tactics
> failed" message appears. Alternatively, I can privately distribute a
> link to the 8 GB OVA file, and the sample that I've been asked to use
> for quick testing. The truth is, several other Rodin users have tested
> the virtual environment with their own code, and get the same behaviour,
> so there's nothing unique to the sample that I've been given.   Any help
> would be greatly appreciated.  I'm trying to finalize this image for a
> course that starts very soon.   Helping me solve the problem will put
> Rodin in our students hands, leading to better code everywhere :)
>
> Thanks in advance for any help that you can provide!
>
> Jason.
>
> ------------------------------------------------------------------------------
> _______________________________________________
> Rodin-b-sharp-user mailing list
> Rod...@li...
> https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user