UCM command reference

This document lists all the current UCM commands, gives basic usage instructions and links to further reading. Commands are listed alphabetically in this document.


This is how you add new definitions to the codebase. It tries to add all definitions from the most recent typechecked file.

x = 42
.> add

Adds x to the root namespace. If we first cd foo.bar, then the add creates foo.bar.x in the codebase. That is, the names in the most recent typechecked file are added underneath the current namespace.

FAQ about the add command

I got an error about "these definitions failed" on add

This message happens when some of the definitions couldn't be added to the codebase. UCM shows a table of definitions along with the reason why they didn't succeed, like this:

  x These definitions failed:

    needs alias   List.sum   : [Nat] -> Nat

    Tip: Use `help filestatus` to learn more.

Here's what these reasons mean:

  • needs update: The scratch file has a definition with the same name as an existing definition. Doing update instead of add will turn this failure into a successful update.
  • conflicted: The file has a definition whose name is currently conflicted. Resolving the conflict (see concurrent work and resolving conflicts to learn more) and then trying an update again will turn this into a successful update.
  • term/ctor collision: A definition with the same name as an existing constructor for some data type. Rename your definition or the data type before trying again to add or update.
  • ctor/term collision: A type defined in the file has a constructor that's named the same as an existing term. Rename that term or your constructor before trying again to add or update.
  • needs alias: A definition in the file already has another name. You can use the alias.term or alias.type commands to create new names for existing definitions.
  • blocked: This definition couldn't be added because it dependended on another definition in the file that had a failed status.
  • extra dependency: This definition was added because it was a dependency of a definition explicitly selected.

I want to undo a partially completed add where some of the definitions failed

Just do undo!