Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] coq library std++ 1.3 / coq 8.11

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] coq library std++ 1.3 / coq 8.11


Chronological Thread 
  • From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
  • To: Ralf Jung <jung AT mpi-sws.org>, "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] coq library std++ 1.3 / coq 8.11
  • Date: Mon, 23 Mar 2020 14:31:50 +0000
  • Accept-language: en-US
  • Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=anu.edu.au; dmarc=pass action=none header.from=anu.edu.au; dkim=pass header.d=anu.edu.au; arc=none
  • Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=SsoStov92F3t17ocPThYL49ipyCcmNsgCV1dJdCoF/g=; b=J8SchewsRpKjS9QOnZun91w3C69Px/zD4J++FFf5XidusDUQS9cNu/VptTAmox//K4qGR0T8cMJ7hm+1+p01XqOLL+GG3ubiaf8E3XXg8mmQIVvsB66dB6wz33FkmmLBBdWaSuEEQquz2yA80/HNyHQzq4YA1zpnnnH3QGPaZ59nx16xaGso8DPTwpKqLYBbwfdLXxkii/ebMXQg67YxVGWl733nxXf3nhPdX1ffw6YZ7341Ts9d7PKp03T3qGq7KplpLKaxwSl/amqsiZ/dvqBGpMp3NtOOJ73mqceEowGCJ9KSszMRdrJG5JTYHT4iDOz0QiGhDUfHZnOoj27oyg==
  • Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=IGnhLgoUV+o5fOZcr8WhUIPCm+5+DbakKMrPJ5WTi6JYi7v7rAhGDXeKn9tIYAsvAavdSMY6hCcQuni5GIF9PfqYBujLLwr6T09yj57Udy4ygGPd7fmHZ1OEaUi5avyBvMgo2Uxq9IbQPkL7XdyxdAyGpGegONxfL2WNwTUvIXr42/xjR7qdDP6hN4mQfsTVBj1fVwAt7LNwMdFac+VyWXXIveO+ymJNMHOcWuxMcVplg+jZDtIQvsTHrG3hAtxwRrkuiclOxA9LSJhp7gLlk2K3dC4CPZzNmbfU9EDhXzPMfk4ujj91b/dCGjflexQes/A5y6SETEIHt5KmftEFlw==
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-SY3-obe.outbound.protection.outlook.com
  • Ironport-phdr: 9a23:HqNLtRZjbA/HkfQlJZq9aNn/LSx+4OfEezUN459isYplN5qZrsm6bnLW6fgltlLVR4KTs6sC17OK9fm8CSdeut6oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUhrwOhBoKevrB4Xck9q41/yo+53Ufg5EmCexbal9IRmrogjdrNQajIRhJ6o+yxbErGZDdvhLy29vOV+ckBHw69uq8pV+6SpQofUh98BBUaX+Yas1SKFTASolPW4o+sDlrAHPQgST6HQSVGUWiQdIDBPe7B7mRJfxszD1ufR71SKHIMD5V7E0WTCl76d2VB/ljToMOjAl/G3LjMF7kblWqwy9qRNh34HUYZmVNPtgcaPbYdMaXndKUsJIWyBcHo+wc44DAuwcNuhasob9vUMDoxugCwexGOPhxDxGhnH00q073esuDQ7I0wM7EtISq3vZtsn5OLscXO23yqTD0DXNb+lR2Tf48IXGdg4uoeuSUrJ1ccva1EchGBnLj1WLrozlOS6e2+MJvWeF9epvS+evim49pw9/uDeuyNwsio7Pho8O0F/E8zh5zJwrKtKlVU53e8SrEIZJuiycKoB4TMQiQ2RytyY7zL0LoZ+7fC4QyJQm3RHTcfKHc5KO7xn+V+iROS91iX15dL6lmhq+7UqtxvfhWsS60ltGtDdJnsTCu3wV2BHe7tKLRuZ+80u9wzqDyh7f5+BeLUwplqfXNpgsyaMqmJUJq0TMBCr2lV32jKCIckUk/fCl5vjpbbv7upOQKpZ4hBz8Pakgg8C/Bv83PRYUU2ic5OS8yKbs/UrkQLVMk/I6iLHZsIrdJcQHuKG2HxNV0ock6xa5FTum18kYnWUDLFJCfxKHjJLlNE3JIPD9Ffu/glKsnyl3x/3eMbDtHo/BImXfnLrjZ7px9kBRxQgpwdxC+p5ZBKkNIPfpVU/wsNzYAAU5Mwuxw+v/DNtyyJkeVnyKAq6ZKq/cv0WH5+w0I+mLYo8YoyzyK/445/L0k3A2hEIdcbOz0psKcHy4BOhpI12FYXrwhdcMCXsFvg0nTODzlFKCVSNTaG2pUqIn5jA7DZqmAp3ZSoCshryBxia7EYdMamBIEFDfWUvvIr+NX/lESj+ULYc1kCECWpCkU45kzg618gjgxOwjZqDf/TRdvpb+3vB04ffSnFc873Y8W8+ayiSGS3x+tmIOXT4/mq5l9x9T0FCGhIp1mfFdBJR/7uxSVQFyYbzR1eF/GpbeUx3aedGhQVC7BNiqHHc4U4RikJc1f09hFoD63Vj41C2wDupQzuTTXcBmwufnx3H0Yv1F5TPezqB41QsvRNYJOGG7wKdipVCKVtz51n6BnqPvTpwymSvE9WON122L5RsKWQhtF6jJQDYWexmP9Imr1gb5V7arTI8fHE5BxMqFdvQYQ+DS1QwDf8a4fdPUbiS2hnu6AguOyvWUdo32dm4B3SLbTk8ZjwQU+nXAPg87VH6s
Hi Ralf,

Thanks - I tried opam update, and then as its output suggested doing
opam upgrade, I tried that.

However it (apparently) tried to reinstall coq 8.8.2 (why?) and failed,
saying ERROR while compiling coq.8.8.2

It suggested running
opam switch import
"/home/jeremy/opam-coq.8.8.2/ocaml-base-compiler.4.02.3/.opam-switch/backup/state-20200323132407.export"

which seemed to hang at the point Processing 9/13: [coq: make]

I think at the moment I have a working version of coq thanks to the
fedora package of coq, but how can I tell which version of the library
it is using?

Thanks

Jeremy

On 3/23/20 7:04 PM, Ralf Jung wrote:
> Hi Jeremy,
>
> std++ 1.3 is compatible with Coq 8.8.2 (and even with Coq 8.7.2), so that
> cannot
> be the problem. It looks like your package definitions are quite outdated,
> given that it cannot even find Coq 8.11.0. Did you try "opam update"?
>
> Kind regards,
> Ralf
>
> On 23.03.20 03:26, Jeremy Dawson wrote:
>>
>> Hi,
>>
>> > This release of the std++ library adds support for Coq 8.11 and is
>> available in Coq's opam repository.
>>
>> At present I have Coq 8.8.2 on my machine, and I don't know what version
>> of the standard library. How do I find that out?
>> How do I install a new version of the standard library (ie what do I do
>> to make use of the fact that it is "available in Coq's opam repository"?
>>
>> Trying opam install coq-stdpp seems to start installing coq-stdpp 1.1.0
>> which I assume is not what I want.
>>
>> In any event I assume I have to upgrade to Coq 8.11 to make use of it,
>> would that be right?
>>
>> I've tried to do that, following instructions at
>> https://coq.inria.fr/opam-using.html but part way through I get
>>
>> [jeremy@localhost sysadmin]$ opam pin add coq 8.11.0
>> [ERROR] Package coq has no known version 8.11.0 in the repositories
>>
>> What do I need to do?
>>
>> Thanks
>>
>> Jeremy
>>
>

Archive powered by MHonArc 2.6.18.

Top of Page