coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] QuickChick installation issues

From: Yishuai Li <yishuai AT cis.upenn.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] QuickChick installation issues
Date: Wed, 17 Oct 2018 14:07:27 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=yishuai AT cis.upenn.edu; spf=Pass smtp.mailfrom=yishuai AT seas.upenn.edu; spf=None smtp.helo=postmaster AT mail-it1-f177.google.com
Ironport-phdr: 9a23:+eb+uxApwdMNCnOdRQi9UyQJP3N1i/DPJgcQr6AfoPdwSPv9r8bcNUDSrc9gkEXOFd2Cra4c1KyO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUhjexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoIODA5/2PXhMJ+j6xVvQyvqABkzoHOfI2YLuBzcr/Bcd4YQ2dKQ8ZfVzZGAoO5d4YADesBPf1Yr4ngvVQOrAa1Cw+tBOjyzTJJhn723bY60+Q8Cw7G3RctEM4PsHTPttn1Kb8SXv6zzKnO1znMce5Z2Srk5YXObxsvr/aMXbdqfsrQz0kiDwzFjlSMqYzlIjOazf4BvHSc7+plU++klm0pqxlprzSx2sshjpPFi4EVx1ze6Cl0wYc4KcelREN5Y9OoCIVcuz2eOodsQc4vQ3tktDs7x7AHo5K3YSkHxZAhyhXCcfKIaZKI7QjmVOuJITd3mnZleLWniha360egy+n8WtC10FZWsyZJi9fMum0P2hHR8MSHRfx9/kCu2TaLyQ/f8P1LIUcxlabDKp4hxKA/loYLvEjdAiP7nF/6gayWe0k+5+Sl6uXqbq/7qpKeNYJ4kgT+Pb4vmsy7D+Q4KA8OX22D9OW81b3j5k35QKhQgf03iaTZq47VKt4ApqKjHg9Vypgs6xC5Dzu8ztsXgGQHIEpfeB2bl4jpJ03OIPfgAPijhFSsiS5nyOzCPr38GZrANWPDkbfkfbZl8UFQ0gszzdZF55JVEL4NOvzzWlWi/ODfWxQ+Kkm/x/vtINR7zIIXH2yVUYGDN6aHgF6T5v8mIqGoZcdBqTfmK+Us5tbljGR/hEcQe6/v0JcKPiPrVs96KlmUNCK/yuwKFn0H61JnHb7azWaaWDsWXE6cGqc15zU1EoWjVNmRXY2km/qcxCq9GNtban0UUwnQQ0etTJ2NXrI3UAzXOtVoy2FWXrm6DZI52Beo8gL21ug/d7eGymgjrZvmkeNNyajTmBU1r2ImCs2c1ySMUzgxkDpXGHk526dwpUE7wVCGg/B1

How did you install CoqIDE? I could not locate CoqIDE in Applications bar after installing it via OPAM.

This issue is also being tracked in QuickChick/QuickChick#120.

Klaus Ostermann <klaus.ostermann AT uni-tuebingen.de> 于2018年10月16日周二下午3:52写道：

I want to use QuickChick with CoqIDE, but I can't get it to work properly.

I installed CoqIDE and QuickChick according to the official instructions.

QuickChick works fine when I run it inside coqtop.

For CoqIDE, I get the following strange behavior:

1. If I run CoqIDE from the command line, QuickChick works but the
output of QuickChick
is displayed in the console from which I started CoqIDE, not within CoqIDE.

2. If I run CoqIDE directly from the Applications bar (not via terminal
window),
I get an error "Could not compile mli file" when I execute a QuickChick
command.

I use Coq 8.8.2 with opam 2.0.0 on a Mac with OS version 10.13.2.

Any ideas?

Klaus

[Coq-Club] QuickChick installation issues, Klaus Ostermann, 10/16/2018
- Re: [Coq-Club] QuickChick installation issues, Yishuai Li, 10/17/2018
- Re: [Coq-Club] QuickChick installation issues, Yishuai Li, 10/17/2018