coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Christoph-Simon Senjak <christoph.senjak AT ifi.lmu.de>
To: coq-club AT inria.fr
Subject: [Coq-Club] Trying to build Ynot under Coq 8.6.1
Date: Thu, 9 Nov 2017 16:40:28 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=christoph.senjak AT ifi.lmu.de; spf=None smtp.mailfrom=christoph.senjak AT ifi.lmu.de; spf=None smtp.helo=postmaster AT acheron.ifi.lmu.de
Ironport-phdr: 9a23:PmtBDRwlo4sZ26rXCy+O+j09IxM/srCxBDY+r6Qd0uIRIJqq85mqBkHD//Il1AaPBtqLra8cw8Pt8IneGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2UXSJ/Sb3tWJaWkindFk9GuOgEYnLys+zyuqa+pvJYgwOiiDuT6l1KUCdrR/QrdURmYsnEac0zR2BmXZOee1VjTdjJUiShAr7/sf255Nl8S1Tk/Mv9ohEVLi8c6luHu8QNygvL21gvJ6jjhLEVwbauyMR

Hi.

I was trying to build Ynot [1] under Coq 8.6.1 (in a Nix-Shell). When trying to build, I get the error

File "./PermModel.v", line 33, characters 15-26:
Error: Cannot find a physical path bound to logical path matching suffix
Ynot.

And when trying to bind it with -R and importing Ynot, it is never found as a library.

I thought of directly writing to the given mailinglist on the Ynot website [2], but I cannot open the link, so I am asking here.

Best Regards,
Christoph-Simon Senjak

[1]:http://ynot.cs.harvard.edu/
[2]:https://lists.eecs.harvard.edu/mailman/listinfo/ynot-users

[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