From 4d9014f25d27027164971d0254b3f40d97bd03ef Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 29 Sep 2024 22:01:20 +0200 Subject: [PATCH 1/2] [ci] [worker] Make the build flexible for non-vendored setups. --- Makefile | 21 ++++++++++++++------- controller-js/dune | 2 +- 2 files changed, 15 insertions(+), 8 deletions(-) diff --git a/Makefile b/Makefile index aadf72e4..00cceaa6 100644 --- a/Makefile +++ b/Makefile @@ -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 ") \ @@ -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 diff --git a/controller-js/dune b/controller-js/dune index 123b03de..845c86a8 100644 --- a/controller-js/dune +++ b/controller-js/dune @@ -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") From 7e50a215dcebed90d5973d14a2f2d1857df67843 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 29 Sep 2024 22:05:34 +0200 Subject: [PATCH 2/2] [makefile] [worker] Unset VENDORED_SETUP for CI build --- Makefile | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 9fc645ac..1f0e683b 100644 --- a/Makefile +++ b/Makefile @@ -154,7 +154,8 @@ patch-for-js: _LIBROOT=$(shell opam var lib) # At some point this may be the better idea -VENDORED_SETUP:=true +# Not true in this branch +# VENDORED_SETUP:=true ifdef VENDORED_SETUP _CCROOT=_build/install/default/lib/coq-core