# DarcsWeb
A web interface for browsing [darcs](https://darcs.net) repositories, inspired
by gitweb. Built in Haskell using the darcs library API directly (no CLI
invocation) and the [Scotty](https://github.com/scotty-web/scotty) web
framework. Pure server-side HTML and CSS, no client-side JavaScript.
## Building
DarcsWeb uses [Stack](https://docs.haskellstack.org/) as its build system.
### Prerequisites
Install Stack if you don't have it:
```
curl -sSL https://get.haskellstack.org/ | sh
```
Or via your package manager. A recent version of Stack is recommended (>= 2.9).
If you have an older version, upgrade with:
```
stack upgrade
```
Stack will automatically download and manage the correct GHC version.
You also need [Rocq](https://rocq-prover.org/) (formerly Coq) installed and
available as `rocq` on your `PATH`. The project uses Rocq to compile formally
verified pure functions that are extracted to Haskell during the build. Rocq can
be installed via [opam](https://opam.ocaml.org/):
```
opam install rocq-core rocq-stdlib
```
### Build
```
stack build
```
On the first run this downloads GHC and all dependencies, which takes a while.
Subsequent builds are fast.
The build automatically compiles the Rocq sources in `verified/` and extracts
Haskell modules into `gen/` before compiling the Haskell code (via a custom
`Setup.hs` pre-build hook).
### Test
```
stack test
```
This runs two phases:
1. **Rocq proof verification** -- checks all formal proofs in
`verified/*_proofs.v`.
2. **QuickCheck property tests** -- runs property-based tests for the pure
Haskell functions that are not formally verified.
### Install
To install the `darcsweb` binary into `~/.local/bin`:
```
stack install
```
## Configuration
DarcsWeb is configured through a plain-text configuration file. The `-c` flag
pointing to this file is required to start the application.
Copy the example and adjust it:
```
cp darcsweb.conf.example /etc/darcsweb.conf
```
### Configuration keys
| Key | Description | Default |
|----------|---------------------------------------------------|---------------|
| `bind` | IP address to bind to | `127.0.0.1` |
| `port` | TCP port to listen on | `3000` |
| `repos` | Directory containing darcs repositories | `.` |
| `title` | Site title shown in the page header | `DarcsWeb` |
| `static` | Path to the static assets directory | `static` |
The file format is one `key = value` pair per line. Blank lines and lines
starting with `#` are ignored.
Example configuration:
```
# /etc/darcsweb.conf
bind = 0.0.0.0
port = 8080
repos = /srv/darcs
title = My Repositories
static = /usr/share/darcsweb/static
```
### Repository descriptions
To show a description for a repository on the index page, create the file
`_darcs/prefs/repo_description` inside the repository:
```
echo "My awesome project" > /srv/darcs/myrepo/_darcs/prefs/repo_description
```
## Running
```
darcsweb -c FILE [-d]
```
| Flag | Description |
|--------------|------------------------------------------|
| `-c FILE` | Path to the configuration file (required)|
| `-d` | Run as daemon |
If `-c` is omitted, a usage message is printed and the process exits.
### Foreground mode (default)
Without `-d`, DarcsWeb runs in the foreground and logs to stdout:
```
stack run -- -c /etc/darcsweb.conf
```
Or, if installed:
```
darcsweb -c /etc/darcsweb.conf
```
### Daemon mode
With `-d`, DarcsWeb forks into the background, detaches from the terminal, and
logs to syslog (facility `daemon`):
```
darcsweb -c /etc/darcsweb.conf -d
```
Messages appear in the system log under the identifier `darcsweb`, e.g.:
```
journalctl -t darcsweb
```
### Docker
The included `Dockerfile` produces a minimal image with just the `darcsweb`
binary and static assets. The base images (`haskell:9.6-slim`,
`debian:bookworm-slim`) are multi-arch, so this works on both x86-64 and ARM64
hosts such as the Raspberry Pi 5.
Build the image:
```
docker build -t darcsweb .
```
Run it, bind-mounting your host repositories read-only:
```
docker run -d -p 3000:3000 -v /srv/darcs:/srv/darcs:ro darcsweb
```
The `:ro` mount is sufficient -- DarcsWeb only reads `_darcs/` contents. Because
bind mounts reflect the host filesystem in real time, new patches and new
repositories show up immediately without restarting the container.
To override the built-in configuration, mount your own file:
```
docker run -d -p 8080:8080 \
-v /srv/darcs:/srv/darcs:ro \
-v /etc/darcsweb.conf:/etc/darcsweb.conf:ro \
darcsweb
```
Multiple repository directories can be served by mounting them under a common
prefix:
```
docker run -d -p 3000:3000 \
-v /home/user/repos:/srv/darcs/personal:ro \
-v /srv/shared:/srv/darcs/shared:ro \
darcsweb
```
#### Cross-building for Raspberry Pi 5
If you prefer to build the image on a faster x86-64 machine and deploy to
a Pi 5:
```
docker buildx build --platform linux/arm64 -t darcsweb:arm64 --load .
docker save darcsweb:arm64 | ssh pi@raspberrypi docker load
```
This requires Docker Buildx with QEMU emulation (`docker run --privileged
--rm tonistiigi/binfmt --install arm64`).
#### TLS with Let's Encrypt
The included `docker-compose.yml` and `nginx.conf` add an nginx reverse proxy
with automatic Let's Encrypt certificates via certbot.
1. Replace `darcs.example.com` with your domain in both `nginx.conf` and the
certbot command below.
2. If your repositories are not in `/srv/darcs`, update the volume mount in
`docker-compose.yml`.
3. Start nginx and darcsweb (certbot needs nginx running for the ACME
challenge):
```
docker compose up -d nginx darcsweb
```
4. Obtain the initial certificate:
```
docker compose run --rm certbot certonly --webroot \
-w /var/www/certbot -d darcs.example.com
```
5. Reload nginx to pick up the new certificate, then start the certbot
renewal sidecar:
```
docker compose exec nginx nginx -s reload
docker compose up -d certbot
```
The certbot container renews certificates automatically every 12 hours (a
no-op when they are not yet due). After renewal nginx must be reloaded; a
cron entry on the host handles this:
```
0 */12 * * * docker compose exec nginx nginx -s reload
```
Certificate data is stored in the `certbot_conf` volume and persists across
restarts.
## Pages
| Route | Description |
|--------------------------------|----------------------------------------------|
| `/` | Repository index -- lists all repositories |
| `/repo/:name/summary` | Repository overview with recent patches and tags |
| `/repo/:name/shortlog` | Compact patch log (date, author, name) |
| `/repo/:name/log` | Full patch log with descriptions and summaries |
| `/repo/:name/tags` | All tagged patches |
| `/repo/:name/patch/:hash` | Single patch detail with full diff |
## Formal Verification
Security-critical pure functions are implemented in Gallina (the Rocq/Coq
specification language), formally proven correct, and extracted to Haskell for
use at runtime. This follows the same approach as
[hopify](https://github.com/...) -- identify pure functions, reimplement them in
Gallina, and export them to the target language.
### Verified functions
| Function | Source | Replaces |
|---|---|---|
| `esc` / `esc_char` | `verified/html_pure.v` | HTML entity escaping in `DarcsWeb.Html` |
| `is_safe_sub_path` / `split_path` | `verified/path_pure.v` | Path traversal validation in `DarcsWeb.Darcs` |
| `add_trailing_slash` | `verified/path_pure.v` | Jail-check path normalisation in `Main` |
### Proven properties
The proof files (`verified/*_proofs.v`) establish:
- **Concrete correctness**: each dangerous character (`<`, `>`, `&`, `"`, `'`)
maps to the correct HTML entity.
- **Security theorems**: the output of `esc` contains no raw `<`, `>`, or `"`
characters -- proven by exhaustive case analysis over all 256 ASCII values
combined with structural induction over the input string.
- **Path safety**: `is_safe_sub_path` rejects `..`, `_darcs`, `.git`, hidden
files (names starting with `.`), and empty paths; accepts legitimate nested
paths.
- **Idempotence**: `add_trailing_slash` applied twice equals applying it once.
### Property-based tests
Functions that remain in Haskell (because they depend on types or libraries not
easily represented in Gallina) are tested with QuickCheck:
| Function | Properties |
|---|---|
| `highlightDiff` | Correct CSS class wrapping for `+`/`-`/`@@` prefixed lines |
| `shortAuthor` | Email stripping, plain name preservation |
| `formatSize` | Correct unit suffix (`B`/`KiB`/`MiB`) for each size range |
| `formatAbsolute` | Short strings unchanged, long date strings gain separators |
### Project layout
```
verified/ Rocq/Coq sources and Makefile
html_pure.v HTML escaping implementation + extraction
path_pure.v Path validation implementation + extraction
html_pure_proofs.v Proofs for HTML escaping
path_pure_proofs.v Proofs for path validation
Makefile Build rules for extraction and proof checking
gen/ Auto-generated Haskell (do not edit)
HtmlPure.hs Extracted from html_pure.v
PathPure.hs Extracted from path_pure.v
Setup.hs Custom build hooks (runs Rocq extraction before build)
test/
Spec.hs Test runner (proofs + QuickCheck)
Properties/Html.hs QuickCheck property definitions
```
## License
GPL-2.0-or-later (same as darcs).
/ darcsweb / blob / README.md