Stream: Beginner Questions

Topic: ✔ adding development version afp components breaks Isabelle


view this post on Zulip Chengsong Tan (Oct 16 2021 at 23:43):

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!

view this post on Zulip Wenda Li (Oct 17 2021 at 14:59):

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.

view this post on Zulip Chengsong Tan (Oct 17 2021 at 15:55):

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!

view this post on Zulip Chengsong Tan (Oct 17 2021 at 16:06):

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 :)

view this post on Zulip Wenda Li (Oct 17 2021 at 16:18):

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...

view this post on Zulip Chengsong Tan (Oct 17 2021 at 16:22):

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?

view this post on Zulip Wenda Li (Oct 17 2021 at 16:58):

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.

view this post on Zulip Notification Bot (Oct 18 2021 at 14:56):

Chengsong Tan has marked this topic as resolved.


Last updated: Mar 29 2024 at 04:18 UTC