From 382ee49700c4b4ee78ba95b2e86866ebd3b35d74 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 7 Mar 2018 01:33:17 +0100
Subject: [stm] Make toplevels standalone executables.

We turn coqtop "plugins" into standalone executables, which will be
installed in `COQBIN` and located using the standard `PATH`
mechanism. Using dynamic linking for `coqtop` customization didn't
make a lot of sense, given that only one of such "plugins" could be
loaded at a time. This cleans up some code and solves two problems:

- `coqtop` needing to locate plugins,
- dependency issues as plugins in `stm` depended on files in `toplevel`.

In order to implement this, we do some minor cleanup of the toplevel
API, making it functional, and implement uniform build rules. In
particular:

- `stm` and `toplevel` have become library-only directories,
- a new directory, `topbin`, contains the new executables,
- 4 new binaries have been introduced, for coqide and the stm.
- we provide a common and cleaned up way to locate toplevels.
---
 dev/base_include                                |  2 +-
 dev/ci/ci-pidetop.sh                            | 15 +++++++++++++--
 dev/ci/user-overlays/06859-ejgallego-stm+top.sh |  6 ++++++
 3 files changed, 20 insertions(+), 3 deletions(-)
 create mode 100644 dev/ci/user-overlays/06859-ejgallego-stm+top.sh

(limited to 'dev')

diff --git a/dev/base_include b/dev/base_include
index 2f7183dd63..2f5d8aa843 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -231,7 +231,7 @@ let _ = Flags.in_toplevel := true
 let _ = Constrextern.set_extern_reference
   (fun ?loc _ r -> CAst.make ?loc @@ Libnames.Qualid (Nametab.shortest_qualid_of_global Id.Set.empty r));;
 
-let go () = Coqloop.loop ~state:Option.(get !Coqloop.drop_last_doc)
+let go () = Coqloop.(loop ~opts:Option.(get !drop_args) ~state:Option.(get !drop_last_doc))
 
 let _ =
  print_string
diff --git a/dev/ci/ci-pidetop.sh b/dev/ci/ci-pidetop.sh
index d04b9637c0..2ac4d21671 100755
--- a/dev/ci/ci-pidetop.sh
+++ b/dev/ci/ci-pidetop.sh
@@ -8,6 +8,17 @@ pidetop_CI_DIR="${CI_BUILD_DIR}/pidetop"
 
 git_checkout "${pidetop_CI_BRANCH}" "${pidetop_CI_GITURL}" "${pidetop_CI_DIR}"
 
-( cd "${pidetop_CI_DIR}" && coq_makefile -f Make -o Makefile.top && make -f Makefile.top "-j${NJOBS}" && make install-toploop -f Makefile.top )
+# Travis / Gitlab have different filesystem layout due to use of
+# `-local`. We need to improve this divergence but if we use Dune this
+# "local" oddity goes away automatically so not bothering...
+if [ -d "$COQBIN/../lib/coq" ]; then
+   COQOCAMLLIB="$COQBIN/../lib/"
+   COQLIB="$COQBIN/../lib/coq/"
+else
+   COQOCAMLLIB="$COQBIN/../"
+   COQLIB="$COQBIN/../"
+fi
 
-echo -en '4\nexit' | coqtop -main-channel stdfds -toploop pidetop
+( cd "${pidetop_CI_DIR}" && OCAMLPATH="$COQOCAMLLIB" jbuilder build @install )
+
+echo -en '4\nexit' | "$pidetop_CI_DIR/_build/install/default/bin/pidetop" -coqlib "$COQLIB" -main-channel stdfds
diff --git a/dev/ci/user-overlays/06859-ejgallego-stm+top.sh b/dev/ci/user-overlays/06859-ejgallego-stm+top.sh
new file mode 100644
index 0000000000..ca0076b468
--- /dev/null
+++ b/dev/ci/user-overlays/06859-ejgallego-stm+top.sh
@@ -0,0 +1,6 @@
+#!/bin/sh
+
+if [ "$CI_PULL_REQUEST" = "6859" ] || [ "$CI_BRANCH" = "stm+top" ] || [ "$CI_BRANCH" = "pr-6859" ]; then
+    pidetop_CI_BRANCH=stm+top
+    pidetop_CI_GITURL=https://bitbucket.org/ejgallego/pidetop.git
+fi
-- 
cgit v1.2.3