search

runtimeverification / plutus-core-semantics

BSD 3-Clause "New" or "Revised" License
27 stars 5 forks source link

Contract compile and contract prove #378

Closed ChristianoBraga closed 2 years ago

ChristianoBraga commented 2 years ago 
- Add shell scripts `contract-compile` and `contract-prove` to KPlutus executable directory.
  * Change `Makefile` to do so.
  * Add the above scripts.
  * Update `README.md` with a draft explanation on how to use the scripts.

- With this PR and #376, assuming the directory structure and files
  exlpained in `README.md/Compiling contracts`, one just need to hit
  `contract-contract` and `contract-prove` to get one's properties
  proven.
ChristianoBraga commented 2 years ago

My working tree is not OK