From 58682be3e6302845d2e3be583c6368510034d767 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 7 Dec 2019 11:20:09 +0100 Subject: Fixes #11254 (not requiring coqlib to be set to report about coqtop version). --- .../08-tools/11255-master+fix11254-coqtop-version.rst | 4 ++++ toplevel/coqtop.ml | 18 +++++++++++------- 2 files changed, 15 insertions(+), 7 deletions(-) create mode 100644 doc/changelog/08-tools/11255-master+fix11254-coqtop-version.rst diff --git a/doc/changelog/08-tools/11255-master+fix11254-coqtop-version.rst b/doc/changelog/08-tools/11255-master+fix11254-coqtop-version.rst new file mode 100644 index 0000000000..ecc134748d --- /dev/null +++ b/doc/changelog/08-tools/11255-master+fix11254-coqtop-version.rst @@ -0,0 +1,4 @@ +- **Fixed:** + ``coqtop --version`` was broken when called in the middle of an installation process + (`#11255 `_, by Hugo Herbelin, fixing + `#11254 `_). diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 309f5b657a..46dd693155 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -155,12 +155,20 @@ let print_style_tags opts = let () = List.iter iter tags in flush_all () +let init_setup = function + | None -> Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg)); + | Some s -> Envars.set_user_coqlib s + let print_query opts = function | PrintVersion -> Usage.version () | PrintMachineReadableVersion -> Usage.machine_readable_version () - | PrintWhere -> print_endline (Envars.coqlib ()) + | PrintWhere -> + let () = init_setup opts.config.coqlib in + print_endline (Envars.coqlib ()) | PrintHelp h -> Usage.print_usage stderr h - | PrintConfig -> Envars.print_config stdout Coq_config.all_src_dirs + | PrintConfig -> + let () = init_setup opts.config.coqlib in + Envars.print_config stdout Coq_config.all_src_dirs | PrintTags -> print_style_tags opts.config (** GC tweaking *) @@ -188,10 +196,6 @@ let init_gc () = Gc.minor_heap_size = 33554432; (* 4M *) Gc.space_overhead = 120} -let init_setup = function - | None -> Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg)); - | Some s -> Envars.set_user_coqlib s - let init_process () = (* Coq's init process, phase 1: OCaml parameters, basic structures, and IO @@ -256,11 +260,11 @@ type ('a,'b) custom_toplevel = let init_toplevel custom = let () = init_process () in let opts, customopts = init_parse custom.parse_extra custom.help custom.opts in - let () = init_setup opts.config.coqlib in (* Querying or running? *) match opts.main with | Queries q -> List.iter (print_query opts) q; exit 0 | Run -> + let () = init_setup opts.config.coqlib in let customstate = init_execution opts (custom.init customopts) in opts, customopts, customstate -- cgit v1.2.3