Billy Price (Nov 15 2020 at 12:37): Billy Price (Nov 15 2020 at 12:37):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
Gaëtan Gilbert (Nov 15 2020 at 13:06):I'm guessing this is due to the bad setup.
no
Billy Price (Nov 15 2020 at 13:13):Any ideas what it could be?
Billy Price (Nov 15 2020 at 13:27):When I say bad setup I mean "probably not configured to work with VS Coq"
Fabian Kunze (Nov 15 2020 at 13:33):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?
https://github.com/fakusb/vscoq/releases/tag/0.3.3-alpha3-custom
NOTE:
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 ^^'
Fabian Kunze (Nov 15 2020 at 13:34):(.vsix files package extensions and can be installed by choosing the "..."-menu in the extension sidebar tab)
Fabian Kunze (Nov 15 2020 at 13:34):vscoq is suposed to "just work" if you opened a folder with a _CoqProject on toplevel
Billy Price (Nov 15 2020 at 13:41):Thanks! First attempt works perfectly on all files. Will report back if the issue arises during further use.
Matthieu Sozeau (Nov 16 2020 at 11:29):@Fabian Kunze thanks, that will be helpful to me too :)
Fabian Kunze (Nov 16 2020 at 11:31):@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 ^^'
Matthieu Sozeau (Nov 16 2020 at 11:32):Ok, noted!
Paolo Giarrusso (Nov 16 2020 at 12:18):Thanks for the warning Fabian, but we're thankful anyway.
Matthieu Sozeau (Nov 19 2020 at 20:09):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: Apr 18 2024 at 23:01 UTC