diff options
| -rw-r--r-- | .travis.yml | 2 | ||||
| -rw-r--r-- | configure.ml | 39 | ||||
| -rw-r--r-- | dev/doc/setup.txt | 8 |
3 files changed, 28 insertions, 21 deletions
diff --git a/.travis.yml b/.travis.yml index e79498124..13bdd6fb2 100644 --- a/.travis.yml +++ b/.travis.yml @@ -155,7 +155,7 @@ script: - set -e - echo 'Configuring Coq...' && echo -en 'travis_fold:start:coq.config\\r' -- ./configure -local -usecamlp5 -native-compiler ${NATIVE_COMP} ${EXTRA_CONF} +- ./configure -local -native-compiler ${NATIVE_COMP} ${EXTRA_CONF} - echo -en 'travis_fold:end:coq.config\\r' - echo 'Building Coq...' && echo -en 'travis_fold:start:coq.build\\r' diff --git a/configure.ml b/configure.ml index a5204d5b5..b2c027522 100644 --- a/configure.ml +++ b/configure.ml @@ -301,33 +301,37 @@ let args_options = Arg.align [ "-emacslib", arg_string_option Prefs.emacslib, "<dir> Where to install emacs files"; "-emacs", Arg.String (fun s -> - printf "Warning: obsolete -emacs option\n"; + prerr_endline "Warning: -emacs option is deprecated. Use -emacslib instead."; Prefs.emacslib := Some s), - "<dir> Obsolete: same as -emacslib"; + "<dir> Deprecated: same as -emacslib"; "-coqdocdir", arg_string_option Prefs.coqdocdir, "<dir> Where to install Coqdoc style files"; "-ocamlfind", arg_string_option Prefs.ocamlfindcmd, "<dir> Specifies the ocamlfind command to use"; "-lablgtkdir", arg_string_option Prefs.lablgtkdir, "<dir> Specifies the path to the Lablgtk library"; - "-usecamlp5", Arg.Unit (fun () -> ()), - "Deprecated"; + "-usecamlp5", Arg.Unit (fun () -> + prerr_endline "Warning: -usecamlp5 option is deprecated. Camlp5 is already a required dependency."), + " Deprecated: Camlp5 is a required dependency (Camlp4 is not supported anymore)"; "-camlp5dir", Arg.String (fun s -> Prefs.camlp5dir:=Some s), "<dir> Specifies where is the Camlp5 library and tells to use it"; "-arch", arg_string_option Prefs.arch, "<arch> Specifies the architecture"; - "-opt", Arg.Unit (fun () -> printf "Warning: obsolete -opt option\n"), - " Obsolete: native OCaml executables detected automatically"; + "-opt", Arg.Unit (fun () -> + prerr_endline "Warning: -opt option is deprecated. Native OCaml executables are detected automatically."), + " Deprecated: native OCaml executables detected automatically"; "-natdynlink", arg_bool Prefs.natdynlink, "(yes|no) Use dynamic loading of native code or not"; "-coqide", Arg.String (fun s -> Prefs.coqide := Some (get_ide s)), - "(opt|byte|no) Specifies whether or not to compile Coqide"; + "(opt|byte|no) Specifies whether or not to compile CoqIDE"; "-nomacintegration", Arg.Clear Prefs.macintegration, - " Do not try to build coqide mac integration"; + " Do not try to build CoqIDE MacOS integration"; "-browser", arg_string_option Prefs.browser, "<command> Use <command> to open URL %s"; - "-nodoc", Arg.Clear Prefs.withdoc, + "-nodoc", Arg.Unit (fun () -> + prerr_endline "Warning: -nodoc option is deprecated. Use -with-doc no instead."; + Prefs.withdoc := false), " Deprecated: use -with-doc no instead"; "-with-doc", arg_bool Prefs.withdoc, "(yes|no) Compile the documentation or not"; @@ -335,18 +339,23 @@ let args_options = Arg.align [ "(yes|no) Use Geoproof binding or not"; "-byte-only", Arg.Set Prefs.byteonly, " Compiles only bytecode version of Coq"; - "-byteonly", Arg.Set Prefs.byteonly, - " Compiles only bytecode version of Coq"; - "-debug", Arg.Set Prefs.debug, - " Deprecated"; + "-byteonly", Arg.Unit (fun () -> + prerr_endline "Warning: -byteonly option is deprecated. Use -byte-only instead."; + Prefs.byteonly := true), + " Deprecated: use -byte-only instead"; + "-debug", Arg.Unit (fun () -> + prerr_endline "Warning: -debug option is deprecated. Coq is compiled in debug mode by default."; + Prefs.debug := true), + " Deprecated: Coq is compiled in debug mode by default"; "-nodebug", Arg.Clear Prefs.debug, " Do not add debugging information in the Coq executables"; "-profile", Arg.Set Prefs.profile, " Add profiling information in the Coq executables"; "-annotate", Arg.Set Prefs.annotate, " Dumps ml annotation files while compiling Coq"; - "-makecmd", Arg.String (fun _ -> printf "Warning: obsolete -makecmd option\n"), - "<command> Obsolete: name of GNU Make command"; + "-makecmd", Arg.String (fun _ -> + prerr_endline "Warning: -makecmd option is deprecated and doesn't have any effect."), + "<command> Deprecated"; "-native-compiler", arg_bool Prefs.nativecompiler, "(yes|no) Compilation to native code for conversion and normalization"; "-coqwebsite", Arg.Set_string Prefs.coqwebsite, diff --git a/dev/doc/setup.txt b/dev/doc/setup.txt index 1b016a4e2..0c6d3ee80 100644 --- a/dev/doc/setup.txt +++ b/dev/doc/setup.txt @@ -12,7 +12,7 @@ How to compile Coq Getting build dependencies: - sudo apt-get install make opam git mercurial darcs + sudo apt-get install make opam git opam init --comp 4.02.3 # Then follow the advice displayed at the end as how to update your ~/.bashrc and ~/.ocamlinit files. @@ -41,7 +41,7 @@ Building coqtop: cd ~/git/coq git checkout trunk make distclean - ./configure -annotate -with-doc no -local -debug -usecamlp5 + ./configure -annotate -local make clean make -j4 coqide printers @@ -49,8 +49,6 @@ The "-annotate" option is essential when one wants to use Merlin. The "-local" option is useful if one wants to run the coqtop and coqide binaries without running make install -The "-debug" option is essential if one wants to use ocamldebug with the coqtop binary. - Then check if - bin/coqtop - bin/coqide @@ -60,7 +58,7 @@ behave as expected. A note about rlwrap ------------------- -Running "coqtop" under "rlwrap" is possible, but there is a catch. If you try: +Running "coqtop" under "rlwrap" is possible, but (on Debian) there is a catch. If you try: cd ~/git/coq rlwrap bin/coqtop |