Last modified: January 28, 2024.
We will use the following ebook to learn to use the Coq proof assistant:
The machines in the Zoo are named as follows:
aphid bumblebee cardinal chameleon cicada
cobra cricket frog gator giraffe
grizzly hippo hornet jaguar ladybug
lion macaw monkey newt peacock
perch python rattlesnake rhino scorpion
swan termite tick turtle viper
If you plan to take the course for credit, you should get an account on these machines as soon as possible. Please visit the following web site to create a cs428 class directory:
http://zoo.cs.yale.edu/accounts.html
NOTE: this step is required if you want to use the submit/unsubmit
commands on the Zoo machines.
Problem sets are due at 11:59 PM on the date specified.
Each student is given 144 discretionary late hours for assignments, but any one assignment may only be up to 72 hours late. These are calendar hours, not business hours. As the homework assignments are submitted electronically, the "write date" on the student's homework file will be considered the completion date for late assignments.
After you use up all of your discretionary late hours, assignments turned in late will be graded according to the following formula: S = R * (1 - t / c), where S is the grade given, R is the grade the work would have gotten if turned in on time, t is the amount of time by which the work was late, and c is equal to four days. Thus, the value of a late assignment decays daily, with a half-life of just over two days. Examples: work turned in five minutes late gets 99.9% credit, one hour late gets 99.0% credit, six hours late gets 93.8% credit, one day late gets 75.0% credit, two days late gets 50.0%, and three days late gets 25.0%. Assignments submitted more than 72 hours late will not be accepted.
/c/cs428/bin/submit number filesnumber is the assignment number and files is the list of files for that assignment. For example,
/c/cs428/bin/submit 3 README Basics.v Induction.vsubmits the files README, Basics.v, and Induction.v for a fictitious assignment 3.
The submit command copies your files to the directory /c/cs428/SUBMIT/number/login and lists all the files that you have submitted for assignment number. Here, login is your user account name.
There is also unsubmit, which allows you to retract one or more files. For example,
/c/cs428/bin/unsubmit 3 Basics.vwould remove your Basics.v from the submission directory.
You can also check what files you have submitted by using the check command. For example,
/c/cs428/bin/check 3would list all the files your have submitted so far for assignment 3.
Usually, you can omit the /c/cs428/bin/ prefix if /c/cs428/bin/ is already added to your PATH variable.