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
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and