Showing 25 of 25 projects
A library operating system for building secure, performant unikernels in OCaml.
A fast, composable build system for OCaml that handles low-level compilation details with a simple project description.
An editor service providing modern IDE features like context-sensitive completion for OCaml in Vim and Emacs.
A lightweight and colorful test framework for OCaml with quiet output and expressive test selection.
A dependable, cross-platform distribution of the Rocq proof assistant with a curated selection of libraries and tools.
A wrapper over opam/dune providing a cargo-like experience for creating and managing OCaml projects with integrated documentation and CI.
A library of Coq definitions, theorems, and tactics for use in other Coq developments.
Generates Nix expressions from OPAM packages to build OCaml projects within the Nix ecosystem.
A complete OCaml interface to the Slack API with a command-line notification tool.
A packager for distributing OCaml software with an API to describe installation files and distribution procedures.
A Windows-friendly distribution of OCaml focused on native development with mixed OCaml/C projects.
A Coq library extending Mathematical Components with finite sets, finite maps, and multisets on choicetypes.
A Coq library formalizing graph theory results, including Menger's Theorem, Hall's Marriage Theorem, and Wagner's Theorem.
Docker images for Coq proof assistant versions 8.4 to 8.20, based on Debian Slim with opam 2.x.
OCaml build rules for Bazel, enabling native and bytecode binary compilation with OPAM dependency management.
Extends Coq's zify tactic to support Mathematical Components library definitions for arithmetic solving.
Converts OASIS metadata to OPAM package descriptions for OCaml projects.
A Coq implementation of Sokoban, the Japanese warehouse keeper puzzle game.
Templates for generating configuration files and boilerplate for Coq projects, including CI setup and documentation.
Proof scripts and materials for tutorials on the Mathematical Components library and small-scale reflection in Coq.
A Coq library of formally verified mathematical theorems and tools covering arithmetic, real analysis, and complex analysis.
An open-source social database server built with OCaml and PostgreSQL for managing user profiles and relationships.
An Emacs minor mode for selecting and switching between OCaml opam switches via menu or command.
Coq lessons and exercises introducing the SSReflect proof language and Mathematical Components library.
Docker images providing stable versions of the Mathematical Components library for the Coq proof assistant.
Open-Awesome is built by the community, for the community. Submit a project, suggest an awesome list, or help improve the catalog on GitHub.