Installation
This guide will help you install Ursus and all its dependencies. The installation process is straightforward and takes about 15-30 minutes.
Overview
Ursus is built on top of the Coq proof assistant and requires several components:
- OPAM - OCaml package manager
- Coq - The proof assistant (version 8.13 or later)
- Dependencies - Required Coq libraries
- Ursus Libraries - The Ursus language and tools
Quick Start
If you're experienced with Coq and OPAM:
# Install OPAM and Coq
opam install coq.8.13.2
# Install Ursus dependencies
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-mathcomp-ssreflect coq-elpi
# Clone and install Ursus (contact Pruvendo for repository access)
git clone <ursus-repository-url>
cd ursus
make install
Detailed Installation
For a step-by-step guide, follow these sections:
1. Install OPAM
OPAM is the OCaml package manager used to install Coq and its libraries.
What you'll do:
- Install OPAM for your operating system
- Initialize OPAM environment
- Set up an OPAM switch for Coq
Time: ~5 minutes
2. Install Coq
Coq is the proof assistant that Ursus is built on.
What you'll do:
- Install Coq 8.13.2 (recommended version)
- Verify Coq installation
- Install CoqIDE (optional but recommended)
Time: ~10 minutes
3. Install Pruvendo Libraries
Install Ursus and its dependencies.
What you'll do:
- Install required Coq libraries
- Clone Ursus repositories
- Build and install Ursus
- Verify installation
Time: ~15 minutes
System Requirements
Supported Operating Systems
- Linux - Ubuntu 20.04+, Debian 10+, Fedora 33+
- macOS - 10.15 (Catalina) or later
- Windows - WSL2 (Windows Subsystem for Linux)
Hardware Requirements
- RAM: 4 GB minimum, 8 GB recommended
- Disk Space: 2 GB for Coq and Ursus
- CPU: Any modern processor (compilation can be slow on older CPUs)
Installation Methods
Method 1: OPAM (Recommended)
Install using OPAM package manager. This is the recommended method as it handles dependencies automatically.
Pros:
- Automatic dependency management
- Easy updates
- Multiple Coq versions support
Cons:
- Requires OPAM setup
- Can be slow on first install
Guide: Follow OPAM Installation → Coq Installation → Pruvendo Libraries
Method 2: Docker
Use pre-built Docker image with everything installed.
Pros:
- No local installation needed
- Consistent environment
- Quick setup
Cons:
- Requires Docker
- Larger disk usage
- May have performance overhead
Guide: See Docker Installation (coming soon)
Method 3: From Source
Build everything from source code.
Pros:
- Full control
- Latest development version
- Custom optimizations
Cons:
- Complex setup
- Manual dependency management
- Longer installation time
Guide: Advanced users only - see individual component documentation
Verification
After installation, verify everything works:
# Check Coq version
coqc --version
# Should show: The Coq Proof Assistant, version 8.13.2
# Check Ursus installation
coqc -Q . Ursus -R . UrsusEnvironment
# Should compile without errors
Troubleshooting
Common Issues
OPAM not found:
# Make sure OPAM is in your PATH
eval $(opam env)
Coq version mismatch:
# Switch to correct Coq version
opam switch create ursus 4.12.0
opam install coq.8.13.2
Build errors:
# Clean and rebuild
make clean
make -j4
Getting Help
If you encounter issues:
- Check the FAQ (coming soon)
- Contact Pruvendo team for support
- Review the documentation thoroughly
Next Steps
Once installed, you're ready to start:
- Quick Start - Write your first contract in 10 minutes
- Ursus Language - Learn the language
- Examples - Browse ursus-patterns repository for example contracts
Alternative: Try Online
Don't want to install locally? Try Ursus online:
- Coq Playground - Run Ursus in your browser (coming soon)
- Cloud IDE - Cloud development environment (coming soon)
Ready to install? Start with OPAM Installation →