Package Details: compcert 3.5-4

Git Clone URL: https://aur.archlinux.org/compcert.git (read-only)
Package Base: compcert
Description: The formally verified C compiler
Upstream URL: http://compcert.inria.fr
Keywords: compiler
Licenses: custom:INRIA Non-Commercial License Agreement
Submitter: xuanruiqi
Maintainer: xuanruiqi
Last Packager: xuanruiqi
Votes: 1
Popularity: 0.107188
First Submitted: 2019-04-27 04:40
Last Updated: 2019-06-06 05:43

Pinned Comments

xuanruiqi commented on 2019-07-10 23:36

The latest version of ocaml-menhir cannot be used to build CompCert.

I just uploaded the ocaml-menhir-compcert package, which provides the latest release of Menhir that can be used to build the latest release of CompCert. It provides ocaml-menhir=20181113, so if you use an AUR helper, this probably can be automated.

You have two other options:

  1. install a prebuilt version of this package from my personal repository;
  2. use compcert-git.

xuanruiqi commented on 2019-04-27 04:45

The venerable CompCert verified C compiler is finally packaged for Arch. Note that you might need to build this and ocaml-menhir in a clean chroot if you have OCaml and Coq installed via OPAM. I recommend using clean-chroot-manager for this purpose.

Keep in mind, however, that using ccomp as CC is usually not a great idea: unless you are building a package for high-assurance systems, CompCert is not yet on par with GCC or Clang in terms of either optimization or feature set. Also, it has no support for relocatable code or separate compilation yet, so often it won't work.

The lack of RELRO in /usr/bin/ccomp is intentional because of stated reasons (no support for relocatable code).

Latest Comments

xuanruiqi commented on 2019-07-10 23:36

The latest version of ocaml-menhir cannot be used to build CompCert.

I just uploaded the ocaml-menhir-compcert package, which provides the latest release of Menhir that can be used to build the latest release of CompCert. It provides ocaml-menhir=20181113, so if you use an AUR helper, this probably can be automated.

You have two other options:

  1. install a prebuilt version of this package from my personal repository;
  2. use compcert-git.

xuanruiqi commented on 2019-04-27 04:45

The venerable CompCert verified C compiler is finally packaged for Arch. Note that you might need to build this and ocaml-menhir in a clean chroot if you have OCaml and Coq installed via OPAM. I recommend using clean-chroot-manager for this purpose.

Keep in mind, however, that using ccomp as CC is usually not a great idea: unless you are building a package for high-assurance systems, CompCert is not yet on par with GCC or Clang in terms of either optimization or feature set. Also, it has no support for relocatable code or separate compilation yet, so often it won't work.

The lack of RELRO in /usr/bin/ccomp is intentional because of stated reasons (no support for relocatable code).