coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] A plugin to disable positivity check, guard check and termination check

From: Talia Ringer <tringer AT cs.washington.edu>
To: Coq-Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] A plugin to disable positivity check, guard check and termination check
Date: Thu, 21 Jun 2018 22:40:01 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=tringer AT cs.washington.edu; spf=None smtp.mailfrom=tringer AT cs.washington.edu; spf=None smtp.helo=postmaster AT mail-ua0-f179.google.com
Ironport-phdr: 9a23:7ZaBqRMTHiU9L9eVdxIl6mtUPXoX/o7sNwtQ0KIMzox0Lfv6rarrMEGX3/hxlliBBdydt6oZzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlIiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSgFOT438G/ZhM9tgqxFvB2svAZwz5LObYyPKPZyYqHQcNUHTmRBRMZRUClBD5uiYYQVC+oBPPxXpJThqVsPqxu+ChejBPnywTJPmn/2x6w60+IuEQ7YxgwtBM4BsG/OoNT7LqgSSuC1zKjOzTXMc/NW3jH95JLWfR88vPGBRLR9etffx0koEgPKlFSQqYr9MjOa1+QNr2ib7/d7Wu61l2EnrARxrz6yzckvkonEnpwZxkzA+Cljw4s4Jce0RFBmbdOmCpdcqiOXOo9wT8g/WW9nojw6xacDuZOjfCgF1pAnxxnHZvyCaYeI4xbjWP+MIThimH5pYby/iwuw/EWk0OH8Wc600FFFripBjNbArGwC1xvW6sSfS/t9+Fmu2SqX2gzN9u1JJVo4mKnbJpI73LI8i5gevV7eEiL0nEj6lKqWeV8l+uis5eTneLLmppqEOo9okAH+M6IumsOhDuQiKQUBQ3Ob9f6y1bL55k35QLRKjvs5kqnFt5DaI94XqbCkDA9Iyooj8QqwDy+60NQEmnkKNE5KeBWej4TwJ17OJO34AuykjlS3kDZrwujGMaf7DpXMKHjDirbhcqxn505S0gpghexYsrlTE/QqJO/5Ehv6s8WdBRskOSS1xfzmAZNzzNVNd3iIB/qlOafTuBey5+QgLvPEMJMPuTDyJuIN7OWoknYimV4bcrWu290aZG3uTacuGFmQfXe52oRJKmwNpAdrFLW72m3HaiZaYjOJZ4x54zg6DIy8CoKaF9Kmm/qe1Ty7H5tZemdATF2ADCWwLtnWa7I3cCuXZ/RZvHkcT7H4Gt0qzlexvRT6yrxoMu3SvCAUqMC7jYUn16jojRg3sAdMIYGd3mWKFT8mm2oJQ3or1fg6rxUimxGM1q93h/EeHttWtatE

Out of curiosity, is it documented at all which flags we could set from the plugin level that would lead to unsafe behavior? My impression is it'd be hard to do this by accident, but I still would love to know what to avoid, as a plugin developer.

On Thu, Jun 21, 2018 at 1:40 AM, Simon Boulier <simon.boulier AT inria.fr> wrote:

Dear all,

I made a plugin to experiment with type in type, non positive inductive
types and non terminating fixpoints:

https://github.com/SimonBoulier/TypingFlags

Enjoy!

Simon Boulier

[Coq-Club] A plugin to disable positivity check, guard check and termination check, Simon Boulier, 06/21/2018
- Re: [Coq-Club] A plugin to disable positivity check, guard check and termination check, Talia Ringer, 06/22/2018