Email Gateway (Apr 17 2025 at 16:29): Email Gateway (Apr 17 2025 at 16:29):From: Paolo Crisafulli <cl-isabelle-users@lists.cam.ac.uk>
Hi,
I have the following ROOT file which allows me to quickly build session
HOL-CyberPhi, as it's built on top of a heap which contains session
HOL-CSPM and theory Ordinary_Differential_Equations.Linear_ODE, both of
which are very long to build.
session "HOL-CSP-ODE" in "HOL-CSP-ODE" = "HOL-CSPM" +
options [document = false, timeout=1200]
sessions
"Ordinary_Differential_Equations"
theories
"Ordinary_Differential_Equations.Linear_ODE"
session "HOL-CyberPhi" (AFP) = "HOL-CSP-ODE" +
options [document = pdf, document_output = "output", timeout=1200]
directories examples
theories
"CyberPhi_Core"
"Safety_Props"
"ODE_Kinematics"
"Bouncing_Ball"
"Oscillator"
document_files
"root.tex"
As it is, HOL-CSP-ODE contains no thy file of its own. Nevertheless, I
have to keep an empty HOL-CSP-ODE dir, otherwise (after removing the 'in
"HOL-CSP-ODE"' clause) I'm getting:
*** Duplicate use of directory "/home/paolo/dev/hol-cyberphi"
*** for session "HOL-CSP-ODE" (line 45 of
"/home/paolo/dev/hol-cyberphi/ROOT")
*** vs. session "HOL-CyberPhi" (line 52 of
"/home/paolo/dev/hol-cyberphi/ROOT")
As a perfectionist, I'm wondering: is there a way to get rid of the
HOL-CSP-ODE dir/clause? Or is there another, better, way to achieve the
same goal (having a base heap to build fast)?
In advance, thank you very much for your help!
Cheers,
Paolo
Email Gateway (Apr 24 2025 at 12:47):From: Makarius <makarius@sketis.net>
On 17/04/2025 18:28, Paolo Crisafulli (via cl-isabelle-users Mailing List) wrote:
I have the following ROOT file which allows me to quickly build session HOL-
CyberPhi, as it's built on top of a heap which contains session HOL-CSPM and
theory Ordinary_Differential_Equations.Linear_ODE, both of which are very long
to build.As a perfectionist, I'm wondering: is there a way to get rid of the HOL-CSP-
ODE dir/clause? Or is there another, better, way to achieve the same goal
(having a base heap to build fast)?
Every session requires its own unique directory, so there is presently no way
around it.
You don't need the auxiliary session at all, if your motivation is to speed-up
the build for Isabelle/jEdit. See options -A and -R for "isabelle jedit", as
explained in the "isabelle doc jedit".
Overall, performance is often improved by removing too many intermediate
sessions. Thus option -A, which could be as extreme as "-A HOL" to skip
everything in between and just load the requirements into the background image.
Makarius
Email Gateway (May 01 2025 at 13:04):From: Paolo Crisafulli <cl-isabelle-users@lists.cam.ac.uk>
Thank you very much for your answer.
I'm now using the following ROOT file:
session "HOL-CyberPhi" (AFP) = "HOL-CSPM" +
options [document = pdf, document_output = "output", timeout=1200,
quick_and_dirty=true]
sessions
"Ordinary_Differential_Equations"
directories examples
theories
"CyberPhi_Core"
"Safety_Props"
"ODE_Kinematics"
"Bouncing_Ball"
"Oscillator"
"Forward_Stepwise_Kinematics"
document_files
"root.tex"
The following command produces the expected result: JEdit starts without
recompiling Ordinary_Differential_Equations and its ancestors.
isabelle jedit -d . -R HOL-CyberPhi ::
Is there a way to get a similar speed up with "isabelle build"?
Currently, without the intermediate session, all dependencies of
Ordinary_Differential_Equations get built each time I change a file in
my session and build again, which is huge.
Thank you,
Paolo
On 24/04/2025 14:39, Makarius wrote:
On 17/04/2025 18:28, Paolo Crisafulli (via cl-isabelle-users Mailing
List) wrote:I have the following ROOT file which allows me to quickly build
session HOL- CyberPhi, as it's built on top of a heap which contains
session HOL-CSPM and theory
Ordinary_Differential_Equations.Linear_ODE, both of which are very
long to build.As a perfectionist, I'm wondering: is there a way to get rid of the
HOL-CSP- ODE dir/clause? Or is there another, better, way to achieve
the same goal (having a base heap to build fast)?Every session requires its own unique directory, so there is presently
no way around it.You don't need the auxiliary session at all, if your motivation is to
speed-up the build for Isabelle/jEdit. See options -A and -R for
"isabelle jedit", as explained in the "isabelle doc jedit".Overall, performance is often improved by removing too many
intermediate sessions. Thus option -A, which could be as extreme as
"-A HOL" to skip everything in between and just load the requirements
into the background image.Makarius
Last updated: May 30 2025 at 04:27 UTC