The Coq mailing list

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

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