Email Gateway (Aug 19 2022 at 13:29): Email Gateway (Aug 19 2022 at 13:29):From: "Roger H." <s57076@hotmail.com>
Hi,
im writing a class in the folder scr/HOL/Myclass
and everytime i open it, like 20 other classes need to be compiled.
Using jEdit, isabelle 2013-1, how do i build them, so that the compiler only needs to run through only my own class?
Thank you!
Email Gateway (Aug 19 2022 at 13:29):From: Lawrence Paulson <lp15@cam.ac.uk>
I assume that when you say “class” you actually mean “Isabelle theory”.
In the manuals (Isabelle/HOL: A Proof Assistant for Higher-Order Logic or Programming and Proving in Isabelle/HOL), you should quickly reach the advice that you should base any theory that you write on the theory Main. In that case, no other theories should need to be loaded. The only other theory to adopt as a starting point is Complex_Main, which includes some analysis. It is generally a mistake to import other theories from src/HOL or to store your own theories there.
But even so, I am puzzled by your question. Isabelle/HOL pre-loads all the theories in the directory you mention, so I cannot see how they could be loaded again. I wonder whether the phenomenon you mention is simply that, when run for the first time, the system will automatically build Isabelle/HOL for you.
Another remark: Isabelle2013-1 was found to have issues and was quickly replaced by Isabelle2013-2, which I advise you to download and use instead.
Larry Paulson
Email Gateway (Aug 19 2022 at 13:30):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Roger,
im writing a class in the folder scr/HOL/Myclass
(I suspsect that this »thing« is a theory, not a »class«)
and everytime i open it, like 20 other classes need to be compiled.
some clues which might help you:
Have a look at the description of the »isabelle build« tool in the
system manual.
Do not place your own developments in src/HOL without striking reason…
Cheers,
Florian
signature.asc
Last updated: Apr 25 2024 at 20:15 UTC