export updated information to proof_status folder #44
Conversation
| uv --project mir-semantics/kmir run -- \ | ||
| kmir show --proof-dir artefacts/proof p-token.smir.$start \ | ||
| --full-printer > artefacts/proof/${name}-full.txt | ||
| uv --project mir-semantics/kmir run -- \ | ||
| kmir show --dir artefacts/proof p-token.smir.$start \ | ||
| --statistics --leaves >> "${status_file}" |
There was a problem hiding this comment.
We might not need an extra proof_status directory... How about we put the commit hash of solana-token at the end of the proof directory?
This will prevent overwriting earlier results, and we can just go by file date of the proof directory.
There was a problem hiding this comment.
I think this might be another feature different from this one. The goal for this PR in my mind is to replace the previous proof_status.md file which only provides the structure of the proof that is not easy to investigate the error and update #24 . Additionally, we can have a proof status shared with all the team without rerunning on our own machine.
On the other hand, I think this feature is a version control of proofs which I want to introduce in another PR.
I'd like to merge this pr first and provide an issue to track this required feature. What do you think?
There was a problem hiding this comment.
- Here it is: Proof version control for solana-token #45
| REPO_COMMIT=$(git rev-parse --short HEAD 2>/dev/null || echo "unknown") | ||
| MIR_COMMIT=$(git -C mir-semantics rev-parse --short HEAD 2>/dev/null || echo "unknown") |
There was a problem hiding this comment.
We could mark the commits with -dirty if there are uncommitted changes.
2 participants
The goal here is to allow us sync up the proof information with minimal but sufficient information for quick investigation.
The updated run-proof.sh will:
solana-tokenandmir-semanticskmir show --statistics --leaves.