Email Gateway (Aug 18 2022 at 18:35): Email Gateway (Aug 18 2022 at 18:35):From: John Nicol <nicol.john@gmail.com>
Hi,
I ran the following steps (on two different x64 Ubuntu Linux
machines), and got the same error on both:
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"
Open "Isabelle2011-1/src/ZF/Arith.thy".
JEdit prompts me to autoload other libraries to resolve theory
imports (including Univ.thy). I click OK.
The right-hand bar is pink (not loaded, I'm guessing). As I
scroll down the file, the right-hand bar becomes red (errors).
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.
Are there environment variables that need to be set?
Thanks,
John
Email Gateway (Aug 18 2022 at 18:36):From: Lars Noschinski <noschinl@in.tum.de>
This probably means Univ.thy could not be loaded because of some error.
Have a look at the "theory status" tab on the bottom.
-- Lars
Email Gateway (Aug 18 2022 at 18:36):From: Makarius <makarius@sketis.net>
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
Last updated: Apr 25 2024 at 16:19 UTC