Bug in the "hammer" tactic with parallel proof processing in CoqIDE (minor)

lukaszcz / coqhammer

CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory

Other

217 stars 31 forks source link

Bug in the "hammer" tactic with parallel proof processing in CoqIDE (minor) #86

Open richardDap opened 4 years ago

richardDap commented 4 years ago

Coq version: 8.12 Operating System: Ubuntu 20.04 interface: CoqIde (8.12?) the problem occurs for any lemmas. Code example: Lemma not_True : (~ True) = False. Proof. hammer. Qed. which generates the following error: CoqHammer bug: please report: Not_found I am working in classical logic with proof irrelevance (Coq.Logic.Classical_Prop and Coq.Logic.PropExtensionality libraries) Does anyone has an idea of what is wrong? Thanks in advance.

lukaszcz commented 4 years ago

This seems to be related to issue #64 but now it is in "hammer" instead of in "sauto". The "CoqHammer bug: Not_found" error occurs when trying to compile a whole file in CoqIDE which contains invocations of the "hammer" tactic. This is a minor issue because one should not leave the "hammer" tactic in files in the first place - one should immediately upon success replace "hammer" with the reconstruction tactic shown in the response window.