; The easiest way to generate a portable absolute path is to use OCaml
; itself to print it
(executable
 (name ocaml_pwd)
 (modules ocaml_pwd))

(rule
 (targets libpath.inc)
 (action (with-stdout-to %{targets} (run ./ocaml_pwd.exe -quoted ../../install/%{context_name}/lib/coq/ ))))

(rule
 (targets summary.log)
 (deps
   ; File that should be promoted.
   misc/universes/all_stdlib.v
   ; Dependencies of the legacy makefile
   ../Makefile.common
   ../config/Makefile
   ; Stuff for the compat script test
   ../dev/header.ml
   ../dev/tools/update-compat.py
   ../doc/stdlib/index-list.html.template
   ; For the misc/printers.sh test
   ../dev/incdir_dune
   ../dev/base_include
   ../dev/inc_ltac_dune
   ../dev/include_printers
   ../dev/include_dune
   ../dev/top_printers.ml
   ../dev/vm_printers.ml
   ; For the changelog test
   ../config/coq_config.py
   (source_tree doc/changelog)
   (package coq)
   ; For fake_ide
   (package coqide-server)
   (source_tree .))
   ; Finer-grained dependencies would look like this and be generated
   ; by coqdep; that would allow tests to be run incrementally.
   ; ../tools/CoqMakefile.in
   ; ../theories/Init/Prelude.vo
   ; %{bin:coqc}
   ; %{bin:coq_makefile}
   ; %{bin:fake_ide}
 (action
  (progn
   (bash "make -j %{env:NJOBS=2} BIN= COQLIB=%{read:libpath.inc} PRINT_LOGS=1 UNIT_TESTS=%{env:COQ_UNIT_TEST=unit-tests}"))))