Skip to content

Latest commit

 

History

History
33 lines (19 loc) · 1.19 KB

builder-options.md

File metadata and controls

33 lines (19 loc) · 1.19 KB
Raw

Other ways to run the dev container

Just serve it, not constantly recompiling

  • Run scripts/builder --compile --serve

(Not) Rebuilding the dev container

If you pull a commit with a Dockerfile update, and then restart your scripts/builder script -- it will rebuild as much of the container as possible.

If you don't want to rebuild the container, use NEVER_REBUILD_DOCKER=1 scripts/builder ... to make the the build script use the last built one.

In another shell you can now kick off a scripts/builder --compile to rebuild the container in parallel with your currently working one.

You can use export CURRENTLY_REBUILDING_DOCKER=1 to make your run-in-docker invocations, including say ocamlmerlin, use the old+running container as opposed to attempting to use the container that has an in progress build.

Preserving battery life

The're a poll during building that is a great drain on battery life. To reduce the frequency of the poll, run script/builder using POLL_FREQUENCY, which is the number of times per second to check.

  • POLL_FREQUENCY=0.1 scripts/builder --etc

You can also disable the polling (and consequently the building):

  • scripts/builder --compile --serve