This instance will be upgraded to Heptapod 0.23.0rc (GitLab 13.12) on 2021-06-17 at 14:00 UTC+2 (a few minutes of down time)

using.tpl 1.68 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
{% extends "base.tpl" %}

{% block headline %}
<font class="first">R</font>eferring to
<font class="first">A</font>FP
<font class="first">E</font>ntries
{% endblock %}

{% block content %}
<table width="80%" class="descr">
  <tbody>
    <tr><td>

<p>
Once you have downloaded the AFP, you can include its articles and theories in
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>
Gerwin Klein's avatar
Gerwin Klein committed
20
If you are using Isabelle2021, and have downloaded your AFP directory to
21
<code>/home/myself/afp</code>, for Linux/Mac you can run the following command to make the AFP session ROOTS available to Isabelle:</p>
22 23
<p>
<pre class="code">
Gerwin Klein's avatar
Gerwin Klein committed
24
    echo "/home/myself/afp/thys" >> ~/.isabelle/Isabelle2021/ROOTS
25
</pre>
26 27 28 29 30 31 32 33 34 35 36 37 38
This adds the path <code>/home/myself/afp/thys/</code> to the ROOTS file, which
Isabelle will scan by default. You can also manually edit and/or create that
ROOTS file. There are many other ways to achieve the same outcome, this is just
one option.
</p>
<p>
For Windows, the idea is the same just the path is slightly different. If the
AFP is in <code>C:\afp</code>, you should be able to run the following in a
Cygwin terminal.
<pre class="code">
    echo "/cygdrive/c/afp/thys" >> ~/.isabelle/Isabelle2021/ROOTS
</pre>
</p>
39 40 41 42 43 44

<p>
You can now refer to article <code>ABC</code> from the AFP in some theory of
yours via</p>

<pre class="code">
45
    imports "ABC.Some_ABC_Theory"
46 47 48 49 50 51 52 53 54 55 56 57 58
</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>&nbsp;</p>

    </td></tr>
  </tbody>
</table>
{% endblock %}