This instance will be upgraded to Heptapod 0.25.0 (final) on 2021-09-22 at 15:00 UTC+2 (a few minutes of down time)

Commit 3089093d authored by Gerwin Klein's avatar Gerwin Klein
Browse files

clearer style rules; link to style guide; clarify component installation

parent 11952ac46f28
......@@ -298,3 +298,18 @@ pre.bibtex {
border-width: thin thin thin thin;
border-style: solid;
}
code {
background-color: #F2F2F2;
color: #303030;
padding: 1px 2px 2px 2px;
border-radius: 4px;
}
pre.code {
white-space: pre;
background-color: #F2F2F2;
color: #303030;
padding: 10px 2px 10px 2px;
border-radius: 4px;
}
......@@ -57,9 +57,10 @@
If you feel this is necessary for your submission, please email <a
href="&#109;&#97;&#105;&#108;&#116;&#111;:&#97;&#102;&#112;-&#115;&#117;&#98;&#109;&#105;&#116;&#64;&#105;&#110;&#46;&#116;&#117;&#109;&#46;&#100;&#101;">&#97;&#102;&#112;-&#115;&#117;&#98;&#109;&#105;&#116;&#64;&#105;&#110;&#46;&#116;&#117;&#109;&#46;&#100;&#101;</a>.</p>
<p>The submission must follow these Isabelle style guidelines:</p>
<p>The submission must follow the following Isabelle style rules.
For additional guidelines on Isabelle proofs, also see the this <a href="http://proofcraft.org/blog/isabelle-style.html">guide</a> (feel free to follow all of these; only the below are mandatory).</p>
<ul>
<li>No use of the command <code>back</code>.</li>
<li>No use of the commands <code>sorry</code> or <code>back</code>.</li>
<li>Instantiations must not use Isabelle-generated names such as
<code>xa</code> &mdash; use Isar or <code>rename_tac</code> to avoid
......@@ -75,6 +76,8 @@ href="&#109;&#97;&#105;&#108;&#116;&#111;:&#97;&#102;&#112;-&#115;&#117;&#98;&#1
indented by <code>n</code> spaces relative to the first
<code>apply</code> in the sequence.</li>
<li>Only named lemmas should carry attributes such as <code>[simp]</code>.</li>
<li>We prefer structured Isar proofs over apply style, but do not
mandate them.</li>
......
......@@ -35,19 +35,21 @@ 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>Let <code>PATH</code> be the absolute path where you have put the unpacked
AFP directory that you downloaded. Add <code>PATH</code> on a separate line to
the file <code>~/.isabelle/IsabelleXYZ/etc/components</code>, where XYZ is the
Isabelle release you are working with, for example XYZ=2013. (In case you are
working with the development version of Isabelle, the file is simply
<code>~/.isabelle/etc/components</code>). You may need to create this file.</p>
<p>
If you are using Isabelle 2016, 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>
<p>
<pre class="code">
mkdir -p ~/.isabelle/Isabelle2016/etc/
echo "/home/myself/afp" >> ~/.isabelle/Isabelle2016/etc/components
</pre>
<p>
You can now refer to article <code>ABC</code> from the AFP in some theory of
yours via</p>
<pre>
<pre class="code">
imports "$AFP/ABC/Some_ABC_Theory"
</pre>
......@@ -55,21 +57,23 @@ yours via</p>
theories. Users of your distribution also need to install the AFP in the above
manner.</p>
Note that referring to <strong>another AFP entry from inside an AFP
entry</strong> is much easier:
<pre class="code">
imports "../ABC/Some_ABC_Theory"
</pre>
This is the preferred method for working inside the AFP,
because it interacts correctly with multiple AFP installations side by side.
<p>&nbsp;</p>
<p>
Example: you are using Isabelle2013, and have downloaded your afp directory to
<code>/home/myself/afp</code>. You would add the line
<code>/home/myself/afp</code> to the file
<code>~/.isabelle/Isabelle2013/etc/components</code>. Note that shell expansion,
e.g. <code>~/afp</code>, will not work in this file.
<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>
Note that referring to another AFP entry from <strong>inside an AFP
entry</strong> is much easier: just use
<pre>
imports "../ABC/Some_ABC_Theory"
</pre>
in your theory. This is the preferred
method for working inside the AFP.
</td></tr> </tbody> </table>
</div>
......
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