Skip to Content.
Sympa Menu

ssreflect - Re: [ssreflect] Problem compilation mathcomp-1.6

Subject: Ssreflect Users Discussion List

List archive

Re: [ssreflect] Problem compilation mathcomp-1.6


Chronological Thread 
  • From: Enrico Tassi <>
  • To:
  • Subject: Re: [ssreflect] Problem compilation mathcomp-1.6
  • Date: Sat, 19 Dec 2015 10:35:24 +0100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None ; spf=None ; spf=None
  • Ironport-phdr: 9a23:tI95FBP74SFq8qTwUUIl6mtUPXoX/o7sNwtQ0KIMzox0KPj5rarrMEGX3/hxlliBBdydsKIazbKO+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuStCU15z//tvx0qOQSj0AvCC6b7J2IUf+hiTqne5Sv7FfLL0swADCuHpCdrce72ppIVWOg0S0vZ/or9YwuxhX7uk67cNOVajxY4w9VqYdDTI8Mmlz5cvxtBCFQxHcyGEbVzA7lABJCA+N0BjhRZa55ib8rOt232+GNNbtTJg1Xy6j5uFlUkm72288Kzcl/TSP2YRLh6VBrUf5qg==
On Fri, Dec 18, 2015 at 11:33:58PM +0100, Florent Hivert wrote:
> Dear all,
>
> I tried to compile the brand new mathcomp-1.6 and I'm running into
> trouble. The output show a lot of error messages such as
>
> mkdir: cannot create directory ‘bkpcoqdep’: File exists
> mv: cannot stat ‘bkpcoqdep/algebra/interval.v’: No such file or directory
> find: ‘bkpcoqdep’: No such file or directory

Dear Florent, looks like the etc/utils/ssrcoqdep does not work properly
for you.

I'll look into it next week.

Best,
--
Enrico Tassi

Archive powered by MHonArc 2.6.18.

Top of Page