package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Logtk.UtilSource

Some helpers

Various helpers for the provers.

It provides counters for statistics, basic profilers, helper functions, debugging functions…

Time facilities

Sourceval total_time_s : unit -> float

time elapsed since start of program, in seconds

Misc

Sourcemodule Section : sig ... end

Debug section

Sourceval set_debug : int -> unit

Set debug level of Section.root

Sourceval get_debug : unit -> int

Current debug level for Section.root

Sourceval break_on_debug : bool ref

Shall we wait for user input after each debug message?

Sourceval debugf : ?section:Section.t -> int -> ('a, Format.formatter, unit, unit) format4 -> ('a -> unit) -> unit

Print a debug message, with the given section and verbosity level. The message might be dropped if its level is too high.

Sourceval debug : ?section:Section.t -> int -> string -> unit

Cheap non-formatting version of debugf

Sourceval ksprintf_noc : f:(string -> 'a) -> ('b, Format.formatter, unit, 'a) format4 -> 'b

Same as CCFormat.ksprintf, but without colors

Sourceval err_spf : ('b, Format.formatter, unit, string) format4 -> 'b

Version of sprintf that adds a colored "error" prefix

Sourceval warn : string -> unit

Emit warning

Sourceval warnf : ('a, Format.formatter, unit, unit) format4 -> 'a

Emit warning, with formatting

Sourceexception Error of string * string

generalist error that do not really belong elsewhere. Error (where,what) means that error what was raised from where.

Sourceval error : where:string -> string -> 'a

error msg raises Error msg

Sourceval errorf : where:string -> ('b, Format.formatter, unit, 'a) format4 -> 'b

Formatting version of error

Sourceval pp_pos : Lexing.position -> string
Sourceval set_memory_limit : int -> unit

Limit the amount of memory available to the process (in MB)

Sourceval set_time_limit : int -> unit

Limit the CPU time available to the process (in seconds)

OCaml Stack

requires ocaml >= 4.01

  • since 0.8
Sourcemodule Exn : sig ... end

profiling facilities

Sourcetype profiler
Sourceval enable_profiling : bool ref

Enable/disable profiling

Sourceval mk_profiler : string -> profiler

Create a named profiler

Sourceval enter_prof : profiler -> unit

Enter the profiler

Sourceval exit_prof : profiler -> unit

Exit the profiler

Sourceval with_prof : profiler -> ('a -> 'b) -> 'a -> 'b

Runtime statistics

Sourcetype stat
Sourceval mk_stat : string -> stat
Sourceval print_global_stats : comment:string -> unit -> unit

comment prefix

Sourceval incr_stat : stat -> unit
Sourceval add_stat : stat -> int -> unit

Flags as integers

Sourcemodule Flag : sig ... end

Others

Sourceval finally : do_:(unit -> unit) -> (unit -> 'a) -> 'a

finally ~do_ f calls f () and returns its result. If it raises, the same exception is raised; in any case, do_ () is called after f () terminates.

Sourceval pp_pair : ?sep:string -> 'a CCFormat.printer -> 'b CCFormat.printer -> ('a * 'b) CCFormat.printer
Sourceval pp_list : ?sep:string -> 'a CCFormat.printer -> 'a list CCFormat.printer

Print a list without begin/end separators

Sourceval pp_seq : ?sep:string -> 'a CCFormat.printer -> 'a Iter.t CCFormat.printer
Sourceval pp_list0 : ?sep:string -> 'a CCFormat.printer -> 'a list CCFormat.printer

Print a list with a whitespace in front if it's non empty, or does nothing if the list is empty Default separator is " "

Sourceval tstp_needs_escaping : string -> bool

Is this name a proper TSTP identifier, or does it need ' ' around it?

Sourceval pp_str_tstp : string CCFormat.printer

possibly escaping

Sourceval pp_var_tstp : string CCFormat.printer
Sourceval ord_option : 'a CCOrd.t -> 'a option CCOrd.t
Sourceval take_drop_while : ('a -> bool) -> 'a list -> 'a list * 'a list
Sourceval map_product : f:('a -> 'b list list) -> 'a list -> 'b list list
Sourceval seq_map_l : f:('a -> 'b list) -> 'a list -> 'b list Iter.t
Sourceval seq_zipi : 'a Iter.t -> (int * 'a) Iter.t
Sourceval invalid_argf : ('a, Format.formatter, unit, 'b) format4 -> 'a
Sourceval failwithf : ('a, Format.formatter, unit, 'b) format4 -> 'a
Sourcemodule Int_map : CCMap.S with type key = int
Sourcemodule Int_set : CCSet.S with type elt = int
Sourceval escape_dot : string -> string

String escaping for graphviz

File utils

Sourcetype 'a or_error = ('a, string) CCResult.t
Sourceval popen : cmd:string -> input:string -> string or_error

Run the given command cmd with the given input, wait for it to terminate, and return its stdout.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct