Quellcode-Bibliothek coq_config.mli 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)         *)
(************************************************************************)

type relocatable_path =
  | NotRelocatable of string (* absolute path *)
  | Relocatable of string (* relative to the inferred prefix *)

(* The fields below are absolute paths *)
val install_prefix : relocatable_path   (* Install prefix passed by the user *)
val coqlib : relocatable_path     (* where the std library is installed *)
val configdir : relocatable_path  (* where configuration files are installed *)
val datadir : relocatable_path    (* where extra data files are installed *)
val docdir : relocatable_path     (* where the doc is installed *)

(* The fields below are paths relative to the installation prefix *)
(* However, if an absolute path, it means discarding the actual prefix *)
val coqlibsuffix : string    (* std library relative to installation prefix *)
val configdirsuffix : string (* config files relative to installation prefix *)
val datadirsuffix : string   (* data files relative to installation prefix *)
val docdirsuffix : string    (* doc directory relative to installation prefix *)

(* used in envars (likely for coq_makefile) *)
val ocamlfind : string

(* used in envars for coq_makefile *)
val caml_flags : string     (* arguments passed to ocamlc (ie. CAMLFLAGS) *)

(* Used in rocqide *)
val arch : string       (* architecture *)

(* dubious use in envars, use in coqmakefile *)
val arch_is_win32 : bool

val version : string    (* version number of Rocq *)
val caml_version : string    (* OCaml version used to compile Rocq *)
val caml_version_nums : int list    (* OCaml version used to compile Rocq by components *)
val vo_version : int32

(* used in envars for coq_makefile *)
val all_src_dirs : string list

(* Used in micromega *)
val exec_extension : string (* "" under Unix, ".exe" under MS-windows *)

(* Used in rocqide *)
val browser : string
(** default web browser to use, may be overridden by environment
    variable COQREMOTEBROWSER *)

(* used in coqdep *)
val has_natdynlink : bool

(* used in coqdoc *)
val wwwcoq : string
val wwwstdlib : string

(* used in rocqide *)
val wwwrefman : string

(* for error reporting *)
val wwwbugtracker : string

val bytecode_compiler : bool
type native_compiler = NativeOff | NativeOn of { ondemand : bool }
val native_compiler : native_compiler

quality95%

¤ 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.0.11Bemerkung: (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.