Email Gateway (Aug 22 2022 at 17:19): Email Gateway (Aug 22 2022 at 17:19):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Hi,
I have to learn to use Isabelle 2017, and I can't find where to start in
the documentation.
I've successfully got a theory file called HOL_Gen.thy,
and fixed all the errors which show up when I run
/home/users/jeremy/Isabelle2017/bin/isabelle process -T HOL_Gen
but now I want to develop proofs interactively.
When I run the executable called Isabelle2017, I get a window with
multiple subwindows, but I gather from seeing this sort of thing in the
past that maybe I should type in there something like the following:
theory Scratch
imports HOL_Gen
begin
lemma ...
but it complains
Bad theory import "Draft.HOL_Gen"
What would be going wrong here? Is the use of this tool documented
anywhere?
In Isabelle2005 you could get to a terminal type interface to Isar by,
as I recall, using the command Isabelle instead of isabelle. Is
anything like this possible in Isabelle 2017? (I've seen the reference
to isabelle console, but that's for entering ML commands not Isar commands)
Thanks
Jeremy
Email Gateway (Aug 22 2022 at 17:20):From: Sebastien Gouezel <sebastien.gouezel@univ-nantes.fr>
Run
/home/users/jeremy/Isabelle2017/bin/isabelle jedit
to open the interactive editor.
Sebastien
Email Gateway (Aug 22 2022 at 17:20):From: Lars Hupel <hupel@in.tum.de>
Dear Jeremy,
this looks like it is an Isabelle/jEdit window.
Importing without any qualifiers (in your example, "HOL_Gen"), should
work fine, given that the referenced theory file resides in the same
directory as your "Scratch.thy". It looks like this is not the case. You
can save the file there, or alternatively, use a path name as import,
i.e. "path/to/HOL_Gen" (absolute paths are discouraged these days,
though).
Cheers
Lars
Email Gateway (Aug 22 2022 at 17:20):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Hi Lars,
Thanks - there is no file Scratch.thy until the program offers to create
one, when I try to close it (ie, this Isabelle/jEdit window), but then
it offers to create it in my home directory.
So if I copy the file HOL_Gen.thy to my home directory, then I make more
progress. But I don't want my home directory cluttered up with Isabelle
files.
I tried the suggestion of a path name, but it didn't seem to like the
symbol /
How do I tell this tool where to look for theory files? And is its use
documented anywhere?
Cheers,
Jeremy
Email Gateway (Aug 22 2022 at 17:20):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Hi Sebastian,
Thanks - so far as I can see this gives me (almost) the same result as I
had by running the executable called Isabelle2017, with the same issues
Jeremy
Email Gateway (Aug 22 2022 at 17:20):From: Lars Hupel <hupel@in.tum.de>
Thanks - there is no file Scratch.thy until the program offers to create
one, when I try to close it (ie, this Isabelle/jEdit window), but then
it offers to create it in my home directory.
Isabelle/jEdit is primarily an editor. As such, you may of course edit
unsaved files, but there is no good reason to. When you start your
theory, you can directly save it without waiting until your program
exits. Press "Ctrl-S" (or "Cmd-S" on a Mac I believe) to save and select
a more appropriate location.
I tried the suggestion of a path name, but it didn't seem to like the
symbol /
Path-qualified names have to be enclosed in double quotes.
How do I tell this tool where to look for theory files? And is its use
documented anywhere?
Isabelle will always, with some exceptions like "Main", look for imports
relative to the location of the theory you are editing. There is, as far
as I know, no way to change this (and it is hardly necessary).
(However, it is also possible to use so-called session-qualified
imports. Whether or not that is necessary depends on your project.)
There is a dedicated manual for Isabelle/jEdit:
<https://isabelle.in.tum.de/dist/Isabelle2017/doc/jedit.pdf>
Hope that helps!
Last updated: Apr 25 2024 at 16:19 UTC