Package Details: compcert-git 3.5.r77.ga8c84a52-2

Git Clone URL: https://aur.archlinux.org/compcert-git.git (read-only)
Package Base: compcert-git
Description: The formally verified C compiler
Upstream URL: http://compcert.inria.fr
Keywords: compiler
Licenses: custom:INRIA Non-Commercial License Agreement
Conflicts: compcert
Provides: compcert=3.5.r77.ga8c84a52
Submitter: xuanruiqi
Maintainer: xuanruiqi
Last Packager: xuanruiqi
Votes: 1
Popularity: 0.432224
First Submitted: 2019-04-27 05:17
Last Updated: 2019-07-11 00:16

Dependencies (7)

Required by (0)

Sources (1)

Pinned Comments

xuanruiqi commented on 2019-04-27 05:23

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-04-27 05:23

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).