On this page:
5.1 Accessing Marmoset
5.2 Submitting Assignments
6.6

5 Marmoset

5.1 Accessing Marmoset

Go to the Marmoset home page and log in using your Quest/WatIAM userid and password. Click the "as" button under "Authenticate". You should only have one choice here (unless you are taking another course that uses Marmoset). Click "CS798 (Fall 2016):".

If you don’t see what you’re supposed to see in the steps above, then you are probably not yet added as a student to CS 798 on Marmoset. Contact Prabhakar to resolve this issue. Note that only registered students need to or should want to use Marmoset.

You should now be able to see the assignments that have been set up on Marmoset for CS 798. You can submit your assignment files to Marmoset via the "web submission" page for each assignment question.

5.2 Submitting Assignments

If only one file is required for an assignment question, you can submit only that file. If multiple files are required for an assignment question, you must zip all of the required files and submit the zip file. Make sure that all of the required files with a required name are named correctly; otherwise, you will receive "did not compile" as the test result.

If you have used Marmoset before, you will find this experience a ittle different. Normally Marmoset runs a series of tests on your code, gives you some information about the results, and allows you to submit again in a controlled fashion if you didn’t pass them all. But since Coq itself checks your proofs, there is no need for real tests. Marmoset will have one "public test" that runs Coq on your submission, parses the output, and reports on which exercises you have completed and your total score (which you should know already; this is just a sanity check). There are no "release tests". Of course, exercises that require hand-marking will not be scored correctly in this report. You may submit multiple times; your latest on-time submission is the one that will count.