Pruvendo libraries

Using Ursus requires installing numerous Pruvendo packages. Such as:

  1. coq-finproof-base
  2. pruvendo-base-lib
  3. coq-elpi-mod (modified by Pruvendo version of coq-elpi package)
  4. solidity-monadic-language
  5. ursus-standard-library
  6. pruvendo-ursus-tvm
  7. ursus-contract-creator
  8. ursus-environment
  9. ursus-quickhick

These packages requires several others packages:

  1. coq-mathcomp-zify
  2. 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