feat: bind /tmp/ as a tmpfs for bv_decide to create temp files

[bollu]

Since bv_decide uses temporary files to communicate with cadical, we bind /tmp as a read-write mount. This allows bv_decide to be successfully used in a hosted instance of lean4web: Link here.

The line of code that perform this is:

-- https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean#L167-L168
Frontend/BVDecide.lean
167:    IO.FS.withTempFile fun _ lratFile => do
168:      let cfg ← BVDecide.Frontend.TacticContext.new lratFile

CC @hargoniX

[joneugster]

Oh I thought I've answered a while ago:

I'm not sure adding more --bind by default is a good idea. Especially since this gives any user the write-permission to write arbitrary files onto the server, which I don't know if that imposes a potential security risk.

Could we just explain this setup in the documentation (README or a MD file in docs/) or maybe implement this in a configurable way so that --bind is not used by default?

[hargoniX]

You do not need to setup this bind to allow access to /tmp. Lean's temp file mechanism does respect the TMPDIR environment variable: https://github.com/leanprover/lean4/blob/b87562719814447e77c17ff03492f7c11573f475/src/runtime/io.cpp#L847 so it is entirely possible to give it its own /tmp directory to play with.

[bollu]

@joneugster We switch to using --tmpfs, which creates a temporary file system for /tmp that's not visible to the host machine at all. This offers isolation from the lean server that's running inside bubblewrap to the lean host machine.

This should be setup by default, now that bv_decide and cadical are being shipped as part of Lean core.