search

leanprover / LNSym

Armv8 Native Code Symbolic Simulator in Lean
Apache License 2.0
60 stars 18 forks source link

feat: enable fuel for CSE #130

Closed bollu closed 1 month ago

bollu commented 2 months ago

In doing so, we also cleanup the logging code, since the process of adding fuel involves visiting each call site, which is exactly where we want to add logging information!

Supercedes #113, as the fixes from that PR have been merged in. Foo #124 , #114

bollu commented 1 month ago

@shigoel ready for merge!

shigoel commented 1 month ago

@bollu Looks good in general, but I'm concerned whether the traces give a verbose make output.

bollu commented 1 month ago

@shigoel I understand, I cleaned up the one that wasn't guarded. All of the other trace messages are #guard_msgs, so we should be good!

bollu commented 1 month ago

@shigoel ready for merge, methinks!

shigoel commented 1 month ago

Thanks, @bollu!