Re: [isabelle] JEdit IDE shows error when loading Arith.thy



On Thu, 27 Oct 2011, John Nicol wrote:

I ran the following steps (on two different x64 Ubuntu Linux
machines), and got the same error on both:

1.  Install 2011-1 bundle for x64 Linux, following requirements from
http://www.cl.cam.ac.uk/research/hvg/isabelle/download.html.  Run
"Isabelle2011-1/bin/isabelle jedit"
2.  Open "Isabelle2011-1/src/ZF/Arith.thy".
3.  JEdit prompts me to autoload other libraries to resolve theory
imports (including Univ.thy).  I click OK.
4.  The right-hand bar is pink (not loaded, I'm guessing).  As I
scroll down the file, the right-hand bar becomes red (errors).
5.  The first error is under "theory Arith imports Univ begin".  The error is:
  Missing theory (file "/home/jnicol/isabelle/Isabelle2011-1/src/ZF/Univ.thy")
However, that file exists at that path.

This looks fine so far. Errors in imported theories need to be expected manually, by jumping to that file. You also get an overview in the "Prover Session / Theory Status".

Loading the initial ZF session into Isabelle/jEdit is a bit difficult, though. This is because it bootstraps a few Isar commands, but the current editor protocol does not cope with that. See the slightly cryptic specification in "Prover Session / README":

  Crude management of new Isar commands that are defined within the
  running session.
  Workaround: Force re-parsing of files using such commands via reload
  menu of jEdit.

Instead of fiddling with that, it is better to start from a pre-built ZF images, and merely edit the example sessions.


	Makarius





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