coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] detecting opaque defintions that block computing

From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] detecting opaque defintions that block computing
Date: Fri, 26 Jun 2020 18:25:14 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk1-f177.google.com
Ironport-phdr: 9a23:8/OA6BHPt/vC87qPKoSiWZ1GYnF86YWxBRYc798ds5kLTJ7ypsywAkXT6L1XgUPTWs2DsrQY0reQ6vG6EjRRqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5yIRmssAncstcajYR+Jqs11xDEvmZGd+NKyG1yOFmdhQz85sC+/J5i9yRfpfcs/NNeXKv5Yqo1U6VWACwpPG4p6sLrswLDTRaU6XsHTmoWiBtIDBPb4xz8Q5z8rzH1tut52CmdIM32UbU5Uims4qt3VBPljjoMOjgk+2/Vl8NwlrpWrhyhqRJh3oDaY4abO/Vica3SZt4aWWhMU9xNWyFbHo+wcY0CBPcBM+ZCqIn9okMDoRW8BQmrAuPvyzxIiWHy3aIkzessCg7G3Ak6ENIPtHTYtsn6NKAXUey70aLFyjfDb/RQ2Tf864jHbBQhru+SUr9rfsrRzFMgFwLBjlmKtYPlODaV2/0LvmOG4OVuSfihhHQ7qwFtvDev3MEsh5HUio8Vyl7J+jt0zJopKNC4SkN2b8KpHZRMuyyaKod4TN8uTmVptSg6ybALp4K3cTQXxZg5xRPSd+GKfoaI7xztUuuaPDR2hGp9db6hmxq/9VKsx+78W8WuzlpGsDRJnsPRun0P1RHf8taLR/ph8ku83DuDygTe5f1BLE07lKfXN4Itz7s/m5UJrUjMACr7l1nqg6KWaEkp//Sn5uvpYrXoo5KcOZF7hRvxP6krgMOyBeU1PwcIUmOG4+qzzqfj8lf8QLhSjv05jK3ZsJfCKMQevKG5AgtV3p866xa8EjuqydoYkWQFIV9HYh6HgI/pO1bBIPD8E/izmUijkDBux/zeP73hBIvCLmTbnbv/Ybpw71RQxQkzwNxF+Z5YFK8NLOjuVkLzttHUFho5PBa1w+bjBtV9zIQeWWeXD6+bN6PSt16I5uExLOmIeoAapi3wK/cg5/H0jH85nUURcrWu3ZsScHy4BOhpI12FYXrwhdcMCXsFvg0nTODzlFKCVSNTaG2pUqIn5jA7DZqmAp3ZSoCshryBxia7EYdMamBIEFDfWUvvIo6DQrIHbD+YaptqlSVBXry8Qacg0wuvvUn00ew0APDT/3hSt5Xl1dt44+DevR43/D1wSc+a1ivFG2NzmGILSjs70YhwpEV8zhGI1q0u0K8QLsBa+/4cClRyDpXb1eEvU4mjCDKERc+ATROdevvjBDgwStwrxNpXOhRyHtyjilbI2C/4WuZJxYzOP4Q99+fn51a0P9x0ki+U26wojl1gScxKZzX/2/xPsjPLDouMqH230qancaNGgnzI/WaHiHON5QRWCVEvF6rCWn8baw3dqtGrvk4=

Is there a way in Coq to detect which opaque functions used in
the definition of a transparent function will block computing with
the transparent one?

Other than attempting to compute with test cases?

If I Print Opaque Dependencies, that shows too much, as not all
dependencies are involved in computing.

I think there used to be messages printed out during recursive
extraction when it encountered an opaque function, but I don't see that
anymore.

[Coq-Club] detecting opaque defintions that block computing, jonikelee AT gmail.com, 06/27/2020
- Re: [Coq-Club] detecting opaque defintions that block computing, Abhishek Anand, 06/27/2020
  - Re: [Coq-Club] detecting opaque defintions that block computing, jonikelee AT gmail.com, 06/27/2020
    - Re: [Coq-Club] detecting opaque defintions that block computing, Gregory Malecha, 06/30/2020