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

[ CVSweb ] [ Homepage ] [ RSS feed ]

Version: 3.8, Package name: compcert-3.8
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: 2664.701 KB
Version History (View Complete History)
  • (2020-11-17) Updated to version: compcert-3.8
  • (2020-11-15) Updated to version: compcert-3.7.20201114
  • (2020-07-28) Updated to version: compcert-3.7.20200727
  • (2020-07-17) Updated to version: compcert-3.7.20200715
  • (2020-07-08) Updated to version: compcert-3.7.20200707
  • (2020-07-02) Updated to version: compcert-3.7.20200701
  • (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
[show/hide] View available PLISTS (Can be a lot of data)

CVS Commit History:

   2020-11-16 21:13:18 by Daniel Dickman | Files touched by this commit (2)
Log message:
update to tagged release of 3.8
Adds coq 8.12.1 support along with the usual spate of improvements.
   2020-11-14 20:02:19 by Daniel Dickman | Files touched by this commit (4)
Log message:
update to commit 27beb944
   2020-07-28 02:35:31 by Daniel Dickman | Files touched by this commit (2)
Log message:
Update to commit 0132b8aa for improved builtin support.
   2020-07-16 17:43:32 by Daniel Dickman | Files touched by this commit (4)
Log message:
Update to commit 72f78307 with additional updates to support bytecode-only
platforms.
   2020-07-07 17:03:10 by Daniel Dickman | Files touched by this commit (3)
Log message:
Update to commit 9af28924 so bytecode-only platforms can be supported.
   2020-07-01 20:36:51 by Daniel Dickman | Files touched by this commit (2)
Log message:
Update to commit bb9fa555 for coq 8.11.2 support.
   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.