diff --git a/metadata/templates/about.tpl b/metadata/templates/about.tpl --- a/metadata/templates/about.tpl +++ b/metadata/templates/about.tpl @@ -1,76 +1,76 @@ {% extends "base.tpl" %} {% block headline %} Archive of Formal Proofs {% endblock %} {% block content %}
AboutThe Archive of Formal Proofs is a collection of proof libraries, examples, and larger scientific developments, mechanically checked in the theorem prover Isabelle. It is organized in the way of a scientific journal. Submissions are refereed. -The archive repository is hosted on Bitbucket to + The archive repository is hosted on Heptapod 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. EditorsThe editors of the archive are
WhyWe aim to strengthen the community and to foster the development of formal proofs. We hope that the archive will provide
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 easier 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. License-All entries in the Archive of Formal Proofs are licensed under + All entries in the Archive of Formal Proofs are licensed under a BSD-style License or the GNU LGPL. This means they are free to download, free to use, free to change, and free to redistribute with minimal restrictions. The authors retain their full copyright on their original work, -including their right to make the development available under another, +including their right to make the development available under another, additional license in the future. |
Test status of entries in the AFP development version
|
[{{entry.status}}] | {{entry.name}} |
Please send your submission via this web page. The submission must follow the following Isabelle style rules. For additional guidelines on Isabelle proofs, also see the this guide (feel free to follow all of these; only the below are mandatory). Technical details about the submission process and the format of the submission are explained on the submission site.
Your submission must contain an abstract to be displayed on the web site – usually this will be the same as the abstract of your proof document in the root.tex file. You can use LaTeX formulae in this web site abstract, either inline formulae in the form $a+b$ or \(a+b\) or display formulae in the form $$a + b$$ or \[a + b\]. Other occurrences of these characters must be escaped (e.g. \$ or \\(). Note that LaTeX in the title of an entry is not allowed. Most basic LaTeX functionality should be supported. For details on what parts of LaTeX are supported, see the MathJax documentation. It is possible and encouraged to build on other archive entries in your submission. There is a standardised way to refer to other AFP entries in your theories. 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. If you have questions regarding your submission, please email afp-submit@in.tum.de. If you need help with Isabelle, please use the isabelle-users@cl.cam.ac.uk mailing list. It is always a good idea to subscribe. |
ChangeThe 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. This conflicts with the purpose of archiving and preserving -entries as they have been submitted and with the purpose of +entries as they have been submitted and with the purpose of providing a clear and simple interface to readers. The AFP deals with this by synchronizing such updates with Isabelle releases:
Significant changes of an entry should be recorded in the metadata of the entry using the keyword "extra-history". The resulting web page should look something like this. MonotonicityUpdating an entry should be mostly monotone: you add new material, but you do not modify existing material in a major way. Ideally, entries (by other people) that build on yours should not be affected. Otherwise you have to liaise with them first. If you intend to carry out major non-monotone changes, you will need to submit a completely new entry (with a description of how it relates to the old one). This should be required only very rarely: AFP entries should be mature enough not to require major changes to their interface (i.e. the main functions and theorems provided). Major monotone changes, e.g. adding a new concept rather than more results on existing concepts, may also call for a new entry, but one that builds on the existing one. This depends on how you would like to organize your entries. If you are an authorThe 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. To achieve this, you should base your changes on the mercurial +href="https:/foss.heptapod.net/isa-afp/afp-devel/">mercurial development version of your AFP entry and test it against the current Isabelle development version. -If you would like to get write access to your entry in the +If you would like to get write access to your entry in the mercurial repository or if you need assistance, please contact the editors. |
|
Archive of Formal Proofs
|
|
Statistics
|
|
Submission Guidelines
|
|
Updating Entries
|