coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Question about ATPs in CoqHammer

From: Richard Dapoigny <richard.dapoigny AT univ-smb.fr>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Question about ATPs in CoqHammer
Date: Fri, 11 Feb 2022 23:36:06 +0100 (CET)
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=richard.dapoigny AT univ-smb.fr; spf=Pass smtp.mailfrom=richard.dapoigny AT univ-smb.fr; spf=None smtp.helo=postmaster AT smtpout01-ext2.partage.renater.fr
Ironport-sdr: 4hZZ78xKnJhZgIQKve0mq1U7xvPDwlaRFRX2ciF6VwZ8NZ2DZcWt9WvC3+bvwVfhPQQ+tWo/am lYrakMTyhNJYVl0/XmcOWJ8Gw6O00F/XmwQiLc0QMKgnC/Hh/oBNPiYzmLyBGiKuKUXnNSK0T6 XuLomWyvsrFSIvc7agM5KlnfC6HAnbJ2JsudXhObubg81Cwn10HxW8PNLIrZFj1NVsKUXaWyyd cVXBA8DfOPIDwz69O7be9Mf+wIpIEal1Lyal3g8RjpjAIctDwZIV1dMD+TzHEwOMXHYnq9gl1M GdNMWUU3p5l9a3Xqxizz+gIP

Dear Coq users,

I had a previous version of Coq (Coq8.12 with CoqHammer v1.3) and the usual four ATPs (Eprover, z3_TPTP, cvc4 and Vampire) that worked fine with a xxx.v file.

Recently, I migrate to the Coq 8.14 version with CoqHammer (on another computer), and I have re-installed the four ATPs. Unfortunately, when i compile my xxx.v file i run into problems with a strange error message: some previously proved theorems appear in red with the following message "Dynlink error: execution of module initializers in the shared library failed: CErrors.UserError(_, _)".

If someone has an idea of the origin of this problem and eventually what can solve it?

Thanks in advance,

Cheers,

Richard

[Coq-Club] Question about ATPs in CoqHammer, Richard Dapoigny, 02/11/2022
- Re: [Coq-Club] Question about ATPs in CoqHammer, Michael Soegtrop, 02/12/2022