package coq

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

This file provides facilities to access OCaml compiler and dynamic linker, used by the native compiler.

val output_dir : CUnix.physical_path Stdlib.ref
val include_dirs : CUnix.physical_path list Stdlib.ref
val get_load_paths : (unit -> string list) Stdlib.ref
val load_obj : (string -> unit) Stdlib.ref
val get_ml_filename : unit -> string * string
val compile : string -> Nativecode.global list -> profile:bool -> string

compile file code ~profile will compile native code to file, and return the name of the object file; this name depends on whether are in byte mode or not; file is expected to be .ml file

type native_library = Nativecode.global list * Nativevalues.symbols
val compile_library : native_library -> string -> unit

compile_library (code, _) file is similar to compile file code but will perform some extra tweaks to handle code as a Coq lib.

val execute_library : prefix:string -> string -> Nativecode.code_location_updates -> Nativevalues.t * Nativevalues.t

execute_library file upds dynamically loads library file, updates the library locations upds, and returns the values stored in rt1 and rt2

val enable_library : string -> Names.DirPath.t -> unit

enable_library marks the given library for dynamic loading the next time link_libraries is called.

val rt1 : Nativevalues.t Stdlib.ref
val rt2 : Nativevalues.t Stdlib.ref
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