aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile.build19
-rw-r--r--Makefile.common5
-rw-r--r--idetop/coqidetop.mllib1
-rw-r--r--idetop/ide_slave.ml (renamed from toplevel/ide_slave.ml)7
-rw-r--r--stm/stmworkertop.ml (renamed from toplevel/ide_slave.mli)12
-rw-r--r--stm/stmworkertop.mllib1
-rw-r--r--toplevel/coqinit.ml4
-rw-r--r--toplevel/coqtop.ml56
-rw-r--r--toplevel/coqtop.mli6
-rw-r--r--toplevel/mltop.ml5
-rw-r--r--toplevel/mltop.mli1
-rw-r--r--toplevel/toplevel.mllib1
12 files changed, 75 insertions, 43 deletions
diff --git a/Makefile.build b/Makefile.build
index 6d12063ca..0f05dc606 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -210,7 +210,7 @@ miniopt: $(COQTOPEXE) pluginsopt
minibyte: $(COQTOPBYTE) pluginsbyte
ifeq ($(BEST),opt)
-$(COQTOPEXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN)
+$(COQTOPEXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs)
$(SHOW)'COQMKTOP -o $@'
$(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) -thread -o $@
$(STRIP) $@
@@ -219,7 +219,7 @@ $(COQTOPEXE): $(COQTOPBYTE)
cp $< $@
endif
-$(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN)
+$(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA)
$(SHOW)'COQMKTOP -o $@'
$(HIDE)$(COQMKTOP) -boot -top $(BYTEFLAGS) -thread -o $@
@@ -301,8 +301,8 @@ IDEFILES=$(wildcard ide/coq*.lang) ide/coq_style.xml ide/coq.png ide/mac_default
coqide-binaries: coqide-$(HASCOQIDE)
coqide-no:
-coqide-byte: $(COQIDEBYTE) $(COQIDE)
-coqide-opt: $(COQIDEBYTE) $(COQIDE)
+coqide-byte: $(COQIDEBYTE) $(COQIDE) $(IDETOPLOOPCMA)
+coqide-opt: $(COQIDEBYTE) $(COQIDE) $(IDETOPLOOPCMA) $(IDETOPLOOPCMA:.cma=.cmxs)
coqide-files: $(IDEFILES)
ifeq ($(HASCOQIDE),opt)
@@ -334,6 +334,11 @@ endif
install-ide-bin:
$(MKDIR) $(FULLBINDIR)
$(INSTALLBIN) $(COQIDE) $(FULLBINDIR)
+ $(MKDIR) $(FULLCOQLIB)/toploop
+ $(INSTALLBIN) $(IDETOPLOOPCMA) $(FULLCOQLIB)/toploop/
+ifeq ($(BEST),opt)
+ $(INSTALLBIN) $(IDETOPLOOPCMA:.cma=.cmxs) $(FULLCOQLIB)/toploop/
+endif
install-ide-devfiles:
$(MKDIR) $(FULLCOQLIB)
@@ -618,6 +623,12 @@ install-coqlight: install-binaries install-library-light
install-binaries: install-tools
$(MKDIR) $(FULLBINDIR)
$(INSTALLBIN) $(COQC) $(COQTOPBYTE) $(COQTOPEXE) $(CHICKEN) $(FULLBINDIR)
+ $(MKDIR) $(FULLCOQLIB)/toploop
+ $(INSTALLBIN) $(TOPLOOPCMA) $(FULLCOQLIB)/toploop/
+ifeq ($(BEST),opt)
+ $(INSTALLBIN) $(TOPLOOPCMA:.cma=.cmxs) $(FULLCOQLIB)/toploop/
+endif
+
install-tools:
$(MKDIR) $(FULLBINDIR)
diff --git a/Makefile.common b/Makefile.common
index d971e9b2e..4b6cc764a 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -72,7 +72,7 @@ PLUGINS:=\
SRCDIRS:=\
$(CORESRCDIRS) \
- tools tools/coqdoc \
+ tools tools/coqdoc idetop\
$(addprefix plugins/, $(PLUGINS))
IDESRCDIRS:=\
@@ -159,6 +159,8 @@ CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \
parsing/parsing.cma printing/printing.cma tactics/tactics.cma \
stm/stm.cma toplevel/toplevel.cma parsing/highparsing.cma tactics/hightactics.cma
+TOPLOOPCMA:=stm/stmworkertop.cma
+
GRAMMARCMA:=tools/compat5.cmo grammar/grammar.cma
OMEGACMA:=plugins/omega/omega_plugin.cma
@@ -212,6 +214,7 @@ LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa)
IDEDEPS:=lib/clib.cma lib/xml_lexer.cmo lib/xml_parser.cmo lib/xml_printer.cmo lib/errors.cmo lib/spawn.cmo
IDECMA:=ide/ide.cma
+IDETOPLOOPCMA=idetop/coqidetop.cma
LINKIDE:=$(IDEDEPS) $(IDECMA) ide/coqide_main.ml
LINKIDEOPT:=$(IDEOPTDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide_main.ml
diff --git a/idetop/coqidetop.mllib b/idetop/coqidetop.mllib
new file mode 100644
index 000000000..782687744
--- /dev/null
+++ b/idetop/coqidetop.mllib
@@ -0,0 +1 @@
+Ide_slave
diff --git a/toplevel/ide_slave.ml b/idetop/ide_slave.ml
index 8f2fa69a0..2185084a0 100644
--- a/toplevel/ide_slave.ml
+++ b/idetop/ide_slave.ml
@@ -444,3 +444,10 @@ let loop () =
done;
pr_debug "Exiting gracefully.";
exit 0
+
+let () = Coqtop.toploop_init := (fun args ->
+ Flags.make_silent true;
+ init_stdout ();
+ args)
+
+let () = Coqtop.toploop_run := loop
diff --git a/toplevel/ide_slave.mli b/stm/stmworkertop.ml
index fb927cf33..50afd97ab 100644
--- a/toplevel/ide_slave.mli
+++ b/stm/stmworkertop.ml
@@ -6,12 +6,10 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(** [Ide_slave] : an implementation of [Ide_intf], i.e. mainly an interp
- function and a rewind function. This specialized loop is triggered
- when the -ideslave option is passed to Coqtop. Currently CoqIDE is
- the only one using this mode, but we try here to be as generic as
- possible, so this may change in the future... *)
+let () = Coqtop.toploop_init := (fun args ->
+ Flags.make_silent true;
+ Stm.slave_init_stdout ();
+ args)
-val init_stdout : unit -> unit
+let () = Coqtop.toploop_run := Stm.slave_main_loop
-val loop : unit -> unit
diff --git a/stm/stmworkertop.mllib b/stm/stmworkertop.mllib
new file mode 100644
index 000000000..78b54b2ea
--- /dev/null
+++ b/stm/stmworkertop.mllib
@@ -0,0 +1 @@
+Stmworkertop
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 85a59c50e..45aa980b7 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -92,6 +92,10 @@ let init_load_path () =
(* NOTE: These directories are searched from last to first *)
(* first, developer specific directory to open *)
if Coq_config.local then coq_add_path (coqlib/"dev") "dev";
+ (* main loops *)
+ Mltop.add_ml_dir (coqlib/"toploop");
+ if Coq_config.local then Mltop.add_ml_dir (coqlib/"stm");
+ if Coq_config.local then Mltop.add_ml_dir (coqlib/"idetop");
(* then standard library *)
add_stdlib_path ~unix_path:(coqlib/"theories") ~coq_root ~with_ml:false;
(* then plugins *)
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index a4770b348..0523ffd44 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -38,6 +38,20 @@ let print_header () =
ppnl (str ("Welcome to Coq "^ver^" ("^rev^")"));
pp_flush ()
+let warning s = msg_warning (strbrk s)
+
+let toploop = ref None
+let toploop_init = ref (fun x -> x)
+let toploop_run = ref (fun () ->
+ if Dumpglob.dump () then begin
+ if_verbose warning "Dumpglob cannot be used in interactive mode.";
+ Dumpglob.noglob ()
+ end;
+ Coqloop.loop();
+ (* Initialise and launch the Ocaml toplevel *)
+ Coqinit.init_ocaml_path();
+ Mltop.ocaml_toploop())
+
let output_context = ref false
let memory_stat = ref false
@@ -201,8 +215,6 @@ let error_missing_arg s =
prerr_endline "See --help for the syntax of supported options";
exit 1
-let warning s = msg_warning (strbrk s)
-
let filter_opts = ref false
let exitcode () = if !filter_opts then 2 else 0
@@ -217,6 +229,7 @@ let get_async_proofs_mode opt next = function
| "on" -> Flags.APonParallel 0
| "worker" ->
let n = int_of_string (next()) in assert (n > 0);
+ toploop := Some "stmworkertop";
Flags.APonParallel n
| "lazy" -> Flags.APonLazy
| _ -> prerr_endline ("Error: on/off/lazy/worker expected after "^opt); exit 1
@@ -341,7 +354,7 @@ let parse_args arglist =
|"-async-proofs-j" ->
Flags.async_proofs_n_workers := (get_int opt (next ()))
|"-async-proofs-worker-flags" ->
- Flags.async_proofs_worker_flags := Some (next ())
+ Flags.async_proofs_worker_flags := Some (next ());
|"-compat" -> Flags.compat_version := get_compat_version (next ())
|"-compile" -> add_compile false (next ())
|"-compile-verbose" -> add_compile true (next ())
@@ -363,6 +376,7 @@ let parse_args arglist =
|"-main-channel" -> Spawned.main_channel := get_host_port opt (next())
|"-control-channel" -> Spawned.control_channel := get_host_port opt (next())
|"-vi2vo" -> add_compile false (next ()); Flags.compilation_mode := Vi2Vo
+ |"-toploop" -> toploop := Some (next ())
(* Options with zero arg *)
|"-batch" -> set_batch_mode ()
@@ -377,7 +391,7 @@ let parse_args arglist =
|"-h"|"-H"|"-?"|"-help"|"--help" -> usage ()
|"--help-XML-protocol" ->
Serialize.document Xml_printer.to_string_fmt; exit 0
- |"-ideslave" -> Flags.ide_slave := true
+ |"-ideslave" -> toploop := Some "coqidetop"; Flags.ide_slave := true
|"-impredicative-set" -> set_engagement Declarations.ImpredicativeSet
|"-indices-matter" -> Indtypes.enforce_indices_matter ()
|"-just-parsing" -> Vernac.just_parsing := true
@@ -436,27 +450,22 @@ let init arglist =
begin
try
let extras = parse_args arglist in
- if not (List.is_empty extras) && not !filter_opts then begin
- prerr_endline ("Don't know what to do with " ^ String.concat " " extras);
- prerr_endline "See --help for the list of supported options";
- exit 1
- end;
(* If we have been spawned by the Spawn module, this has to be done
* early since the master waits us to connect back *)
Spawned.init_channels ();
Envars.set_coqlib Errors.error;
- if !print_where then (print_endline (Envars.coqlib ()); exit (exitcode ()));
+ if !print_where then (print_endline(Envars.coqlib ()); exit(exitcode ()));
if !print_config then (Usage.print_config (); exit (exitcode ()));
if !filter_opts then (print_string (String.concat "\n" extras); exit 0);
- if !Flags.ide_slave then begin
- Flags.make_silent true;
- Ide_slave.init_stdout ()
- end else if Flags.async_proofs_is_worker () then begin
- Flags.make_silent true;
- Stm.slave_init_stdout ()
+ init_load_path ();
+ Option.iter Mltop.load_ml_object_raw !toploop;
+ let extras = !toploop_init extras in
+ if not (List.is_empty extras) then begin
+ prerr_endline ("Don't know what to do with "^String.concat " " extras);
+ prerr_endline "See --help for the list of supported options";
+ exit 1
end;
if_verbose print_header ();
- init_load_path ();
inputstate ();
Mltop.init_known_plugins ();
set_vm_opt ();
@@ -500,18 +509,7 @@ let start () =
let () = init_toplevel (List.tl (Array.to_list Sys.argv)) in
(* In batch mode, Coqtop has already exited at this point. In interactive one,
dump glob is nothing but garbage ... *)
- if !Flags.ide_slave then
- Ide_slave.loop ()
- else if Flags.async_proofs_is_worker () then
- Stm.slave_main_loop ()
- else
- let () = if Dumpglob.dump () then
- let () = if_verbose warning "Dumpglob cannot be used in interactive mode." in
- Dumpglob.noglob () in
- Coqloop.loop();
- (* Initialise and launch the Ocaml toplevel *)
- Coqinit.init_ocaml_path();
- Mltop.ocaml_toploop();
+ !toploop_run ();
exit 1
(* [Coqtop.start] will be called by the code produced by coqmktop *)
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index ee511edbb..875cf2ec0 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -14,3 +14,9 @@
val init_toplevel : string list -> unit
val start : unit -> unit
+
+
+(* For other toploops *)
+val toploop_init : (string list -> string list) ref
+val toploop_run : (unit -> unit) ref
+
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index 11f00d6e5..695fd3b82 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -211,7 +211,8 @@ let file_of_name name =
let suffix = get_ml_object_suffix name in
let fail s =
errorlabstrm "Mltop.load_object"
- (str"File not found on loadpath : " ++ str s) in
+ (str"File not found on loadpath : " ++ str s ++ str"\n" ++
+ str"Loadpath: " ++ str(String.concat ":" !coq_mlpath_copy)) in
if is_native then
let name = match suffix with
| Some ((".cmo"|".cma") as suffix) ->
@@ -290,6 +291,8 @@ let load_ml_object mname fname=
add_known_module mname;
init_ml_object mname
+let load_ml_object_raw fname = dir_ml_load (file_of_name fname)
+
(* Summary of declared ML Modules *)
(* List and not String.Set because order is important: most recent first. *)
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli
index 196c0bf94..a4ba732d2 100644
--- a/toplevel/mltop.mli
+++ b/toplevel/mltop.mli
@@ -54,6 +54,7 @@ val add_rec_path : unix_path:string -> coq_root:Names.DirPath.t -> implicit:bool
val add_known_module : string -> unit
val module_is_known : string -> bool
val load_ml_object : string -> string -> unit
+val load_ml_object_raw : string -> unit
(** {5 Initialization functions} *)
diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib
index a5519d586..d22524e5c 100644
--- a/toplevel/toplevel.mllib
+++ b/toplevel/toplevel.mllib
@@ -15,7 +15,6 @@ Mltop
Vernacentries
Whelp
Vernac
-Ide_slave
Usage
Coqloop
Coqinit
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 20:07:58 +0000