package coq

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

Source file usage.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq 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)         *)
(************************************************************************)

let version () =
  Printf.printf "The Coq Proof Assistant, version %s\n" Coq_config.version;
  Printf.printf "compiled with OCaml %s\n" Coq_config.caml_version

let machine_readable_version () =
  Printf.printf "%s %s\n"
    Coq_config.version Coq_config.caml_version

(* print the usage of coqtop (or coqc) on channel co *)

let print_usage_common co command =
  output_string co command;
  output_string co "Coq options are:\n";
  output_string co
"  -I dir                 look for ML files in dir\
\n  -include dir           (idem)\
\n  -R dir coqdir          recursively map physical dir to logical coqdir\
\n  -Q dir coqdir          map physical dir to logical coqdir\
\n  -top coqdir            set the toplevel name to be coqdir instead of Top\
\n  -topfile f             set the toplevel name as though compiling f\
\n  -coqlib dir            set the coq standard library directory\
\n  -exclude-dir f         exclude subdirectories named f for option -R\
\n\
\n  -boot                  don't bind the `Coq.` prefix to the default -coqlib dir\
\n  -noinit                don't load Coq.Init.Prelude on start \
\n  -nois                  (idem)\
\n  -compat X.Y            provides compatibility support for Coq version X.Y\
\n\
\n  -load-vernac-source f  load Coq file f.v (Load \"f\".)\
\n  -l f                   (idem)\
\n  -load-vernac-source-verbose f  load Coq file f.v (Load Verbose \"f\".)\
\n  -lv f	           (idem)\
\n  -load-vernac-object lib\
\n                         load Coq library lib (Require lib)\
\n  -rfrom root lib        load Coq library lib (From root Require lib.)\
\n  -require-import lib, -ri lib\
\n                         load and import Coq library lib\
\n                         (equivalent to Require Import lib.)\
\n  -require-export lib, -re lib\
\n                         load and transitively import Coq library lib\
\n                         (equivalent to Require Export lib.)\
\n  -require-import-from root lib, -rifrom root lib\
\n                         load and import Coq library lib\
\n                         (equivalent to From root Require Import lib.)\
\n  -require-export-from root lib, -refrom root lib\
\n                         load and transitively import Coq library lib\
\n                         (equivalent to From root Require Export lib.)\
\n\
\n  -where                 print Coq's standard library location and exit\
\n  -config, --config      print Coq's configuration information and exit\
\n  -v, --version          print Coq version and exit\
\n  -print-version         print Coq version in easy to parse format and exit\
\n  -list-tags             print highlight color tags known by Coq and exit\
\n\
\n  -quiet                 unset display of extra information (implies -w \"-all\")\
\n  -w (w1,..,wn)          configure display of warnings\
\n  -d (d1,..,dn)          configure display of debug messages\
\n                         some common values are:\
\n                           all         print all debugging information\
\n                           backtrace   same as -bt\
\n                         use the vernac command \"Test Debug\" to see all\
\n\
\n  -color (yes|no|auto)   configure color output\
\n  -emacs                 tells Coq it is executed under Emacs\
\n\
\n  -q                     skip loading of rcfile\
\n  -init-file f           set the rcfile to f\
\n  -bt                    print OCaml backtraces\
\n  -diffs (on|off|removed) highlight differences between proof steps\
\n  -impredicative-set     set sort Set impredicative\
\n  -allow-sprop           allow using the proof irrelevant SProp sort\
\n  -disallow-sprop        forbid using the proof irrelevant SProp sort\
\n  -indices-matter        levels of indices (and nonuniform parameters) contribute to the level of inductives\
\n  -type-in-type          disable universe consistency checking\
\n  -mangle-names x        mangle auto-generated names using prefix x\
\n  -set \"Foo Bar\"         enable Foo Bar (as Set Foo Bar. in a file)\
\n  -set \"Foo Bar=value\"   set Foo Bar to value (value is interpreted according to Foo Bar's type)\
\n  -unset \"Foo Bar\"       disable Foo Bar (as Unset Foo Bar. in a file)\
\n  -time                  display the time taken by each command\
\n  -profile-ltac          display the time taken by each (sub)tactic\
\n  -m, --memory           display total heap size at program exit\
\n                         (use environment variable\
\n                          OCAML_GC_STATS=\"/tmp/gclog.txt\"\
\n                          for full Gc stats dump)\
\n  -bytecode-compiler (yes|no)        enable the vm_compute reduction machine\
\n  -native-compiler (yes|no|ondemand) enable the native_compute reduction machine\
\n  -native-output-dir     <directory> set the output directory for native objects\
\n  -nI dir                OCaml include directories for the native compiler (default if not set) \
\n  -h, -help, --help      print this list of options\
\n"

(* print the usage *)

type specific_usage = {
  executable_name : string;
  extra_args : string;
  extra_options : string;
}

let print_usage co { executable_name; extra_args; extra_options } =
  print_usage_common co ("Usage: " ^ executable_name ^ " <options> " ^ extra_args ^ "\n\n");
  output_string co extra_options
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