Commit 71ade75b authored by kleing's avatar kleing
Browse files

using AFP entries (for non-editors) is now more uniform

parent f5408d5b219f
......@@ -17,13 +17,12 @@ your own developments. If you would like to make your work available to others
<i>without</i> having to include the AFP articles you depend on, here is how to do it.
</p>
<p>
If you are using Isabelle 2016-1, and have downloaded your AFP directory to
<code>/home/myself/afp</code>, you should run the following commands
<a href="#1">[1]</a> <a href="#2">[2]</a>:</p>
If you are using Isabelle 2017, and have downloaded your AFP directory to
<code>/home/myself/afp</code>, you should run the following command
<a href="#1">[1]</a> to make the AFP session ROOTS available to Isabelle:</p>
<p>
<pre class="code">
mkdir -p ~/.isabelle/Isabelle2016-1/etc/
echo "/home/myself/afp" >> ~/.isabelle/Isabelle2016-1/etc/components
echo "/home/myself/afp/thys" >> ~/.isabelle/Isabelle2017/ROOTS
</pre>
<p>
......@@ -31,44 +30,19 @@ You can now refer to article <code>ABC</code> from the AFP in some theory of
yours via</p>
<pre class="code">
imports "$AFP/ABC/Some_ABC_Theory"
imports "ABC.Some_ABC_Theory"
</pre>
<p>This allows you to distribute your material separately from any AFP
theories. Users of your distribution also need to install the AFP in the above
manner.</p>
<p>
Note that referring to <strong>another AFP entry from inside an AFP
entry</strong> is different and much easier:
<pre class="code">
imports "../ABC/Some_ABC_Theory"
</pre>
For working inside the AFP, this is the mandated option.
It interacts correctly with multiple AFP installations side by side.
</p>
<p>You can also use this method in your own work outside the AFP, you only
need to place the AFP entries you refer to next to your development in the
correct location in the directory hierarchy.</p>
<p>
If you build on one other AFP entry, your ROOT file should make this explicit:
<pre>
session my_session = base_session +
</pre>
This avoids rerunning the <tt>base_session</tt> theories by building
on the <tt>base_session</tt> image instead. Thus running times of AFP
regression tests are reduced!
</p>
<p>&nbsp;</p>
<p>
<a name="1">[1]:</a> Tested for Linux and Mac installations &dash; it should be the same under cygwin on Windows.
</p>
<p>
<a name="2">[2]:</a> This is one method for installing the AFP as a component. Any other method for adding Isabelle components will work as well.</p>
</td></tr>
</tbody>
</table>
......
......@@ -76,13 +76,12 @@ your own developments. If you would like to make your work available to others
<i>without</i> having to include the AFP articles you depend on, here is how to do it.
</p>
<p>
If you are using Isabelle 2016-1, and have downloaded your AFP directory to
<code>/home/myself/afp</code>, you should run the following commands
<a href="#1">[1]</a> <a href="#2">[2]</a>:</p>
If you are using Isabelle 2017, and have downloaded your AFP directory to
<code>/home/myself/afp</code>, you should run the following command
<a href="#1">[1]</a> to make the AFP session ROOTS available to Isabelle:</p>
<p>
<pre class="code">
mkdir -p ~/.isabelle/Isabelle2016-1/etc/
echo "/home/myself/afp" >> ~/.isabelle/Isabelle2016-1/etc/components
echo "/home/myself/afp/thys" >> ~/.isabelle/Isabelle2017/ROOTS
</pre>
<p>
......@@ -90,44 +89,19 @@ You can now refer to article <code>ABC</code> from the AFP in some theory of
yours via</p>
<pre class="code">
imports "$AFP/ABC/Some_ABC_Theory"
imports "ABC.Some_ABC_Theory"
</pre>
<p>This allows you to distribute your material separately from any AFP
theories. Users of your distribution also need to install the AFP in the above
manner.</p>
<p>
Note that referring to <strong>another AFP entry from inside an AFP
entry</strong> is different and much easier:
<pre class="code">
imports "../ABC/Some_ABC_Theory"
</pre>
For working inside the AFP, this is the mandated option.
It interacts correctly with multiple AFP installations side by side.
</p>
<p>You can also use this method in your own work outside the AFP, you only
need to place the AFP entries you refer to next to your development in the
correct location in the directory hierarchy.</p>
<p>
If you build on one other AFP entry, your ROOT file should make this explicit:
<pre>
session my_session = base_session +
</pre>
This avoids rerunning the <tt>base_session</tt> theories by building
on the <tt>base_session</tt> image instead. Thus running times of AFP
regression tests are reduced!
</p>
<p>&nbsp;</p>
<p>
<a name="1">[1]:</a> Tested for Linux and Mac installations &dash; it should be the same under cygwin on Windows.
</p>
<p>
<a name="2">[2]:</a> This is one method for installing the AFP as a component. Any other method for adding Isabelle components will work as well.</p>
</td></tr>
</tbody>
</table>
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment