Isabelle version:2021Feb
operating system version: MAC OS X 10.15.7
I wanted to load and read some theories from afp.
To resolve dependencies,
I decided to clone and use the afl repository.
After cloning it I to a folder, I followed the instructions
https://www.isa-afp.org/using.html
and successfully executed the command
isabelle components -u ~/Dropbox/Workspace/afp/afp-devel
with output
Added component "/Users/cstan/Dropbox/Workspace/afp/afp-devel/thys"
Now when I restart isabelle,
I got this error message
Screenshot-2021-10-17-at-00.39.10.png
Sourced file: inline evaluation of:
`` new isabelle.jedit.Isabelle_Export.VFS(); ;'' : No static field or inner class: VFS of class isabelle.jedit.Isabelle_Export : at Line: 2 :
in file: inline evaluation of: new isabelle.jedit.Isabelle_Export.VFS(); ;''
: isabelle .jedit .Isabelle_Export .VFS
at org.gjt.sp.jedit.bsh.UtilEvalError.toEvalError(UtilEvalError.java:84)
at org.gjt.sp.jedit.bsh.UtilEvalError.toEvalError(UtilEvalError.java:89)
at org.gjt.sp.jedit.bsh.BSHAmbiguousName.toObject(BSHAmbiguousName.java:64)
at org.gjt.sp.jedit.bsh.BSHAllocationExpression.objectAllocation(BSHAllocationExpression.java:86)
at org.gjt.sp.jedit.bsh.BSHAllocationExpression.eval(BSHAllocationExpression.java:62)
at org.gjt.sp.jedit.bsh.BSHPrimaryExpression.eval(BSHPrimaryExpression.java:102)
at org.gjt.sp.jedit.bsh.BSHPrimaryExpression.eval(BSHPrimaryExpression.java:47)
at org.gjt.sp.jedit.bsh.Interpreter.eval(Interpreter.java:644)
at org.gjt.sp.jedit.bsh.Interpreter.eval(Interpreter.java:738)
at org.gjt.sp.jedit.bsh.Interpreter.eval(Interpreter.java:727)
at org.gjt.sp.jedit.BeanShellFacade._eval(BeanShellFacade.java:153)
at org.gjt.sp.jedit.BeanShellFacade.eval(BeanShellFacade.java:117)
at org.gjt.sp.jedit.BeanShell.eval(BeanShell.java:382)
at org.gjt.sp.jedit.ServiceManager$Descriptor.getInstance(ServiceManager.java:337)
at org.gjt.sp.jedit.ServiceManager.getService(ServiceManager.java:262)
at org.gjt.sp.jedit.io.VFSManager.getVFSForProtocol(VFSManager.java:158)
at org.gjt.sp.jedit.MiscUtilities.isURL(MiscUtilities.java:590)
at org.gjt.sp.jedit.io.VFSManager.getVFSForPath(VFSManager.java:176)
at org.gjt.sp.jedit.MiscUtilities.pathsEqual(MiscUtilities.java:1206)
at org.gjt.sp.jedit.BufferHistory.getEntry(BufferHistory.java:88)
at org.gjt.sp.jedit.jEdit.composeBufferPropsFromHistory(jEdit.java:4418)
at org.gjt.sp.jedit.jEdit.openTemporary(jEdit.java:1859)
at org.gjt.sp.jedit.jEdit.openTemporary(jEdit.java:1825)
at org.gjt.sp.jedit.jEdit.openTemporary(jEdit.java:1778)
at org.gjt.sp.jedit.BeanShell._runScript(BeanShell.java:328)
at org.gjt.sp.jedit.BeanShell._runScript(BeanShell.java:291)
at org.gjt.sp.jedit.BeanShell.runScript(BeanShell.java:217)
at org.gjt.sp.jedit.Macros$BeanShellHandler.runMacro(Macros.java:1115)
at org.gjt.sp.jedit.jEdit.runStartupScripts(jEdit.java:4001)
at org.gjt.sp.jedit.jEdit.main(jEdit.java:552)
at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:64)
at java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
at java.base/java.lang.reflect.Method.invoke(Method.java:564)
at isabelle.Main$.$anonfun$main$4(main.scala:129)
at isabelle.Main$.main(main.scala:138)
at isabelle.Main.main(main.scala)
``
And after I click OK I got
/Applications/Isabelle2021.app/src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar:
Cannot start:
*** Unknown option "document_preprocessor"
*** The error(s) above occurred in session entry "Huffman" (line 3 of "/Users/cstan/Dropbox/Workspace/afp/afp-devel/thys/Huffman/ROOT")
And after that I could not get isabelle working properly (processing input, giving out messages etc.)
And the jedit interface looks like the below picture.
Screenshot-2021-10-17-at-00.42.18.png
Am I missing something important?
Thanks in advance!
Chengsong Tan said:
isabelle components -u ~/Dropbox/Workspace/afp/afp-devel
Which AFP version are you using? To me, it appears that you are probably using the development version rather than the most recent stable one (that is compatible with Isabelle2021). You can check if your AFP is correctly referenced by Isabelle by typing something like Wendas-MBP:~ wenda$ cat ~/.isabelle/Isabelle2021/ROOTS
in you terminal. In my case, the command gives
# Additional session root directories
#
# * each line contains one directory entry in Isabelle path notation
# * lines starting with "#" are stripped
# * changes require application restart
#
#:mode=text:encoding=UTF-8:
/Users/wenda/Workspace/afp2021/thys/
where the last line is the path pointing to the theory directory of the downloaded AFP. You can later manually modify the Isabelle2021/ROOTS
file as you see fit.
Wenda Li said:
Chengsong Tan said:
isabelle components -u ~/Dropbox/Workspace/afp/afp-devel
Which AFP version are you using? To me, it appears that you are probably using the development version rather than the most recent stable one (that is compatible with Isabelle2021). You can check if your AFP is correctly referenced by Isabelle by typing something like
Wendas-MBP:~ wenda$ cat ~/.isabelle/Isabelle2021/ROOTS
in you terminal. In my case, the command gives# Additional session root directories # # * each line contains one directory entry in Isabelle path notation # * lines starting with "#" are stripped # * changes require application restart # #:mode=text:encoding=UTF-8: /Users/wenda/Workspace/afp2021/thys/
where the last line is the path pointing to the theory directory of the downloaded AFP. You can later manually modify the
Isabelle2021/ROOTS
file as you see fit.
Thanks a lot for the reply!
Yes, I directly cloned from the afp mercurial repository so it is probably not
the stable release.
When I run the command cat ~/.isabelle/Isabelle2021/ROOTS,
I got
# Additional session root directories
#
# * each line contains one directory entry in Isabelle path notation
# * lines starting with "#" are stripped
# * changes require application restart
#
#:mode=text:encoding=UTF-8:
which means I don't have afp referenced correctly.
I downloaded a stable version from the afp website
and executed the same command with the new stable version afp directory:
isabelle components -u ~/Dropbox/Workspace/formalizing/afp-2021-10-13/thys
but this time the same error message appears when I open Isabelle2021,
and using the
cat ~/.isabelle/Isabelle2021/ROOTS
command gives me the same
# Additional session root directories
#
# * each line contains one directory entry in Isabelle path notation
# * lines starting with "#" are stripped
# * changes require application restart
#
#:mode=text:encoding=UTF-8:
message.
Is there a way to "roll back" to the isabelle configuration state before I did the
isabelle components ...
command? Are there any manuals on these configuration options?
Thanks a lot!
I just found the "roll back" option for this: isabelle components -x ~/Dropbox/Workspace/afp/afp-devel
-x
means to remove that component.
https://isabelle.in.tum.de/dist/Isabelle2021/doc/system.pdf
is where you can find relevant manual information on
isabelle components.
Now trying to add the stable version first and see if it works :)
Glad to find out that you have figured out the solution, which is actually something I didn't know. Personally, I often manually add the AFP path to ROOTS every time I update Isabelle...
Screenshot-2021-10-17-at-17.19.52.png
Just added the stable afp version and it works!
I can now look at the theory files interactively as shown in the screenshot :o)
And thanks @Wenda Li for the suggestion on the version problem, I was running out of ideas yesterday.
How do you do a manual AFP path adding?
Chengsong Tan said:
How do you do a manual AFP path adding?
Ahh, that is easy -- just edit the ROOTS file using your favourite text editor and save :-) To me, isabelle components -u
updates the ROOTS file when we don't know where it is located, but once we know its location ourselves it is straightforward to edit the file directly.
Chengsong Tan has marked this topic as resolved.
Last updated: Oct 12 2024 at 20:18 UTC