Stream: Coq users

Topic: pow_pos_strict moved?

Ralf Jung (Jun 16 2021 at 18:41):

I am seeing a CI failure with Coq master

The reference ZifyInst.pow_pos_strict was not found in the current

The same code works fine in 8.13.2. I am trying to figure out what happened with that lemma, but can't find anything by grepping the changelog folder or searching in GH PRs...

Gaëtan Gilbert (Jun 16 2021 at 18:43):

looks like it was deleted https://github.com/coq/coq/commit/8193ca191cc435c108a4842ae38a11d74c7c20a5

Ralf Jung (Jun 16 2021 at 18:44):

from that diff maybe pow_nonneg works as a substitute

Ralf Jung (Jun 16 2021 at 18:44):

but the deletion should still be mentioned in the changelog, shouldnt it?

Ralf Jung (Jun 16 2021 at 18:45):

hm, no, pow_nonneg gives me a ≤ but I need a <

Ralf Jung (Jun 16 2021 at 18:45):

ah, pow_pos_nonneg works :)

Gaëtan Gilbert (Jun 16 2021 at 19:44):

Ralf Jung said:

but the deletion should still be mentioned in the changelog, shouldnt it?

I don't know
somehow random lemmas in ZifyInst should be internal details, but we don't have the tech to make that happen

Ralf Jung (Jun 16 2021 at 22:36):

Would be good to at least hide them from SearchAbout (if it had not shown up there, I would not have used it to begin with)

Ralf Jung (Jun 16 2021 at 22:39):

e.g. SearchAbout could skip Local Lemma

Last updated: Oct 13 2024 at 01:02 UTC