The Coq mailing list

[Michael Shulman <shulman AT sandiego.edu>]

Thanks.  If I do try, I'll let you know how it goes and ask questions
-- but since it sounds like it'll be a lot of pain and I'm not very
skilled with MacOS (there's an understatement) I probably won't find
the time+energy to try for a while.

On Fri, Aug 28, 2015 at 3:16 PM, Pierre Boutillier
<pierre.boutillier AT pps.univ-paris-diderot.fr>
 wrote:
> 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
>