Email Gateway (Oct 19 2022 at 08:42): Email Gateway (Oct 19 2022 at 08:42):From: Minh Christian Tran <mctran312@gmail.com>
Hi,
I am having problems running Isabelle on windows 10 and am wondering if you
could help me out.
I just downloaded Isabelle2021-1.exe from
https://isabelle.in.tum.de/installation.html and then unpacked it when it
was done. This is what I get when I run Isabelle
[image: image.png]
Thanks in advance
image.png
Email Gateway (Oct 19 2022 at 09:34):From: Makarius <makarius@sketis.net>
Can you try Isabelle2022? It is presently approximated by Isabelle2022-RC4 and
will become final next week:
https://isabelle.sketis.net/website-Isabelle2022-RC4
Makarius
Email Gateway (Oct 19 2022 at 11:06):From: Makarius <makarius@sketis.net>
So how about Isabelle2021 (not Isabelle2021-1)?
Makarius
Email Gateway (Oct 19 2022 at 14:18):From: Makarius <makarius@sketis.net>
OK. Next experiment:
* Open the unpacked directory of Isabelle2022-RC4
* Edit the file Isabelle2022-RC4.lj4 and add a line: -Disabelle.debug=true
* Now start Isabelle2022-RC4.exe as before. With some luck we get an
informative exception trace in the dialog window.
The exception is probably java.nio.charset.MalformedInputException, which has
to do with bad UTF8 encoding of text. E.g. see
http://biercoff.com/malformedinputexception-input-length-1-exception-solution-for-scala-and-java
Makarius
Email Gateway (Oct 19 2022 at 14:36):From: Minh Christian Tran <mctran312@gmail.com>
I tried the 2022 version as well but still got the same error, however,
when I tried the 2020 version it worked fine.
ons. 19. okt. 2022 kl. 11:34 skrev Makarius <makarius@sketis.net>:
Email Gateway (Oct 19 2022 at 14:36):From: Minh Christian Tran <mctran312@gmail.com>
Yes, it works.
ons. 19. okt. 2022 kl. 13:05 skrev Makarius <makarius@sketis.net>:
Email Gateway (Oct 19 2022 at 18:28):From: Makarius <makarius@sketis.net>
OK, never mind. We shall try something else.
The exception reported here is a plugin start-error: Somehow bad UTF-8 text
gets in the way while loading one of the two Isabelle/jEdit plugins.
Since the plugins are copied into your local $ISABELLE_HOME_USER directory on
startup, something encoding-critical might be going on over there. What is the
result of the following command in the Cygwin-Terminal?
isabelle getenv HOME USER_HOME ISABELLE_HOME_USER
Moreover, with some luck we may actually see the exception trace in the
activity.log of jEdit: it can be browsed within Isabelle/jEdit via the menu
"Utilities / Troubleshooting / Activity log".
Makarius
Email Gateway (Oct 19 2022 at 21:11):From: Makarius <makarius@sketis.net>
On 19/10/2022 22:30, Minh Christian Tran wrote:
This is what i get in the Cygwin-Terminal:
This looks fine.
As for what you want me to do in Isabelle/jEdit, I get the problem when I try
to open it so I'm afraid I can't do anything about it unless you want me to
use a version that works e.g. the 2021 and 2020
We need the activity.log from one of the bad versions. Do you see an exception
trace here?
C:\Users\minh\.isabelle\Isabelle2022-RC4\jedit\activity.log
Makarius
Email Gateway (Oct 20 2022 at 09:35):From: Minh Christian Tran <mctran312@gmail.com>
Hello,
I edited the Isabelle2022-RC4.lj4 file as you said, but still get the same
error message I got earlier.
[image: image.png]
[image: image.png]
ons. 19. okt. 2022 kl. 16:17 skrev Makarius <makarius@sketis.net>:
image.png
image.png
Email Gateway (Oct 20 2022 at 09:35):From: Minh Christian Tran <mctran312@gmail.com>
This is what i get in the Cygwin-Terminal:
[image: image.png]
As for what you want me to do in Isabelle/jEdit, I get the problem when I
try to open it so I'm afraid I can't do anything about it unless you want
me to use a version that works e.g. the 2021 and 2020, in which I get this:
- 22:25:09 [main] [message] Log: When reporting bugs, please include the
following information:
- 22:25:09 [main] [message] Log: java.version=15.0.2
- 22:25:09 [main] [message] Log: java.vm.version=15.0.2+7
- 22:25:09 [main] [message] Log: java.vm.name=OpenJDK 64-Bit Server VM
- 22:25:09 [main] [message] Log: java.runtime.version=15.0.2+7
- 22:25:09 [main] [message] Log: java.runtime.name=OpenJDK Runtime
Environment
- 22:25:09 [main] [message] Log: java.vendor=Azul Systems, Inc.
- 22:25:09 [main] [message] Log: java.compiler=null
- 22:25:09 [main] [message] Log: os.name=Windows 10
- 22:25:09 [main] [message] Log: os.version=10.0
- 22:25:09 [main] [message] Log: os.arch=amd64
- 22:25:09 [main] [message] Log: user.home=C:\Users\minh
- 22:25:09 [main] [message] Log:
java.home=C:\Isabelle\Isabelle2021\contrib\jdk-15.0.2+7\x86_64-windows
- 22:25:09 [main] [message] Log:
java.class.path=C:\Isabelle\Isabelle2021\lib\classes\Pure.jar;C:\Isabelle\Isabelle2021\contrib\flatlaf-1.0\lib\flatlaf-1.0.jar;C:\Isabelle\Isabelle2021\contrib\jfreechart-1.5.1\lib\iText-2.1.5.jar;C:\Isabelle\Isabelle2021\contrib\jfreechart-1.5.1\lib\jfreechart-1.5.1.jar;C:\Isabelle\Isabelle2021\contrib\jortho-1.0-2\jortho.jar;C:\Isabelle\Isabelle2021\contrib\kodkodi-1.5.6\jar\antlr-runtime-3.1.1.jar;C:\Isabelle\Isabelle2021\contrib\kodkodi-1.5.6\jar\kodkod-1.5.jar;C:\Isabelle\Isabelle2021\contrib\kodkodi-1.5.6\jar\kodkodi-1.5.6.jar;C:\Isabelle\Isabelle2021\contrib\kodkodi-1.5.6\jar\sat4j-2.3.jar;C:\Isabelle\Isabelle2021\contrib\postgresql-42.2.18\postgresql-42.2.18.jar;C:\Isabelle\Isabelle2021\contrib\scala-2.13.4-1\lib\jline-3.16.0.jar;C:\Isabelle\Isabelle2021\contrib\scala-2.13.4-1\lib\jna-5.3.1.jar;C:\Isabelle\Isabelle2021\contrib\scala-2.13.4-1\lib\scala-compiler.jar;C:\Isabelle\Isabelle2021\contrib\scala-2.13.4-1\lib\scala-library.jar;C:\Isabelle\Isabelle2021\contrib\scala-2.13.4-1\lib\scala-parallel-collections_2.13-1.0.0.jar;C:\Isabelle\Isabelle2021\contrib\scala-2.13.4-1\lib\scala-parser-combinators_2.13-1.1.2.jar;C:\Isabelle\Isabelle2021\contrib\scala-2.13.4-1\lib\scala-reflect.jar;C:\Isabelle\Isabelle2021\contrib\scala-2.13.4-1\lib\scala-swing_2.13-2.1.1.jar;C:\Isabelle\Isabelle2021\contrib\scala-2.13.4-1\lib\scala-xml_2.13-1.3.0.jar;C:\Isabelle\Isabelle2021\contrib\scala-2.13.4-1\lib\scalap-2.13.4.jar;C:\Isabelle\Isabelle2021\contrib\sqlite-jdbc-3.34.0\sqlite-jdbc-3.34.0.jar;C:\Isabelle\Isabelle2021\contrib\ssh-java-20190323\lib\jsch-0.1.55.jar;C:\Isabelle\Isabelle2021\contrib\ssh-java-20190323\lib\jzlib-1.1.3.jar;C:\Isabelle\Isabelle2021\contrib\ssh-java-20190323\lib\jce.jar;C:\Isabelle\Isabelle2021\contrib\xz-java-1.8\lib\xz.jar;C:\Isabelle\Isabelle2021\contrib\naproche-755224402e36\Isabelle\naproche.jar;C:\Isabelle\Isabelle2021\src\Tools\jEdit\dist\jedit.jar
- 22:25:09 [main] [message] jEdit: starting with command line arguments:
-settings=C:\Users\minh\.isabelle\Isabelle2021\jedit -server=Isabelle2021
-reuseview -nobackground -nosplash -log=9 C:\Users\minh\Scratch.thy
- 22:25:09 [main] [debug] jEdit: before splash screen activation:331 ms
- 22:25:09 [main] [debug] jEdit: after splash screen activation:346 ms
- 22:25:09 [main] [debug] MiscUtilities: Saving backup of file
"C:\Users\minh\.isabelle\Isabelle2021\jedit\activity.log" to
"C:\Users\minh\.isabelle\Isabelle2021\jedit\settings-backup\activity.log~1~"
- 22:25:09 [main] [notice] jEdit: jEdit version 5.6.0
- 22:25:09 [main] [message] jEdit: Settings directory is
C:\Users\minh\.isabelle\Isabelle2021\jedit
- 22:25:09 [main] [message] jEdit: jEdit home directory is
C:\Isabelle\Isabelle2021\src\Tools\jEdit\dist
- 22:25:09 [main] [message] BeanShell: Beanshell Init
- 22:25:09 [main] [debug] jEdit: Loading site snippet:
C:\Isabelle\Isabelle2021\src\Tools\jEdit\dist\properties\jEdit.props
- 22:25:09 [main] [debug] GUIUtilities: Icon theme set to: tango
- 22:25:09 [main] [debug] GUIUtilities: Loading icon theme from:
jeditresource:/org/gjt/sp/jedit/icons/themes/tango/
- 22:25:09 [main] [debug] EditServer: jEdit server started on port 50982
- 22:25:09 [main] [debug] EditServer: Authorization key is 602548447
- 22:25:10 [main] [debug] jEdit: initPLAF non-edt
old=javax.swing.plaf.metal.MetalLookAndFeel
requested=com.formdev.flatlaf.FlatLightLaf
new=com.formdev.flatlaf.FlatLightLaf
- 22:25:10 [main] [debug] ActionSet: Loading actions from
jar:file:/C:/Isabelle/Isabelle2021/src/Tools/jEdit/dist/jedit.jar!/org/gjt/sp/jedit/actions.xml
- 22:25:10 [main] [debug] DockableWindowManager: Loading dockables from
jar:file:/C:/Isabelle/Isabelle2021/src/Tools/jEdit/dist/jedit.jar!/org/gjt/sp/jedit/dockables.xml
- 22:25:10 [AWT-EventQueue-0] [debug] EditBus:
SearchSettingsChanged[source=null]
- 22:25:10 [main] [notice] jEdit: Loading plugins from
C:\Isabelle\Isabelle2021\src\Tools\jEdit\dist\jars
- 22:25:10 [AWT-EventQueue-0] [debug] EditBus:
PluginUpdate[what=LOADED,exit=false,version=0.7,source=C:\Isabelle\Isabelle2021\src\Tools\jEdit\dist\jars\Code2HTML.jar,class=code2html.Code2HTMLPlugin]
- 22:25:10 [AWT-EventQueue-0] [debug] EditBus:
PluginUpdate[what=LOADED,exit=false,version=1.7.4,source=C:\Isabelle\Isabelle2021\src\Tools\jEdit\dist\jars\CommonControls.jar,class=CommonControlsPlugin]
- 22:25:10 [AWT-EventQueue-0] [debug] EditBus:
PluginUpdate[what=LOADED,exit=false,version=5.1.4,source=C:\Isabelle\Isabelle2021\src\Tools\jEdit\dist\jars\Console.jar,class=console.ConsolePlugin]
- 22:25:10 [AWT-EventQueue-0] [debug] EditBus:
PluginUpdate[what=LOADED,exit=false,version=2.3,source=C:\Isabelle\Isabelle2021\src\Tools\jEdit\dist\jars\ErrorList.jar,class=errorlist.ErrorListPlugin]
- 22:25:10 [AWT-EventQueue-0] [debug] EditBus:
PluginUpdate[what=LOADED,exit=false,version=2.2,source=C:\Isabelle\Isabelle2021\src\Tools\jEdit\dist\jars\Highlight.jar,class=gatchan.highlight.HighlightPlugin]
- 22:25:10 [AWT-EventQueue-0] [debug] EditBus:
PluginUpdate[what=LOADED,exit=false,version=null,source=C:\Isabelle\Isabelle2021\src\Tools\jEdit\dist\jars\idea-icons.jar]
- 22:25:10 [AWT-EventQueue-0] [debug] EditBus:
PluginUpdate[what=LOADED,exit=false,version=1.0,source=C:\Isabelle\Isabelle2021\src\Tools\jEdit\dist\jars\Isabelle-jEdit-base.jar,class=isabelle.jedit_base.Plugin]
- 22:25:10 [AWT-EventQueue-0] [debug] EditBus:
PluginUpdate[what=LOADED,exit=false,version=11.2,source=C:\Isabelle\Isabelle2021\src\Tools\jEdit\dist\jars\Isabelle-jEdit.jar,class=isabelle.jedit.Plugin]
- 22:25:10 [AWT-EventQueue-0] [debug] EditBus:
PluginUpdate[what=LOADED,exit=false,version=null,source=C:\Isabelle\Isabelle2021\src\Tools\jEdit\dist\jars\jsr305-2.0.0.jar]
- 22:25:10 [AWT-EventQueue-0] [debug] EditBus:
PluginUpdate[what=LOADED,exit=false,version=null,source=C:\Isabelle\Isabelle2021\src\Tools\jEdit\dist\jars\kappalayout.jar]
- 22:25:10 [AWT-EventQueue-0] [debug] EditBus:
PluginUpdate[what=LOADED,exit=false,version=2.7,source=C:\Isabelle\Isabelle2021\src\Tools\jEdit\dist\jars\Navigator.jar,class=ise.plugin.nav.NavigatorPlugin]
- 22:25:10 [AWT-EventQueue-0] [debug] EditBus:
PluginUpdate[what=LOADED,exit=false,version=5.0,source=C:\Isabelle\Isabelle2021\src\Tools\jEdit\dist\jars\QuickNotepad.jar,class=QuickNotepadPlugin]
- 22:25:10 [AWT-EventQueue-0] [debug] EditBus:
PluginUpdate[what=LOADED,exit=false,version=1.8,source=C:\Isabelle\Isabelle2021\src\Tools\jEdit\dist\jars\SideKick.jar,class=sidekick.SideKickPlugin]
- 22:25:10 [main] [notice] jEdit: Loading plugins from
C:\Users\minh\.isabelle\Isabelle2021\jedit\jars
- 22:25:10 [main] [message] HistoryModel: Loading history
- 22:25:10 [main] [message] BufferHistory: Loading
C:\Users\minh\.isabelle\Isabelle2021\jedit\recent.xml
- 22:25:10 [main] [message] KillRing: Loading
C:\Users\minh\.isabelle\Isabelle2021\jedit\killring.xml
- 22:25:11 [main] [debug] jEdit: initPLAF non-edt
old=com.formdev.flatlaf.FlatLightLaf
requested=com.formdev.flatlaf.FlatLightLaf
new=com.formdev.flatlaf.FlatLightLaf
- 22:25:11 [main] [debug] jEdit: SOCKS proxy disabled
- 22:25:11 [main] [debug] jEdit: HTTP proxy disabled
- 22:25:11 [AWT-EventQueue-0] [debug] EditBus:
PropertiesChanged[source=null]
- 22:25:11 [main] [message] jEdit: Loading mode catalog file
C:\Isabelle\Isabelle2021\src\Tools\jEdit\dist\modes\catalog
- 22:25:11 [main] [debug] jEdit: Loading user mode catalog
- 22:25:11 [main] [message] jEdit: Loading mode catalog file
C:\Users\minh\.isabelle\Isabelle2021\jedit\modes\catalog
- 22:25:11 [main] [debug] PluginJAR: Activating
code2html.Code2HTMLPlugin because of startup
- 22:25:11 [main] [debug] PluginJAR: Opening
C:\Isabelle\Isabelle2021\src\Tools\jEdit\dist\jars\Code2HTML.jar
- 22:25:11 [main] [debug] PluginJAR: Activating console.ConsolePlugin
because of startup
- 22:25:11 [AWT-EventQueue-0] [debug] EditBus:
PluginUpdate[what=ACTIVATED,exit=false,version=0.7,source=C:\Isabelle\Isabelle2021\src\Tools\jEdit\dist\jars\Code2HTML.jar,class=code2html.Code2HTMLPlugin]
- 22:25:11 [main] [debug] PluginJAR: Opening
C:\Isabelle\Isabelle2021\src\Tools\jEdit\dist\jars\Console.jar
- 22:25:11 [AWT-EventQueue-0] [debug] EditBus:
DynamicMenuChanged[menu=plugin.console.ConsolePlugin.menu,source=null]
- 22:25:11 [main] [debug] ConsolePlugin: Loaded 17 Actions
- 22:25:11 [main] [debug] PluginJAR: Opening
C:\Isabelle\Isabelle2021\src\Tools\jEdit\dist\jars\ErrorList.jar
- 22:25:11 [AWT-EventQueue-0] [debug] EditBus:
PluginUpda
[message truncated]
Email Gateway (Oct 20 2022 at 09:35):From: Minh Christian Tran <mctran312@gmail.com>
Hi,
I am unable to retrieve the activity.log as the folders of the bad versions
are empty.
[image: image.png]
ons. 19. okt. 2022 kl. 23:11 skrev Makarius <makarius@sketis.net>:
image.png
Email Gateway (Oct 20 2022 at 10:10):From: Makarius <makarius@sketis.net>
This is bad.
Since the problem appears to be a low-level Java breakdown of UTF8 encoding,
it might be related to language and locale settings of Windows.
Can you send me (privately) the result of the "systeminfo" tool? Not as a
screenshot, but as text file, e.g. "systeminfo > info.txt" within the
Cygwin-Terminal.
Makarius
Email Gateway (Oct 20 2022 at 21:43):From: Makarius <makarius@sketis.net>
Back from the private thread ...
The result of the investigation is here for the final Isabelle2020 release
next week: https://isabelle.sketis.net/repos/isabelle-release/rev/ea79c21bcc47
The strictness of java.nio.file.Files.readString does not fit into the
picture. These Java 7 functions are generally quite good, but one always needs
to question all fine points thoroughly.
Makarius
Last updated: Apr 25 2024 at 16:19 UTC