Pruvendo libraries
Using Ursus requires installing numerous Pruvendo packages. Such as:
- coq-finproof-base
- pruvendo-base-lib
- coq-elpi-mod (modified by Pruvendo version of coq-elpi package)
- solidity-monadic-language
- ursus-standard-library
- pruvendo-ursus-tvm
- ursus-contract-creator
- ursus-environment
- ursus-quickhick
These packages requires several others packages:
- coq-mathcomp-zify
- coq-quickchick.1.6.4
Main script for installing whole environment (all package folders need to be in the same folder):
opam pin add coq 8.16.0 -y
cd coq-elpi-mod && opam install .
cd ../coq-finproof-base && opam install .
cd ../pruvendo-base-lib && opam install . -y
cd ../coq-elpi-mod && opam install . --ignore-pin-depends
cd ../solidity-monadic-language && opam install . -y --ignore-pin-depends
opam repo add coq-released https://coq.inria.fr/opam/released && opam install coq-mathcomp-zify
cd ../ursus-standard-library && opam install . -y --ignore-pin-depends
cd ../pruvendo-ursus-tvm && opam install . -y --ignore-pin-depends
cd ../ursus-contract-creator && opam install . -y --ignore-pin-depends
cd ../ursus-environment && opam install . -y --ignore-pin-depends
opam install coq-quickchick.1.6.4 -y
cd ../ursus-quickchick && opam install . -y --ignore-pin-depends