search

coq-community / vscoq

A Visual Studio Code extension for Coq [maintainers=@rtetley,@maximedenes,@huynhtrankhanh,@thery,@Blaisorblade]
MIT License
321 stars 68 forks source link

handling external compilation #768

Open vzaliva opened 2 months ago

vzaliva commented 2 months ago

Currently, it's challenging to use VsCoq for Coq development involving multiple inter-dependent (.v) modules. Since it doesn't compile them (an issue possibly addressed by https://github.com/coq-community/vscoq/issues/252), one must compile through an external build system like dune (as discussed in https://github.com/coq-community/vscoq/issues/134) or make.

However, when files are recompiled outside VSCode, it fails to recognize changes in .vo files and continues to display errors based on old definitions. There are a few potential fixes for this:

  1. A minimal solution could be to force the reloading of all .vo files when the compilation is done via the Terminal -> Run Build Task menu.

  2. A more sophisticated solution would be to monitor .vo files and reload them once they change. This would allow for running dune build --watch externally, which would automatically recompile changed files, with VsCoq then picking up these changes automatically as well.

vzaliva commented 2 months ago

Sorry, I forgot to mention: I am using VsCoq v2.1.2