Skip to content

Commit ca461e7

Browse files
committed
ci: build lean wrapper without make
1 parent de12777 commit ca461e7

1 file changed

Lines changed: 10 additions & 1 deletion

File tree

.github/workflows/lean-verification.yml

Lines changed: 10 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -65,7 +65,16 @@ jobs:
6565
run: |
6666
source $HOME/.elan/env
6767
cd impl/ocaml
68-
make build-c
68+
lean_prefix="$(lean --print-prefix)"
69+
lean_include="$lean_prefix/include"
70+
lean_lib="$lean_prefix/lib/lean"
71+
gcc -shared -fPIC -o liblean_vsh.so \
72+
lean_wrapper.c \
73+
../../proofs/lean4/.lake/build/ir/Extraction.c \
74+
-I"$lean_include" \
75+
-L"$lean_lib" \
76+
-lleanshared \
77+
-Wl,-rpath,"$lean_lib"
6978
7079
- name: Verify shared library
7180
run: |

0 commit comments

Comments
 (0)