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 e7f7328
Show file tree
Hide file tree
Showing 149 changed files with 12,862 additions and 10,503 deletions.
12 changes: 11 additions & 1 deletion .github/workflows/coq.yml
Original file line number Diff line number Diff line change
Expand Up @@ -19,14 +19,24 @@ jobs:
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_image: coqorg/coq:8.19-ocaml-4.14-flambda
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 e7f7328

Please sign in to comment.