Re: [isabelle] Browsing finished theories in Isabelle/jEdit



On 08/02/17 10:30, Timothy Bourke wrote:
> I want to use Isabelle to better understand the Knaster-Tarski
> fixpoint theorem. So, I fire up Isabelle/jEdit and use the "Search in
> Directory..." feature to look for "Knaster-Tarski" (BTW, it would be
> great if the directory list in the dialog box automatically included
> $ISABELLE_HOME).

Note that the regular jEdit file dialog provides various Isabelle entry
points via "Favorites".

For directory search, anything needs to be typed manually, and in the
still official jEdit release, the one bundled with Isabelle2016-1,
environment variables cannot be used here. Some months ago, we have
actually sorted this out on the jedit-devel list, but the jEdit guys are
far behind their release schedule, so it did not make it into our
December 2016 release.


> Now, looking at the theorem, I want to know the exact definition of a
> complete lattice, so I COMMAND/CTRL-click on "complete_lattice". The
> Complete_Lattices.thy file opens at the correct position but is not
> processed (everything is pink) due to the error "Cannot update
> finished theory". This means, in particular, that I cannot continue
> COMMAND/CTRL-clicking to follow the definitions further.

This is an old omission in the PIDE document model. Already loaded
sources are "dead" and cannot be explored. After so many years it is
still not properly done, but I have already quite concrete ideas how to
do it soon: using offline PIDE markup in some SQLite database that is
used as "Isabelle application file format". It will eventually replace
the old log files.


> Thus this naive question from someone who no longer uses Isabelle
> every day (sniff):

Maybe you can occasionally show your fellow non-Isabelle users the state
of sophistication of Isabelle at the end of 2016. I am still hoping for
other ITP systems to catch up eventually, such that the general ideas
from our communities get more users out there -- not just proof-geeks
who like to have a complicated and inaccesible system for their private
entertainment.


	Makarius


Attachment: signature.asc
Description: OpenPGP digital signature



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