The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Sorry for the late response. My responses are below:

 

For syntax highlighting, wouldn’t it be easier to use the *.glob file ?

Is there a (semi) formal description of the syntax and semantics of the *.glob file?

I could not make a confident-enough guess, especially about its semantics.

I do not know the details on how coqtop -ideslave works, but as an
interpreter, I guess it does not expect an end of file, and if you were
to add an "end of file" command to get the .vo files, then it would be
a .vo of an interactive session, which may be different from the
contents of the .v file. For instance, if the .vo files stores a hash
of the .v file, then as I do not think that the coqtop process receives
the layout of the file, you could be in a situation where the .vo file
you would get with coqc would differ from what your interactive session
would get. Same thing if the session does not send all the contents of
the file, or sends extra commands.

How about offloading the job of hash calculation to the IDE? The end-of-file

command could provide the hash as an argument.

The implementation of the "Require Import/Export" commands already

checks the correctness of the hash in the *.vo file w.r.t the corresponding *.v file, doesn't it?

(I remember being forced to recompile my *.v files even when I merely changed some comments.)

I agree that in the general case, IDEs might need to employ sophisticated algorithms to 

determine the correct hash. But it should be simple in my specific use case as

I need the file B.vo only if B.v (in my example) had no errors.

In that case, my plugin/IDE will sequentially send the entire contents and no

other extra commands.

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/