coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Trying to build Ynot under Coq 8.6.1

From: Aleksandar Nanevski <aleks.nanevski AT imdea.org>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Trying to build Ynot under Coq 8.6.1
Date: Thu, 9 Nov 2017 18:15:29 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=aleks.nanevski AT imdea.org; spf=Pass smtp.mailfrom=aleks.nanevski AT imdea.org; spf=None smtp.helo=postmaster AT estafeta21.imdea.org
Dkim-filter: OpenDKIM Filter v2.10.3 estafeta21.imdea.org F19EB136CA2
Ironport-phdr: 9a23:B3HR7xFVL7r/00Idt3V5fJ1GYnF86YWxBRYc798ds5kLTJ76r8ywAkXT6L1XgUPTWs2DsrQf1LqQ7viocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TWEwzEeIjLafUoof6WmUrLV2s+wzqW5/4DZSwROnju0J71ofzusqgCEn80bgpBrLKo40FPvq31FZf9VxCs8LFaenA264M628YB48CV4uvct+scGVr/1KfdrBYdEBSgrZjhmrPbgsgPOGFbW6w==

Hi Christoph.

If you're not interested in concurrency, you can look at HTT, a related project to Ynot at

https://software.imdea.org/~aleks/htt/

It compiles with Coq 8.7.

Best,
-Aleks

On 09/11/17 17:07, Matthieu Sozeau wrote:

Hi Christoph,

you might be interested in Nanevsky's et al. related FCSL's library, which is available for Coq 8.5 at least http://software.imdea.org/fcsl/

Best,

-- Matthieu

On Thu, Nov 9, 2017 at 4:43 PM Adam Chlipala <adamc AT csail.mit.edu> wrote:

Sorry, Ynot is a dead project, with no particular expectation that
anything builds on any recent version of Coq.

On 11/09/2017 10:40 AM, Christoph-Simon Senjak wrote:
> I was trying to build Ynot [1] under Coq 8.6.1 (in a Nix-Shell).

[Coq-Club] Trying to build Ynot under Coq 8.6.1, Christoph-Simon Senjak, 11/09/2017
- Re: [Coq-Club] Trying to build Ynot under Coq 8.6.1, Adam Chlipala, 11/09/2017
  - Re: [Coq-Club] Trying to build Ynot under Coq 8.6.1, Matthieu Sozeau, 11/09/2017
    - Re: [Coq-Club] Trying to build Ynot under Coq 8.6.1, Ralf Jung, 11/09/2017
    - Re: [Coq-Club] Trying to build Ynot under Coq 8.6.1, Aleksandar Nanevski, 11/09/2017