Tag Archives: Software

Installation Of Coq On Ubuntu

When I talked in my my first post about giving stuff back, I also thought about simple tutorial like installing software. While such tutorials are not strictly necessary, they save time… They saved me a lot of time! Especially when you’re new to an operating system, university, a programming language etc etc. And sometimes you’re a lot of those things at once.
To put it simply, sometimes it’s just good being able to outsource something so that you can spend your time thinking about more urgent stuff.

So here we go… Today I will show how I installed Coq on my system, which is a software for writing and managing logical proofs. I need this software for my lecture Introduction to Computational Logic, which will take use of it.

For the impatient amongst you, I suggest you to skip to end… Just saying. :’D

So let me first show you, which Ubuntu release I’m using. Depending on your exact operating system, distribution and release your installation might vary.

lsb_release -d
## Description: Ubuntu 18.04.2 LTS

Alright, now that you know that, I first have to install opam, which is the package manager for OCaml. Phew… What a luck. With a Linux distribution based on Debian, it is available through the package manager. So I can just install it by typing:

sudo apt-get install opam

Subsequently I have to initialize the state of opam

opam init

Now let’s list all the through opam available packages.

opam list -a | head
## # Available packages for system:
## 0install                                --  The antidote to app-stores
## aacplus                                 --  Bindings for the aacplus library whi
## abella                                  --  Interactive theorem prover based on 
## abt                                     --  OCaml port of CMU's abstract binding
## acgtk                                   --  Abstract Categorial Grammar developm
## acme                                    --  A library to interact with the acme 
## acpc                                    --  Chemoinformatics tool for ligand-bas
## aez                                     --  Alt-Ergo Zero is an OCaml library fo
## afl                                     --  American Fuzzy Lop fuzzer by Michal 
## Fatal error: exception Sys_error("Broken pipe")

I piped the output into head, because there are quite a lot of packages, with whom I don’t wanna clutter up this post. Don’t mind the Broken pipe error, that’s because head kills opam after reading its first five lines.

Which packages we now want are Coq and the CoqIDE. We can achieve this by simply typing:

opam install coq coqide

OK… Didn’t work. What did opam say?

=> This package relies on external (system) dependencies that may be missing.
   `opam depext conf-gtksourceview.2' may help you find the correct
   installation for your system.

The former state can be restored with:
    opam switch import "~/.opam/system/backup/state-20190310192746.export"

Therefor let’s do, what the output tells us to:

opam depext conf-gtksourceview.2

And by installing some additional packages this command took care for me of it.
Afterwards let’s try to install CoqIDE again, because Coq itself worked fine the first time.

opam install coqide

This time it worked… Perfect!

A Much Simpler Way


OK, after I didn’t find out how to start this IDE I did some googling and found out, that I could also just install it from the Ubuntu repository using the following command:

sudo apt-get install coqide
A screenshot of the installed CoqIDE on Ubuntu
Screenshot of the CoqIDE on my system

I should’ve probably checked this first and I would’ve probably saved a lot of time. Now it works! x)
Maybe my foolishness of not checking the Ubuntu repo first teaches you something.

Have a nice evening!

Please follow and like us: