The Coq mailing list

[Michael Shulman <shulman AT sandiego.edu>]

Any instructions at all for building the MacOS binary installer, even
on a Mac, would be appreciated...

On Thu, Aug 27, 2015 at 4:17 PM, Enrico Tassi 
<enrico.tassi AT inria.fr>
 wrote:
> 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