search

lukaszcz / coqhammer

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

Support for Coq 8.19 #175

Closed SnarkBoojum closed 7 months ago

SnarkBoojum commented 9 months ago

I just tried to compile coq-hammer against Coq 8.19 ; it fails with:

File "src/lib/hhutils.ml", line 236, characters 27-49:
236 |          destruct_app evd (Tacred.try_red_product (Global.env ()) evd t)
                                 ^^^^^^^^^^^^^^^^^^^^^^
Error: Unbound value Tacred.try_red_product

(no further investigation done)

lukaszcz commented 9 months ago

Coq 8.19 is not yet supported -- there is no branch for it. I will add support soon, definitely before the next Coq Platform release. The master branch of CoqHammer tracks the master branch of Coq. Going a few commits back on master should achieve compatibility with Coq 8.19 -- you can try that if you don't want to wait.

SnarkBoojum commented 9 months ago

I don't care that much about the Coq Platform -- Debian is another distribution entirely.

I'd rather package an official version than a patched-up one, so I'll wait. There are other packages missing compatible versions, so no hurry.

Thanks.

lukaszcz commented 7 months ago

The 1.3.2 release for Coq 8.19 is now available. It should soon be available from opam.