Commit e160d9b1 authored by Max "Ammerbauer" Haslbeck's avatar Max "Ammerbauer" Haslbeck
Browse files

Create all sites (except download.shtml) with Jinja2

* add Example-Submission to metadata
* use extra key no-index in metadata for entries like Example-Submission
parent 6ea260994b82
......@@ -43,7 +43,7 @@ class afp_entry:
afp_dict.
It still relies on information created by the entries-dict in sitegen.py.
"""
def __init__(self, name, entry_dict, afp_dict):
def __init__(self, name, entry_dict, afp_dict, no_index = False):
self.name = name
self.afp_dict = afp_dict
self.path = os.path.join(self.afp_dict.path, self.name)
......@@ -52,7 +52,8 @@ class afp_entry:
self.authors = []
for name, _address in entry_dict['author']:
self.authors.append(afp_dict.authors[name])
afp_dict.authors[name].articles.add(self)
if not no_index:
afp_dict.authors[name].articles.add(self)
self.publish_date = datetime.strptime(entry_dict['date'], "%Y-%m-%d")
#add UTC timezone to date
self.publish_date = self.publish_date.replace(tzinfo = pytz.UTC)
......@@ -188,11 +189,20 @@ class afp_dict(dict):
dict.__init__(self, *args)
self.path = normpath(afp_thys_path)
self.authors = dict()
for e in entries:
for name, address in entries[e]['author']:
# Extra dict for entries which don't show up in index and statistics
#TODO: document how it works, improve how it works
self.no_index = dict()
for entry in entries.values():
for name, address in entry['author']:
self.authors[name] = afp_author(name, address)
for e in entries:
self[e] = afp_entry(e, entries[e], self)
for name, entry in entries.items():
if 'extra' in entry and 'no-index' in entry['extra']:
self.no_index[name] = afp_entry(name, entry, self,
no_index = True)
else:
self[name] = afp_entry(name, entry, self)
for name in self.no_index.keys():
del entries[name]
# all_thys is a dict which maps a thy file to its corresponding AFP
# entry
self.all_thys = dict()
......
......@@ -270,6 +270,9 @@ if __name__ == "__main__":
builder.generate_index()
builder.generate_entries()
builder.generate_statistics()
for s in ["about", "citing", "updating", "search",
"submitting", "using"]:
builder.generate_standard(s + ".shtml", s + ".tpl")
builder.generate_rss(30)
if options.build_download:
builder.generate_download()
......
......@@ -113,6 +113,11 @@ class Builder():
with open(os.path.join(self.root_output_dir, filename), 'wb') as f:
f.write(template.render(values).encode('utf8'))
def generate_standard(self, filename, template_name):
template = self.j2_env.get_template(template_name)
self.write_file(filename, template, {})
terminal.success("Generated {}".format(filename))
def generate_topics(self):
template = self.j2_env.get_template("topics.tpl")
tree = collect_topics(self.entries)
......@@ -139,12 +144,16 @@ class Builder():
counter = 0
template = self.j2_env.get_template("entry.tpl")
for name, entry in self.afp_entries.items():
counter += 1
#TODO: Solve more elegantly
entry.imports = sorted(entry.imports, key = lambda x: x.name)
entry.used = sorted(entry.used, key = lambda x: x.name)
self.write_file(os.path.join("entries", name + ".shtml"), template,
{'entry': entry, 'is_devel': self.is_devel})
counter += 1
for name, entry in self.afp_entries.no_index.items():
self.write_file(os.path.join("entries", name + ".shtml"), template,
{'entry': entry, 'is_devel': self.is_devel})
counter += 1
terminal.success("Generated shtml files for {:d} entries".format(counter))
def generate_download(self):
......
{% extends "base.tpl" %}
{% block headline %}
<font class="first">A</font>rchive of
<font class="first">F</font>ormal
<font class="first">P</font>roofs</h1>
{% endblock %}
{% block content %}
<table width="80%" class="descr">
<tbody>
<tr><td>
<h2>About</h2>
<p>The Archive of Formal Proofs is a collection of proof libraries, examples,
and larger scientific developments, mechanically checked in the theorem prover
<a href="http://isabelle.in.tum.de/">Isabelle</a>. It is organized in the way
of a scientific journal. <a href="submitting.shtml">Submissions</a> are
refereed.</p>
<p>The archive repository is hosted on <a href="https://bitbucket.org">Bitbucket</a> to
provide easy free access to archive entries. The entries are
tested and maintained continuously against the current stable release of
Isabelle. Older versions of archive entries will remain available.</p>
<h2>Editors</h2>
<p><a name="editors">The editors of the archive are</a></p>
<ul>
<li><a href="http://www.cse.unsw.edu.au/~kleing/">Gerwin Klein</a>,
<a href="http://www.data61.csiro.au">Data61</a></li>
<li><a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a>,
<a href="http://www.tum.de/">Technische Universit&auml;t M&uuml;nchen</a></li>
<li><a href="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a>,
<a href="http://www.cam.ac.uk/">University of Cambridge</a></li>
<li><a href="http://cl-informatik.uibk.ac.at/users/thiemann/">René Thiemann</a>,
<a href="https://www.uibk.ac.at/">University of Innsbruck</a></li>
</ul>
<h2>Why</h2>
<p>We aim to strengthen the community and to foster the development of formal
proofs.</p>
<p>We hope that the archive will provide</p>
<ul>
<li>a resource of knowledge, examples, and libraries for users,</li>
<li>a large and relevant test bed of theories for Isabelle developers, and</li>
<li>a central, citable place for authors to publish their theories</li>
</ul>
<p>We encourage authors of publications that contain Isabelle developments
to make their theories available in the Archive of Formal Proofs and to refer
to the archive entry in their publication. It makes it easer for referees to
check the validity of theorems (all entries in the archive are
mechanically checked), it makes it easier for readers of the publication to
understand details of your development, and it makes it easier to use and
build on your work.</p>
<h2>License</h2>
<p>All entries in the Archive of Formal Proofs are licensed under
a <a href="LICENSE">BSD-style License</a> or
the <a href="http://www.gnu.org/copyleft/lesser.html">GNU LGPL</a>.
This means they are free to download, free to use, free to change, and
free to redistribute with minimal restrictions.</p>
<p>The authors retain their full copyright on their original work,
including their right to make the development available under another,
additional license in the future.</p>
</td></tr>
</tbody>
</table>
{% endblock %}
{% extends "base.tpl" %}
{% block headline %}
<font class="first">C</font>iting
<font class="first">E</font>ntries
{% endblock %}
{% block content %}
<table width="80%" class="descr">
<tbody>
<tr><td>
<p>The following gives an example of the preferred way for citing
entries in the AFP:</p>
<div class="cite">
M. Jaskelioff and S. Merz, Proving the Correctness of Disk
Paxos. <em>Archive of Formal Proofs</em>, June 2005, <a
href="http://isa-afp.org/entries/DiskPaxos.shtml"><tt>http://isa-afp.org/entries/DiskPaxos.shtml</tt></a>, Formal proof development.
</div>
<p>
The bibtext entry for this would be:
</p>
<pre class="bibtext">
@article{Jaskelioff-Merz-AFP05,
author = {Mauro Jaskelioff and Stephan Merz},
title = {Proving the Correctness of Disk Paxos},
journal = {Archive of Formal Proofs},
month = Jun,
year = 2005,
note = {\url{http://isa-afp.org/entries/DiskPaxos.shtml}, Formal proof development},
ISSN = {2150-914x}
}
</pre>
</td></tr>
</tbody>
</table>
{% endblock %}
{% extends "base.tpl" %}
{% block headline %}
<font class="first">S</font>earch the <font class="first">A</font>rchive
{% endblock %}
{% block content %}
<div align="center"><!-- SiteSearch Google -->
<p>Use Google to search the archive. It will look in entry descriptions
as well as in the Isabelle theories and PDF proof documents.</p>
<p>&nbsp;</p>
<FORM method=GET action="https://www.google.com/search">
<TABLE bgcolor="#FFFFFF"><tr><td>
<A HREF="https://www.google.com/">
<IMG SRC="https://www.google.com/logos/Logo_40wht.gif"
border="0" ALT="Google"></A>
</td>
<td>
<INPUT TYPE=text name=q size=31 maxlength=255 value="">
<INPUT type=submit name=btnG VALUE="Google Search">
<font size=-1>
<input type=hidden name=domains value="isa-afp.org"><br><input type=radio name=sitesearch value=""> Web <input type=radio name=sitesearch value="isa-afp.org" checked>Archive of Formal Proofs<br>
</font>
</td></tr></TABLE>
</FORM>
<!-- SiteSearch Google -->
<p>&nbsp;</p>
<p>Google may take some time to index new pages. Very new Submissions might be missed.</p>
</div>
{% endblock %}
{% extends "base.tpl" %}
{% block headline %}
<font class="first">S</font>ubmission
<font class="first">G</font>uidelines
{% endblock %}
{% block content %}
<table width="80%" class="descr">
<tbody>
<tr><td>
<p>Please send your submission
<a href="https://ci.isabelle.systems/afp-submission/">via this web page</a>.
</p>
<p>You will need to supply the following information:</p>
<ul>
<li>Title, authors and abstract in plain text.</li>
<li>A short name. It will become the directory name of the archive
entry.</li>
<li>Name/contact of the maintainer of the entry (usually the author).</li>
<li>URL or email address of authors to display on the web page.</li>
<li>The topic(s) the entry should be listed under in <a href="topics.shtml">the index</a>.</li>
<li>A tar file with the theory files, ROOT file, and
document directory. The theories should work with the current
release of <a href="http://isabelle.in.tum.de/">Isabelle</a>.
<li>A notice whether you license your submission under BSD
or LGPL if accepted. For LGPL submissions, please include the
header "License: LGPL" in each file.</li>
</ul>
<p>The submission must build with the current Isabelle release version.
Submissions for older Isabelle versions are not accepted.</p>
<p>Submissions for the Isabelle development version are also acceptable,
but publication of the entry on the front page will be deferred until the
next Isabelle release. In the meantime the entry will only be visible on
the <a href="https://devel.isa-afp.org">development pages</a>.
In this case,
submit your article as described above. Because your article is tested
against the release version, this will fail (otherwise your article does
not need the development version!) and you cannot perform the final step
in the submission process. When that happens, simply copy the url of the
submission page at that point into an email to <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 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 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
such names.</li>
<li>No use of the command <code>smt</code>. The result of this
command depends on external tools that are not under our control and
may stop working in the future.</li>
<li><code>apply</code> scripts should be indented by subgoal as in
the Isabelle distribution. If an <code>apply</code> command is
applied to a state with <code>n+1</code> subgoals, it must be
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>
<li>If there are proof steps that take significant time, i.e. longer
than roughly 1 min, please add a short comment to that step, so
maintainers will know what to expect.</li>
</ul>
<p>There is an
<a href="entries/Example-Submission.shtml">example submission</a>
that contains further information.</p>
<p>It is possible and encouraged to build on other archive entries
in your submission. There is a standardised way to
<a href="using.shtml">refer to other AFP entries</a> in your
theories.</p>
<p>Your submission will be refereed and you will receive notification
as soon as possible. If accepted, you must agree to maintain your
archive entry or nominate someone else to maintain it. The Isabelle
development team will assist with maintenance, but it does not have the
resources to fully maintain the complete archive.</p>
<p>If you have questions regarding 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>.
If you need help with Isabelle, please use the
<a href="mailto:isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a>
mailing list. It is always a good idea to <a
href="https://lists.cam.ac.uk/mailman/listinfo/cl-isabelle-users">subscribe</a>.</p>
</td></tr>
</tbody>
</table>
{% endblock %}
{% extends "base.tpl" %}
{% block headline %}
<font class="first">U</font>pdating
<font class="first">E</font>ntries
{% endblock %}
{% block content %}
<table width="80%" class="descr">
<tbody>
<tr><td>
<h2>Change</h2>
<p>
The Archive of Formal Proofs is an online resource and therefore
more dynamic than a normal scientific journal. Existing entries
can and do evolve and can also be updated significantly by their
authors.
</p>
<p>
This conflicts with the purpose of archiving and preserving
entries as they have been submitted and with the purpose of
providing a clear and simple interface to readers.
</p>
<p>
The AFP deals with this by synchronizing such updates with
Isabelle releases:
</p>
<ul>
<li>
The entries released and visible on the main site are always
working with the most recent stable Isabelle version and do not
change.
</li>
<li>
In the background, the archive maintainers evolve all entries to
be up to date with the current Isabelle development
version. Authors can contribute changes to this version which is
available as a <a
href="https://bitbucket.org/isa-afp/afp-devel/">bitbucket
mercurial repository</a> or as tar.gz package on the <a href="download.shtml">
download page</a>.
</li>
<li>
When a new Isabelle version is released, the above mentioned
development version of AFP is frozen and turns into the main
version displayed on the front page. Older versions (including the
original submission) of all entries are archived and remain
accessible.
</li>
</ul>
<h2>If you are an author</h2>
<p>
The above means that if you are an author and would like to
provide a new, better version of your AFP entry, you can do so.
</p>
<p>
To achieve this, you should base your changes on the <a
href="https://bitbucket.org/isa-afp/afp-devel/">mercurial
development version</a>
of your AFP entry and test it against the current <a
href="http://isabelle.in.tum.de/devel/">Isabelle development
version</a>.
</p>
<p>
If you would like to get write access to your entry in the
mercurial repository or if you need
assistance, please contact the <a href="about.shtml#editors">editors</a>.
</p>
</td></tr>
</tbody>
</table>
{% endblock %}
{% 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>
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 class="code">
imports "$AFP/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>
{% endblock %}
......@@ -5283,3 +5283,15 @@ abstract =
Brandon Bohrer, Vincent Rahli, Ivana Vukotic, Marcus Völp, André
Platzer: Formally verified differential dynamic logic. CPP 2017.
[Example-Submission]
title = Example Submission
author = Gerwin Klein <http://www.cse.unsw.edu.au/~kleing/>
topic = Mathematics/Analysis, Mathematics/Number Theory
date = 2004-02-25
notify = kleing@cse.unsw.edu.au
abstract =
This is an example submission to the Archive of Formal Proofs. It shows
submission requirements and explains the structure of a simple typical
submission.
extra-no-index = no-index: true
<!DOCTYPE public "-//w3c//dtd html 4.01 transitional//en"
"http://www.w3.org/TR/html4/loose.dtd">
<html>
<!DOCTYPE html>
<html lang="en">
<head>
<title>Archive of Formal Proofs</title>
<link rel="stylesheet" type="text/css" href="front.css">
<link rel="icon" href="images/favicon.ico" type="image/icon">
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<meta charset="utf-8">
<title>Archive of Formal Proofs</title>
<link rel="stylesheet" type="text/css" href="front.css">
<link rel="icon" href="images/favicon.ico" type="image/icon">
<link rel="alternate" type="application/rss+xml" title="RSS" href="rss.xml">
</head>
<body>
<table width="100%">
<tbody>
<tbody>
<tr>
<!-- Navigation -->
<td width="20%" align="center" valign="top">
<p>&nbsp;</p>
<a href="http://isabelle.in.tum.de">
<img src="images/isabelle.png" width="100" height="86" border=0>
</a>
<p>&nbsp;</p>
<p>&nbsp;</p>
<table class="nav" width="80%">
<tr>
<td class="nav" width="100%"><a href="index.shtml">Home</a></td>
</tr>
<tr>
<td class="nav"><a href="about.shtml">About</a></td>
</tr>
<tr>
<td class="nav"><a href="submitting.shtml">Submission Guidelines</a></td>
</tr>
<tr>
<td class="nav"><a href="updating.shtml">Updating entries</a></td>
</tr>
<tr>
<td class="nav"><a href="using.shtml">Using entries</a></td>
</tr>
<tr>
<td class="nav"><a href="search.shtml">Search</a></td>
</tr>
<tr>
<td width="20%" align="center" valign="top">
<!-- navigation -->
<!--#include file="nav.html"-->
</td>
<td width="80%" valign="top">
<!-- content -->
<td class="nav"><a href="statistics.shtml">Statistics</a></td>
</tr>
<tr>
<td class="nav"><a href="topics.shtml">Index</a></td>
</tr>
<tr>
<td class="nav"><a href="download.shtml">Download</a></td>
</tr>
</table>
<p>&nbsp;</p>
<p>&nbsp;</p>
</td>
<!-- Content -->
<td width="80%" valign="top">
<div align="center">
<p>&nbsp;</p>
<h1><font class="first">A</font>rchive of
<font class="first">F</font>ormal
<font class="first">P</font>roofs</h1>
<p>&nbsp;</p>
<p>&nbsp;</p>
<h1><font class="first">A</font>rchive of
<font class="first">F</font>ormal
<font class="first">P</font>roofs</h1>
</h1>
<p>&nbsp;</p>
<table width="80%" class="descr">
<tbody>
......@@ -84,11 +124,19 @@ free to redistribute with minimal restrictions.</p>
<p>The authors retain their full copyright on their original work,
including their right to make the development available under another,
additional license in the future.</p>
</td></tr>
</td></tr>