P415/P515 Homework Procedures

This class uses Subversion (SVN), a version-control system for multi-person projects. We do not require all of SVN's functionality in this course; it just serves as a homework depository. To turn an assignment in, you will post ("up-load") a local copy of your work SVN. The instructor will also post grading information, which you can retrieve periodically by updating your local copy.

You will need to conform to a standard file organization for the homework, but you may also create additional directories for maintaining other activities relating to the course, such as presentations.

Homework Organization

Note: Homework assignment number n must be deposited in sub-directory class/logid/n

For a typical PVS assignment, you should post

1. the .PVS and .PRF files.
2. a PVS proof status file. One way to do this is to
   1. Open (M-x ff) X.pvs in PVS;
   2. Invoke either the command M-x status-proof-pvs-file, or the command M-x prove-pvs-file (which re-runs X.prf first).
   3. Save the resulting PVS Status buffer (C-x C-w as X.status)
3. You can do your work in you working copy of the repository. Alternatively, you can do the work elsewhere and transfer it to your working copy.
4. Important: For each file or directory you transfer into your working copy, you must inform SVN that it should be added to the repository by invoking svn add file, or svn add directory, respectively.
5. No changes, additions, or deletions "take effect" until you invoke the command svn commit -m "your message here".

Example

There are on-line SVN user manuals on the web [HTM]. Chapter 2 (Basic Usage) covers the commands we need. In fact, the example that follows should be adequate for posting homework.

• The link https://batson.cs.indiana.edu/svn/csci_p415_svn opens a directory browser. This is the way to navigate the repository and verify what you have posted. It is mandatory to use https. You will be prompted for a password (handed out in class).

• First, participant astudent "checks out" (makes a local copy) of their SVN subdirectory using the command svn co url dir. Argument dir is the name of astudent's local directory.

  % svn co https://batson.cs.indiana.edu/svn/csci_p415_svn/class/astudent/ p415_working_copy A p415_working_copy/0 A p415_working_copy/0/0.txt A p415_working_copy/1 A p415_working_copy/1/A.pvs A p415_working_copy/1/B.pvs A p415_working_copy/10 A p415_working_copy/11 A p415_working_copy/2 A p415_working_copy/12 A p415_working_copy/3 A p415_working_copy/4 A p415_working_copy/5 A p415_working_copy/6 A p415_working_copy/7 A p415_working_copy/project A p415_working_copy/8 A p415_working_copy/9 Checked out revision 330.

• Astudent looks at the content of the local copy to see that it is initialized with subdirectories for the homework assignments. Not only that, but the instructor has already placed PVS source files in subdirectory 1

  % cd p415_hw % ls % 0/ 1/ 10/ 2/ 3/ 4/ 5/ 6/ 7/ 8/ 9/ project/ % cd 1 % ls A.pvs B.pvs

• Astudent runs pvs4, creating A.PRF and and A.status.txt files.

  % pvs4 % ls A.prf A.pvs A.status.txt B.pvs PVSBIN/

• Very Important: Astudent must tell SVN which of these new files should be added to the repository. Do not add .pvscontext or the sub-directory PVSBIN/, a directory of large binary files that is regenerated whenever PVS is run.

  % svn add A.prf A A.prf % svn add A.status.txt A A.status.txt

• Changes to the local copy do not take effect in the repository until the owner invokes svn commit dir -m message. The -m message option deposits a message with the update.

  % cd .. % svn commit -m "Homework 1 (A) finished." Adding 1/A.prf Adding 1/A.status.txt Transmitting file data .. Committed revision 7.