Installing Coq

Coq is the proof assistant that Ursus is built on. We use Coq 8.16.1.

Prerequisites

Make sure you have OPAM installed first.

Clean Previous Installations

Remove old Coq versions to avoid conflicts:

# Check if Coq is installed
coqc --version

# If found, remove it
opam remove coq

Install Coq

Create OPAM Switch

opam switch create coq-8.16 4.12.0
eval $(opam env)

Install Coq 8.16.1

opam pin add coq 8.16.1
eval $(opam env)

Verify Installation

coqc --version
# Should show: The Coq Proof Assistant, version 8.16.1

Install IDE

VS Code (Recommended)

1. Install VS Code: Download here

2. Install Coq Extension:

   • Open VS Code
   • Go to Extensions (Cmd+Shift+X / Ctrl+Shift+X)
   • Search for "vscoq1"
   • Install VsCoq

3. Install Math Unicode Extension (optional):

   • Search for "unicode-math-vscode"
   • Install Unicode Math

4. Test It:

   • Open any .v file
   • Use Alt+↓ to step forward
   • Use Alt+↑ to step backward

CoqIDE (Alternative)

opam install coqide

Common Issues

Build fails with missing system packages:

# Ubuntu/Debian
sudo apt-get install build-essential m4

# macOS
xcode-select --install

OPAM environment not updated:

eval $(opam env)
# Add to ~/.bashrc or ~/.zshrc:
echo 'eval $(opam env)' >> ~/.bashrc

Next Steps

Continue to Pruvendo Libraries Installation →

Reference

• Official Coq Installation
• Coq Documentation