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
orupdate
. - 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
orupdate
. - needs alias: A definition in the file already has another name. You can use the
alias.term
oralias.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.