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

[Jason K. <ja...@cs...>]

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.