The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

Any chance this patch making it into math-classes packake in coq-stable opam 
package (https://github.com/coq/repo-stable.git)? That would allow 
math-classes Mac users to switch
to OPAM-based package instead of compiling it manually.

Thanks!

Vadim


> On May 11, 2015, at 9:21 , Vadim Zaliva 
> <vzaliva AT cmu.edu>
>  wrote:
> 
> 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
> 

Sincerely,
Vadim Zaliva

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