./lang/compcert [high assurance C compiler]
[+] Add this package to your ports tracker

[ CVSweb ] [ Homepage ] [ RSS feed ]

Version: 3.7.20200601, Package name: compcert-3.7.20200601
Maintained by: The OpenBSD ports mailing-list
Master sites:
Description
The CompCert C verified compiler is a compiler for a large subset
of the C programming language that generates code for the PowerPC,
ARM and x86 processors.

The distinguishing feature of CompCert is that it has been formally
verified using the Coq proof assistant: the generated assembly code
is formally guaranteed to behave as prescribed by the semantics of
the source C code.

CompCert is not free software. This non-commercial release can only
be used for evaluation, research, educational and personal purposes.
A commercial version of CompCert, without this restriction and with
professional support, can be purchased from AbsInt. See the file
LICENSE for more information.

Filesize: 2662.265 KB
Version History (View Complete History)
  • (2020-06-02) Updated to version: compcert-3.7.20200601
  • (2020-04-07) Updated to version: compcert-3.7
  • (2020-02-16) Updated to version: compcert-3.6.20200212
  • (2019-09-20) Updated to version: compcert-3.6
  • (2019-09-08) Updated to version: compcert-3.5.20190905
  • (2019-08-18) Updated to version: compcert-3.5.20190813
  • (2019-04-21) Updated to version: compcert-3.5
  • (2015-09-05) Package added to openports.se, version compcert-2.5 (created)
[show/hide] View available PLISTS (Can be a lot of data)

CVS Commit History:

   2020-06-02 06:58:22 by Daniel Dickman | Files touched by this commit (3)
Log message:
Update to commit 08491de0 for coq 8.11.1 support.
   2020-04-06 11:27:01 by Daniel Dickman | Files touched by this commit (2)
Log message:
Update to CompCert 3.7.
   2020-03-09 21:31:45 by Daniel Dickman | Files touched by this commit (8)
Log message:
drop maintainer
   2020-02-15 21:34:23 by Daniel Dickman | Files touched by this commit (4)
Log message:
Update to commit 9b881b79 for coq 8.11.0 and ocaml 4.10 support.
   2019-10-30 00:08:15 by Daniel Dickman | Files touched by this commit (2)
Log message:
support coq 8.10.1
   2019-10-15 18:08:35 by Daniel Dickman | Files touched by this commit (2)
Log message:
Backport fix for compcert so configure can work with coq 8.10.0 and
a few other minor tweaks.
   2019-09-20 05:32:16 by Daniel Dickman | Files touched by this commit (3)
Log message:
Update to CompCert 3.6.
   2019-09-07 11:24:37 by Daniel Dickman | Files touched by this commit (2)
Log message:
Update to commit d3eba507 for ocaml 4.08.1 support.
   2019-08-29 16:48:30 by Daniel Dickman | Files touched by this commit (2)
Log message:
Make an effort to fix the build on powerpc.
As seen in landry@'s powerpc bulk build report.
   2019-08-24 10:50:27 by Christopher Zimmermann | Files touched by this commit (2)
Log message:
Patch to configure against coq 8.10+beta2
ok daniel@
   2019-08-17 19:15:12 by Daniel Dickman | Files touched by this commit (4)
Log message:
Update to latest git commit to add support for ocaml 4.08 and coq 8.10.
This should allow chrisz@ to move forward with updates of those ports.
   2019-07-13 18:39:40 by Christian Weisgerber | Files touched by this commit (118)
Log message:
Switch to PERMIT_PACKAGE.  CDROM restrictions are no longer applicable.
   2019-04-28 15:08:27 by Christian Weisgerber | Files touched by this commit (20)
Log message:
Bump all ports that depend on ports-gcc on the clang archs.
SYSTEM_VERSION didn't quite work out how we expected and it's
easier|safer to do it this way than fiddle with pkg_add now.
   2019-04-20 16:12:41 by Daniel Dickman | Files touched by this commit (2)
Log message:
Drop dependency on base gcc and switch to ports gcc instead.
   2019-03-16 21:26:54 by Brian Callahan | Files touched by this commit (3)
Log message:
Update to compcert-3.5
ok daniel@ (MAINTAINER)
   2019-03-16 12:33:15 by Jeremie Courreges-Anglas | Files touched by this commit (1)
Log message:
Remove BROKEN, math/coq has been updated
ok daniel@ (maintainer)
   2018-10-26 19:16:42 by Daniel Dickman | Files touched by this commit (4)
Log message:
Update to Compcert 3.4. Still marked BROKEN until coq is updated.
   2018-09-11 22:58:49 by Daniel Dickman | Files touched by this commit (6)
Log message:
Update to CompCert 3.3 as requested by danj@ but mark BROKEN until we
get coq updated. Biggest improvement in this update is support for
amd64.
CompCert is not free software. This non-commercial release can only
be used for evaluation, research, educational and personal purposes.