Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[ci] [worker] Make the build flexible for non-vendored setups. #842

Merged
merged 1 commit into from
Sep 29, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
21 changes: 14 additions & 7 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -154,17 +154,25 @@ patch-for-js:

_LIBROOT=$(shell opam var lib)

# At some point this may be the better idea
VENDORED_SETUP:=true

ifdef VENDORED_SETUP
_CCROOT=_build/install/default/lib/coq-core
else
_CCROOT=$(shell coqc -where)/../coq-core
endif

# Super-hack
controller-js/coq-fs-core.js: COQVM = no
controller-js/coq-fs-core.js: coq_boot
dune build --profile=release --display=quiet $(PKG_SET) etc/META.threads
for i in $$(find _build/install/default/lib/coq-core/plugins -name *.cma); do js_of_ocaml --dynlink $$i; done
for i in $$(find $(_CCROOT)/plugins -name *.cma); do js_of_ocaml --dynlink $$i; done
for i in $$(find _build/install/default/lib/coq-lsp/serlib -wholename */*.cma); do js_of_ocaml --dynlink $$i; done
cd _build/install/default/lib && \
js_of_ocaml build-fs -o coq-fs-core.js \
$$(find coq-core/ \( -wholename '*/plugins/*/*.js' -or -wholename '*/META' \) -printf "%p:/static/lib/%p ") \
$$(find coq-lsp/ \( -wholename '*/serlib/*/*.js' -or -wholename '*/META' \) -printf "%p:/static/lib/%p ") \
../../../../etc/META.threads:/static/lib/threads/META \
js_of_ocaml build-fs -o controller-js/coq-fs-core.js \
$$(find $(_CCROOT)/ \( -wholename '*/plugins/*/*.js' -or -wholename '*/META' \) -printf "%p:/static/lib/%p ") \
$$(find _build/install/default/lib/coq-lsp/ \( -wholename '*/serlib/*/*.js' -or -wholename '*/META' \) -printf "%p:/static/lib/%p ") \
./etc/META.threads:/static/lib/threads/META \
$$(find $(_LIBROOT) -wholename '*/str/META' -printf "%p:/static/lib/%P ") \
$$(find $(_LIBROOT) -wholename '*/seq/META' -printf "%p:/static/lib/%P ") \
$$(find $(_LIBROOT) -wholename '*/uri/META' -printf "%p:/static/lib/%P ") \
Expand All @@ -189,7 +197,6 @@ controller-js/coq-fs-core.js: coq_boot
$$(find $(_LIBROOT) -wholename '*/ppx_deriving_yojson/META' -printf "%p:/static/lib/%P ")
# These libs are actually linked, so no cma is needed.
# $$(find $(_LIBROOT) -wholename '*/zarith/*.cma' -printf "%p:/static/lib/%P " -or -wholename '*/zarith/META' -printf "%p:/static/lib/%P ")
cp _build/install/default/lib/coq-fs-core.js controller-js

# Serlib plugins require:
# ppx_compare.runtime-lib
Expand Down
2 changes: 1 addition & 1 deletion controller-js/dune
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,7 @@
(package coq-stdlib))
(action
(bash
"cd ../vendor/coq && js_of_ocaml build-fs -o ../../controller-js/coq-fs.js $(find theories user-contrib \\( -wholename 'theories/*.vo' -or -wholename 'theories/*.glob' -or -wholename 'theories/*.v' -or -wholename 'user-contrib/*.vo' -or -wholename 'user-contrib/*.v' -or -wholename 'user-contrib/*.glob' \\) -printf '%p:/static/coqlib/%p ')")))
"export COQW=$(coqc -where) && js_of_ocaml build-fs -o coq-fs.js $(cd $COQW && find theories user-contrib \\( -wholename 'theories/*.vo' -or -wholename 'theories/*.glob' -or -wholename 'theories/*.v' -or -wholename 'user-contrib/*.vo' -or -wholename 'user-contrib/*.v' -or -wholename 'user-contrib/*.glob' \\) -printf \"$COQW/%p:/static/coqlib/%p \")")))

; for coq-fs-core.js
; js_of_ocaml build-fs -o coq-fs-core.js $(find coq-core/ -wholename '*/plugins/*/*.cma' -or -wholename '*/META' -printf "%p:/lib/%p")
Expand Down