andriusvelykis / isabelle-eclipse

Eclipse integration for Isabelle proof assistant.
http://andriusvelykis.github.io/isabelle-eclipse
Eclipse Public License 1.0
12 stars 4 forks source link

Slight confusion of Linux x86 and x86_64 #48

Closed makarius closed 11 years ago

makarius commented 11 years ago

Trying to run the x86 version on x86_64 Linux causes the launcher to die -- the Sourceforge download also makes it difficult to distinguish the different variants with their long and unwieldy names.

Strictly speaking the user could be blamed for choosing the wrong platform, but many Linux users don't even know if they have x86 or x86_64. I had the same problem for Isabelle2012 and changed that for Isabelle2013: the default download for Linux is hybrid, able to adapt dynamically to the actual platform. This affects also some fine points about Poly/ML run in x86 mode on x86_64 if that is possible (depending on 32bit C/C++ shared libraries): 32bit Poly/ML is slightly faster and requires much less memory than the 64bit version.

So on x86_64 Linux the best combination is x86_64 for Java and x86 for Poly/ML, if the latter is possible, otherwise x86_64 for Poly/ML, too.

andriusvelykis commented 11 years ago

I would agree that the long names are not very user friendly. To circumvent that, I have updated the upload to place each distribution in a separate directory. This should make it easier to find the correct distribution (see screenshot).

However, I will have to leave the burden of choosing the correct platform to the user. The target platforms are generated by the Eclipse build and I don't think there is an easy way to achieve a hybrid download. See, for example, Eclipse downloads page that lists all possible downloads for user to choose.

About running Poly/ML in 32-bit mode - where is this configuration? I could try replicating it during Isabelle_System initialisation if it is configurable via options, e.g. environment variables.

product-folders

makarius commented 11 years ago

Maybe you should say "linux-32bit" and "linux-64bit" to make it both explicit, otherwise 32bit looks like a default, but most Linux installations these days are actually 64bit by default (without the user knowing it).

The problem of Poly/ML (re)configuration is a different one. It is implicit in the etc/settings of the polyml component. I need to reconsider this on my side, to tell users more explicitly about options and enforced defaults due to lack of shared libraries. (It is similar to Z3_NON_COMMERCIAL, but harder to change from outside.)

andriusvelykis commented 11 years ago

Sure, changed to linux-32bit for Linux.

Leaving windows as-is since 32-bit Java still seems to be the recommended one even on 64-bit Windows? So windows would be somewhat 'default'.


Aren't Isabelle settings read automatically for the given Isabelle distribution during Isabelle_System.init()? I see it uses isabelle getenv -d. If these component settings are read, then Isabelle/Eclipse should be ok as well.. Or is this for reading system environment settings?

makarius commented 11 years ago

Yes, nothing to change on your side for the Isabelle settings environment. You get by default what the component shell script works out for you.

andriusvelykis commented 11 years ago

Thanks - closing the issue then.