sandboxing doesn't copy files in the install directory

[Alizter]

I have a rule which depends on some things in the install directory (bad practice I know) however when (sandbox always) is added it doesn't work because the install directory in the sandbox (which I get using --always-show-command-line) is completely empty but has the correct directory structure.

cc @rgrinberg

Here is what one sandbox looks like:

Sandbox

``` tree . ├── default │ ├── test-suite │ │ ├── debug │ │ │ ├── bug_1362.glob │ │ │ ├── bug_1362.v -> ../../../../../default/test-suite/debug/bug_1362.v │ │ │ └── bug_1362.v.log │ │ └── prerequisite │ │ ├── admit.vo -> ../../../../../default/test-suite/prerequisite/admit.vo │ │ ├── bind_univs.vo -> ../../../../../default/test-suite/prerequisite/bind_univs.vo │ │ ├── make_local.vo -> ../../../../../default/test-suite/prerequisite/make_local.vo │ │ ├── make_notation.vo -> ../../../../../default/test-suite/prerequisite/make_notation.vo │ │ ├── module_bug7192.vo -> ../../../../../default/test-suite/prerequisite/module_bug7192.vo │ │ ├── module_bug8416.vo -> ../../../../../default/test-suite/prerequisite/module_bug8416.vo │ │ ├── ssr_mini_mathcomp.vo -> ../../../../../default/test-suite/prerequisite/ssr_mini_mathcomp.vo │ │ └── ssr_ssrsyntax1.vo -> ../../../../../default/test-suite/prerequisite/ssr_ssrsyntax1.vo │ ├── theories │ │ ├── Init │ │ │ ├── Byte.vo -> ../../../../../default/theories/Init/Byte.vo │ │ │ ├── Datatypes.vo -> ../../../../../default/theories/Init/Datatypes.vo │ │ │ ├── Decimal.vo -> ../../../../../default/theories/Init/Decimal.vo │ │ │ ├── Hexadecimal.vo -> ../../../../../default/theories/Init/Hexadecimal.vo │ │ │ ├── Logic.vo -> ../../../../../default/theories/Init/Logic.vo │ │ │ ├── Ltac.vo -> ../../../../../default/theories/Init/Ltac.vo │ │ │ ├── Nat.vo -> ../../../../../default/theories/Init/Nat.vo │ │ │ ├── Notations.vo -> ../../../../../default/theories/Init/Notations.vo │ │ │ ├── Number.vo -> ../../../../../default/theories/Init/Number.vo │ │ │ ├── Peano.vo -> ../../../../../default/theories/Init/Peano.vo │ │ │ ├── Prelude.vo -> ../../../../../default/theories/Init/Prelude.vo │ │ │ ├── Specif.vo -> ../../../../../default/theories/Init/Specif.vo │ │ │ ├── Tactics.vo -> ../../../../../default/theories/Init/Tactics.vo │ │ │ ├── Tauto.vo -> ../../../../../default/theories/Init/Tauto.vo │ │ │ └── Wf.vo -> ../../../../../default/theories/Init/Wf.vo │ │ ├── micromega │ │ │ └── Lia.vo -> ../../../../../default/theories/micromega/Lia.vo │ │ └── ZArith │ │ └── ZArith.vo -> ../../../../../default/theories/ZArith/ZArith.vo │ └── user-contrib │ └── Ltac2 │ ├── Array.vo -> ../../../../../default/user-contrib/Ltac2/Array.vo │ ├── Bool.vo -> ../../../../../default/user-contrib/Ltac2/Bool.vo │ ├── Char.vo -> ../../../../../default/user-contrib/Ltac2/Char.vo │ ├── Constr.vo -> ../../../../../default/user-contrib/Ltac2/Constr.vo │ ├── Control.vo -> ../../../../../default/user-contrib/Ltac2/Control.vo │ ├── Env.vo -> ../../../../../default/user-contrib/Ltac2/Env.vo │ ├── Fresh.vo -> ../../../../../default/user-contrib/Ltac2/Fresh.vo │ ├── Ident.vo -> ../../../../../default/user-contrib/Ltac2/Ident.vo │ ├── Ind.vo -> ../../../../../default/user-contrib/Ltac2/Ind.vo │ ├── Init.vo -> ../../../../../default/user-contrib/Ltac2/Init.vo │ ├── Int.vo -> ../../../../../default/user-contrib/Ltac2/Int.vo │ ├── List.vo -> ../../../../../default/user-contrib/Ltac2/List.vo │ ├── Ltac1.vo -> ../../../../../default/user-contrib/Ltac2/Ltac1.vo │ ├── Ltac2.vo -> ../../../../../default/user-contrib/Ltac2/Ltac2.vo │ ├── Message.vo -> ../../../../../default/user-contrib/Ltac2/Message.vo │ ├── Notations.vo -> ../../../../../default/user-contrib/Ltac2/Notations.vo │ ├── Option.vo -> ../../../../../default/user-contrib/Ltac2/Option.vo │ ├── Pattern.vo -> ../../../../../default/user-contrib/Ltac2/Pattern.vo │ ├── Printf.vo -> ../../../../../default/user-contrib/Ltac2/Printf.vo │ ├── Std.vo -> ../../../../../default/user-contrib/Ltac2/Std.vo │ └── String.vo -> ../../../../../default/user-contrib/Ltac2/String.vo └── install └── default ├── bin ├── doc │ └── coq-core ├── lib │ ├── coq-core │ │ ├── boot │ │ ├── clib │ │ ├── config │ │ ├── engine │ │ ├── gramlib │ │ ├── interp │ │ ├── kernel │ │ ├── lib │ │ ├── library │ │ ├── parsing │ │ ├── plugins │ │ │ ├── btauto │ │ │ ├── cc │ │ │ ├── derive │ │ │ ├── extraction │ │ │ ├── firstorder │ │ │ ├── funind │ │ │ ├── ltac │ │ │ ├── ltac2 │ │ │ ├── micromega │ │ │ ├── nsatz │ │ │ ├── number_string_notation │ │ │ ├── ring │ │ │ ├── rtauto │ │ │ ├── ssreflect │ │ │ ├── ssrmatching │ │ │ ├── tauto │ │ │ ├── tutorial │ │ │ │ ├── p0 │ │ │ │ ├── p1 │ │ │ │ ├── p2 │ │ │ │ └── p3 │ │ │ └── zify │ │ ├── pretyping │ │ ├── printing │ │ ├── proofs │ │ ├── stm │ │ ├── sysinit │ │ ├── tactics │ │ ├── tools │ │ │ └── coqdoc │ │ ├── toplevel │ │ ├── top_printers │ │ ├── vernac │ │ └── vm │ └── stublibs ├── man │ └── man1 └── share └── texmf └── tex └── latex └── misc 70 directories, 49 files ```

This is the specific rule for reference:

Rule

``` (rule (alias runtest) (targets .bug_1362.aux bug_1362.vo bug_1362.glob bug_1362.v.log) (deps (alias csdp-cache) (sandbox always) (glob_files %{project_root}/test-suite/prerequisite/*.vo) (glob_files %{project_root}/theories/Init/*.vo) (glob_files %{project_root}/user-contrib/Ltac2/*.vo) (glob_files %{project_root}/../install/default/lib/coq-core/plugins/*/*) (package coq-core) ../debug/bug_1362.v .././../theories/ZArith/ZArith.vo .././../theories/micromega/Lia.vo) (action (setenv COQLIB %{project_root} (with-outputs-to bug_1362.v.log (run %{bin:coqc} -boot -I ../../../install/default/lib -R ../../theories Coq -R ../prerequisite TestSuite -Q ../../user-contrib/Ltac2 Ltac2 -bt bug_1362.v))))) ```

Obviously this works completely fine when sandboxing is not enabled.

[Alizter]

@rgrinberg I've created an example of this behaviour in https://github.com/ocaml/dune/pull/5717

[Alizter]

Had a discussion with @rgrinberg, and we could make depending on the install file an error and/or document this being unsupported behaviour.

[ejgallego]

That would break quite a few of scripts in the wild I bet; indeed, the issue of "runtime dependencies" is a tricky one and we may need to think about it.

Do you know how is (env (bin ...)) implemented?

[rgrinberg]

The binaries in (env (bin ..)) are accessible through PATH even with sandboxing.

[ejgallego]

@rgrinberg I mean, where does PATH point to, to a place inside _build/install ?

[Alizter]

@ejgallego It's not _build/install but rather _build/install/../.bin.

[ejgallego]

@ejgallego It's not _build/install but rather _build/install/../.bin.

Yes, thanks, I meant "inside _build/install" .

So indeed, if env is working that way, that's a dependency on _install, isn't it?

[Alizter]

@ejgallego Actually sorry what I wrote was in correct, the .bin folder is in _build/default not in install. So no dep on the install dir.

[ejgallego]

Aha! So it creates a .bin folder. So I guess we then need to do something similar for the runtime env for OCaml / findlib dynload.

[ejgallego]

And extend OCAMLPATH accordingly. In fact, it is then even questionable why install/bin and install/lib are added to the vars.

I still get the feeling that we need to handle runtime deps in a bit more principled way.

[Alizter]

I still get the feeling that we need to handle runtime deps in a bit more principled way.

Use dune action plugin in Coq to find the binary.

[ejgallego]

Use dune action plugin in Coq to find the binary.

Can you provide an example how you replace an (env (bin runtime dep with the dune action plugin?

[Alizter]

In coq, when we invoke the need to call a proof worker, we would instead call it through the dune action plugin. If it is available, then great it will run, if not then the DAP will try to build it, and if that isn't possible it will error.

[ejgallego]

How's that better than just making the worker a runtime dep of coqc ?

It seems quite a bit worse in the sense that DAP would require two calls to coqc, which can become very costly.

[Alizter]

How's that better than just making the worker a runtime dep of coqc ?

Because not every coqc invocation needs that binary around.

It seems quite a bit worse in the sense that DAP would require two calls to coqc, which can become very costly.

DAP isn't calling coqc, coqc is using DAP to compile / find the proof worker.

[ejgallego]

DAP isn't calling coqc, coqc is using DAP to compile / find the proof worker.

Dune is calling coqc, but it has to call it twice if using DAP.

[ejgallego]

How's that better than just making the worker a runtime dep of coqc ?

Because not every coqc invocation needs that binary around.

Indeed, that'd be an over approximation, but I think a harmless one, wouldn't it?

[Alizter]

DAP isn't calling coqc, coqc is using DAP to compile / find the proof worker.

Dune is calling coqc, but it has to call it twice if using DAP.

I think you are misunderstanding me. What I am proposing is that in coqc, when we need to call the worker binary, we do it through DAP. I.e. coqc is using the dune DAP API.

I am not proposing using the DAP in the coq rules in dune that would be pointless.

How's that better than just making the worker a runtime dep of coqc ?

Because not every coqc invocation needs that binary around.

Indeed, that'd be an over approximation, but I think a harmless one, wouldn't it?

What I am suggesting above would mean there is no over approximation and no overhead. We need it when we need it.

[ejgallego]

Yes, I understand what you mean, but are you sure dune doesn't call coqc twice? Moreover, DAP has to disable the cache?

[Alizter]

@ejgallego Can you explain how you think dune will call coqc twice? The way I see it:

• Call coqc
• Coqc needs proof worker, asks DAP for it, so either
  • DAP builds proof worker and lets coqc continue
  • DAP find proof worker and lets coqc continue
  • DAP cannot do either for build worker so fails

I don't see coqc being run twice.

[ejgallego]

Maybe I'm misunderstaind how DAP works, can you provide an example of the code to add in coqc?

[ejgallego]

I guess that only happens if you use stage, which we may need to do indeed.

I think using DAP is an interesting experiment, however it is also my impression that putting the whole of coqc in the DAP monad is not something that's gonna happen in the near future, and given than in our cases we know the dependencies without having to run coqc in an already very good way, a simpler solution for runtime dependencies is convenient.

I agree that ITPs are not just compiler, but greatly benefit from embedding a build system, and in fact Isabelle already does that since quite a long time to name an example.

[rgrinberg]

Just to clarify that the DAP monad is something that I plan to eliminate. It's something that you need today for the following reason: when you ask for dependencies with dap today, dune needs to rerun your binary. To rerun it from the point where it was left off, we need to stage the computation. Once we re-implement dap with dune's rpc, there will be no need to re-run any binaries. There will still be a monad that you will need to insantiate the dap api with, but that's only to allow for asynchronous IO for RPC. If you don't want to pollute the rest of the code with monads, you would be able to instantiate it with Id, and suffer from the synchronous IO (at least until OCaml 5.0 comes).

[Alizter]

Closing this as there is not much that we can do from the Dune side. _build/install locations are not supported for sandboxing (where everything should come from _build/defalt).