Package Details: compcert 3.15-1

Git Clone URL: https://aur.archlinux.org/compcert.git (read-only, click to copy)
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: 2
Popularity: 0.000000
First Submitted: 2019-04-27 04:40 (UTC)
Last Updated: 2025-03-20 16:39 (UTC)

Dependencies (6)

Required by (0)

Sources (1)

Pinned Comments

xuanruiqi commented on 2019-04-27 04:45 (UTC) (edited on 2019-04-27 05:23 (UTC) by xuanruiqi)

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

PatrickZhang commented on 2024-08-28 16:06 (UTC) (edited on 2024-08-28 16:06 (UTC) by PatrickZhang)

Refer to the PKGBUILD, it will install ocaml-5.2.0-1 coq-8.19.2-1, but CompCert require Coq's version to be 8.19.1 or below, ocaml's version to be 4.14 or below (https://compcert.org/man/manual002.html). So the installation fails with the following error message : "make: *** No rule to make target 'all'. Stop.". When I met CompCert's prerequisites by compiling coq and ocaml manually, the installation succeeded. Are there any way to handle this conflict?

dmaggot commented on 2024-08-23 19:47 (UTC)

As of

https://github.com/AbsInt/CompCert/commit/901425a8be68b0351715bf44edef78040fd00f12

the test folder is empty so either one needs to separately download the tests or modify check() accordingly.

xuanruiqi commented on 2020-12-11 05:16 (UTC)

I think it's just your Coq is too new. But I just realized that CompCert 3.8 came out and I will update to 3.8, which should support your Coq and OCaml version.

Crazycolorz5 commented on 2020-12-10 20:06 (UTC) (edited on 2020-12-10 20:06 (UTC) by Crazycolorz5)

Builds for this are failing for me. I've tried with both ocaml-menhir and ocaml-menhir-compcert.

File "./lib/Floats.v", line 226, characters 47-48:
Error:
Syntax error: '|' or ',' or ')' expected after [constr:operconstr level 200] (in [constr:operconstr]).

make[1]: *** [Makefile:195: lib/Floats.vo] Error 1
make[1]: Leaving directory '/tmp/aura/build/compcert-965135708768560181/compcert/src/CompCert-3.7'
make: *** [Makefile:136: all] Error 2
==> ERROR: A failure occurred in build().
    Aborting...

My versions of ocaml and coq are as follows:

$ pacman -Q coq ocaml
coq 8.12.0-2
ocaml 4.11.1-1

xuanruiqi commented on 2019-09-19 05:02 (UTC)

New release of CompCert!

xuanruiqi commented on 2019-07-10 23:36 (UTC) (edited on 2019-07-11 06:12 (UTC) by xuanruiqi)

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 (UTC) (edited on 2019-04-27 05:23 (UTC) by xuanruiqi)

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