| 13 May 2022 |
 koding | Is it as in this case, the accounts don't matter as all executions end up in revert. And as there are no accounts the evm visualisation fails? | 14:48:38 |
| koding | * (The value _31 is there in all branches without change.) Is it as in this case, the accounts don't matter as all executions end up in revert. And as there are no accounts the evm visualisation fails? | 14:49:31 |
 everett.hildenbrandt | Right, so I think I disabled generating the accounts cells because I wanted to minimize how much state was being mentioned, and those paths do end in revert. | 17:04:13 |
| everett.hildenbrandt | But I guess disabling that breaks some assuptions about KLab's visualization. | 17:04:25 |
| koding | I found that it breaks finding the name of the contract that is being debugged. :-) EVM and Stack work (for example, when I hardcode contract name in evmv.js). | 17:10:46 |
| everett.hildenbrandt | Which version of KLab are you using? | 17:14:47 |
| everett.hildenbrandt | If you have a patch that makes it work correctly, or lets the user usppyl contract name on command-line, then I'm sure we can get it merged. | 17:15:07 |
| koding | v0.4.0, commit f226560 | 17:16:02 |
| everett.hildenbrandt | Yeah but which repo? | 17:20:04 |
| everett.hildenbrandt | There are several forks. | 17:20:07 |
| koding | Good point. https://github.com/dapphub/klab
I will have a closer look on Tuesday or Wednesday and see what patch I can come up with. | 17:41:02 |
| everett.hildenbrandt | There is a makerdao/klab fork which I think is more up to date. | 17:41:59 |
| everett.hildenbrandt | You might try that one. | 17:42:06 |
| 16 May 2022 |
|  @usatokenshash:matrix.org joined the room. | 10:19:28 |
|  @idahotokens:matrix.org joined the room. | 11:16:38 |
 max.kopinsky | in the Haskell backend, we had a script which used to collect kore files from kprove commands using --save-temps. It seems like that's no longer supported, is there an alternative? | 16:07:52 |
| max.kopinsky | I'm not clear on if --save-proof-definition-to is what I want | 16:08:23 |
| max.kopinsky | its help text says "binary version" and not "kore version" so I do not think it is | 16:08:52 |
 radu.mereuta | Can you be more clear about your use case? I'm not sure I understand what you are trying to do.
But kprove/kprovex should have the option --save-temps which doesn't delete the temp files from the .kprove-xxx directory. You may also want to try --debug to get more information. | 16:11:25 |
| max.kopinsky | They do not have that option. | 16:13:57 |
| max.kopinsky | They used to, but they don't now. | 16:14:03 |
| max.kopinsky | $ kprovex --help , grep -e '--save-temps'
$
| 16:14:43 |
| max.kopinsky | [Error] Critical: Only one main parameter allowed but found several:
"tests/specs/examples/sum-to-n-spec.k" and "--save-temps"
(from kprovex as well) | 16:15:13 |
| max.kopinsky | we want to do exactly this, and then we search that directory for definition.kore and vdefinition.kore and save them. That way we can build a script to run the proof again without having to go through the frontend and such. We use this to generate regression tests in the Haskell backend | 16:16:06 |
| max.kopinsky | $ kprovex --version
K version: 5.3.36
Build date: Fri May 06 14:46:04 CDT 2022
| 16:16:36 |
| radu.mereuta | kprovex --debug spec.k should do what you are looking for. It keeps the .kprove-xxx folder in which it stores the spec.kore and result.kore file which are given as input to the haskell backend. vdefinition.kore doesn't exist anymore. We're using the unmodified definition.kore from the kompiled directory. | 16:26:15 |
| @idahotokens:matrix.org left the room. | 16:26:51 |
| max.kopinsky | I'll give that a shot | 16:30:44 |
| max.kopinsky | OK, I think that's working. Thanks! | 16:31:11 |
| @usatokenshash:matrix.org left the room. | 21:41:27 |
