Das Dokumentations-System sphinx

Sphinx ist ein in Python geschriebenes Shell-Programm, das aus einer bzw. mehreren Textdateien mit RestructuredText-Syntax auf dem lokalen Rechner wahlweise eine PDF-Datei oder eine bzw. mehrere HTML-Dateien erzeugen kann.[1]

Da die Syntax von RestructuredText leicht erlernbar ist, erspart man sich dank Sphinx (mindestens) die Hälfte an Arbeit, die gewöhnlich nötig ist, wenn man Dokumente sowohl als Textform (beispielsweise zum einfachen Versenden via Email) vorliegen haben als auch im Internet und/oder in druckbarer Form publizieren möchte.

Dursuchen von RST-Dateien

Da es sich bei den Quelldateien um reine Textdateien mit der Endung .rst handelt, können diese auch sehr leicht nach Inhalten durchsucht werden. Persönlich habe ich mir dazu folgende Abkürzung in der Konfigurationsdatei ~/.bashrc definiert:

alias rstgrep='find ./ -name "*.rst" | xargs grep'

In einer Shell kann damit mittels rstgrep Suchbegriff nach einem Begriff oder einem regulären Ausdruck in allen rst-Dateien eines Projekts (inklusive aller Unterverzeichnisse) gesucht werden. Dabei können selbstverständlich auch die üblichen Optionen von grep genutzt werden.

Installation von Sphinx

Sphinx sowie einige nützliche Zusatz-Pakete können unter Linux folgendermaßen installiert werden:

sudo aptitude install python3-setuptools python3-numpy python3-matplotlib python3-docutils dvipng

sudo easy_install3 Sphinx

Mit sudo easy_install3 -U Sphinx (Update) kann Sphinx jederzeit auf den aktuellsten Stand gebracht werden.

Zur Erzeugung von PDF-Druckversionen genügt bereits ein minimales LaTeX-System, wie es nach Installation der oben genannten Pakete automatisch vorhanden ist. Um beispielsweise in naturwissenschaftlichen Publikationen einen umfangreichen mathematischen Formelsatz nutzen zu können, sollte bei Bedarf ein volles LaTeX-System installiert werden.


Anmerkung:

[1]Um die erzeugten HTML-Dateien im Internet zu publizieren, müssen sie lediglich in einen gemeinsamen Ordner auf einem Webserver kopiert werden. Weist man diesem Ordner anschließend über einen Domain-Anbieter eine feste Webadresse (URL) zu, so ist die Seite bereits fertig!