add

myProject/main> add
myProject/main> add myNewTerm

Adds all the definitions from the most recently typechecked file to the codebase.

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:

Reason
needs update   myFunction : Doc

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 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

You can use the undo command in the case of an undesired partially completed add.