discover · compare · collections · requirements · contribute · feed · watching · stats · help with your tokens

lenianiva/Prismriver · source

Snapshot 0 · 2026-11-04T12:47:28Z · Lean · Apache-2.0

GitHub description at capture

(Mirror) A Music formalization library and DSL in Lean 4

README at capture

# Prismriver

[![arXiv](https://img.shields.io/badge/cs.LO-2606.19936-f1eeee?labelColor=1b1b1b&logo=arxiv&logoColor=red)](https://arxiv.org/abs/2606.19936)

A Music formalization library and DSL in Lean 4 for:

1. Formalization of music theory including pitches, accidentals, scales, chords,
   durations, parts
2. Algorithmic analysis (e.g. key estimation) and composition (counterpoint)
3. Mathematical modeling of music
4. Lilypond compatible music syntax

## Structure

### Tuning and Scale

Scales are handled in [Scale.lean](Prismriver/Repr/Scale.lean) and
[Classical.lean](Prismriver/Repr/Classical.lean). We do not distinguish between
tuning systems and scales. A `PseudoScale` is a list of pitches. A `Scale` is a
list of pitches with a fundamental interval. This flexibility handles
xenharmonic tuning systems that are not based on Western music theory. Equal
temperament is a scale. A `Tuning` system maps one scale to another. For
example, under the equal temperament tuning system, C♯ and D♭ are enharmonic.

[Classical.lean](Prismriver/Repr/Classical.lean) handles Western Classical
music. Each pitch is the combination of a name (`Hep`), an accidental, and an
octave, with the octave being the fundamental interval. An interval has a letter
distance and a semitone distance. We can transpose a note using arithmetic
operations `+` and `-`. In some sense, the intervals form a group action on
pitches. This also recalls properties of affine spaces.

Whether an interval is consonant or dissonant is dependent on the physical
properties of the instrument and this varies across cultures, and hence the
choice of consonant intervals is left as free parameters in composition
algorithms. We still provide convenient shortcuts such as `p5` or `ma6` for
intervals.

### Time

We handle time, the other axis of music, in
[Time.lean](Prismriver/Repr/Time.lean). To allow arbitrary musical sequences,
the most general form of time only consists of an instance type `I` and a
duration type `D`. `MeasuredTime` is a representation based on bars and rational
offsets. This abstraction is out of consideration of flexibility. The time as
written on paper may not exactly match the time of performance.

### Composition and Analysis

[Score](Prismriver/Repr/Score.lean) contains an implementation of music scores.
Each score is a list of ordered events along time instances.

In [Composition](Prismriver/Composition), we implemented algorithmic composition
of [counterpoints](Prismriver/Composition/Counterpoint.lean).

### Syntax and Playback

A [LilyPond](https://lilypond.org/)-like DSL is provided in
[Syntax.lean](Prismriver/Syntax.lean).

Prismriver supports playback using [Alda](https://alda.io/). Alda is optional,
but it is necessary for playing music.

This command plays the first 5 notes of Necrofantasia

```lean
import Prismriver
#play ♩[e4 c'4 b4 d4 e2]
```

Prismriver supports output to MusicXML. Alda can also play MusicXML generated by
Prismriver's IO:

``` sh
alda import -i musicxml -f $NAME.musicxml | alda play
```

### Troubleshooting

If during compilation, Lean complains

```
error loading library, libLake_shared.so: cannot open shared object file: No such file or directory
```

it may be necessary to setup the environment:

``` sh
export LEAN_ROOT=$(lean --print-prefix)
export LD_LIBRARY_PATH=$LEAN_ROOT/lib/lean:$LD_LIBRARY_PATH
```

## Contributing

Every commit must pass through pre-commit hooks. Install `prek` (provided in
[`shell.nix`](shell.nix)), and run

``` sh
prek install
```

See [roadmap](doc/roadmap.typ) (need to be compiled with Typst).

### Contributors and Acknowledgments

- [Leni Aniva](https://leni.sh)
- [Claire Wang](https://clairewang.net)

References

- [Lulu](https://github.com/iehality/Lulu)
- [Music: A Mathematical Offering](https://logosfoundation.org/kursus/music_math.pdf)