search

coq-tactician / coq-tactician-api

An API for interfacing with Coq through Tactician by external agents
https://coq-tactician.github.io/api/introduction
MIT License
2 stars 1 forks source link

Add the entropy of the base tactics distribution to the sanity check summary #5

Closed LasseBlaauwbroek closed 2 years ago

LasseBlaauwbroek commented 2 years ago

I wonder what the most numerically stable formula for entropy is...

LasseBlaauwbroek commented 2 years ago

We agreed that this metric is certainly not the perfect metric. But for now, it is better than nothing. So I'm merging....