- Haskell 60.7%
- Agda 26.7%
- TeX 5.3%
- HTML 4%
- Emacs Lisp 1.9%
- Other 1.4%
| .woodpecker | ||
| benchmark | rename Set to Type | |
| cubical @fe3394eba7 | ||
| doc | rename Set to Type | |
| mk | ||
| notes | ||
| src | with display: always reconstruct head term | |
| test | chore: make fix-whitespace | |
| .editorconfig | ||
| .gitignore | ||
| .gitmodules | ||
| .hlint.yaml | ||
| .mailmap | ||
| cabal.project | ||
| cabal.project.ghc-9.14.1 | fix reference to Mikan (instead of Agda) in cabal.project.ghc-9.14.1 | |
| cabal.project.tc | ||
| CHANGELOG.md | docs: update CHANGELOG | |
| CODE_OF_CONDUCT.md | ||
| CONTRIBUTING.md | docs: flesh out README | |
| fix-whitespace.yaml | ||
| flake.lock | ||
| flake.nix | ||
| HACKING.md | ||
| LICENSE | ||
| Makefile | ||
| Mikan.cabal | feat: with-application | |
| README.md | fix Cachix instructions in README | |
| weeder.toml | ||
Mikan (/mɪˈkɑːn/, after the Japanese name for Citrus unshiu) is a free and libre interactive proof assistant for cubical type theory, featuring a computational interpretation of univalence among a variety of schemas for inductive and coinductive definitions. Proofs are constructed incrementally in a flexible concrete syntax based on mixfix operators, and organised through an expressive system of parametrised modules. Mikan is a part of the 1Lab project.
Mikan was forked from the dependently-typed programming language Agda
during development of upstream version 2.9.0; specifically, the last
commit that is part of upstream history is a96a3920. You can learn
more about the motivation for the fork in the original announcement.
An up-to-date FAQ is hosted on the 1Lab.
Installation
The recommended way of installing Mikan is using the Nix flake. Our
continuous integration populates a Cachix binary cache with a ready-to-use
build of the latest commit on the main branch. Install Nix and
Cachix, then run:
$ cachix use mikan # enable our binary cache
$ nix profile add . # actually install Mikan
Mikan is primarily used through its interactive Emacs mode, which, at
the moment, is compatible with agda2-mode version 2.9.0. The Mikan
executable ships with a compatible version of its Emacs mode. Make sure
your init files contain the following:
; tell agda2-mode to call the mikan executable
(customize-set-variable 'agda2-program-name "mikan")
; load the emacs mode.
(load-file (let ((coding-system-for-read 'utf-8))
(shell-command-to-string "mikan --emacs-mode locate")))
Manual compilation
Mikan is an ordinary Haskell package, which can be built and installed with Cabal. However, Cabal installation requires additional first-time setup steps to copy the data files (the Emacs mode and built-in modules) into the proper place. Run:
$ cabal update # if necessary
$ cabal install -foptimise-heavily exe:mikan
$ mikan --setup # unpack data files
For practical use, the optimise-heavily build flag is mandatory.