SkySkimmer on master
Define sphinx replacements for … Fix a De Bruijn bug in the comp… Merge PR #10904: Fix a De Bruij… (compare)
inversion H on this
H : Some (plug (pierce (class t) (core (get_option (locate (class t) fs) (fs_derive_obligation_1 A fs t pre i))) (layers (get_option (locate (class t) fs) (fs_derive_obligation_1 A fs t pre i))) (fs_derive_obligation_2 A fs t pre i)) t) = Some fs'
and it's taking 3 seconds. I made opaque these:
Opaque class. Opaque fs_derive_obligation_1. Opaque get_option. Opaque layers. Opaque core. Opaque plug. Opaque pierce. Opaque locate.
This is strange no?
plugwhich are defined through
Equations(replacing either one with dummy
Admittedfunctions make the inversion go through easily). When printing these functions, I see this message
plug is basically transparent but considered opaque for reduction. Is there a way to make these functions really opaque for all tactics?
congruenceare not respecting opacity?
reflexivitydoes not respect
c = Some y
inversionjust silently ignores
not parallelization which anyways in coq is gonna be quite hard to do soundly once you look at the dep graph
yeah, this I can easily imagine. The real structure of the state in Coq as it is today is very complex (lots of inter-dependencies)
Opaqueis not enough, you can try something like stdpp's
seal— example here: https://gitlab.mpi-sws.org/iris/iris/blob/master/theories/algebra/ofe.v#L304-308