The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

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