The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

This is a problem that is fixable within MathClasses, and would require much more of a change in Coq; on case-insensitive filesystems, Coq doesn't know whether [Require Import List] means [Require Import MathClasses.implementations.list.] or [Require Import Coq.Lists.List.].  The appropriate solution is to always use absolute names for Imports.  Fixing Coq would require treating the filename on a case-insensitive system as case-sensitive, perhaps by not just saying "OS, give me the files of the form 'List.vo' in this directory" but additionally filtering that list for files whose names don't match "List.vo" in case, if such a thing is possible on case-insensitive systems (or filtering out files whose library names don't match the given library name in case).  I shall be submitting a pull request that fixes this on the trunk branch shortly.

-Jason

On Thu, May 7, 2015 at 1:46 PM, Vadim Zaliva <vzaliva AT cmu.edu> wrote:

On May 7, 2015, at 4:33 , Bas Spitters <b.a.w.spitters AT gmail.com> wrote:

I haven't thought deeply about case sensitivity, but if it requires a minor change, I'd be willing to accept a pull request.

Case-sensitivity problem is very annoying on MacOS. Here is a background: default MacOS file system is case-insensitive

but case-preserving. So you you create file “A” it will be shown in upper case but you can open it either as “a” or “A”. Here is

what happens with MathClasses:

$ coqc -verbose -R . MathClasses -q implementations/list_finite_set.v

Require Import

  List SetoidList implementations.list

  abstract_algebra interfaces.finite_sets interfaces.orders

  theory.lattices orders.lattices.

Warning: List.vo has been found in

[ /Users/lord/tmp/math-classes/implementations ;

  /Volumes/CoqLibs/coq/lib/coq/theories/Lists ];

loading /Users/lord/tmp/math-classes/implementations/List.vo

File "./implementations/list_finite_set.v", line 1, characters 0-148:

Error: The file /Users/lord/tmp/math-classes/implementations/List.vo contains library

MathClasses.implementations.list and not library

MathClasses.implementations.List

I think it is not really MathClasses problem. It could occur whenever you import some module of which you have several

versions in your search path with names in different case.

I think the proper solution is for coq to ignore files where file name does not match enclosed implementation, perhaps issuing a warning instead of an error. This should be a trivial patch to Coq itself. Maybe right now before 8.5 release it is a good way to put it in? MacOS users will benefit from it.

Sincerely,
Vadim Zaliva

--

CMU ECE PhD candidate

Mobile: +1(510)220-1060

Skype: vzaliva