aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/usage.ml
Commit message (Collapse)AuthorAge
* Merge PR #6582: Mangle auto-generated namesGravatar Maxime Dénès2018-03-08
|\
* | Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
| |
| * Implement name mangling optionGravatar Jasper Hugunin2018-02-17
|/
* Remove GeoProof support.Gravatar Maxime Dénès2017-10-11
| | | | | Julien Narboux confirmed that it was dead code (GeoProof is not to be confused with GeoCoq).
* [flags] Remove XML output flag.Gravatar Emilio Jesus Gallego Arias2017-08-01
| | | | | | | | This is a second try at removing the hooks for the legacy xml export system which can't currently be tested. It is also not included in the API, so it should either be included in it or this PR be applied.
* Adding -print-version in addition to -print-version for consistency.Gravatar Hugo Herbelin2017-07-25
|
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Merge PR#645: [stm] Tweak debug options.Gravatar Maxime Dénès2017-05-25
|\
* | Document --print-version in UsageGravatar Enrico Tassi2017-05-23
| |
* | Usage.print_config moved to EnvarsGravatar Enrico Tassi2017-05-23
| |
| * [stm] Tweak debug options.Gravatar Emilio Jesus Gallego Arias2017-05-18
|/ | | | | | | | We allow for a dynamic setting of the STM debug flag, and we print some more information about the result of `process_transaction`. We also fix a printing bug due to mixing `Printf` and `Format`, which are not compatible.
* coqtop -help: don't die if coqlib can't be foundGravatar Gaetan Gilbert2017-05-05
|
* Warning 29: non escaped end of line may be non portableGravatar Gaetan Gilbert2017-04-27
|
* [toplevel] Remove unusable option -notopGravatar Emilio Jesus Gallego Arias2017-03-14
| | | | | | | | | | | | | | | | | | | | | | | Maxime points out that -notop cannot be used as the kernel requires all constants to belong into a module. Indeed: ``` $ rlwrap ./bin/coqtop -notop Coq < Definition foo := True. Toplevel input, characters 0-23: > Definition foo := True. > ^^^^^^^^^^^^^^^^^^^^^^^ Error: No session module started (use -top dir) Coq < Module M. Definition foo := True. End M. Module M is defined Coq < Locate foo. Constant If you see this, it's a bug.M.foo (shorter name to refer to it in current context is M.foo) ``` My rationale for the removal is that this kind of incomplete features are often confusing to newcomers ─ it has happened to me many times ─ as it can be seen for example in #397 .
* Stop parsing -compat-notations options, which are no longer supported (bug ↵Gravatar Guillaume Melquiond2016-11-21
| | | | #3339).
* Do not mention "none" in warnings doc, as it is there for compatibility.Gravatar Maxime Dénès2016-11-14
|
* Add documentation for [Set Warnings] and the -w option.Gravatar Cyprien Mangin2016-11-04
|
* Fix indentation of -profile-ltac in -helpGravatar Jason Gross2016-09-17
|
* --print-version produces machine readable version infoGravatar Enrico Tassi2016-06-16
| | | | | | | | What one needs to know in 3rd party makefiles, like plugins ones, is the Coq version and the OCaml version number. This option prints the 2 values on a single line separated by spaces. The already existing --version outputs the same piece of info but in a format meant for user consumption, and hence harder to parse.
* Merge remote-tracking branch 'origin/pr/166' into trunkGravatar Enrico Tassi2016-06-14
|\ | | | | | | Add -o option to coqc
* | -profileltac -> -profile-ltac, as per @herbelinGravatar Jason Gross2016-06-05
| | | | | | | | | | | | | | | | https://github.com/coq/coq/pull/150#issuecomment-219141596 ```bash git grep --name-only profileltac | xargs sed s'/profileltac/profile-ltac/g' -i ```
* | LtacProf for Coq trunkGravatar Jason Gross2016-06-05
| | | | | | | | | | | | This add LtacProfiling. Much of the code was written by Tobias Tebbi (@tebbi), and Paul A. Steckler was invaluable in porting the code to Coq v8.5 and Coq trunk.
| * fix blanks in usage messageGravatar Enrico Tassi2016-05-19
| |
| * coqc: support -o option to specify output file nameGravatar Enrico Tassi2016-05-19
|/ | | | | | | | | | | | | | | | The -o option lets one put .vo or .vio files in a directory of choice, i.e. decouple the location of the sources and the compiled files. This ease the integration of Coq in already existing IDEs that handle the build process automatically (eg Eclipse) and also enables one to compile/run at the same time 2 versions of Coq on the same sources. Example: b.v depending on a.v coq8.6/bin/coqc -R out8.6 Test src/a.v -o out8.6/a.vo coq8.6/bin/coqc -R out8.6 Test src/b.v -o out8.6/b.vo coq8.7/bin/coqc -R out8.7 Test src/a.v -o out8.7/a.vo coq8.7/bin/coqc -R out8.7 Test src/b.v -o out8.7/b.vo
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
| * Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Gravatar Maxime Dénès2016-01-15
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-09-25
|\|
| * The -require option now accepts a logical path instead of a physical one.Gravatar Pierre-Marie Pédrot2015-09-25
| |
| * Updating the documentation and the toolchain w.r.t. the change in -compile.Gravatar Pierre-Marie Pédrot2015-09-25
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-08-05
|\|
| * For convenience, making yes and on, and no and off synonymous inGravatar Hugo Herbelin2015-08-02
| | | | | | | | | | command line. Documenting only the former for simplicity and uniformity with predating option -with-geoproof.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-06-24
|\|
| * improve --help documentation: the -m|--memory option was missingGravatar Gabriel Scherer2015-06-24
| |
* | All invocations to ocaml compilers go through ocamlfindGravatar Pierre Boutillier2015-06-22
|/ | | | | Nothing is done for camlp4 There is an issue with computing camlbindir
* Fix usage about -color.Gravatar Pierre Courtieu2015-05-18
|
* Adding an option -w to control Coq warning output.Gravatar Pierre-Marie Pédrot2015-05-14
| | | | | | | For now, warnings are still ignored by default, but this may change. This commit at least allows to print them whenever desired. The -w syntax is also opened to future additions to further control the display of warnings.
* Disable precompilation for native_compute by default.Gravatar Guillaume Melquiond2015-05-14
| | | | | | | | | | | | | | Note that this does not prevent using native_compute, but it will force on-the-fly recompilation of dependencies whenever it is used. Precompilation is enabled for the standard library, assuming native compilation was enabled at configuration time. If native compilation was disabled at configuration time, native_compute falls back to vm_compute. Failure to precompile is a hard error, since it is now explicitly required by the user.
* Removing references to deprecated syntax -I/-R -as.Gravatar Pierre-Marie Pédrot2015-03-31
|
* coqc: fix --helpGravatar Enrico Tassi2015-03-25
|
* add -type-in-type to the usage messageGravatar Daniel R. Grayson2015-03-18
|
* Fix typos about .vio files (thanks Arthur for spotting them)Gravatar Enrico Tassi2015-02-12
|
* Add -no-native-compiler flag to list dumped by --help.Gravatar Maxime Dénès2015-01-12
|
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* For consistency with other coqtop flags, use -help rather than --help in usage.Gravatar Hugo Herbelin2014-11-16
|
* Adding a command line option to print out accepted color tags.Gravatar Pierre-Marie Pédrot2014-11-15
|
* Reworking the -color flag of coqtop.Gravatar Pierre-Marie Pédrot2014-11-15
|
* toploop plugins taken into account when printing --help (close: 3535)Gravatar Enrico Tassi2014-09-09
| | | | | | | | | | | | | E.g. Coq options are: -I dir look for ML files in dir -include dir (idem) [...] -h, --help print this list of options With the flag '-toploop coqidetop' these extra option are also available: --help-XML-protocol print the documentation of the XML protocol used by CoqIDE
* Removing dead code relative to the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
|
* Removing documentation related to the deprecated State machinery.Gravatar Pierre-Marie Pédrot2014-08-16
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-24 23:58:20 +0000