Email Gateway (Aug 19 2022 at 17:10): Email Gateway (Aug 19 2022 at 17:10):From: "lyj238@ios.ac.cn" <lyj238@ios.ac.cn>
Dear Christian, David, Markus:
Thanks for your answering. I have used it in my machine, it works.
After looking up the manuals and my requirements for development of case studies, I have some further questions:
In my experience, the public theory files cache.thy and localesDef.thy should be checked only once, will be imported each time in each later case studies.
I think, the ideal status is that the checked ublic theory files cache.thy and localesDef.thy should be stored in internal format ( is image files?), and not be checked again If we develop a proof script on a case of a protocol.
For instance, if I model and verify the case study: 'mutualEx' protocol, I simply write a 'mutual.thy', import the checked 'cache.thy' and 'localesDef.thy'. Ideally, at this time, the two basic files Should be imported directly without checking again because they are checked and not modified, Thus I try to write my ROOT file as follows:
session cache_Session = HOL +
theories
cache
localesDef
session mutualEx_Session= HOL +
theories
mutualEx
session german_Session= HOL +
theories
german
,where german is another case study on german protocol,
After building cache_Session, I build german, I see cache.thy and localesDef.thy are loaded and checked again, it seemed that "build" neglect the fact that cache.thy and localesDef.thy have been checked.
I EXTREMLY want to make these clearly:
(a)after session cache_Session is finished, cache and localesDef theories will be stored in an internal format?
(b)In the subsequent development of case study, cache and localesDef can be impoted without checking again?
(c) I checked the directory after executing the 'build' command, I found nothing more than the thy files;
(d) I think that there should be a mechanism to support "a public theory once checked -then used for more times"
(d) is important to develop a large proof script, for instance, if 50% of the script is checked, and an error is found. If the checked 50% is ok, and no need to modify, then I store the former 50%, and develop the later 50% by directly importing the former 50% (without checking).
2.There is too little information to indicate the status of building process.
The most terrible thing is that some "auto", "simp","metis" command is executed and the building process is stucked.
At this time, no information is given.
It is preferable to have a hint message that which line are executed.
Reagrds!
-----邮件原件-----
发件人: cl-isabelle-users-bounces@lists.cam.ac.uk [mailto:cl-isabelle-users-bounces@lists.cam.ac.uk] 代表 Christian Sternagel
发送时间: 2015年2月5日 21:41
收件人: isabelle-users@cl.cam.ac.uk
抄送: lyj238@ios.ac.cn
主题: Re: [isabelle] Fwd: Fw: The development of a large proof script.
Dear lyj238,
what constitutes a single session has to be put into a "driver"/"project"/"session" file (I'm not sure whether there is any official name for this file, except for ROOT) called ROOT (see "System Manual", Section 2.1).
In your case the ROOT file could contain:
session Main_Session = HOL +
theories
mutualEx
which defines a session called "Main_Session" on top of HOL (for bigger developments, as suggested by David, you can have several of these sessions built on top of each other). The session consists of the theory "mutualEx" (and implicitly all the theories on which "mutualEx" depends and that are not yet part of the "HOL" session).
Now, in order to build this newly defined session you have to tell "isabelle build" where your ROOT file is and which session to build (since there could be several sessions in a single ROOT file). This is done via
isabelle build -d . -b Main_Session
adding "-v" will give you some more details about your environment which might be interesting here, in order to analyze the error you obtain.
E.g,. on my machine
isabelle build -v -d . -b Main_Session
results in
##################################################
ISABELLE_BUILD_OPTIONS="threads=4"
ML_PLATFORM="x86_64-linux"
ML_HOME="/usr/local/Isabelle2014/contrib/polyml-5.5.2-1/x86_64-linux"
ML_SYSTEM="polyml-5.5.2-1"
ML_OPTIONS="-H 500"
Session Pure/Pure
Session HOL/HOL (main)
Session Unsorted/Main_Session
Building Main_Session ...
Main_Session: theory cache
Main_Session: theory localesDef
Main_Session: theory mutualEx
Timing Main_Session (4 threads, 6.904s elapsed time, 20.347s cpu time, 0.749s GC time, factor 2.95) Finished Main_Session (0:00:20 elapsed time, 0:00:43 cpu time, factor 2.15) Finished at Thu Feb 5 14:38:53 CET 2015
0:00:26 elapsed time, 0:00:55 cpu time, factor 2.11 ##################################################
cheers
chris
Side remark: Conventionally you would start theory-names (as well as
session-names) with a capital letter and use underscores to delimit words (not CamelCaseAsIsConvetionForSomeProgrammingLanguages).
Email Gateway (Aug 19 2022 at 17:10):From: "lyj238@ios.ac.cn" <lyj238@ios.ac.cn>
Dear Christian, David, Markus:
Thanks for your answering. I have used it in my machine, it works.
After looking up the manuals and my requirements for development of case studies, I have some further questions:
In my experience, the public theory files cache.thy and localesDef.thy should be checked only once, will be imported each time in each later case studies.
I think, the ideal status is that the checked ublic theory files cache.thy and localesDef.thy should be stored in internal format ( is image files?), and not be checked again If we develop a proof script on a case of a protocol.
For instance, if I model and verify the case study: 'mutualEx' protocol, I simply write a 'mutual.thy', import the checked 'cache.thy' and 'localesDef.thy'. Ideally, at this time, the two basic files Should be imported directly without checking again because they are checked and not modified, Thus I try to write my ROOT file as follows:
session cache_Session = HOL +
theories
cache
localesDef
session mutualEx_Session= HOL +
theories
mutualEx
session german_Session= HOL +
theories
german
,where german is another case study on german protocol,
After building cache_Session, I build german, I see cache.thy and localesDef.thy are loaded and checked again, it seemed that "build" neglect the fact that cache.thy and localesDef.thy have been checked.
I EXTREMLY want to make these clearly:
(a)after session cache_Session is finished, cache and localesDef theories will be stored in an internal format?
(b)In the subsequent development of case study, cache and localesDef can be impoted without checking again?
(c) I checked the directory after executing the 'build' command, I found nothing more than the thy files;
(d) I think that there should be a mechanism to support "a public theory once checked -then used for more times"
(d) is important to develop a large proof script, for instance, if 50% of the script is checked, and an error is found. If the checked 50% is ok, and no need to modify, then I store the former 50%, and develop the later 50% by directly importing the former 50% (without checking).
2.There is too little information to indicate the status of building process.
The most terrible thing is that some "auto", "simp","metis" command is executed and the building process is stucked.
At this time, no information is given.
It is preferable to have a hint message that which line are executed.
Reagrds!
-----邮件原件-----
发件人: cl-isabelle-users-bounces@lists.cam.ac.uk [mailto:cl-isabelle-users-bounces@lists.cam.ac.uk] 代表 Christian Sternagel
发送时间: 2015年2月5日 21:41
收件人: isabelle-users@cl.cam.ac.uk
抄送: lyj238@ios.ac.cn
主题: Re: [isabelle] Fwd: Fw: The development of a large proof script.
Dear lyj238,
what constitutes a single session has to be put into a "driver"/"project"/"session" file (I'm not sure whether there is any official name for this file, except for ROOT) called ROOT (see "System Manual", Section 2.1).
In your case the ROOT file could contain:
session Main_Session = HOL +
theories
mutualEx
which defines a session called "Main_Session" on top of HOL (for bigger developments, as suggested by David, you can have several of these sessions built on top of each other). The session consists of the theory "mutualEx" (and implicitly all the theories on which "mutualEx" depends and that are not yet part of the "HOL" session).
Now, in order to build this newly defined session you have to tell "isabelle build" where your ROOT file is and which session to build (since there could be several sessions in a single ROOT file). This is done via
isabelle build -d . -b Main_Session
adding "-v" will give you some more details about your environment which might be interesting here, in order to analyze the error you obtain.
E.g,. on my machine
isabelle build -v -d . -b Main_Session
results in
##################################################
ISABELLE_BUILD_OPTIONS="threads=4"
ML_PLATFORM="x86_64-linux"
ML_HOME="/usr/local/Isabelle2014/contrib/polyml-5.5.2-1/x86_64-linux"
ML_SYSTEM="polyml-5.5.2-1"
ML_OPTIONS="-H 500"
Session Pure/Pure
Session HOL/HOL (main)
Session Unsorted/Main_Session
Building Main_Session ...
Main_Session: theory cache
Main_Session: theory localesDef
Main_Session: theory mutualEx
Timing Main_Session (4 threads, 6.904s elapsed time, 20.347s cpu time, 0.749s GC time, factor 2.95) Finished Main_Session (0:00:20 elapsed time, 0:00:43 cpu time, factor 2.15) Finished at Thu Feb 5 14:38:53 CET 2015
0:00:26 elapsed time, 0:00:55 cpu time, factor 2.11 ##################################################
cheers
chris
Side remark: Conventionally you would start theory-names (as well as
session-names) with a capital letter and use underscores to delimit words (not CamelCaseAsIsConvetionForSomeProgrammingLanguages).
Last updated: Apr 24 2024 at 20:16 UTC