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. --- tools/fake_ide.ml | 16 ++-------------- 1 file changed, 2 insertions(+), 14 deletions(-) (limited to 'tools') diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index d48c6d0af..47bd2493f 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -297,19 +297,7 @@ let main = (Sys.Signal_handle (fun _ -> prerr_endline "Broken Pipe (coqtop died ?)"; exit 1)); let def_args = ["--xml_format=Ppcmds"; "-ideslave"] in - let coqtop_name = (* from ide/ideutils.ml *) - let prog_name = "fake_ide" in - let len_prog_name = String.length prog_name in - let fake_ide_path = Sys.executable_name in - let fake_ide_path_len = String.length fake_ide_path in - let pos = fake_ide_path_len - len_prog_name in - let rex = Str.regexp_string prog_name in - try - let i = Str.search_backward rex fake_ide_path pos in - String.sub fake_ide_path 0 i ^ "coqtop" ^ - String.sub fake_ide_path (i + len_prog_name) - (fake_ide_path_len - i - len_prog_name) - with Not_found -> assert false in + let idetop_name = System.get_toplevel_path "coqidetop" in let coqtop_args, input_file = match Sys.argv with | [| _; f |] -> Array.of_list def_args, f | [| _; f; ct |] -> @@ -318,7 +306,7 @@ let main = | _ -> usage () in let inc = if input_file = "-" then stdin else open_in input_file in let coq = - let _p, cin, cout = Coqide.spawn coqtop_name coqtop_args in + let _p, cin, cout = Coqide.spawn idetop_name coqtop_args in let ip = Xml_parser.make (Xml_parser.SChannel cin) in let op = Xml_printer.make (Xml_printer.TChannel cout) in Xml_parser.check_eof ip false; -- cgit v1.2.3