Currently when using the pyk library, we have to get a "blank" configuration to use for manipulating K terms and stuff. To produce this, I run a garbage proof out to depth 0, and strip the configuration. For example, I may run this proof out to depth 0:
claim <k> #execute => . ... </k>
This will give me a configuration that looks like this:
<generatedTop>
<kevm>
<k> #execute ... </k>
<mode> _0 </mode>
<schedule> _1 </schedule>
...
</generatedTop>
Which I then strip to look like:
<generatedTop>
<kevm>
<k> K_CELL </k>
<mode> MODE_CELL </mode>
<schedule> SCHEDULE_CELL </schedule>
...
</generatedTop>
So it would be nice if when I call kompile --emit-json, it dumped the empty configuration to a file empty-config.json in the *-kompiled directory. Then I could just read that file off instead using this ad-hoc way of generating it.
Currently when using the pyk library, we have to get a "blank" configuration to use for manipulating K terms and stuff. To produce this, I run a garbage proof out to depth 0, and strip the configuration. For example, I may run this proof out to depth 0:
This will give me a configuration that looks like this:
Which I then strip to look like:
So it would be nice if when I call
kompile --emit-json, it dumped the empty configuration to a fileempty-config.jsonin the*-kompileddirectory. Then I could just read that file off instead using this ad-hoc way of generating it.