rust.yml

name: Rust

on:
  push:
    branches: [ "main" ]
  pull_request:
    branches: [ "main" ]

env:
  CARGO_TERM_COLOR: always

jobs:
  build:

    runs-on: ubuntu-latest

    steps:
    - uses: actions/checkout@v3
    - name: Download Git submodules
      run: git submodule update --init --recursive
    - uses: coq-community/docker-coq-action@v1
      with:
        custom_image: coqorg/coq:8.17-ocaml-4.14-flambda
        custom_script: |
          startGroup "Install dependencies"
            curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y
            source "$HOME/.cargo/env"
            cargo --version
            sudo ln -s `which python3` /usr/bin/python
            opam install -y --deps-only CoqOfRust/coq-of-rust.opam
          endGroup
          startGroup "Build"
            sudo chown -R $(whoami) .
            cargo build --verbose
          endGroup
          startGroup "Install"
            cargo install --path lib/
          endGroup
          startGroup "Format check"
            cargo fmt --check
          endGroup
          startGroup "Lint"
            cargo clippy --all-targets --all-features -- -D warnings
          endGroup
          startGroup "Translate Rust examples"
            python run_tests.py
          endGroup
          startGroup "Pre-process the smart contracts"
            cd contracts
            python source_to_generated.py
            cd generated
            for dir in * ; do cd $dir ; cargo check ; cd .. ; done
            cd ../..
          endGroup
          # We disable for now this translation as this makes a panic!
          # startGroup "Translate Ink! library"
          #   cd CoqOfRust
          #   ./generate_ink_example.sh
          #   cd ..
          # endGroup
          startGroup "Save space"
            cargo clean
          endGroup
          startGroup "Translate the alloc library"
            cd third-party/rust/library/alloc
            cp ../../../../rust-toolchain ./
            cargo build
            touch src/lib.rs
            cargo coq-of-rust
            rsync -acv src/ ../../../../CoqOfRust/alloc/ --include='*/' --include='*.v' --exclude='*'
            cd ../../../..
          endGroup
          startGroup "Translate the core library"
            cd third-party/rust/library/core
            cp ../../../../rust-toolchain ./
            cargo build
            touch src/lib.rs
            cargo coq-of-rust
            rsync -acv src/ ../../../../CoqOfRust/core/ --include='*/' --include='*.v' --exclude='*'
            cd ../../../..
          endGroup
          startGroup "Save space"
          cd third-party/rust/library/alloc
            cargo clean
            cd ../../../..
            cd third-party/rust/library/core
            cargo clean
            cd ../../../..
          endGroup
          startGroup "Translate Revm"
            cd third-party/revm
            cp ../../rust-toolchain ./
            cd crates
            # We compile each library twice to avoid errors. TODO: investigate why this is needed
            # interpreter
            cd interpreter
            cargo coq-of-rust
            touch src/lib.rs
            cargo coq-of-rust
            rsync -acv src/ ../../../../CoqOfRust/revm/translations/interpreter/ --include='*/' --include='*.v' --exclude='*'
            cd ..
            # precompile
            cd precompile
            cargo coq-of-rust
            touch src/lib.rs
            cargo coq-of-rust
            rsync -acv src/ ../../../../CoqOfRust/revm/translations/precompile/ --include='*/' --include='*.v' --exclude='*'
            cd ..
            # primitives
            cd primitives
            cargo coq-of-rust
            touch src/lib.rs
            cargo coq-of-rust
            rsync -acv src/ ../../../../CoqOfRust/revm/translations/primitives/ --include='*/' --include='*.v' --exclude='*'
            cd ..
            # revm
            cd revm
            cargo coq-of-rust
            touch src/lib.rs
            cargo coq-of-rust
            rsync -acv src/ ../../../../CoqOfRust/revm/translations/revm/ --include='*/' --include='*.v' --exclude='*'
            cd ..
            cd ../../..
          endGroup
          startGroup "Translate Move Sui"
            cd third-party/move-sui
            cp ../../rust-toolchain ./
            cd crates
            # move-abstract-stack
            cd move-abstract-stack
            cargo coq-of-rust
            touch src/lib.rs
            cargo coq-of-rust
            rsync -acv src/ ../../../../CoqOfRust/move_sui/translations/move_abstract_stack/ --include='*/' --include='*.v' --exclude='*'
            cd ..
            # move-binary-format
            cd move-binary-format
            cargo coq-of-rust
            touch src/lib.rs
            cargo coq-of-rust
            rsync -acv src/ ../../../../CoqOfRust/move_sui/translations/move_binary_format/ --include='*/' --include='*.v' --exclude='*'
            cd ..
            # move-bytecode-verifier
            cd move-bytecode-verifier
            cargo coq-of-rust
            touch src/lib.rs
            cargo coq-of-rust
            rsync -acv src/ ../../../../CoqOfRust/move_sui/translations/move_bytecode_verifier/ --include='*/' --include='*.v' --exclude='*'
            cd ..
            # move-bytecode-verifier-meter
            cd move-bytecode-verifier-meter
            cargo coq-of-rust
            touch src/lib.rs
            cargo coq-of-rust
            rsync -acv src/ ../../../../CoqOfRust/move_sui/translations/move_bytecode_verifier_meter/ --include='*/' --include='*.v' --exclude='*'
            cd ..
            # move-core-types
            cd move-core-types
            cargo coq-of-rust
            touch src/lib.rs
            cargo coq-of-rust
            rsync -acv src/ ../../../../CoqOfRust/move_sui/translations/move_core_types/ --include='*/' --include='*.v' --exclude='*'
            cd ..
            cd ../../..
          endGroup
          startGroup "Check that the diff is empty (excluding submodules)"
            git -c color.ui=always diff --exit-code --ignore-submodules=dirty
          endGroup
          startGroup "Compile Coq translations"
            cd CoqOfRust
            python ./make_and_detect_warnings.py
            cd ..
          endGroup