30 Commits

Author SHA1 Message Date
daniel
a5da984f02 update to release 3.9 2021-05-11 01:55:14 +00:00
daniel
dcab255fce update to commit 19e1039a 2021-05-08 20:36:21 +00:00
daniel
a4bf1a704e update to commit d54fef19 for coq 8.13.2 support 2021-04-30 05:51:44 +00:00
daniel
7172a904c7 update to commit 6bf310dd for coq 8.13.1 support
from Yozo Toda
2021-03-10 15:00:53 +00:00
daniel
f23afa3bcc update to commit 25483cf1 for coq 8.12.2 and 8.13.0 support 2021-02-13 17:46:38 +00:00
daniel
91ef93d6d1 update to tagged release of 3.8
Adds coq 8.12.1 support along with the usual spate of improvements.
2020-11-17 04:13:18 +00:00
daniel
c59394dd0b update to commit 27beb944 2020-11-15 03:02:19 +00:00
daniel
b9b92f85e7 Update to commit 0132b8aa for improved builtin support. 2020-07-28 08:35:31 +00:00
daniel
7ceaf0c63b Update to commit 72f78307 with additional updates to support bytecode-only
platforms.
2020-07-16 23:43:32 +00:00
daniel
c8549b0b90 Update to commit 9af28924 so bytecode-only platforms can be supported. 2020-07-07 23:03:10 +00:00
daniel
6f46ad37f1 Update to commit bb9fa555 for coq 8.11.2 support. 2020-07-02 02:36:51 +00:00
daniel
f2247bcb5f Update to commit 08491de0 for coq 8.11.1 support. 2020-06-02 12:58:22 +00:00
daniel
4a5663734f Update to CompCert 3.7. 2020-04-06 17:27:00 +00:00
daniel
add32f09f8 drop maintainer 2020-03-10 03:31:45 +00:00
daniel
9e317f5c99 Update to commit 9b881b79 for coq 8.11.0 and ocaml 4.10 support. 2020-02-16 04:34:23 +00:00
daniel
b7a017b3cd support coq 8.10.1 2019-10-30 06:08:15 +00:00
daniel
915bb27789 Backport fix for compcert so configure can work with coq 8.10.0 and
a few other minor tweaks.
2019-10-16 00:08:35 +00:00
daniel
c0effb3c99 Update to CompCert 3.6. 2019-09-20 11:32:16 +00:00
daniel
d9e1a6e4cd Update to commit d3eba507 for ocaml 4.08.1 support. 2019-09-07 17:24:37 +00:00
daniel
5be0b877bb Make an effort to fix the build on powerpc.
As seen in landry@'s powerpc bulk build report.
2019-08-29 22:48:30 +00:00
chrisz
cd99141b90 Patch to configure against coq 8.10+beta2
ok daniel@
2019-08-24 16:50:27 +00:00
daniel
d508909eea 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-08-18 01:15:12 +00:00
naddy
7ab397505a Switch to PERMIT_PACKAGE. CDROM restrictions are no longer applicable. 2019-07-14 00:39:34 +00:00
naddy
3e042ba62d 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-28 21:08:26 +00:00
daniel
aa4bbca17d Drop dependency on base gcc and switch to ports gcc instead. 2019-04-20 22:12:41 +00:00
bcallah
155ab44de2 Update to compcert-3.5
ok daniel@ (MAINTAINER)
2019-03-17 03:26:53 +00:00
jca
3e9567b10a Remove BROKEN, math/coq has been updated
ok daniel@ (maintainer)
2019-03-16 18:33:15 +00:00
daniel
98274b8b3f Update to Compcert 3.4. Still marked BROKEN until coq is updated. 2018-10-27 01:16:42 +00:00
daniel
01c5ef0515 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.
2018-09-12 04:58:49 +00:00
daniel
3c4bfcc3d7 import lang/compcert. ok sthen@
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.
2015-09-05 00:20:08 +00:00