Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
richardDap opened this issue Sep 1, 2020 · 1 comment
Assignees
Labels
bug Something isn't working

Comments

@richardDap
Copy link

richardDap commented Sep 1, 2020

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 lukaszcz self-assigned this Sep 1, 2020
@lukaszcz lukaszcz added the bug Something isn't working label Sep 1, 2020
@lukaszcz lukaszcz changed the title Problem using Hammer in lemmas Bug in the "hammer" tactic with parallel proof processing in CoqIDE (minor) Sep 2, 2020
@lukaszcz
Copy link
Owner

lukaszcz commented Sep 2, 2020

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
Development

No branches or pull requests

2 participants