The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>]

There is https://coq.inria.fr/cocorico/Installation%20of%20Coq%20on%20Mac
It needs to be translated in real english. It needs more explanations, it 
needs … a lot of things.
I’m too lazy to break my jhbuild installation tonight by trying to install 
the current version of gtk in order to list the current issues.

We've successfully installed lablgtkosx with Jasmin Blanchette using macport 
during the coq coding sprint in June. It took us 1 entire day and I can’t 
remember the correct invocation in the end. Something like
port install gtk-osx-application-gtk2 lablgtk2 camlp5 +no_x11 +quartz 
+gtksourceview2
but then I don't remember if we successfully built a standalone reloadable 
.app from it.

Despite the upset tone of this message, which express how bored I am to 
maintain Coq on MacOS side of MacOS (there is no problem on unix side of 
MacOS), please asks me any question or report trouble you have. I’ve probably 
encounter it already and it is silly to waste time twice :-)

Pierre B.

> Le 28 août 2015 à 22:50, Michael Shulman 
> <shulman AT sandiego.edu>
>  a écrit :
> 
> 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