76 content given in @{text body} (theories and auxiliary source files). |
76 content given in @{text body} (theories and auxiliary source files). |
77 Note that a parent (like @{text "HOL"}) is mandatory in practical |
77 Note that a parent (like @{text "HOL"}) is mandatory in practical |
78 applications: only Isabelle/Pure can bootstrap itself from nothing. |
78 applications: only Isabelle/Pure can bootstrap itself from nothing. |
79 |
79 |
80 All such session specifications together describe a hierarchy (tree) |
80 All such session specifications together describe a hierarchy (tree) |
81 of sessions, with globally unique names. By default, names are |
81 of sessions, with globally unique names. The new session name |
82 derived from parent ones by concatenation, i.e.\ @{text "B\<dash>A"} |
82 @{text "A"} should be sufficiently long to stand on its own in a |
83 above. Cumulatively, this leads to session paths of the form @{text |
83 potentially large library. |
84 "X\<dash>Y\<dash>Z\<dash>W"}. Note that in the specification, |
|
85 @{text B} is already such a fully-qualified name, while @{text "A"} |
|
86 is the new base name. |
|
87 |
|
88 \item \isakeyword{session}~@{text "A! = B"} indicates a fresh start |
|
89 in the naming scheme: the session is called just @{text "A"} instead |
|
90 of @{text "B\<dash>A"}. Here the name @{text "A"} should be |
|
91 sufficiently long to stand on its own in a potentially large |
|
92 library. |
|
93 |
84 |
94 \item \isakeyword{session}~@{text "A (groups)"} indicates a |
85 \item \isakeyword{session}~@{text "A (groups)"} indicates a |
95 collection of groups where the new session is a member. Group names |
86 collection of groups where the new session is a member. Group names |
96 are uninterpreted and merely follow certain conventions. For |
87 are uninterpreted and merely follow certain conventions. For |
97 example, the Isabelle distribution tags some important sessions by |
88 example, the Isabelle distribution tags some important sessions by |
98 the group name called ``@{text "main"}''. Other projects may invent |
89 the group name called ``@{text "main"}''. Other projects may invent |
99 their own conventions, but this requires some care to avoid clashes |
90 their own conventions, but this requires some care to avoid clashes |
100 within this unchecked name space. |
91 within this unchecked name space. |
101 |
92 |
102 \item \isakeyword{session}~@{text "A"}~\isakeyword{in}~@{text "dir"} |
93 \item \isakeyword{session}~@{text "A"}~\isakeyword{in}~@{text "dir"} |
103 specifies an explicit directory for this session. By default, |
94 specifies an explicit directory for this session; by default this is |
104 \isakeyword{session}~@{text "A"} abbreviates |
95 the current directory of the @{verbatim ROOT} file. |
105 \isakeyword{session}~@{text "A"}~\isakeyword{in}~@{text "A"}. This |
|
106 accommodates the common scheme where some base directory contains |
|
107 several sessions in sub-directories of corresponding names. Another |
|
108 common scheme is \isakeyword{session}~@{text |
|
109 "A"}~\isakeyword{in}~@{verbatim "\".\""} to refer to the current |
|
110 directory of the ROOT file. |
|
111 |
96 |
112 All theories and auxiliary source files are located relatively to |
97 All theories and auxiliary source files are located relatively to |
113 the session directory. The prover process is run within the same as |
98 the session directory. The prover process is run within the same as |
114 its current working directory. |
99 its current working directory. |
115 |
100 |
141 *} |
126 *} |
142 |
127 |
143 subsubsection {* Examples *} |
128 subsubsection {* Examples *} |
144 |
129 |
145 text {* See @{file "~~/src/HOL/ROOT"} for a diversity of practically |
130 text {* See @{file "~~/src/HOL/ROOT"} for a diversity of practically |
146 relevant situations. *} |
131 relevant situations, but it uses relatively complex quasi-hierarchic |
|
132 naming conventions like @{text "HOL\<dash>SPARK"}, @{text |
|
133 "HOL\<dash>SPARK\<dash>Examples"}. An alternative is to use |
|
134 unqualified names that are relatively long and descriptive, as in |
|
135 the Archive of Formal Proofs (\url{http://afp.sf.net}), for |
|
136 example. *} |
147 |
137 |
148 |
138 |
149 section {* System build options \label{sec:system-options} *} |
139 section {* System build options \label{sec:system-options} *} |
150 |
140 |
151 text {* See @{file "~~/etc/options"} for the main defaults provided by |
141 text {* See @{file "~~/etc/options"} for the main defaults provided by |