From 2bf243b9c345fdc96d7836d75ad997d857b43719 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 24 Feb 2023 00:24:42 +0100 Subject: [PATCH] wip --- coq/workspace.ml | 24 +++++++++++++++++++++--- 1 file changed, 21 insertions(+), 3 deletions(-) diff --git a/coq/workspace.ml b/coq/workspace.ml index ffa96e2fb..32011228b 100644 --- a/coq/workspace.ml +++ b/coq/workspace.ml @@ -158,6 +158,11 @@ let pp_load_path fmt Format.fprintf fmt "Path %s ---> %s" (Names.DirPath.to_string coq_path) unix_path +let pp_as fmt (d, dl) = Format.fprintf fmt "(%s, %a)" + d Format.(pp_print_list pp_print_string) dl + +let pp_ap fmt (dl, d) = Format.fprintf fmt "(%a, %s)" + Format.(pp_print_list pp_print_string) dl d let describe { coqlib; kind; vo_load_path; ml_include_path; require_libs; _ } = let require_msg = @@ -172,14 +177,27 @@ let describe { coqlib; kind; vo_load_path; ml_include_path; require_libs; _ } = Format.(pp_print_list pp_print_string) ml_include_path in - ( Format.asprintf + let base = + Format.asprintf "@[Configuration loaded from %s@\n\ \ - coqlib is at: %s@\n\ \ - Modules [%s] will be loaded by default@\n\ \ - %d Coq path directory bindings in scope; %d Coq plugin directory \ bindings in scope@]" - kind coqlib require_msg n_vo n_ml - , extra ) + kind coqlib require_msg n_vo n_ml in + let c11 = System.all_subdirs ~unix_path:coqlib in + let c12 = System.all_subdirs ~unix_path:(Filename.concat coqlib "..") in + let c13 = System.all_subdirs ~unix_path:(Filename.(concat (concat coqlib "..") "..")) in + let c2 = Sys.readdir coqlib in + let c3 = System.all_in_path c11 "Prelude.vo" in + let base = Format.asprintf "l1:%a@\nl2:%a@\nl3:%a@\n%a@\n%a@\n@\n%s" + Format.(pp_print_list pp_as) c11 + Format.(pp_print_list pp_as) c12 + Format.(pp_print_list pp_as) c13 + Format.(pp_print_list pp_print_string) (Array.to_list c2) + Format.(pp_print_list pp_ap) c3 + base in + ( base, extra ) (* Require a set of libraries *) let load_objs libs =