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 "CS747 (Spring 2021):".

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 747 on Marmoset (I will add everyone who is registered on the first day but I might miss those who register after that). Contact me to resolve this issue; I will need your 8-character UW userid, and your first and last name. Only registered students need to or should want to use Marmoset. In this course, it won’t provide any additional useful information about your work.

You should now be able to see the assignments that have been set up on Marmoset for CS 747. 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 little 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 Agda itself checks your proofs, there is mostly no need for real tests. Marmoset will have one "public test" that runs Agda on your submission, to make sure it compiles and no types have been changed. Unlike in normal use, here Marmoset gives you no information you could not get for yourself easily.

For example, when you submit 747Naturals.agda, Marmoset will compile it, and then compile a file called TestNaturals.agda. There are no actual tests in that file, which imports your submitted definitions. If you’ve been asked to define a function f with type X, the file will declare a function g with type X, and use the definition g = f. This will fail if you have changed the type of f to some other type Y. Nothing more sophisticated is going on in Marmoset. Any further requirements I have imposed on a solution have to be checked by hand.

Please try to make sure your file compiles (possibly with warnings for uncompleted exercises). Please do not delete uncompleted exercises. If you do, or if your submitted file is in a strange state, I will open it and try to fix it, but this is extra work for me.

You may submit multiple times; your latest on-time submission (or late submission if you have gotten an extension) is the one I will use.