Re: Coq & ocaml 3.08
> I think that the only main change of camlp4 is that locations are now
> handled in OCaml (using Lexing.position instead of int). Do you really
> think it would take so much time to have COQ compiling with 3.08?
(I am just guessing here, I am not informed enough.)
Maybe. I have just tried to recompile Coq with ocaml-3.08.
Coq signals the location of the errors using camlp4 functions whose
input is now a location (i.e. no longer an integer but a structure
line, offset in the line, offset from the begin of file).
This creates two problems:
1. how to generate the other two fields of the structure in the
Coq code
2. how to adapt the Coq based tools to parse the new error
messages
The quick & dirty solution of keeping the old data structure (int * int)
and projecting the last field of the record does not work (unless
a "dummy" location is then used to raise errors).
To summarize: it does not seem a daunting problem, but it is not
immediate to solve either.
Cheers,
C.S.C.
--
----------------------------------------------------------------
Real name: Claudio Sacerdoti Coen
Doctor in Computer Science, University of Bologna
E-mail: sacerdot@cs.unibo.it
http://www.cs.unibo.it/~sacerdot
----------------------------------------------------------------
Reply to: