Commit 4378bcaa authored by gerwin.klein@data61.csiro.au's avatar gerwin.klein@data61.csiro.au
Browse files

strongly encourage, but do not prescribe one session per entry

parent 4aadc6c4e742
......@@ -46,10 +46,17 @@
<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>
<li>The entry must contain a ROOT file with one session that has the
name of the entry. We strongly encourage precisely one session per
entry, but exceptions can be made. All sessions must be in group
(AFP), and all theory files of the submission must be contained in
at least one session. See also the example <a href="https://bitbucket.org/isa-afp/afp-2017/src/default/thys/Example-Submission/ROOT">ROOT</a> file
in the <a href="entries/Example-Submission.html">Example submission</a>.
</ul>
<p>It is possible and encouraged to build on other archive entries
in your submission. There is a standardised way to
in your submission. There is a standardised way to
<a href="using.html">refer to other AFP entries</a> in your
theories.</p>
......
chapter AFP
(* There must be one session with the name of the entry.
This session generates the web document.
There may be further sessions.
All sessions should be in group (AFP) - otherwise they are not
(* There must be one session with the (short) name of the entry.
This session generates the web document and HTML files.
It is strongly encouraged to have precisely one session, but it
if needed, further sessions are permitted.
All sessions must be in group (AFP) - otherwise they are not
run upon submission and by the later automatic regression tests.
Every theory should be included in at least one of the sessions.
Every theory must be included in at least one of the sessions.
*)
(* Session name, add to AFP group, list base session: *)
......@@ -24,7 +28,7 @@ session "Example-Submission" (AFP) = HOL +
(* The top-level theories of the submission: *)
theories
Submission
(* Dependencies on document source files: *)
document_files
"root.bib"
......
......@@ -105,10 +105,17 @@
<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>
<li>The entry must contain a ROOT file with one session that has the
name of the entry. We strongly encourage precisely one session per
entry, but exceptions can be made. All sessions must be in group
(AFP), and all theory files of the submission must be contained in
at least one session. See also the example <a href="https://bitbucket.org/isa-afp/afp-2017/src/default/thys/Example-Submission/ROOT">ROOT</a> file
in the <a href="entries/Example-Submission.html">Example submission</a>.
</ul>
<p>It is possible and encouraged to build on other archive entries
in your submission. There is a standardised way to
in your submission. There is a standardised way to
<a href="using.html">refer to other AFP entries</a> in your
theories.</p>
......
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