Package Details: compcert-git 3.6.r1.gf1637021-3

Git Clone URL: https://aur.archlinux.org/compcert-git.git (read-only, click to copy)
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.6.r1.gf1637021
Submitter: xuanruiqi
Maintainer: xuanruiqi
Last Packager: xuanruiqi
Votes: 1
Popularity: 0.009351
First Submitted: 2019-04-27 05:17
Last Updated: 2019-09-19 05:05

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