The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

I would like to share some more observations related to the issues with Mac 
case-insensitive
file system, Coq and coq-contrib OPAM packages. Please let me know if it is 
not the right forum for this. As interested party I will be glad to help to 
debug and make it all work smoothly.

I am trying to use OPAM-based Coq install on MacOS. I am using coq-stable 
repository a
and encountered the following problems:

Issue #1

Problem: 
https://github.com/coq/repo-stable/tree/master/packages/coq:math-classes/coq:math-classes.1.0.2
 has not yet been updated with latest patch from Jason and does not build on 
MacOS. 

Workaround: I created local copy of OPAM package using last snapshot from 
https://github.com/math-classes/math-classes. I “pinned” it and successfully 
installed via OPAM.

Solution: update stable package with latest math-classes source

Issue #2:

Problem: installing coq:color via OPAM under MacOS seemingly succeeds, but 
library files are not installed. The reason for this is ‘make install’ 
makefile goal does nothing as the distribution contains file INSTALL.
Under case-insensitive file system it matches goal ‘install’, so ‘make' finds 
it and considers goal up to date and never actually copy any files. 
Illustration:

lambda13 ~/tmp/color.1.1.0$ make install
make: `install' is up to date.
lambda13 ~/tmp/color.1.1.0$ ls -l INSTALL
-rw-r-----  1 lord  staff  1377 Mar 10 09:41 INSTALL
lambda13 ~/tmp/color.1.1.0$ ls -l install
-rw-r-----  1 lord  staff  1377 Mar 10 09:41 install

Workaround: in my local pinned copy of the package I removed file INSTALL 
from the archive.

Solution: add “install” to list of phony targets (.PHONY) in Makefile in 
Color.

Issue #3:

Problem: When CoLoR is installed after MathClasses, the installation fails:

...
# "coqc"  -q  -R . CoLoR   Util/List/ListSort
# File "/Users/lord/.opam/system/build/coq:color.1.1.0/Util/List/ListSort.v", 
line 12, characters 0-20:
# Error: The file 
/Users/lord/.opam/system/lib/coq/user-contrib/MathClasses/implementations/List.vo
 contains library
# MathClasses.implementations.list and not library
# MathClasses.implementations.List
### stderr ###
# make[1]: *** [Util/List/ListSort.vo] Error 1
# make[1]: *** Waiting for unfinished jobs....
# make: *** [default] Error 2

Workaround: install CoLoR first, and then MathClasses. (But the problem is 
likely to re-surface again for packages installed after MathClasses!)

Solution: Make changes to Coq file search/open code to check the case of the 
files, as suggested by Pierre Boutillier in 
https://coq.inria.fr/bugs/show_bug.cgi?id=2554 


Sincerely,
Vadim Zaliva

--
CMU ECE PhD candidate
Mobile: +1(510)220-1060
Skype: vzaliva