Next: Sequence Logic, Previous: Customization, Up: Top

## 8 Proof Submission

GNU Aris allows users to submit their proofs to a grading server, which allows instructors to use Aris in their classes. Aris submits proofs through FTP, and allows users to indicate an email for themselves and an optional email for their instructors.

Submission allows for all open proofs to be submitted. This is done by specifying a problem designation (‘`11.10`’, ‘`nats`’, etc.). Only those that have designations are submitted. The designation is changed by editing the text box next to each file name in the submission dialog box.

Grading runs by checking the correctness of the entire proof. It is the responsibility of the grading server to confirm that the proof is the correct proof.

When the files are submitted, Aris submits them to the server, along with a directive file. The directive file will be named ‘`USER.directive`’, where ‘`USER`’ is the base name of the email address specified. The files submitted will be renamed to be ‘`BASE-USER.tle`’, where ‘`BASE`’ is the original basename of the file. This prevents filename conflicts on the FTP server. The grading server will then run Aris in grade mode (see Options), and use the email provided to email the results back to the user. If the user specified an instructor's email address, then Aris will CC the instructor.

Sample scripts are included with GNU Aris. These are the files ‘`doc/collect.sh`’ and ‘`doc/collect.el`’. The grade server would run ‘`collect.sh`’, which will call GNU Emacs in batch mode while loading ‘`collect.el`’. It is ‘`collect.el`’ that handles the emails.