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
