coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq - kernel - interp.c arch-specific code

From: Enrico Tassi <enrico.tassi AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Coq - kernel - interp.c arch-specific code
Date: Fri, 21 Mar 2014 21:12:51 +0100

On Fri, Mar 21, 2014 at 06:23:51PM +0100,
moe45673 AT gmail.com
wrote:
> LINARO project to port existing programs to Arm64. Our focus is on
> converting

I'm not an expert of this code, but I know it is a modified version of
the OCaml bytecode interpreter. The "fork" was surely made before Arm64
came to existence.

IMO the best strategy is to fix this issue in OCaml first (if it is
still present), and then port the fix to Coq.

Regards
--
Enrico Tassi

[Coq-Club] Coq - kernel - interp.c arch-specific code, moe45673, 03/21/2014
- Re: [Coq-Club] Coq - kernel - interp.c arch-specific code, Gabriel Scherer, 03/21/2014
  - Re: [Coq-Club] Coq - kernel - interp.c arch-specific code, Moshe Tenenbaum, 03/24/2014
    - Re: [Coq-Club] Coq - kernel - interp.c arch-specific code, Guillaume Melquiond, 03/24/2014
      - Re: [Coq-Club] Coq - kernel - interp.c arch-specific code, Arnaud Spiwack, 03/24/2014
- Re: [Coq-Club] Coq - kernel - interp.c arch-specific code, Enrico Tassi, 03/21/2014