wip

formal-land · Sep 17, 2024 · 93839a6 · 93839a6
1 parent 5ddc286
commit 93839a6
Show file tree

Hide file tree

Showing 6,005 changed files with 205,483 additions and 205,429 deletions.
diff --git a/.github/workflows/coq.yml b/.github/workflows/coq.yml
@@ -0,0 +1,44 @@
+name: Coq
+
+on:
+  push:
+    branches: [ "develop" ]
+  pull_request:
+    branches: [ "develop" ]
+
+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"
+            sudo apt-get update
+            sudo apt-get install -y cmake
+            opam install -y --deps-only coq/CoqOfSolidity/coq-of-solidity.opam
+          endGroup
+          startGroup "Build"
+            sudo chown -R $(whoami) .
+            mkdir build
+            cd build
+            cmake ..
+            make
+          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 coq/CoqOfSolidity
+            make
+            cd ..
+          endGroup
diff --git a/CoqOfSolidity/blacklist.txt b/CoqOfSolidity/blacklist.txt
diff --git a/...dity/test/libsolidity/semanticTests/abiEncoderV1/abi_decode_dynamic_array/GeneratedTest.v b/...dity/test/libsolidity/semanticTests/abiEncoderV1/abi_decode_dynamic_array/GeneratedTest.v
diff --git a/...idity/test/libsolidity/semanticTests/abiEncoderV1/abi_decode_fixed_arrays/GeneratedTest.v b/...idity/test/libsolidity/semanticTests/abiEncoderV1/abi_decode_fixed_arrays/GeneratedTest.v