| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/config/ (Beweissystem des Inria Version 9.1.0©) Datei vom 15.8.2025 mit Größe 2 kB |
|
Quelle 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 ¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28