Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288(************************************************************************)(* * The Rocq Prover / The Rocq Development Team *)(* v * Copyright INRIA, CNRS and contributors *)(* <O___,, * (see version control and CREDITS file for authors & dates) *)(* \VV/ **************************************************************)(* // * This file is distributed under the terms of the *)(* * GNU Lesser General Public License Version 2.1 *)(* * (see LICENSE file for the text of the license) *)(************************************************************************)
module Path = struct
type t = string
let relative = Filename.concat let to_string x = x let exists x = Sys.file_exists x
end
(* For now just a pointer to coq/lib (for .vo) and rocq-runtime/lib (for plugins) *)type t = { runtimelib: Path.t ; coqlib : Path.t }
(* This code needs to be refactored, for now it is just what used to be in envvars *)
let use_suffix prefix suffix = if Filename.is_relative suffix then Filename.concat prefix suffix else suffix
let canonical_path_name p = let current = Sys.getcwd () in try Sys.chdir p; let p' = Sys.getcwd () in Sys.chdir current; p' with Sys_error _ -> (* We give up to find a canonical name and just simplify it... *) Filename.concat current p
let theories_dir = "theories"let plugins_dir = "plugins"let prelude = Filename.concat theories_dir "Init/Prelude.vo"
let find_in_PATH f = match Sys.getenv_opt "PATH" with | None -> None | Some paths -> let sep = if Coq_config.arch_is_win32 then ';' else ':' in let paths = String.split_on_char sep paths in paths |> List.find_opt (fun path -> Sys.file_exists (if path = "" then f else Filename.concat path f))
let rocqbin = (* avoid following symlinks if possible (Sys.executable_name followed symlinks) *) if Filename.basename Sys.argv.(0) <> Sys.argv.(0) then (* explicit directory (maybe relative to current dir) *) canonical_path_name (Filename.dirname Sys.argv.(0)) else match find_in_PATH Sys.argv.(0) with | Some p -> p | None -> canonical_path_name (Filename.dirname Sys.executable_name)
(** Locate the dune workspace root containing the given path, if any. *)let dune_workspace_root : string -> string option = fun path -> let rec workspace_root path = let parent = Filename.dirname path in if parent = path then None else if Filename.basename path = "_build" then Some parent else workspace_root parent in match workspace_root path with | None -> None | Some root -> (* Check that this indeed looks like a dune workspace. *) let ok = let has file = Sys.file_exists (Filename.concat root file) in List.exists has ["dune-project"; "dune-workspace"] in if ok then Some root else None
(** The following only makes sense when executables are running from source tree (e.g. during build or in local mode). *)let rocqroot = match dune_workspace_root rocqbin with | Some dir -> let dir = Filename.concat dir "_build" in let dir = Filename.concat dir "install" in Filename.concat dir "default" | None -> let rec search = function | [] -> (* couldn't recognize the layout, guess the executable is 1 dir below the root (eg "mybin/rocq") XXX we should search only when we need the root and produce an error if we can't find it *) Filename.dirname rocqbin | path :: rest -> if Sys.file_exists (Filename.concat path "bin") then path else search rest in (* we can be "bin/rocq" or "lib/rocq-runtime/rocqworker" so rocqbin can be "bin/" or "lib/rocq-runtime/" *) let dirname = Filename.dirname in search [ dirname rocqbin; dirname @@ dirname rocqbin ]
let relocate = function | Coq_config.NotRelocatable p -> p | Coq_config.Relocatable p -> Filename.concat rocqroot p
(** [check_file_else ~dir ~file oth] checks if [file] exists in the installation directory [dir] given relatively to [coqroot], which maybe has been relocated. If the check fails, then [oth ()] is evaluated. Using file system equality seems well enough for this heuristic *)let check_file_else ~dir ~file oth = let path = use_suffix rocqroot dir in if Sys.file_exists (Filename.concat path file) then path else oth ()
let guess_coqlib () = match Util.getenv_rocq "LIB" with | Some v -> v | None -> check_file_else ~dir:Coq_config.coqlibsuffix ~file:prelude (fun () -> relocate Coq_config.coqlib)
(* Build layout uses coqlib = coqcorelib XXX we should be using -boot in build layout so is that dead code? *)let guess_coqcorelib lib = match Util.getenv_rocq_gen ~rocq:"ROCQRUNTIMELIB" ~coq:"COQCORELIB" with | Some v -> v | None -> if Sys.file_exists (Path.relative lib plugins_dir) then lib else Path.relative lib "../rocq-runtime"
let fail_lib lib = let open Printf in eprintf "File not found: %s\n" lib; eprintf "The path for Rocq libraries is wrong.\n"; eprintf "Rocq prelude is shipped in the rocq-core package.\n"; eprintf "Please check the ROCQLIB env variable or the -coqlib option.\n"; exit 1
let fail_core plugin = let open Printf in eprintf "File not found: %s\n" plugin; eprintf "The path for Rocq plugins is wrong.\n"; eprintf "Rocq plugins are shipped in the rocq-runtime package.\n"; eprintf "Please check the ROCQRUNTIMELIB env variable.\n"; exit 1
let validate_env ({ runtimelib; coqlib } as env) = let coqlib = Filename.concat coqlib prelude in if not (Sys.file_exists coqlib) then fail_lib coqlib; let plugin = Filename.concat runtimelib plugins_dir in if not (Sys.file_exists plugin) then fail_core plugin; env
type maybe_env = | Env of t | Boot
let env_ref = ref None
(* Should we fail on double initialization? That seems a way to avoid mis-use for example when we pass command line arguments *)let init_with ~coqlib = let coqlib = match coqlib with | None -> guess_coqlib () | Some coqlib -> coqlib in let env = validate_env { coqlib; runtimelib = guess_coqcorelib coqlib } in env_ref := Some (Env env); env
let initialized () = !env_ref
let ignored_coqlib_msg = "Command line options -boot and -coqlib are incompatible, ignored -coqlib."
let maybe_init ~warn_ignored_coqlib ~boot ~coqlib = match boot, coqlib with | true, None -> Boot | false, (None | Some _ as coqlib) -> (Env (init_with ~coqlib)) | true, Some _ -> warn_ignored_coqlib (); Boot
let coqlib { coqlib; _ } = coqliblet runtimelib { runtimelib; _ } = runtimeliblet plugins { runtimelib; _ } = Path.relative runtimelib plugins_dirlet corelib { coqlib; _ } = Path.relative coqlib theories_dirlet user_contrib { coqlib; _ } = Path.relative coqlib "user-contrib"let tool { runtimelib; _ } tool = Path.(relative (relative runtimelib "tools") tool)let revision { runtimelib; _ } = Path.relative runtimelib "revision"
let native_cmi { runtimelib; _ } lib = let install_path = Path.relative runtimelib lib in if Sys.file_exists install_path then install_path else (* Dune build layout, we need to improve this *) let obj_dir = Format.asprintf ".%s.objs" lib in Filename.(concat (concat (concat runtimelib lib) obj_dir) "byte")
(** {2 Caml paths} *)
let ocamlfind () = match Util.getenv_opt "OCAMLFIND" with | None -> Coq_config.ocamlfind | Some v -> v
let docdir () = (* This assumes implicitly that the suffix is non-trivial *) let path = use_suffix rocqroot Coq_config.docdirsuffix in if Sys.file_exists path then path else relocate Coq_config.docdir
(* Print the configuration information *)
let print_config ?(prefix_var_name="") env f = let coqlib = coqlib env |> Path.to_string in let runtimelib = runtimelib env |> Path.to_string in let open Printf in fprintf f "%sCOQLIB=%s/\n" prefix_var_name coqlib; fprintf f "%sCOQCORELIB=%s/\n" prefix_var_name runtimelib; fprintf f "%sDOCDIR=%s/\n" prefix_var_name (docdir ()); fprintf f "%sOCAMLFIND=%s\n" prefix_var_name (ocamlfind ()); fprintf f "%sCAMLFLAGS=%s\n" prefix_var_name Coq_config.caml_flags; fprintf f "%sWARN=%s\n" prefix_var_name "-warn-error +a-3"; fprintf f "%sHASNATDYNLINK=%s\n" prefix_var_name (if Coq_config.has_natdynlink then "true" else "false"); fprintf f "%sCOQ_SRC_SUBDIRS=%s\n" prefix_var_name (String.concat " " Coq_config.all_src_dirs); fprintf f "%sCOQ_NATIVE_COMPILER_DEFAULT=%s\n" prefix_var_name (match Coq_config.native_compiler with | Coq_config.NativeOn {ondemand=false} -> "yes" | Coq_config.NativeOff -> "no" | Coq_config.NativeOn {ondemand=true} -> "ondemand")
let query_getenv = function | Boot -> assert false | Env v -> v
let print_query envopt usage : Usage.query -> unit = function | PrintVersion -> Usage.version () | PrintMachineReadableVersion -> Usage.machine_readable_version () | PrintWhere -> let env = query_getenv envopt in let coqlib = coqlib env |> Path.to_string in print_endline coqlib | PrintHelp -> begin match usage with | Some usage -> Usage.print_usage stderr usage | None -> assert false end | PrintConfig -> let env = query_getenv envopt in print_config env stdout
let query_needs_env : Usage.query -> string option = function | PrintVersion | PrintMachineReadableVersion | PrintHelp -> None | PrintWhere -> Some "-where" | PrintConfig -> Some "-config"
let print_queries_maybe_init ~warn_ignored_coqlib ~boot ~coqlib usage = function | [] -> Ok (maybe_init ~warn_ignored_coqlib ~boot ~coqlib) | _ :: _ as qs -> let needs_env = CList.find_map query_needs_env qs in let res = match boot, needs_env with | true, Some q -> Error ("Command line option -boot is not compatible with " ^ q ^ ".") | true, None -> (* warn_ignored_coqlib if coqlib and boot used together *) Ok (maybe_init ~warn_ignored_coqlib ~boot ~coqlib) | false, None -> Ok Boot | false, Some _ -> Ok (Env (init_with ~coqlib)) in let () = match res with | Error _ -> () | Ok envopt -> List.iter (print_query envopt usage) qs in res