Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Error when Importing Theories from Library


view this post on Zulip Email Gateway (Aug 19 2022 at 13:09):

From: Alfio Martini <alfio.martini@acm.org>
Dear Users,

I have often encountered problems when importing thy files from
Library using jEdit/Isabelle (Windows). For instance, when
I type

"~~/src/HOL/Library/OptionalSugar"

the output windows gives the error "Bad Theory Name".
It took me a while to find a simple workaround: save
the file and reload it.

This seems to happen in all the latest release candidates,
but I bet is an older issue.

Best!

view this post on Zulip Email Gateway (Aug 19 2022 at 13:09):

From: Makarius <makarius@sketis.net>
As far as I can tell this is the standard way up to and including
Isabelle2013-2.

Before getting side-tracked on this second round of a really stable
release, I was actually working towards more smooth file management in
Isabelle/jEdit, but there are remaining problems with its physical buffer
management. The editor uses old-school stateful implementations with
mutable data structures everywhere, and it is hard to work with that
efficiently and reliably.

Makarius


Last updated: Mar 28 2024 at 12:29 UTC