cooltt

To enable cooltt command completions in Zsh, you must add the cooltt/zsh directory to your $fpath and ensure compinit is called. Add the following lines to your ~/.zshrc file, replacing PATH-TO-COOLTT with the actual absolute path to the cooltt installation directory:

fpath=(PATH-TO-COOLTT/zsh $fpath)
compinit #if `compinit` would not be called by the end of your ~/.zshrc

You can install or reinstall the plugin by running the install.sh script from the plugin directory. The plugin is compatible with Vim 8's package system.

./install.sh

To build cooltt using OPAM, ensure you are using OCaml 5.0. You can create a compatible switch using opam switch create 5.0.0.

Follow these steps to install dependencies and build the package:

1. Update opam: opam update
2. Pin the local directory: opam pin add -y cooltt . (only required the first time)
3. Upgrade dependencies: opam upgrade

If you are actively developing the project and using dune, use these commands to manage the environment:

• make upgrade-pins: Updates and upgrades dependencies for active development.
• dune exec cooltt: Runs the cooltt executable from the top-level directory.

# Create OCaml 5.0 switch
$ opam switch create 5.0.0

# Install dependencies
$ opam update
$ opam pin add -y cooltt .
$ opam upgrade

# For active development
$ make upgrade-pins
$ dune exec cooltt

The cooltt command-line tool is used to elaborate and normalize terms in Cartesian cubical type theory. It supports two primary modes: scripting (default), where you provide a file or standard input to process, and interactive, which launches a REPL (Read-Eval-Print Loop).

# Run in scripting mode on a specific file
cooltt my_term.ctt

# Run in interactive REPL mode
cooltt --interactive

# Run in scripting mode using standard input
cat my_term.ctt | cooltt -

If you use the Nix package manager with flakes enabled, you can build or develop with cooltt using the following methods:

To build the binary: Run nix build. This will place the cooltt binary in result/bin/cooltt.

To enter a development environment: Run nix develop. This enters a shell containing the OCaml compiler, dune, and other necessary tools. Once inside the shell, you can follow the OPAM build instructions.

# Build the binary
nix build

# Enter development shell
nix develop

While editing a .cooltt file, you can trigger checks to display the current buffer's status in a separate buffer using the following commands:

• :Cooltt or <LocalLeader>l: Checks the entire current buffer.
• <LocalLeader>p: Performs a partial check, ignoring lines below the current cursor position.

From the resulting output buffer, you can press CTRL-] to jump directly to the location of the message in your source file.

" Examples of commands in Normal mode
:Cooltt
:<LocalLeader>l
:<LocalLeader>p

If the cooltt binary is not available in your system's PATH, you must manually specify its location in your .vimrc using the g:cooltt_path variable.

let g:cooltt_path = '/path/to/the-cooltt-binary'

cooltt uses specific Unicode characters. You can type these in Vim using the digraph feature (via Ctrl-k) or by using their ASCII equivalents.