Email Gateway (Aug 18 2022 at 19:56): Email Gateway (Aug 18 2022 at 19:56):From: li yongjian <lyj238@gmail.com>
Dear Isabelle experts:
my theory imports two pre theory of my own.
For example,
theory test imports myTheory1 myTheory2
begin ..
myTheory1 myTheory2 have been checked and passed.
But after load test.thy each time, myTheory1 and myTheory2 will be
loaded and checked by Isabelle again. If the two theories are long,
I need some time to wait.
How to avoid rechecking the two theories?
regards!
Email Gateway (Aug 18 2022 at 19:56):From: Walther Neuper <wneuper@ist.tugraz.at>
You could do it like that: in a file called "ROOT.ML" you have
/----------------------------------------------------\
use_thys ["myTheory1", "myTheory2"];
\----------------------------------------------------/
Then
$ isabelle usedir -b HOL myTheory12
creates a binary myTheory12 based on HOL, which afterwards can be called
in "test.thy" as follows
/----------------------------------------------------\
theory test imports myTheory12
begin ..
\----------------------------------------------------/
where myTheory12 fetches the binary without evaluating the respective
theories.
PS1: the above identifiers do not conform to Isabelle standards;
see doc/implementation.pdf p.3 section 0.1.2. Naming conventions
PS2: $ find -name ROOT.ML
will tell you further examples
Email Gateway (Aug 18 2022 at 19:56):From: Makarius <makarius@sketis.net>
This depends on your mode of operation. From the implicit description
abive I can merely guess that you are working interactively, with Proof
General or Isabelle/jEdit?
Theories are only reloaded on startup or when they have been changed. If
you want to avoid slow startup, you can wrap up the imports as a separate
"session" image, see "isabelle usedir" in the system manual
http://isabelle.in.tum.de/dist/Isabelle2012/doc/system.pdf
Such images are read-only. There are also ways to work in write-back
mode, but they are now difficult to use in most practical situations.
You can also avoid shutting down, by suspending your operating system
session.
Makarius
Last updated: Apr 25 2024 at 20:15 UTC