Drivers for various EPDs from Waveshare and others

Metaprogramming in Coq

A Coq plugin providing an extensible tactic similar to first.

A presenter console with multi-monitor support for PDF files.

The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environmen…

Prelude is an enhanced Emacs 29.1+ distribution that should make your experience with Emacs both more pleasant and more powerful.

Metaprogramming, verified meta-theory and implementation of Rocq in Rocq