Skip to content

Conversation

@ehildenb
Copy link
Member

  • Improvements to pyk serialization to files when running {krun,kast,kprove}JSON functions.
  • Add function which splits configuration from substitution to pyk.
  • Add definition JSON serialization/deserialization methods.
  • Add --emit-json option to Kompile which emits the json serialized definition to the -kompiled directory (and test of it).

Guy Repta and others added 26 commits September 12, 2019 12:53
@ehildenb ehildenb marked this pull request as ready for review September 13, 2019 03:43
Copy link
Contributor

@dwightguth dwightguth left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What exactly is this being used for? I highly doubt it is going to be possible to serialize, deserialize, and then compile or krun using the result. Not without more work to ensure a faithful rendering.

@ehildenb
Copy link
Member Author

@dwightguth I'm going to use it to build Python unparsers for KLabels automatically using pyks underbarUnparsing function, so that I can get rid of the tons of boilerplate in places like https://github.com/runtimeverification/polkadot-verification/blob/a50120c8493805d4146af4182bfb9dec44d298e0/pykWasm.py#L35 and https://github.com/runtimeverification/beacon-chain-spec/blob/a0975944c17537ecd070051cc08a387b2dda9403/buildConfig.py#L76

I do eventually want to be able to re-load definitions, but I removed the --input json option for komplie from this PR because it is not working yet. That's lower priority than having the definition available in structured form for external tools.

Copy link
Contributor

@dwightguth dwightguth left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks reasonable if you don't intend to deserialize it in the frontend yet.

@ehildenb ehildenb merged commit 91e6990 into master Sep 13, 2019
@ehildenb ehildenb deleted the JsonDefinitions branch September 13, 2019 18:42
Baltoli pushed a commit that referenced this pull request Apr 9, 2024
fixes: #771

This consolidates parameter validation into the Kompile classes so they
don't have to be declared a second time in KBuild.

---------

Co-authored-by: devops <devops@runtimeverification.com>
Baltoli pushed a commit that referenced this pull request Apr 9, 2024
fixes: #771

This consolidates parameter validation into the Kompile classes so they
don't have to be declared a second time in KBuild.

---------

Co-authored-by: devops <devops@runtimeverification.com>
Baltoli pushed a commit that referenced this pull request Apr 9, 2024
fixes: #771

This consolidates parameter validation into the Kompile classes so they
don't have to be declared a second time in KBuild.

---------

Co-authored-by: devops <devops@runtimeverification.com>
Baltoli pushed a commit that referenced this pull request Apr 9, 2024
fixes: #771

This consolidates parameter validation into the Kompile classes so they
don't have to be declared a second time in KBuild.

---------

Co-authored-by: devops <devops@runtimeverification.com>
Baltoli pushed a commit that referenced this pull request Apr 10, 2024
fixes: #771

This consolidates parameter validation into the Kompile classes so they
don't have to be declared a second time in KBuild.

---------

Co-authored-by: devops <devops@runtimeverification.com>
Baltoli pushed a commit that referenced this pull request Apr 10, 2024
fixes: #771

This consolidates parameter validation into the Kompile classes so they
don't have to be declared a second time in KBuild.

---------

Co-authored-by: devops <devops@runtimeverification.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants