;
; Shims for running coq binaries with minimal dependencies
;

; coqtop

(alias
 (name coqtop-prelude)
 (deps
  %{bin:coqtop}
   ; XXX: bug, we are missing the dep on the _install meta file...
  %{project_root}/theories/Init/Prelude.vo))

(rule
 (targets coqtop)
 (deps (alias coqtop-prelude))
 (action
  (with-stdout-to %{targets}
   (progn
    (echo "#!/usr/bin/env bash\n")
    (bash "echo '\"$(dirname \"$0\")\"/%{bin:coqtop} -I \"$(dirname \"$0\")/%{workspace_root}/../install/default/lib\" -coqlib \"$(dirname \"$0\")/%{project_root}\" \"$@\"'")
    (run chmod +x %{targets})))))

; coqidetop

(alias
 (name coqidetop-prelude)
 (deps
  %{bin:coqidetop.opt}
   ; XXX: bug, we are missing the dep on the _install meta file...
  %{project_root}/theories/Init/Prelude.vo))

(rule
 (targets coqidetop.opt)
 (deps (alias coqidetop-prelude))
 (action
  (with-stdout-to %{targets}
   (progn
    (echo "#!/usr/bin/env bash\n")
    (bash "echo '\"$(dirname \"$0\")\"/%{bin:coqidetop.opt} -I \"$(dirname \"$0\")/%{workspace_root}/../install/default/lib\" -coqlib \"$(dirname \"$0\")/%{project_root}\" \"$@\"'")
    (run chmod +x %{targets})))))

; coqc

(alias
 (name coqc-prelude)
 (deps
  %{bin:coqc}
  %{bin:rocqworker}
  %{project_root}/theories/Init/Prelude.vo))

(rule
 (targets coqc)
 (deps (alias coqc-prelude))
 (action
  (with-stdout-to %{targets}
   (progn
    (echo "#!/usr/bin/env bash\n")
    (bash "echo '\"$(dirname \"$0\")\"/%{bin:coqc} -I \"$(dirname \"$0\")/%{workspace_root}/../install/default/lib\" -coqlib \"$(dirname \"$0\")\"/%{project_root} -nI \"$(dirname \"$0\")\"/%{project_root}/kernel/.kernel.objs/byte \"$@\"'")
    (run chmod +x %{targets})))))

; coqtop.byte

(alias
 (name coqtop.byte-prelude)
 (deps
  %{project_root}/theories/Init/Prelude.vo
  %{bin:coqtop.byte}
  %{lib:rocq-runtime.config:config.cma}
  %{lib:rocq-runtime.clib:clib.cma}
  %{lib:rocq-runtime.lib:lib.cma}
  %{lib:rocq-runtime.kernel:kernel.cma}
  %{lib:rocq-runtime.vm:coqrun.cma}
  %{lib:rocq-runtime.vm:../../stublibs/dllcoqrun_stubs.so}
  %{lib:rocq-runtime.library:library.cma}
  %{lib:rocq-runtime.engine:engine.cma}
  %{lib:rocq-runtime.pretyping:pretyping.cma}
  %{lib:rocq-runtime.gramlib:gramlib.cma}
  %{lib:rocq-runtime.interp:interp.cma}
  %{lib:rocq-runtime.proofs:proofs.cma}
  %{lib:rocq-runtime.parsing:parsing.cma}
  %{lib:rocq-runtime.printing:printing.cma}
  %{lib:rocq-runtime.tactics:tactics.cma}
  %{lib:rocq-runtime.vernac:vernac.cma}
  %{lib:rocq-runtime.stm:stm.cma}
  %{lib:rocq-runtime.sysinit:sysinit.cma}
  %{lib:rocq-runtime.toplevel:toplevel.cma}
  %{lib:rocq-runtime.plugins.number_string_notation:number_string_notation_plugin.cma}
  %{lib:rocq-runtime.plugins.tauto:tauto_plugin.cma}
  %{lib:rocq-runtime.plugins.cc:cc_plugin.cma}
  %{lib:rocq-runtime.plugins.firstorder:firstorder_plugin.cma}
  %{lib:rocq-runtime.plugins.ltac:ltac_plugin.cma}
  (alias %{project_root}/dev/ml_toplevel_files)))

(rule
 (targets coqtop.byte)
 (deps (alias coqtop.byte-prelude))
 (action
  (with-stdout-to %{targets}
   (progn
    (echo "#!/usr/bin/env bash\n")
    (bash "echo '\"$(dirname \"$0\")\"/%{bin:coqtop.byte} -I \"$(dirname \"$0\")/%{workspace_root}/../install/default/lib\" -coqlib \"$(dirname \"$0\")\"/%{project_root} \"$@\"'")
    (run chmod +x %{targets})))))

; rocqide

(alias
 (name rocqide-prelude)
 (deps
  ; without this if the gtk libs are not available dune can try to use
  ; rocqide from PATH instead of giving a nice error
  ; there is no problem with the other shims since they don't depend on optional build products
  %{project_root}/ide/rocqide/rocqide_main.exe
  %{bin:rocqworker}
  %{bin:coqidetop}
  %{project_root}/theories/Init/Prelude.vo
  %{project_root}/coqide-server.install
  %{project_root}/rocqide.install))

(rule
 (targets rocqide)
 (deps (alias rocqide-prelude))
 (action
  (with-stdout-to %{targets}
   (progn
    (echo "#!/usr/bin/env bash\n")
    (bash "echo '\"$(dirname \"$0\")\"/%{bin:rocqide} -I \"$(dirname \"$0\")/%{workspace_root}/../install/default/lib\" -coqlib \"$(dirname \"$0\")\"/%{project_root} \"$@\"'")
    (run chmod +x %{targets})))))