search

uwplse / pumpkin-pi

An extension to PUMPKIN PATCH with support for proof repair across type equivalences.
MIT License
49 stars 9 forks source link

8.9.1 #97

Closed tlringer closed 2 years ago

tlringer commented 3 years ago

hi

tlringer commented 3 years ago

There's a regression bug in Example.v, it's temporarily working but the tactics look scary, and this has something to do with certain reductions not running from what I can tell. The most suspicious thing is Datatypes.id hanging out and not reducing. Does opacity suddenly actually matter?

tlringer commented 3 years ago

optimization added, tests run in 180 seconds as opposed to 260 now, this optimization can eventually be generalized so we can have nice custom reducers abstracted away from the code better

still confused about the regression bug though, and need to check all tactic proofs from paper for reference

tlringer commented 3 years ago

Before merging, going to try the fixed/merged decompiler to see if that helps