From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id F2AB97F6CC for ; Thu, 5 Feb 2015 10:59:25 +0100 (CET) X-IronPort-AV: E=Sophos;i="5.09,522,1418079600"; d="asc'?scan'208";a="120372479" Received: from maths.r-prg.net.univ-paris7.fr (HELO [172.23.36.4]) ([81.194.27.158]) by mail2-relais-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES128-SHA; 05 Feb 2015 10:59:25 +0100 Message-ID: <54D33EC3.2050809@inria.fr> Date: Thu, 05 Feb 2015 10:58:27 +0100 From: =?windows-1252?Q?Pierre-Marie_P=E9drot?= User-Agent: Mozilla/5.0 (X11; Linux i686; rv:31.0) Gecko/20100101 Icedove/31.4.0 MIME-Version: 1.0 To: caml-list@inria.fr References: <20150202103256.GA30053@birba.invalid> <54D33020.6010707@lexifi.com> In-Reply-To: <54D33020.6010707@lexifi.com> Content-Type: multipart/signed; micalg=pgp-sha1; protocol="application/pgp-signature"; boundary="4NQF6BUAPdtHNhbSv1uJH4bBkaK9uVT3u" Subject: Re: [Caml-list] unmarshaling large data from string on 32 bits This is an OpenPGP/MIME signed message (RFC 4880 and 3156) --4NQF6BUAPdtHNhbSv1uJH4bBkaK9uVT3u Content-Type: text/plain; charset=windows-1252 Content-Transfer-Encoding: quoted-printable On 05/02/2015 09:56, Alain Frisch wrote: > One possible work-around is to use an alternative implementation of the > demarshaler (there is such a pure OCaml implementation in Frama-C). > Another is to avoid the generic marshaling, either by writing a manual > version for your specific data type or by generating it from your type > definitions (=E0 la bin-prot, I assume). Both workarounds would not work. Indeed, we use closure marshalling in Coq, which is not supported by the two proposed implementations. (Plus, that would be so slow I do not even want to think about it.) PMP --4NQF6BUAPdtHNhbSv1uJH4bBkaK9uVT3u Content-Type: application/pgp-signature; name="signature.asc" Content-Description: OpenPGP digital signature Content-Disposition: attachment; filename="signature.asc" -----BEGIN PGP SIGNATURE----- Version: GnuPG v1 iEYEARECAAYFAlTTPsMACgkQeew3reqJuSXqwQCgkidnv6XKGF0RmNaxnnw+U/wY QuwAnRCuEEj2uPCoW+Kk/3ZjmB5Md5L3 =q9xF -----END PGP SIGNATURE----- --4NQF6BUAPdtHNhbSv1uJH4bBkaK9uVT3u--