Hi there, newbie here.
I'm studying this formal verification of the perceptron algorithm in Coq, and I'd like to work with it in VS Code. However it already has a _Coqproject file and a Makefile, and I don't know what are the necessary changes I need to make to these to get VS Coq working. I've got it working sometimes, but I have a problem I think is related to either _Coqproject or Makefile.
Sometimes when I start interactively interpreting one file, I am unable to get Coq to start interpreting another file. When I execute the "interpret to point" or "step forward" in the second file, it opens up the first file and executes the command there. Doing
Coq: Reset doesn't fix it, and it only works when I fully restart vscode and open up the second file. I'm guessing this is due to the bad setup.
Is there anything obvious in _Coqproject or Makefile here that I should change? https://github.com/tm507211/CoqPerceptron
I'm guessing this is due to the bad setup.
Any ideas what it could be?
When I say bad setup I mean "probably not configured to work with VS Coq"
If you got vscoq to start, and then it decided to stop, it's probably a bug in vscoq.
There are a few bugs I fixed that are not yet released in the official extension marketplace. Some of these fixes are related to opening multiple files.
Would you mind trying if those improve on your situation?
I screwed up by not looking at which version number my build uses and I think if you use it, vscode will not update to the next upstream-version (as that official release probably has the same number). So remember to update by hand once upstream updates ^^'
.vsix files package extensions and can be installed by choosing the "..."-menu in the extension sidebar tab)
vscoq is suposed to "just work" if you opened a folder with a
_CoqProject on toplevel
Thanks! First attempt works perfectly on all files. Will report back if the issue arises during further use.
@Fabian Kunze thanks, that will be helpful to me too :)
@Matthieu Sozeau @Billy Price :
I screwed up by not looking at which version number my eta uses and I think your vscode will not update to the next upstream-version (as that official release probably has the same number). So remember to update by hand once upstream updates ^^'
Thanks for the warning Fabian, but we're thankful anyway.
Indeed it's a great improvement, multi-projects files are way less buggy, and I don't have to resize the windows constantly. Thanks :)
Last updated: Jan 30 2023 at 18:04 UTC