The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

Yes,

The patch from Jason does just that and solves the problem with MathClasses.

Vadim

> On May 7, 2015, at 11:51 , Guillaume Claret 
> <guillaume AT claret.me>
>  wrote:
> 
> Does it work if you replace the `Require Import` with:
> 
>    Require Import
>      Coq.Lists.List SetoidList implementations.list
>      abstract_algebra interfaces.finite_sets interfaces.orders
>      theory.lattices orders.lattices.
> 
> I mean, all the imports should be fully prefixed to avoid a maximum of 
> ambiguities.
> 
> Best,
> Guillaume
> 
> The 05/07/2015 19:46, Vadim Zaliva wrote:
>> 
>>> On May 7, 2015, at 4:33 , Bas Spitters 
>>> <b.a.w.spitters AT gmail.com
>>> <mailto: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
>> 

Sincerely,
Vadim Zaliva

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