coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] QuickChick installation issues

From: Klaus Ostermann <klaus.ostermann AT uni-tuebingen.de>
To: coq-club AT inria.fr
Subject: [Coq-Club] QuickChick installation issues
Date: Tue, 16 Oct 2018 21:51:37 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=klaus.ostermann AT uni-tuebingen.de; spf=Pass smtp.mailfrom=klaus.ostermann AT uni-tuebingen.de; spf=None smtp.helo=postmaster AT mx03.uni-tuebingen.de
Ironport-phdr: 9a23:iaZgshCdgRndZf6lXEIpUyQJP3N1i/DPJgcQr6AfoPdwSPv8ocbcNUDSrc9gkEXOFd2Cra4c1KyO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUhjexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoJKT43/nzUhMJ+gq1Urw6uqRNkzo7IYoyYLuZycr/TcN4YQ2dKQ8ZfVzZGAoO5d4YBCu4BMvxFr4nmulAAtAC+BRWyC+P1zz9HnHn23asn2OkmEgHG2BYvH88VsHjOq9X1L7sSXv6vzKnN1zrDafVW1Czg6IjOcxAtuO2MXa9ufsXKyEkvEQzFgUuWqYD/IjyayP0Avm6G5ORjTeKik3Mrpg9+rzS12MsgkInEipgLxlzZ+yh12IQ4KN6iREN0b9OoCpRduz2AO4drTM4vTWdlszsgxLIco560Zi0KxYwnxxHBb/yHdJCF4hfsVeqNLzp0nm9leLS+hxqr7Uig1/PzWdK10FZMoSpKjN/MumoQ2BPN8sSHS/198Vm92TuXygze5O5JLVoqmabBK5Mt2KA8mocdvEjbGy/5gkT2jKuYdkU+/eio7vzqYrbippCGKo90kRvyMqM1msyjH+s4KA0OUHKd+eS6z7Dj4Ev5QLRTgv0qj6nWrovVJcUdpq62HQBV1Jwv5AuhADu+ytQXgWEHLE5ZeBKAl4XmJ1bOIOnhAfijh1SsjSxkyuvdPrzhB5XNNmLMnK3gfbZ78U5cyRA8wcpR55JOWfk9J6f4XVa0v9jFBDc4NRa1yqDpEoZTzIQbDEGLC7KCeITJrVKS4+spJaHYZ4scpS27LOM56uTrhHk/sUIbfOy1wJYdaXa3E/IgL0jPMimkucsIDWpf5ll2d+ftklDXCWcCNUb3ZLo143QAMKzjCI7CQo63h7nYjHWmGJwTen1LAFGKHnruMYmJCa5VNHCiZ/R5mzlBboCPDpc73Ej+5hL8yv97M+fe+ysXuJSl2NUnv7SOxyF3ziR9CoGm60/IT2xwmTlTFTomhPs5vEp8j0ue3KJ5hfNVE5pf6qERXw==
Openpgp: preference=signencrypt

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