package logtk

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

Some helpers

Various helpers for the provers.

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

Time facilities

val total_time_s : unit -> float

time elapsed since start of program, in seconds

Misc

module Section : sig ... end

Debug section

val set_debug : int -> unit

Set debug level of Section.root

val get_debug : unit -> int

Current debug level for Section.root

val break_on_debug : bool Stdlib.ref

Shall we wait for user input after each debug message?

val debugf : ?section:Section.t -> int -> ('a, Stdlib.Format.formatter, unit, unit) Stdlib.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.

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

Cheap non-formatting version of debugf

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

Same as CCFormat.ksprintf, but without colors

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

Version of sprintf that adds a colored "error" prefix

val warn : string -> unit

Emit warning

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

Emit warning, with formatting

exception Error of string * string

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

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

error msg raises Error msg

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

Formatting version of error

val pp_pos : Stdlib.Lexing.position -> string
val set_memory_limit : int -> unit

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

val set_time_limit : int -> unit

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

OCaml Stack

requires ocaml >= 4.01

  • since 0.8
module Exn : sig ... end

profiling facilities

type profiler
val enable_profiling : bool Stdlib.ref

Enable/disable profiling

val mk_profiler : string -> profiler

Create a named profiler

val enter_prof : profiler -> unit

Enter the profiler

val exit_prof : profiler -> unit

Exit the profiler

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

Runtime statistics

type stat
val mk_stat : string -> stat
val print_global_stats : comment:string -> unit -> unit

comment prefix

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

Flags as integers

module Flag : sig ... end

Others

val 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.

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

Print a list without begin/end separators

val pp_seq : ?sep:string -> 'a CCFormat.printer -> 'a Iter.t CCFormat.printer
val 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 " "

val tstp_needs_escaping : string -> bool

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

val pp_str_tstp : string CCFormat.printer

possibly escaping

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

String escaping for graphviz

File utils

type 'a or_error = ('a, string) CCResult.t
val 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