You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Currently, lake build will build all widget/*.tsx files and place them under build/js. This is great for getting demos running easily, but we also use the same build target to create the .tar.gz archives that are distributed to packages that import ProofWidgets. This means that JS code built only for demos, including bundled libraries from NPM, ends up bloating the size of the archive. As of today it is not too bad - just 7M - but it could become a concern as we add more demos that bundle in large libraries. We should better have a separate archive target which produces the JS needed for ProofWidgets.lean and nothing more. It would be even better if Lake could do this for us.
Perhaps instead of a separate target, it would be better to have an enable_demos Lake option.
The text was updated successfully, but these errors were encountered:
Currently,
lake build
will build allwidget/*.tsx
files and place them underbuild/js
. This is great for getting demos running easily, but we also use the same build target to create the.tar.gz
archives that are distributed to packages that import ProofWidgets. This means that JS code built only for demos, including bundled libraries from NPM, ends up bloating the size of the archive. As of today it is not too bad - just 7M - but it could become a concern as we add more demos that bundle in large libraries. We should better have a separatearchive
target which produces the JS needed forProofWidgets.lean
and nothing more. It would be even better if Lake could do this for us.Perhaps instead of a separate target, it would be better to have an
enable_demos
Lake option.The text was updated successfully, but these errors were encountered: