Navigation:
lang compcert
CVSweb ] [ 
Homepage ] [ 
RSS feed ]| Version: 3.10, Package name: compcert-3.10 |
| 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: 2709.1 KB |
| Version History (View Complete History) |
|
| 2021-11-20 19:10:17 by Daniel Dickman | Files touched by this commit (4) |
Log message: update to CompCert 3.10 |
| 2021-10-29 15:37:58 by Jeremie Courreges-Anglas | Files touched by this commit (1) |
Log message: Unbreak sqlports on archs that don't have lang/gcc support (riscv64) Culprit found with help from espie@ |
| 2021-05-10 19:55:15 by Daniel Dickman | Files touched by this commit (2) |
Log message: update to release 3.9 |
| 2021-05-08 14:36:21 by Daniel Dickman | Files touched by this commit (2) |
Log message: update to commit 19e1039a |
| 2021-04-29 23:51:44 by Daniel Dickman | Files touched by this commit (2) |
Log message: update to commit d54fef19 for coq 8.13.2 support |
| 2021-03-10 08:00:53 by Daniel Dickman | Files touched by this commit (2) |
Log message: update to commit 6bf310dd for coq 8.13.1 support from Yozo Toda |
| 2021-02-13 10:46:38 by Daniel Dickman | Files touched by this commit (4) |
Log message: update to commit 25483cf1 for coq 8.12.2 and 8.13.0 support |
| 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. |