Email Gateway (Aug 17 2021 at 15:58): Email Gateway (Aug 17 2021 at 15:58):From: Pedro Sánchez Terraf <sterraf@famaf.unc.edu.ar>
Dear all,
Is it possible to use the "thys" directory of the AFP Mercurial
repository afp-devel as an Isabelle component?
I tried to use isabelle -u with that directory but after starting jEdit
I had long error message that started with:
8:33:58 PM [AWT-EventQueue-0] [error] PluginJAR: Error while starting
plugin isabelle.jedit.Plugin
8:33:58 PM [AWT-EventQueue-0] [error] PluginJAR: *** Unknown option
"document_preprocessor"
8:33:58 PM [AWT-EventQueue-0] [error] PluginJAR: *** The error(s) above
occurred in session entry "Huffman" (line 3 of
"/home/pedro/hg/afp-devel/thys/Huffman/ROOT")
and finally jEdit wasn't able to process the loaded theory.
On the other hand, I was indeed able to load the AFP component by using
the instructions on the website.
My motivation to do this is that I want to edit one of my AFP entries
and I would like to see the effect of the edits live on other theories
I'm developing right now, that depend on the former.
Thanks in advance.
Email Gateway (Aug 17 2021 at 22:49):From: Gerwin Klein <kleing@unsw.edu.au>
Hi Pedro,
it sounds like you might be trying to load the afp development version with Isabelle2021. "document_preprocessor" is an option that was introduced after Isabelle2021. You'll need the isabelle development version for afp-devel.
Cheers,
Gerwin
Email Gateway (Nov 26 2021 at 15:49):From: Stepan Holub <holub@karlin.mff.cuni.cz>
Hi,
I found this old question having encountered the same error message.
It appears when the branch "website-redesign" instead of "default" is
checked out.
Stepan
Email Gateway (Nov 26 2021 at 17:36):From: Pedro Sánchez Terraf <sterraf@famaf.unc.edu.ar>
Thanks, Stepan. IIRC, the suggestion by Gerwin (to use the devel version
of Isabelle) solved the problem.
Best wishes,
Last updated: Jan 04 2025 at 20:18 UTC