Email Gateway (Aug 22 2022 at 15:01): Email Gateway (Aug 22 2022 at 15:01):From: Timothy Bourke <tim@tbrk.org>
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).
I quickly find that there is a well explained example
($ISABELLE_HOME/src/HOL/Isar_Examples/Knaster_Tarski.thy; thanks Makarius).
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.
Thus this naive question from someone who no longer uses Isabelle
every day (sniff): is there a better way of read-only browsing the
contents of an open session in Isabelle/jEdit?
I know that the theory files can be browsed online at
http://isabelle.in.tum.de/dist/library/HOL/HOL-Isar_Examples/Knaster_Tarski.html
but there I cannot click on elements to see their definitions, nor use
the other great features of Isabelle and Isabelle/jEdit.
I also know that, on a Mac, I can launch Isabelle/jEdit with
/Applications/Isabelle2016-1.app/Isabelle/bin/isabelle jedit -l Pure
and then open
/Applications/Isabelle2016-1.app/Isabelle/src/HOL/Main.thy
to browse the theories, but a slip on the keyboard risks a rebuild,
and I thought I would ask the question anyway for those who are even
less experienced than me.
This question is also something I have wondered about when teaching
Isabelle. I explain to students that they can COMMAND/CTRL-click to
follow definitions to learn about the underlying libraries, but they
quickly come face-to-face with the same issue.
Tim.
signature.asc
Email Gateway (Aug 22 2022 at 15:02):From: Makarius <makarius@sketis.net>
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
signature.asc
Email Gateway (Aug 22 2022 at 15:02):From: Timothy Bourke <tim@tbrk.org>
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".
I did not know that. That is very nice. Something similar for the
directory search would be great.
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.
I am happy to hear that it is in the grand design. Thank you.
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.
From time to time, I do exactly that. Without want to gush, I still
find Isabelle great.
Tim.
signature.asc
Last updated: Apr 25 2024 at 08:20 UTC