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