The Coq mailing list

[Michael Greenberg <michael.greenberg AT pomona.edu>]

On 2018-2-7 10:12 AM, Cao Qinxiang wrote:

Hi Michael,

Here is what I did in a small seminar last year (in that seminar, I use an even more complicated Coq library than software foundation)

  1. For windows users, give them all .vo file directly (which were compiled on my windows laptop using Cygwin command line. The audience do not need to install Cygwin.). The reason that it works is that since those audience install the same Coq binary, then both my laptop and their laptop are based on the same set of STD library .vo files. So, loading my .vo file on their laptop will not cause any .vo inconsistency.

The issue I'm having is not that they can't get a .vo file, but rather that CoqIDE doesn't find them when put in the same directory as the .v file!

  2. For Mac and Linux users, teach them how to configure the CONFIGURE file so that they can set up COQBIN in Makefile. Mac and Linux have command line. Let those audience compile .vo files using "make" command.

This seems a little too complicated for our purposes, but it does seem that choosing 'Compile > make makefile' and then 'Compile > make' does work!

Michael

Hope that helps!

Qinxiang

On Wed, Feb 7, 2018 at 1:00 PM, Michael Greenberg <michael.greenberg AT pomona.edu> wrote:
Hi all,

I'm teaching an abbreviated form of Software Foundations' first volume as part of a discrete math course.

Many students are having significant issues with compilation; in particular, it's quite complicated to configure the loadpath in CoqIDE 8.6.1. Students trying to "Compile > Compile buffer" succeed for the initial file, Basics.v, but later dependencies don't show up. Mysteriously, running the code in CoqIDE works fine---that is, the interactive coqtop session can find imports perfectly, but the call to coqc can't. It's critical that students be able to compile their code to ensure that it will run with our autograder.

I found <https://stackoverflow.com/questions/16202666/coqide-cant-load-modules-from-same-folder> as a potential solution, but having students put Add LoadPath directives in submitted code is a non-starter. I haven't found an incantation for _CoqProject that will make it work.

I've shown some students how to access coqc directly themselves, but this is an unsatisfactory solution---for many students, this is their second course in computer science!

The best solution I've found so far has been to set the external for coqc to have a -I flag to the appropriate directory. It's nice because it doesn't change the .v files, but some students don't yet know their way around a filesystem. If there were a way to offer *visual* navigation to the directory, we'd be in better shape. Is there a reason CoqIDE doesn't have a GUI-configurable loadpath option?

Am I missing some other obvious solution that is even better, i.e., requires the students to know even less about their filesystem?

Cheers,
Michael