Re: [isabelle] Using the AFP repo as a component



Thanks, Stepan. IIRC, the suggestion by Gerwin (to use the devel version of Isabelle) solved the problem.

Best wishes,

--
Pedro Sánchez Terraf
CIEM-FAMAF — Universidad Nacional de Córdoba
cs.famaf.unc.edu.ar/~pedro
 
On 26/11/21 12:49, Stepan Holub wrote:
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

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

On 18 Aug 2021, at 01:58, Pedro Sánchez Terraf <sterraf at famaf.unc.edu.ar> wrote:

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.

--
Pedro Sánchez Terraf
CIEM-FAMAF — Universidad Nacional de Córdoba
cs.famaf.unc.edu.ar/~pedro



Logo AVG

Tento e-mail byl zkontrolován na viry antivirovým softwarem AVG.
www.avg.com




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.