Commit Graph

37 Commits

Author SHA1 Message Date
daniel
4abde328ef minor tweaks for compcert
- editing compcert.ini is no longer needed
- bump up the minimum coq version that compcert 3.12 would work with

with Volker Schlecht
2023-01-08 20:34:48 +00:00
daniel
28e912feb8 update to CompCert 3.12; from Volker Schlecht 2023-01-07 13:11:42 +00:00
naddy
e93f9d0ca9 drop RCS Ids 2022-03-11 19:28:46 +00:00
daniel
efd5a97f0a update ocaml to 4.12.1
The ocaml update requires ocaml-camlp4 to be updated in sync and all
dependant ports need a bump.

ok avsm@ (MAINTAINER)
2021-12-10 04:10:59 +00:00
daniel
68420eccff update ocaml to to 4.11.2 and bump all dependant ports
As usual camlp4 and camlp4 need to be updated in sync with ocaml. All
ocaml ports were successfully builds- tested on amd64. coccinelle remains
broken, but was built with the proposed diff floating on ports@

ok chrisz@
2021-12-02 03:59:19 +00:00
daniel
fb948691a7 update to CompCert 3.10 2021-11-21 02:10:17 +00:00
jca
0b62f8247b Unbreak sqlports on archs that don't have lang/gcc support (riscv64)
Culprit found with help from espie@
2021-10-29 21:37:58 +00:00
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