The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Fri, 16 May 2014 20:46:10 -0400,
Abhishek Anand 
<abhishek.anand.iitg AT gmail.com>
 a écrit :

> 1) Is it possible for coqdoc to output the syntax coloring information
> (which it already computes to generate latex/html) in a format that I
> could easily use to implement syntax highlighting in my plugin [1] ?
> Ideally, it could be like a list of triples:
> 
> start_pos, end_pos, color
> 
> The positions index into the .v file.
> Currently, I will have to somehow align the html generated by coqdoc
> with the corresponding .v file in order to figure out the colors that
> my plugin should
> use to render the .v file.
> 
> Is there an easier way to implement a more semantic syntax
> highlighting, similar
> to the agda-emacs, or coqdoc's latex/html outputs, but unlike the
> simplistic style of CoqIDE?
> For example, CoqIDE's colors don't distinguish inductive types from
> defined constants.
> 
> If someone could point me to the parts of coqdoc sources that I need
> to modify, that would be helpful too.


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


> 
> 2) Is it possible to get the .vo  file from the coqtop -ideslave
> process after my plugin (or any other IDE) has fed to it the entire
> contents of a .v file?
> A major use case would be a faster way to automatically compile all
> the dependencies of a .v file that a user opens using my plugin.
> Suppose a user of my plugin opened the file A.v
> and it has a line "Require Export B.v"
> Currently, I compile the B.v using coqc.
> However, if a compilation error occurs,
> I have to open B.v file in the editor and then
> feed the contents of it (to coqtop -ideslave) till the error location.
> The user can then fix the error in B.v.
> This is sometimes a huge waste of time for big files.
> I wish my plugin could use coqtop even to compile the dependencies so
> that if an error occurs, no duplicate work has to be done.


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.

> 
> 
> Proof general already does something similar. I'd be grateful to know
> how it manages to do the dependency compilation efficiently.
> 
> 
> [1] : https://github.com/aa755/nbcoq
> 
> Thanks,
> -- Abhishek
> http://www.cs.cornell.edu/~aa755/