Quelle rocqworker_with_drop.ml Sprache: SML

(************************************************************************)
(*         *      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)         *)
(************************************************************************)

(* We register this handler for lower-level toplevel loading code *)
let () = CErrors.register_handler (function
    | Symtable.Error e ->
      Some (Pp.str (Format.asprintf "%a" Symtable.report_error e))
    | _ ->
      None
  )

(* Another bit of text is printed in the [include_utilities] file, so the default one is not need *)
let () = Clflags.noversion := true

let load_module fmt name =
  if not ((Topdirs.load_file [@ocaml.warning "-3"]) fmt name) then
    CErrors.user_err Pp.(str ("Could not load plugin " ^ name))

let load_plugin fmt ps =
  let lib = Mltop.PluginSpec.to_package ps in
  Topfind.load_deeply [lib]

let ml_loop fmt ?init_file () =
  let init_file = ref init_file in
  Toploop.add_hook (fun event ->
    if event = Toploop.After_setup then begin
      match !init_file with
      | None -> ()
      | Some f ->
        init_file := None; (* Run the initialization file only once *)
        ignore (Coq_byte_config.toploop_use_silently fmt f)
    end
  );
  Coq_byte_config.compenv_handle_exit_with_status_0 (fun () -> Toploop.loop fmt)

let drop_setup () =
  let ppf = Format.std_formatter in
  Mltop.set_top
    { load_plugin = load_plugin ppf
    ; load_module = load_module ppf
    ; add_dir = Topdirs.dir_directory
    ; ml_loop = ml_loop ppf
    }

(* Main coqtop initialization *)
let () =
  drop_setup ();
  Coqtop.(start_coq coqtop_toplevel (List.tl (Array.to_list Sys.argv)))

quality100%

¤ Dauer der Verarbeitung: 0.23 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.