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.
Search Criteria
Package Details: compcert 3.12-1
Package Actions
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: | 2022-12-16 18:29 (UTC) |
Dependencies (6)
- gcc (gccrs-git, gcc-git)
- coq (make)
- ocaml (make)
- ocaml-findlib (make)
- ocaml-menhir (ocaml-menhir-compcert) (make)
- parallel (parallel-rust, parallel-git) (check)
Required by (0)
Sources (1)
Latest Comments
xuanruiqi commented on 2020-12-11 05:16 (UTC)
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:
- install a prebuilt version of this package from my personal repository;
- 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).
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).