The Coq mailing list

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

Hi,
No there is no v8.4pl1 bundle on coq.inria.fr
Why ?
- Because there is no Package Maker on new macOS so I cannot build the 
package that installs coq in /usr/local/
- Because this package was not uninstallable and so upgrades were buggy : 
files of the old version that has disappeared in the new one remained and 
"Inconsistent assumptions over the module …" appeared.

By the way, I've discovered how to uninstall these pkg : all the information 
about what has been installed is stored in : 
/Library/Receipts/some_app.pkg/Contents/Archive.bom
so by doing lsbom -fls /Library/Receipts/some_app.pkg/Contents/Archive.bom | 
(cd /; sudo xargs rm) you erase everything. You can add a pkgutil --forget 
fr.inria.coq to be very clean.
These packages were done for ProofGeneral users I supposed but does someone 
use it in reality ? I would say that Emacs users use a package manager to 
install Coq, don't they ? In this condition, I propose not to build the coq 
package anymore and that people that have an old version installed 
uninstalled it using the above procedure …

- Because coqide 8.4 segfaults on a race condition between gtk threads that I 
do not want to spend time to debug because I know that coqide trunk do not 
use threads anymore and do not have this problem…
- Because Coq need more and more plugins to be fully functional and plugins 
need to be compiled with the exact same build of the ocaml compiler to work. 
So I must either transform myself in a Coq-distribution provider and provide 
new versions of contribs when they are released as well as new version of coq 
or put my ocaml build in the bundle (after gtk and all coq standard library 
it is not that much you may say) but ocaml is not made to be relocable (find 
its lib in a relative path from the binary) so it won't work !
- Because apps need to be signed (I do not use an apple approved key, I will 
never give money to apple for distributing software on their platform) but 
you cannot add anything after the signature of a bundle. So there is no way 
to add libraries in the user-contrib/ folder. That means that extra libraries 
have to be installed in XDG_DATA_DIR but we are back to the upgrade problem : 
any standard macOS user takes a manual care of its 
Library/ApplicationSupport/ folder and I don't want to write the code to 
check the consistency of it myself ! (There may be a space waisting but very 
simple solution to that which is to use $XDG_DATA_DIR/coq/Vfoo/ instead of 
$XDG_DATA_DIR/coq … )
- Because some mistakes remains in pl1 so pl2 should go out soon. 
Consequently, I'll do the manual job to get a more or less working coqide 
with maybe Ssreflect, AACTactics,Containers, DescenteInfinie and 
whatever-you'll-ask-me-to-put in plugins in the version they are in the 
user_contrib repository on the coq web site only for this version.

If you don't care about all these problems but you just want the last coq 
already compiled, please use my nightly builds here : 
http://www.pps.univ-paris-diderot.fr/~pboutill/coq-night/

All the best,
Pierre B.
 
Le 21 janv. 2013 à 16:46, Lucian M. Patcas 
<lucian.patcas AT gmail.com>
 a écrit :

> Hello,
> 
> Is there a binary package of Coq 8.4pl1 for the Mac? Right now only Coq 8.4 
> seems to be available for download at http://coq.inria.fr/download.
> 
> Thanks,
> Lucian