The Coq mailing list

[Michael Shulman <shulman AT sandiego.edu>]

Is there any chance of at least having a binary installer available
for MacOS 10.10?

Some of my students are having trouble with the binary installer from
the Coq web site saying "Failure to load coqtop. Reset the preference
to default?".  I don't know for sure that the problem is the OS
version, but all of them are running MacOS 10.10 while the binary is
labeled as "for MacOS 10.9".  (I've directed them to try
MacPorts/Homebrew/Fink too, but at least one of them doesn't have
enough disk space to install xcode.)

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
>