The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

This should now contain Jason's patch:

https://github.com/coq/repo-stable/tree/master/packages/coq:math-classes/coq:math-classes.1.0.3

On Tue, May 12, 2015 at 2:19 AM, Vadim Zaliva <vzaliva AT cmu.edu> wrote:

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