[Iris-Club] Installing the sources alongside the object files

Dan Frumin dfrumin at cs.ru.nl
Sun Jul 9 20:30:03 CEST 2017


Dear Iris hackers and users,
I am using ProofGeneral with 
[company-coq](https://github.com/cpitclaudel/company-coq) which allows 
me to have a useful shortcut M-. that jumps to a definition. The only 
issue with that: in order to jump to a definition in a module M, the 
source file M.v should be installed alongside the .vo file.

Currently, I just hacked the Makefile.coq myself to add the following line:

     VFILES0=$(patsubst theories/%,%,$(filter theories/%,$(VFILES)))

(Curiously, the makefile generated by coq_makefile already includes the 
installation process for .v files, it's just that the variable `VFILES0` 
is undefined -- does anyone know why is that?)
Maybe it is possible to have a subcommand `make install-src` that would 
install the sources alongside the .vo files?

Best regards,
Dan



More information about the Iris-Club mailing list