Windows 10上的Isabelle HOL

Question

我安装了Windows 10 (64位)。从那时起，伊莎贝尔HOL不再启动，即使在重新安装之后(顺利通过)。错误消息如下：“启动错误:启动Java VM错误”。这发生在我测试的两个版本(2013年-2和2015年)。配置文件中指定的jvm.dll存在于正确的文件夹中。此外，我还在最新版本(8.51)中安装了32位和64位的Java。Windows 10是否存在已知的兼容性问题？伊莎贝尔以前在Windows 7和8上工作，谢谢你的帮助。

Answer 1

最新情况(150822)

在开发人员的邮件列表中，有一个指向测试版本的链接：

• 64-窗口
• 2015年8月21日至

这与Isabelle2015不同，它是如何使用路径来完成某些事情的，所以它可能会找到Windows 10所需的东西，也可能找不到它需要的东西。然而，即使它有效，也可能与Isabelle2015 (在定理证明中)有一些不相容之处。

无论如何，Isabelle每年只发布1到2次，而且我不希望在4到6个月内为Windows 10发布任何特殊的版本。不过，上面的链接表明，M.Wenzel可以打包一个测试版本，但他主要是在用户的邮件列表上操作。

在下面的批处理文件中，我设置了HOMEDRIVE和HOMEPATH，如果您希望.isabelle在C:\user中，则不需要它们。

在这个测试版本中，这些设置不影响我的主路径。它似乎也使用了USER_HOME，尽管我的USER_HOME设置并不能使我的批处理文件在这个测试版本中工作。

无论如何，这个测试版本已经改变了它发现事物的方式，并且可以容纳更多的Windows，如函数路径的新行为所示。

它的工作方式非常不同，并且需要进行足够的更改，所以我应该继续使用Isabelle2015，否则我将无法与官方版本同步。)

原创

(Zeroeth:这类问题通常会在邮件列表中得到处理，但我继续向您展示如何使用批处理文件启动Isabelle，在开始之前我就开始这样做了。)

首先，Isabelle使用的Java位于这个文件夹中：

Isabelle2015\contrib\jdk\x86-cygwin\jre

为Windows执行正常的Java安装不会改变Isabelle使用的Java。

下面，我将为您提供一个批处理文件和bash文件来启动Isabelle/jEdit，这是使用Isabelle2015\Isabelle2015.exe的另一种选择。

对于我自己来说，我所做的就是用jre-8u45-windows-x64.tar.gz中的jre手动替换上面显示的32位jre文件夹。(我重命名了旧的32位文件夹。最近的Java文件可以找到在下载页)。

因此，如果我尝试用Isabelle2015.exe启动伊莎贝尔，我也会得到一个弹出窗口，上面写着“启动错误，启动Java时出错”，但是在Windows8.1上，使用批处理/bash组合启动Isabelle是有效的。

下面我向您展示的内容可能并不能解决您的问题，但我想Isabelle2015.exe必须从操作系统获得一些信息才能正常工作，也许Windows 10已经改变了这一点：

https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2014-December/msg00033.html

您可以将批处理和bash文件放在您拥有或想要的.isabelle文件夹中。将下面的ISAHOME更改为您的伊莎贝尔发行版所在的位置。PATH需要路径中的Cygwin bin，以及我在批处理文件中设置的isabelle路径。

文件: start-isabelle.bat

:: Isabelle2015.exe uses these directly. Setting HOME or USER_HOME doesn't work
set HOMEDRIVE=%~d0
set HOMEPATH=%~p0

:: Cygwin uses HOME, and this is how HOME is set in Cygwin-Terminal.bat
set HOME=%HOMEDRIVE%%HOMEPATH%

:: ADD PATHS: 'cygwin/bin' to start terminal, 'Isabelle2015/bin' for 'isabelle'
set ISAHOME=E:\E_2\d ev\Isabelle2015
set PATH=%PATH%;%ISAHOME%/contrib/cygwin/bin;%ISAHOME%/bin;

set CHERE_INVOKING=true
::MINTTY CONSOLE
start /MIN mintty.exe -i /Cygwin-Terminal.ico "%~dp0start-isabelle.bash"

:: REGULAR WINDOWS CONSOLE
::bash --login -i "%~dp0start-isabelle.bash"

文件: start-isabelle.bash

#!/usr/bin/env bash
#
isabelle jedit -l HOL

使用64位的Java，我可以通过在.isabelle\Isabelle2015\etc\settings中进行这种更改来增加伊莎贝尔使用的内存的大小。

JEDIT_JAVA_OPTIONS="-Xms1g -Xmx4g -Xss4m"
  or
JEDIT_JAVA_OPTIONS="-Xms1024m -Xmx4096m -Xss4m"

使用32位Java，当我这样做时，Isabelle将启动，然后终止。