diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/doc/build-system.dune.md | 4 | ||||
| -rw-r--r-- | dev/shim/dune | 13 |
2 files changed, 15 insertions, 2 deletions
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index a31ab1c511..b1bfac8cc9 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -126,9 +126,9 @@ script again] This will be fixed in the future. ## Dropping from coqtop: -The following sequence is recommended: +After doing `make -f Makefile.dune voboot`, the following commands should work: ``` -dune exec coqtop.byte +dune exec dev/shim/coqbyte-prelude > Drop. # #directory "dev";; # #use "include_dune";; diff --git a/dev/shim/dune b/dev/shim/dune index 85a0d205da..39b4ef492c 100644 --- a/dev/shim/dune +++ b/dev/shim/dune @@ -11,6 +11,19 @@ (run chmod +x %{targets}))))) (rule + (targets coqbyte-prelude) + (deps + %{bin:coqtop.byte} + %{lib:coq.kernel:../../stublibs/dllbyterun_stubs.so} + %{project_root}/theories/Init/Prelude.vo) + (action + (with-outputs-to %{targets} + (progn + (echo "#!/usr/bin/env bash\n") + (bash "echo \"$(pwd)/%{bin:coqtop.byte} -coqlib $(pwd)/%{project_root}\" \"$@\"") + (run chmod +x %{targets}))))) + +(rule (targets coqide-prelude) (deps %{bin:coqqueryworker.opt} |