Skip to content

Commit

Permalink
ci: add translation from Python
Browse files Browse the repository at this point in the history
  • Loading branch information
clarus committed May 21, 2024
1 parent 4dcabf9 commit 3072f0c
Show file tree
Hide file tree
Showing 149 changed files with 12,861 additions and 10,502 deletions.
10 changes: 10 additions & 0 deletions .github/workflows/coq.yml
Original file line number Diff line number Diff line change
Expand Up @@ -23,10 +23,20 @@ jobs:
custom_script: |
startGroup "Install dependencies"
opam install -y --deps-only CoqOfPython/coq-of-python.opam
sudo ln -s `which python3` /usr/bin/python
python --version
endGroup
startGroup "Set the rights"
sudo chown -R $(whoami) .
endGroup
startGroup "Translate the Python code to Coq"
cd ethereum-execution-specs/src
find ethereum -name "*.py" -print0 | xargs -0 -n 1 python ../../main.py
cd ../..
endGroup
startGroup "Make sure there no differences"
git diff --exit-code
endGroup
startGroup "Compile Coq translations"
cd CoqOfPython
make
Expand Down
3 changes: 3 additions & 0 deletions .gitmodules
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
[submodule "ethereum-execution-specs"]
path = ethereum-execution-specs
url = https://github.com/ethereum/execution-specs.git
4 changes: 2 additions & 2 deletions CoqOfPython/coq-of-python.opam
Original file line number Diff line number Diff line change
Expand Up @@ -15,8 +15,8 @@ bug-reports: "https://github.com/formal-land/coq-of-python/issues"
dev-repo: "git+https://github.com/formal-land/coq-of-python.git"
depends: [
"ocaml" {>= "4.08"}
"coq" {>= "8.17.1" & < "8.18"}
"coq-hammer" {>= "1.3.2+8.17" & < "1.3.2+8.18"}
"coq" {>= "8.17.1" }
"coq-hammer"
]
build: [
[make]
Expand Down
Loading

0 comments on commit 3072f0c

Please sign in to comment.