search

lukaszcz / coqhammer

CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
Other
211 stars 31 forks source link

hammer and coqserapi #173

Closed liuxingpeng520521 closed 7 months ago

liuxingpeng520521 commented 7 months ago

Hello, I'm currently trying to use coqserapi to do python interaction with coq, but I've noticed that when python reads a coq file, it has problems with the hammer statement. When I enable sauto i.e. without ”Set Hammer SAutoLimit 0.“, hammer works fine, when I disable sauto i.e. with “Set Hammer SAutoLimit 0.”, hammer reports an error. I think the possible reason is that coqserapi is not able to call solvers like cvc4, z3 etc when it encounters hammer, do you have any insights please?

liuxingpeng520521 commented 7 months ago

Sorry, I found the problem, when looking for Z3 in hamme, the difference in python interpreters (coqserapi in the virtual environment, Z3 uses the main environment) resulted in not finding Z3, which led to an error in the python code clock.