Building compcert

Compcert is a formally verified compiler produced for the French National Institute for Research (INRIA).  It uses machine-verified proofs to guarantee the correctness of generated code.  As such, it’s an interesting tool for exploring compiler correctness.

Below are instructions for building it (from scratch), applicable for the current 1.12 release.

  1. To start with, you need the Objective Caml language and runtime. Unfortunately, the makefile is not safe for multithreaded makes, which slows down the build process (don’t use make -j).

    $ curl -O http://caml.inria.fr/pub/distrib/ocaml-4.00/ocaml-4.00.1.tar.bz2
    $ tar -xjf ocaml-4.00.1.tar.bz2
    $ cd ocaml-4.0
    $ ./configure -prefix /usr/local/compcert
    $ make world.opt
    $ sudo make install
    $ cd ..

    $ export PATH=/usr/local/compcert/bin:$PATH

  2. Next, install the camlp5 preprocessor/pretty-printer.

    $ curl -O http://pauillac.inria.fr/~ddr/camlp5/distrib/src/camlp5-6.07.tgz
    $ tar -xzf camplp5-6.07.tgz
    $ cd campl5-6.0.7
    $ curl -O http://pauillac.inria.fr/~ddr/camlp5/distrib/src/patch-6.07-1
    $ patch -p0 < patch-6.07-1
    $ ./configure -prefix /usr/local/compcert
    $ make -j4 all
    $ make -j4 opt.opt
    $ sudo make install
    $ cd ..

  3. The last dependency for comport is the Coq proof management system. The current version isn’t compatible, so we have to use a slightly older release.

    Unfortunately, the version of sed on MacOS X breaks the build, so if you’re on a Mac, you’ll need to (temporarily) install GNU sed.

    $ curl -O http://ftp.gnu.org/gnu/sed/sed-4.2.2.tar.bz2
    $ tar -xjf sed-4.2.2.tar.bz2
    $ cd sed-4.2.2
    $ ./configure –prefix=/usr/local/compcert
    $ make -j4
    $ sudo make install
    $ cd ..

    $ curl -O http://coq.inria.fr/distrib/V8.3pl5/files/coq-8.3pl5.tar.gz
    $ tar -xzf coq-8.3pl5.tar.gz
    $ cd coq 8.3pl5
    $ ./configure -prefix /usr/local/compcert
    $ make -j4 world
    $ sudo make install
    $ cd ..

    If you get errors about gramlib.cxa, make sure you did ‘make opt.opt’ for camlp5 in the previous step.

    Now we can remove sed.

    $ cd sed-4.2.2
    $ sudo make uninstall
    $ cd ..

  4. Finally, we’re ready to build the compcert compiler itself. Depending on your target, the last argument to configure may be ia32-linux or ia32-macosx (or several others – run ‘./configure’ to see the various options).

    $ curl -O http://compcert.inria.fr/release/compcert-1.12.tgz
    $ tar -xzf compcert-1.12.tgz
    $ cd compcert-1.12
    $ ./configure -prefix /usr/local/compcert ia32-macosx
    $ make -j4 all
    $ sudo make install
    $ cd .. 

    The compiler will be installed as ccomp in the directory /usr/local/compcert/bin 

Comments are closed.