Bump upper bound to < 9.1 for coq-hammer-tactics

[Justme0606]

This PR adds an upper bound < "9.1.0" to the coq dependency for the following package(s):

• coq-hammer-tactics

This is required for compatibility with Rocq 9.0 and was tested successfully as part of the Rocq Platform 9.0 release preparation.

/cc @MSoegtropIMC

[MSoegtropIMC]

@Justme0606 : did you investigate the CI failure?

[Justme0606]

@Justme0606 : did you investigate the CI failure?

Yes sure, i just sending you an email about that.

Dear Michael,

Regarding this failure, I’m wondering if it might be related to coq-hammer.
The coq-hammer-tactics package includes the following constraint:
conflicts: [
"coq-hammer" {!= version}
]
Maybe I need to update coq-hammer to the same version alongside coq-hammer-tactics?

What do you think about this?

Best regards,

[MSoegtropIMC]

Indeed both packages need to be updated. I am not sure if CI will timeout, but since they are related I would suggest to do both updates in one go.

Note though that coq-hammer-tactics can be installed without coq-hammer, but if both are installed, they must have the same version. The coq-hammer-tactics without coq-hammer are useful to replay proofs found by coq-hammer on a different machine.

[Justme0606]

Indeed both packages need to be updated. I am not sure if CI will timeout, but since they are related I would suggest to do both updates in one go.

Note though that coq-hammer-tactics can be installed without coq-hammer, but if both are installed, they must have the same version. The coq-hammer-tactics without coq-hammer are useful to replay proofs found by coq-hammer on a different machine.

Ok, thanks for this explanation. That makes sense.
I updated both packages together accordingly.

[Justme0606]

@lukaszcz
Hello,
I’m encountering an error when I try to change the version constraint to 9.1.0~.
Would you happen to have any idea what might be causing this?
Thanks in advance !
Best Regards,

Installing coq-hammer-tactics.1.3.2+8.20
2363[WARNING] Running as root is not recommended
2364[ERROR] The installation of coq-hammer-tactics failed at "make test-tactics".
2365#=== ERROR while installing coq-hammer-tactics.1.3.2+8.20 =====================#
2366# context 2.1.2 | linux/x86_64 | ocaml-base-compiler.4.09.0 | file:///builds/coq/opam-repositories/released
2367# path ~/opam-root-4.09.0-2.1.2-sandbox/4.09.0/.opam-switch/build/coq-hammer-tactics.1.3.2+8.20
2368# command /usr/bin/make test-tactics
2369# exit-code 2
2370# env-file ~/opam-root-4.09.0-2.1.2-sandbox/log/coq-hammer-tactics-5367-8add14.env
2371# output-file ~/opam-root-4.09.0-2.1.2-sandbox/log/coq-hammer-tactics-5367-8add14.out
2372### output ###
2373# [...]
2374# Use "From Stdlib Require Psatz" or the deprecated "From Coq Require Psatz"
2375# for compatibility with older Coq versions.
2376# [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
2377# File "./tactics_test.v", line 493, characters 4-67:
2378# Error:
2379# Anomaly
2380# "File "pretyping/evarsolve.ml", line 913, characters 61-67: Assertion failed."
2381# Please report at http://coq.inria.fr/bugs/.
2382#
2383# make[1]: *** [Makefile:8: tactics_test.vo] Error 129
2384# make[1]: Leaving directory '/builds/coq/opam-repositories/opam-root-4.09.0-2.1.2-sandbox/4.09.0/.opam-switch/build/coq-hammer-tactics.1.3.2+8.20/tests/tactics'

[MSoegtropIMC]

@Justme0606 : can you please remove the change to coq-hammer again? After the CI went through we need to discuss with the maintainers what to do about this - to me it looks like a bug in the CI (it requires to build conflicting packages).

[Justme0606]

@Justme0606 : can you please remove the change to coq-hammer again? After the CI went through we need to discuss with the maintainers what to do about this - to me it looks like a bug in the CI (it requires to build conflicting packages).

Ok, I rolled back the coq-hammer opam file to version 8.21.~

[MSoegtropIMC]

@palmskog : can you please have a look at this? IMHO this is a bug in the CI. It insists on compiling coq-hammer because coq-hammer tactics says it is only compatible with specific versions of coq-hammer, but it actually does not require it and the matching versions is not available yet. But coq-hammer-tactics would work.

[MSoegtropIMC]

As explained above it is in my opinion a CI bug that CI fails, so I will go ahead and merge this PR today EOB unless someone complains before.

[silene]

I don't understand what you mean. The CI did not try to compile coq-hammer:

+- The following actions failed
| - install coq-hammer-tactics 1.3.2+8.20
+- 
+- The following changes have been performed
| - install conf-gmp            5
| - install conf-linux-libc-dev 0
| - install conf-pkg-config     4
| - install coq                 9.0.0
| - install coq-core            9.0.0
| - install coq-stdlib          9.0.0
| - install coqide-server       9.0.0
| - install dune                3.19.1
| - install ocamlfind           1.9.8
| - install rocq-core           9.0.0
| - install rocq-prover         9.0.0
| - install rocq-runtime        9.0.0
| - install rocq-stdlib         9.0.0
| - install zarith              1.14
+- 

And the error seems to be a genuine incompatibility between coq-hammer-tactics and Rocq 9.0:

File "./tactics_test.v", line 493, characters 4-67:
Error: Anomaly "File "pretyping/evarsolve.ml", line 913, characters 61-67: Assertion failed."
Please report at http://coq.inria.fr/bugs/.

[Justme0606]

I don't understand what you mean. The CI did not try to compile coq-hammer:

+- The following actions failed
| - install coq-hammer-tactics 1.3.2+8.20
+- 
+- The following changes have been performed
| - install conf-gmp            5
| - install conf-linux-libc-dev 0
| - install conf-pkg-config     4
| - install coq                 9.0.0
| - install coq-core            9.0.0
| - install coq-stdlib          9.0.0
| - install coqide-server       9.0.0
| - install dune                3.19.1
| - install ocamlfind           1.9.8
| - install rocq-core           9.0.0
| - install rocq-prover         9.0.0
| - install rocq-runtime        9.0.0
| - install rocq-stdlib         9.0.0
| - install zarith              1.14
+- 

And the error seems to be a genuine incompatibility between coq-hammer-tactics and Rocq 9.0:

File "./tactics_test.v", line 493, characters 4-67:
Error: Anomaly "File "pretyping/evarsolve.ml", line 913, characters 61-67: Assertion failed."
Please report at http://coq.inria.fr/bugs/.

Ok thanks

[MSoegtropIMC]

@silene : sorry for the confusion - there have been a few hence and forth iterations and I was too quick here.

The interesting point is that it does work in the Coq Platform CI of @Justme0606 's 9.0 preliminary pick:

https://github.com/rocq-prover/platform/actions/runs/16447168506/job/46482201062?pr=476#step:5:963

and I also have seen it working locally and I believe I have seen previous CI runs of this PR where trying to install coq-hammer itself was the issue.

I will investigate this deeper together with @Justme0606

[silene]

Does the platform run the package tests? Because the failure seemingly occurs in a test here.

[MSoegtropIMC]

@silene : thanks a very good point! Indeed Coq Platform CI does not install with with-tests enabled.

@Justme0606 : can you please check if only one specific test fails (by installing coq-hammer-tactics and going through the test file(s) in an IDE) or if coq-hammer-tactics fails frequently ... always.

[gares]

The assertion seems related to a misuse of the evarmap:
https://github.com/rocq-prover/rocq/blob/455ab6b39a73261b6dddcf914faed68af90d02ec/pretyping/evarsolve.ml#L912C5-L914
And it does not always fail since
https://github.com/lukaszcz/coqhammer/blob/fc88e83aba295cffd415fa601ff78847e522aad7/tests/tactics/tactics_test.v#L493
it is not the first occurrence of hauto.

[Justme0606]

Thanks Michael.
Yes i can do that. Just to be sure I understood correctly: you would like i manually install coq-hammer-tactics in the Rocq 9.0.0 environment and open in a IDE (VsCoq or COq IDE, right ? ) and run the test file to check whether a single specific test fails or if the file fails at multiple points.
Let me know if that’s the right approach, and I’ll proceed.

[lukaszcz]

I haven't tried to run CoqHammer with Rocq 9.x yet. I'll look into it and try to sort out possible incompatibilities, but probably won't have much time for it before the middle of August, if more changes are needed.

…

On Wed, 23 Jul 2025, 11:42 Enrico Tassi, ***@***.***> wrote: *gares* left a comment (rocq-prover/opam#3472) <#3472 (comment)> The assertion seems related to a misuse of the evarmap: https://github.com/rocq-prover/rocq/blob/455ab6b39a73261b6dddcf914faed68af90d02ec/pretyping/evarsolve.ml#L912C5-L914 And it does not always fail since https://github.com/lukaszcz/coqhammer/blob/fc88e83aba295cffd415fa601ff78847e522aad7/tests/tactics/tactics_test.v#L493 it is not the first occurrence of hauto. — Reply to this email directly, view it on GitHub <#3472 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAAPKH5IVANHX4EAVKS2NSL3J5KIJAVCNFSM6AAAAACB7PW7ESVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZTCMBWG42DENRSGI> . You are receiving this because you were mentioned.Message ID: ***@***.***>

[lukaszcz]

A hack solution would be to comment out whichever lemmas in the CoqHammer tactics test file are causing problems.

…

On Wed, 23 Jul 2025, 11:59 Łukasz Czajka, ***@***.***> wrote: I haven't tried to run CoqHammer with Rocq 9.x yet. I'll look into it and try to sort out possible incompatibilities, but probably won't have much time for it before the middle of August, if more changes are needed. On Wed, 23 Jul 2025, 11:42 Enrico Tassi, ***@***.***> wrote: > *gares* left a comment (rocq-prover/opam#3472) > <#3472 (comment)> > > The assertion seems related to a misuse of the evarmap: > > https://github.com/rocq-prover/rocq/blob/455ab6b39a73261b6dddcf914faed68af90d02ec/pretyping/evarsolve.ml#L912C5-L914 > And it does not always fail since > > https://github.com/lukaszcz/coqhammer/blob/fc88e83aba295cffd415fa601ff78847e522aad7/tests/tactics/tactics_test.v#L493 > it is not the first occurrence of hauto. > > — > Reply to this email directly, view it on GitHub > <#3472 (comment)>, > or unsubscribe > <https://github.com/notifications/unsubscribe-auth/AAAPKH5IVANHX4EAVKS2NSL3J5KIJAVCNFSM6AAAAACB7PW7ESVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZTCMBWG42DENRSGI> > . > You are receiving this because you were mentioned.Message ID: > ***@***.***> >

[MSoegtropIMC]

@Justme0606 : yes.

In general I prefer to include as many packages as possible in the preview, so that potential other issues can be found. But if if it will likely fall apart for every user, it would be better to not include it, because every user would fall into the issues we already know so that we wouldn't learn anything new from including it. We need to do some guess work on the odds.

[gares]

possibly related fix rocq-prover/rocq#20960
I did not check if solves the issue for @lukaszcz but looks very related (not really the primproj part, but the fact that it guards the call to the API that asserts false)

[lukaszcz]

I have updated CoqHammer to work with Rocq 9.0: #3526