The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Thu, Aug 27, 2015 at 08:33:59AM -0700, Michael Shulman wrote:
> Is it possible to build the MSWin and/or MacOS binary installers for
> Coq on a Linux machine?
> 
> An older version of README.win mentioned the possibility of
> cross-compiling with mingw, but that's now been replaced with
> instructions for building the installer on windows (although I do not
> understand the instruction to "Download and unzip in C:\ the SDK for
> windows"; the URL https://coq.inria.fr/distrib/current/files/ given
> does not list any file labeled "SDK").

No, we now build Coq for Windows on Windows.  Believe me, it is much
simpler.

You are right, the SDK was not symbolically linked there, you can find
it here:
  https://coq.inria.fr/distrib/V8.5beta1/files/

I'm not competent for Mac.

> (Reason for my question: I am planning to have my students in a logic
> class use Coq, but with only a small set of tactics that I have
> written myself to match the proof strategies taught in our textbook.
> I would like to customize the "Tactics" menu in CoqIDE so that it will
> show these tactics (and only these), so that the students can enter
> them by point-and-click instead of having to remember their names and
> type them in.  The Tactics menu is hard-coded in ML, but it seems
> fairly easy to modify the source code; however I don't want to ask my
> students to compile Coq from source themselves!)

While you are at it, why don't you make CoqIDE read an external text file
containing the list of tactics to be displayed in the menu? I too find
the default menu too long for teaching purposes.  In other words, pull
requests are welcome ;-)

Best,
-- 
Enrico Tassi