Michael Greenberg (Jul 21 2020 at 22:31): Michael Greenberg (Jul 21 2020 at 22:31):I'm trying to find the right IDE to use for a class of early undergraduates. It's a particular goal to have it be (a) a modern IDE and (b) handle all of the compilation in the multiple files we use.
VS Code would be perfect, so I was excited about VSCoq... but I'm worried I can't use it, because I can't figure out how to get automatic compilation. Am I missing something, or is that not something VSCoq does?
Paolo Giarrusso (Jul 22 2020 at 07:20):You need to use _CoqProject; it's not actually hard to use, but it is a bit hard to learn. For a class, you can likely provide templates... As long as students can install make!
Paolo Giarrusso (Jul 22 2020 at 07:21):(the relevant docs are those for coq_makefile)
Michael Greenberg (Jul 22 2020 at 17:11):I'll go take a look at the docs. As it stands, though, there already _is_ a _CoqProject file, though it just sets the default module via -Q.
Karl Palmskog (Jul 22 2020 at 17:18):possibly-helpful - here is a "standard" delegating Makefile on top of _CoqProject: https://github.com/coq-community/huffman/blob/master/Makefile
Karl Palmskog (Jul 22 2020 at 17:20):but the main issue with _CoqProject+coq_makefile is that all "new" files must be manually added to _CoqProject (this is not the case with, e.g., the alternative build system Dune, but Dune is not as user friendly in other ways)
Michael Greenberg (Jul 22 2020 at 17:20):Hmm. I see. That may not work for us: we're based on SF, which has a more complicated build process. I might be able to adapt it, but it sounds tricky to simultaneously have something that works for our complicated build (pre-CoqDoc processing to split out solutions, etc.) and adapts to the simpler student setting. (They're mostly first-year students and many won't know basic CLI stuff. Some even use---gasp!---windows.)
Karl Palmskog (Jul 22 2020 at 17:26):doesn't VSCode allow you to set up a command to build and provide a button to that effect? Basically, you will just have to tell it to run make
Karl Palmskog (Jul 22 2020 at 17:28):it should be possible to "pre-install" the compiled SF and have a small project of multiple files that simply uses the installed compiled files from SF. This way, that project doesn't depend on the build scripts for SF.
Michael Greenberg (Jul 22 2020 at 18:31):That is true, in principle! My experience of getting tools like make to work on a ~40 student laptops with different configurations is not fun---not fun enough that I'll pay the installation cost of ProofGeneral up front and then have it auto-compile things. :(
Paolo Giarrusso (Jul 22 2020 at 19:04):but the main issue with
_CoqProject+coq_makefileis that all "new" files must be manually added to_CoqProject(this is not the case with, e.g., the alternative build system Dune, but Dune is not as user friendly in other ways)
Paolo Giarrusso (Jul 22 2020 at 19:04):The call to coq_makefile can use a wildcard. Not sure why that's not done more often. (I remember a c
Paolo Giarrusso (Jul 22 2020 at 19:06):*co-author reverting this change, not sure why.
Michael Greenberg (Jul 22 2020 at 19:46):Even with that, I think it's too heavyweight for our purposes: we really need something more or less automatic. Some of our students are sophisticated, but many come into our CS program with zero background.
To be clear, it's not a problem that VsCoq doesn't solve our problem! VS Code and Coq are both serious tools for getting real work done, so it's not surprise that some of it is hard for beginners.
Karl Palmskog (Jul 22 2020 at 19:51):I don't think it would work for this purpose without some (a lot of?) upfront extra work, but just flagging up jsCoq as one possible future solution for teaching Coq: https://x80.org/rhino-coq/v8.11/
Michael Greenberg (Jul 22 2020 at 19:52):Yes, thank you! I've been tracking jsCoq and it will _eventually_ be the right answer. Not yet, though.
Karl Palmskog (Jul 22 2020 at 19:59):I see. Then I don't think we have anything besides PG which solves the full-automation problem. More CLI-sophisticated students may find this useful, e.g., one can set up continuous integration of Coq on GitHub quite easily: https://github.com/coq-community/templates
Michael Greenberg (Jul 22 2020 at 19:59):CoqIDE kind of worked last time I tried... but the non-native UI and Unicode woes made it ultimately not worth the trouble. :(
Hugo Herbelin (Jul 24 2020 at 18:09):Michael Greenberg said:
CoqIDE kind of worked last time I tried... but the non-native UI and Unicode woes made it ultimately not worth the trouble. :(
What kind of Unicode woes do you have?
Last updated: Jun 04 2023 at 22:30 UTC