How to advise a thesis

Things to do in the beginning

Go to the system administrator and ask him to create a new account for the student as well as a redmine project.
Tell the students the important URLs. james.ps.uni-saarland.de for SSH, redmine.ps.uni-saarland.de for git, ps.uni-saarland.de/gosa to change their password and escher.ps.uni-saarland.de to print.
If students want to access the wired network, they have to write down their MAC adress and pass it on to the system administrator.
Students are expected to maintain a website with information on their thesis. See below for how to create a new website.
Students are expected to attend the graduate seminar on Fridays, 14:15, if there is a talk
We have a room for students (that's room 517). Students can get a key from Ute for the duration of both the seminar and thesis phase.
For some students it makes sense to formulate a detailed proposal and work-plan, to get them started in the seminar phase and have something to refer to later.

The seminar phase counts for 9 credit points, that is 270 hours of work. Students should roughly keep track of their invested time.
At about half of the seminar phase, students should give their initial talk on the thesis, explaining what they have done so far and what they plan to do (15 minutes). Advisors have to announce the talk at least one week before on the mailing list with an abstract provided by the student. There's a LaTeX beamer template.
At the end of the seminar phase, students should give their second talk, announcing the start of their thesis (15 minutes). Usually, some familiarity with the first talk is assumed.
Encourage students to write memos after they finished a chunk of work. They can use the lab's LaTeX style (now only requiring Lucida fonts if they are installed).

Students have to officially enroll at the examination office ("Prüfungssekretariat"). The duration of the thesis from this point on is 3 months.
Students should start writing as early as possible. There is a LaTeX-template. Make sure they write an introduction early.
After submitting their thesis, students have to give a final talk of 20 minutes, summarising their work completely without assuming too much familiarity with the topics presented in the first two talks.

Although the Coq IDE is improving rapidly, most members of the lab prefer Proof General.
Installation instructions are at https://yforster.github.io/coqsetup.

There's a LaTeX beamer template, a LaTeX thesis-template and the lab's LaTeX style for memos.
To format Coq-code, use this file, which provides a \begin{coq}\end{coq} environment. Use \usepackage{listings}\usepackage{lstcoq} to include it.
Use this package to link to coqdoc from the pdf document.

The talks are 15,15,20 minutes long respectively.
There's a LaTeX beamer template.
Make sure the students prepare a slide with related work and references and mention it.

The website should from the beginning on contain the (preliminary) title and the name(s) of the advisor(s). In the course of the thesis, an abstract should appear.
A picture on the index-page is not mandatory, but encouraged.
To create a webpage, log in via SSH and type cp -R /home/forster/public_html_template ~/public_html. Open the page homepage.php and add your name and username. Open index.php to add your name and provide some information. Open bachelor.php to add your title and the advisors.
If you want a picture of yourself, upload it first. Use some graphical environment to do this or scp. Then uncomment the line in index.php

To access their webpage, students have to log in via SSH to james.ps.uni-saarland.de using their username by issuing ssh username@james.ps.uni-saarland.de. James has emacs, nano and vi installed.
To access their git repository, students have to save their SSH key in redmine. Afterwards, they can clone their project.
The structure of the repository is up to them, but it makes sense to tell them about _CoqProject files and nice coqdoc. The easiest way for them is it to unzip this. Coq files go to the coq subdirectory where they have to be added to the _CoqProject file in arbitrary order.
Probably, the students want to use some base library. They can use the ICL base library contained in here. Alternatively, they can use a more evolved base library available in the redmine. To get access, contact Yannick.
There's a way to combine nice coqdoc with proviola, if you can make sense out of this.