diff options
| -rw-r--r-- | CONTRIBUTING.md | 2 | ||||
| -rw-r--r-- | INSTALL | 323 | ||||
| -rw-r--r-- | INSTALL.md | 79 | ||||
| -rw-r--r-- | Makefile | 358 | ||||
| -rw-r--r-- | Makefile.make | 366 | ||||
| -rw-r--r-- | README.md | 2 | ||||
| -rwxr-xr-x | dev/build/windows/makecoq_mingw.sh | 2 | ||||
| -rw-r--r-- | dev/doc/INSTALL.make.md | 258 | ||||
| -rw-r--r-- | doc/README.md | 2 |
9 files changed, 711 insertions, 681 deletions
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 1a12360c13..f7661743a2 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -870,7 +870,7 @@ team. #### Building Coq #### The list of dependencies can be found in the first section of the -[`INSTALL`](INSTALL) file. +[`INSTALL.md`](INSTALL.md) file. Today, the recommended method for building Coq is to use `dune`. Run `make -f Makefile.dune` to get help on the various available targets, diff --git a/INSTALL b/INSTALL deleted file mode 100644 index 31758203fe..0000000000 --- a/INSTALL +++ /dev/null @@ -1,323 +0,0 @@ - INSTALLING FROM SOURCES - ----------------------- - - -WHAT DO YOU NEED ? -================== - - To compile Coq yourself, you need: - - - OCaml (version >= 4.05.0) - (available at https://ocaml.org/) - (This version of Coq has been tested up to OCaml 4.09.0) - - - The Num package, which used to be part of the OCaml standard library, - if you are using an OCaml version >= 4.06.0 - - - Findlib (version >= 1.4.1) - (available at http://projects.camlcity.org/projects/findlib.html) - - - GNU Make version 3.81 or later - - - a C compiler - - - an IEEE-754 compliant architecture with rounding to nearest - ties to even as default rounding mode (most architectures - should work nowadays) - - - for CoqIDE, the lablgtk development files (version >= 3.0.0), - and the GTK 3.x libraries including gtksourceview3. - - The IEEE-754 compliance is required by primitive floating-point - numbers (Require Import Floats). Common sources of incompatibility - are checked at configure time, preventing compilation. In the, - unlikely, event an incompatibility remains undetected, using Floats - would enable to prove False on this architecture. - - Note that num and lablgtk should be properly registered with - findlib/ocamlfind as Coq's makefile will use it to locate the - libraries during the build. - - Debian / Ubuntu users can get the necessary system packages for - CoqIDE with: - - $ sudo apt-get install libgtksourceview-3.0-dev - - Opam (https://opam.ocaml.org/) is recommended to install OCaml and - the corresponding packages. - - $ opam install num ocamlfind lablgtk3-sourceview3 - - should get you a reasonable OCaml environment to compile Coq. - - Nix users can also get all the required dependencies by running: - - $ nix-shell - - Advanced users may want to experiment with the OCaml Flambda - compiler as way to improve the performance of Coq. In order to - profit from Flambda, a special build of the OCaml compiler that has - the Flambda optimizer enabled must be installed. For OPAM users, - this amounts to installing a compiler switch ending in `+flambda`, - such as `4.07.0+flambda`. For other users, YMMV. Once `ocamlopt - -config` reports that Flambda is available, some further - optimization options can be used; see the entry about -flambda-opts - below for more details. - -QUICK INSTALLATION PROCEDURE. -============================= - -1. ./configure -2. make -3. make install (you may need superuser rights) - -INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). -================================================= - -1- Check that you have the OCaml compiler installed on your - computer and that "ocamlc" (or, better, its native code version - "ocamlc.opt") lies in a directory which is present in your $PATH - environment variable. At the time of writing this sentence, all - versions of Objective Caml later or equal to 4.05.0 are - supported. - - To get Coq in native-code, (it runs 4 to 10 times faster than - bytecode, but it takes more time to get compiled and the binary is - bigger), you will also need the "ocamlopt" (or its native code version - "ocamlopt.opt") command. - -2- The uncompression and un-tarring of the distribution file gave birth - to a directory named "coq-8.xx". You can rename this directory and put - it wherever you want. Just keep in mind that you will need some spare - space during the compilation (reckon on about 300 Mb of disk space - for the whole system in native-code compilation). Once installed, the - binaries take about 30 Mb, and the library about 200 Mb. - -3- First you need to configure the system. It is done automatically with - the command: - - ./configure <options> - - The "configure" script will ask you for directories where to put - the Coq binaries, standard library, man pages, etc. It will propose - you some default values. - - For a list of options accepted by the "configure" script, run - "./configure -help". The main options accepted are: - --prefix <dir> - Binaries, library, and man pages will be respectively - installed in <dir>/bin, <dir>/lib/coq, and <dir>/man - --bindir <dir> (default: /usr/local/bin) - Directory where the binaries will be installed - --libdir <dir> (default: /usr/local/lib/coq) - Directory where the Coq standard library will be installed - --mandir <dir> (default: /usr/local/share/man) - Directory where the Coq manual pages will be installed - --arch <value> (default is the result of the command "arch") - An arbitrary architecture name for your machine (useful when - compiling Coq on two different architectures for which the - result of "arch" is the same, e.g. Sun OS and Solaris) - --local - Compile Coq to run in its source directory. The installation (step 6) - is not necessary in that case. - --browser <command> - Use <command> to open an URL in a browser. %s must appear in <command>, - and will be replaced by the URL. - --flambda-opts <flags> - This experimental option will pass specific user flags to the - OCaml optimizing compiler. In most cases, this option is used - to tweak the flambda backend; for maximum performance we - recommend using - - -flambda-opts `-O3 -unbox-closures` - - but of course you are free to try with a different combination - of flags. You can read more at - https://caml.inria.fr/pub/docs/manual-ocaml/flambda.html - - There is a known problem with certain OCaml versions and - `native_compute`, that will make compilation to require - a large amount of RAM (>= 10GiB) in some particular files. - - We recommend disabling native compilation (`-native-compiler no`) - with flambda unless you use OCaml >= 4.07.0. - - c.f. https://caml.inria.fr/mantis/view.php?id=7630 - - If you want your build to be reproducible, ensure that the - SOURCE_DATE_EPOCH environment variable is set as documented in - https://reproducible-builds.org/specs/source-date-epoch/ - -4- Still in the root directory, do - - make - - to compile Coq in the best OCaml mode available (native-code if supported, - bytecode otherwise). - - This will compile the entire system. This phase can take more or less time, - depending on your architecture and is fairly verbose. On a multi-core machine, - it is recommended to compile in parallel, via make -jN where N is your number - of cores. - -5- You can now install the Coq system. Executables, libraries, and - manual pages are copied in some standard places of your system, - defined at configuration time (step 3). Just do - - umask 022 - make install - - Of course, you may need superuser rights to do that. - -6- Optionally, you could build the bytecode version of Coq via: - - make byte - - and install it via - - make install-byte - - This version is quite slower than the native code version of Coq, but could - be helpful for debugging purposes. In particular, coqtop.byte embeds an OCaml - toplevel accessible via the Drop command. - -7- You can now clean all the sources. (You can even erase them.) - - make clean - - -INSTALLATION PROCEDURE FOR ADVANCED USERS. -========================================== - - If you wish to write plugins you *must* keep the Coq sources, without - cleaning them. Therefore, to avoid a duplication of binaries and library, - it is not necessary to do the installation step (6- above). You just have - to tell it at configuration step (4- above) with the option -local : - - ./configure -local <other options> - - Then compile the sources as described in step 5 above. The resulting - binaries will reside in the subdirectory bin/. - - Unless you pass the -nodebug option to ./configure, the -g option of the - OCaml compiler will be used during compilation to allow debugging. - See the debugging file in dev/doc and the chapter 15 of the Coq Reference - Manual for details about how to use the OCaml debugger with Coq. - - -THE AVAILABLE COMMANDS. -======================= - - There are two Coq commands: - - coqtop The Coq toplevel - coqc The Coq compiler - - Under architecture where ocamlopt is available, coqtop is the native code - version of Coq. On such architecture, you could additionally request - the build of the bytecode version of Coq via 'make byte' and install it via - 'make install-byte'. This will create an extra binary named coqtop.byte, - that could be used for debugging purpose. If native code isn't available, - coqtop.byte is directly built by 'make', and coqtop is a link to coqtop.byte. - coqc also invokes the fastest version of Coq. Options -opt and -byte to coqtop - and coqc selects a particular binary. - - * `coqtop' launches Coq in the interactive mode. By default it loads - basic logical definitions and tactics from the Init directory. - - * `coqc' allows compilation of Coq files directly from the command line. - To compile a file foo.v, do: - - coqc foo.v - - It will produce a file foo.vo, that you can now load through the Coq - command "Require". - - A detailed description of these commands and of their options is given - in the Reference Manual (which you can get in the doc/ - directory, or read online on http://coq.inria.fr/doc/) - and in the corresponding manual pages. - - -COMPILING FOR DIFFERENT ARCHITECTURES. -====================================== - - This section explains how to compile Coq for several architecture, sharing - the same sources. The important fact is that some files are architecture - dependent (.cmx, .o and executable files for instance) but others are not - (.cmo and .vo). Consequently, you can : - - o save some time during compilation by not cleaning the architecture - independent files; - - o save some space during installation by sharing the Coq standard - library (which is fully architecture independent). - - So, in order to compile Coq for a new architecture, proceed as follows: - - * Omit step 7 above and clean only the architecture dependent files: - it is done automatically with the command - - make archclean - - * Configure the system for the new architecture: - - ./configure <options> - - You can specify the same directory for the standard library but you - MUST specify a different directory for the binaries (of course). - - * Compile and install the system as described in steps 5 and 6 above. - - -MOVING BINARIES OR LIBRARY. -=========================== - - If you move both the binaries and the library in a consistent way, - Coq should be able to still run. Otherwise, Coq may be "lost", - running "coqtop" would then return an error message of the kind: - - Error during initialization : - Error: cannot guess a path for Coq libraries; please use -coqlib option - - You can then indicate the new places to Coq, using the options -coqlib : - - coqtop -coqlib <new directory> - - See also next section. - - -DYNAMICALLY LOADED LIBRARIES FOR BYTECODE EXECUTABLES. -====================================================== - - Some bytecode executables of Coq use the OCaml runtime, which dynamically - loads a shared library (.so or .dll). When it is not installed properly, you - can get an error message of this kind: - - Fatal error: cannot load shared library dllcoqrun - Reason: dllcoqrun.so: cannot open shared object file: No such file or directory - - In this case, you need either: - - to set the CAML_LD_LIBRARY_PATH environment variable to point to the - directory where dllcoqrun.so is; this is suitable when you want to run - the command a limited number of times in a controlled environment (e.g. - during compilation of binary packages); - - install dllcoqrun.so in a location listed in the file ld.conf that is in - the directory of the standard library of OCaml; - - recompile your bytecode executables after reconfiguring the location - of the shared library: - ./configure -vmbyteflags "-dllib,-lcoqrun,-dllpath,<path>" ... - where <path> is the directory where the dllcoqrun.so is installed; - - (not recommended) compile bytecode executables with a custom OCaml - runtime by using: - ./configure -custom ... - be aware that stripping executables generated this way, or performing - other executable-specific operations, will make them useless. diff --git a/INSTALL.md b/INSTALL.md new file mode 100644 index 0000000000..a55e1e9ac2 --- /dev/null +++ b/INSTALL.md @@ -0,0 +1,79 @@ +Installing From Sources +======================= + +Build Requirements +------------------ + +To compile Coq yourself, you need: + +- [OCaml](https://ocaml.org/) (version >= 4.05.0) + (This version of Coq has been tested up to OCaml 4.09.0) + +- The [num](https://github.com/ocaml/num) library; note that it is + included in the OCaml distribution for OCaml versions < 4.06.0 + +- The [findlib](http://projects.camlcity.org/projects/findlib.html) library (version >= 1.8.0) + +- GNU Make (version >= 3.81) + +- a C compiler + +- an IEEE-754 compliant architecture with rounding to nearest + ties to even as default rounding mode (most architectures + should work nowadays) + +- for CoqIDE, the + [lablgtk3-sourceview3](https://github.com/garrigue/lablgtk) library + (version >= 3.0.beta8), and the corresponding GTK 3.x libraries, as + of today (gtk+3 >= 3.18 and gtksourceview3 >= 3.18) + +The IEEE-754 compliance is required by primitive floating-point +numbers (`Require Import Floats`). Common sources of incompatibility +are checked at configure time, preventing compilation. In the, +unlikely, event an incompatibility remains undetected, using Floats +would enable to prove False on this architecture. + +Note that `num` and `lablgtk3-sourceview3` should be properly +registered with `findlib/ocamlfind` as Coq's makefile will use it to +locate the libraries during the build. + +Debian / Ubuntu users can get the necessary system packages for +CoqIDE with: + + $ sudo apt-get install libgtksourceview-3.0-dev + +Opam (https://opam.ocaml.org/) is recommended to install OCaml and +the corresponding packages. + + $ opam switch create coq 4.09.0+flambda + $ eval $(opam env) + $ opam install num ocamlfind lablgtk3-sourceview3 + +should get you a reasonable OCaml environment to compile Coq. See the +OPAM documentation for more help. + +Nix users can also get all the required dependencies by running: + + $ nix-shell + +Advanced users may want to experiment with the OCaml Flambda +compiler as way to improve the performance of Coq. In order to +profit from Flambda, a special build of the OCaml compiler that has +the Flambda optimizer enabled must be installed. For OPAM users, +this amounts to installing a compiler switch ending in `+flambda`, +such as `4.07.1+flambda`. For other users, YMMV. Once `ocamlopt -config` +reports that Flambda is available, some further optimization options +can be used; see the entry about `-flambda-opts` in the build guide +for more details. + +Build and Installation Procedure +-------------------------------- + +Coq offers the choice of two build systems, an experimental one based +on [Dune](https://github.com/ocaml/dune), and the standard +makefile-based one. + +Please see [INSTALL.make.md](dev/doc/INSTALL.make.md) for build and +installation instructions using `make`. If you wish to experiment with +the Dune-based system see the [dune guide for +developers](dev/doc/build-system.dune.md). @@ -8,359 +8,9 @@ ## # (see LICENSE file for the text of the license) ## ########################################################################## - -# Makefile for Coq -# -# To be used with GNU Make >= 3.81. -# -# This Makefile is now separated into Makefile.{common,build,doc}. -# You won't find Makefiles in sub-directories and this is done on purpose. -# If you are not yet convinced of the advantages of a single Makefile, please -# read -# http://aegis.sourceforge.net/auug97.pdf -# before complaining. -# -# When you are working in a subdir, you can compile without moving to the -# upper directory using "make -C ..", and the output is still understood -# by Emacs' next-error. -# -# Specific command-line options to this Makefile: -# -# make VERBOSE=1 # restore the raw echoing of commands -# make NO_RECALC_DEPS=1 # avoid recomputing dependencies -# -# Nota: the 1 above can be replaced by any non-empty value -# -# ---------------------------------------------------------------------- -# See dev/doc/build-system*.txt for more details/FAQ about this Makefile -# ---------------------------------------------------------------------- - - -########################################################################### -# File lists -########################################################################### - -# NB: due to limitations in Win32, please refrain using 'export' too much -# to communicate between make sub-calls (in Win32, 8kb max per env variable, -# 32kb total) - -# !! Before using FIND_SKIP_DIRS, please read how you should in the !! -# !! FIND_SKIP_DIRS section of dev/doc/build-system.dev.txt !! -FIND_SKIP_DIRS:='(' \ - -name '{arch}' -o \ - -name '.svn' -o \ - -name '_darcs' -o \ - -name '.git' -o \ - -name '.bzr' -o \ - -name 'debian' -o \ - -name "$${GIT_DIR}" -o \ - -name '_build' -o \ - -name '_build_ci' -o \ - -name '_install_ci' -o \ - -name 'gramlib' -o \ - -name 'user-contrib' -o \ - -name 'test-suite' -o \ - -name '.opamcache' -o \ - -name '.coq-native' -o \ - -name 'plugin_tutorial' \ -')' -prune -o - -define find - $(shell find . user-contrib/Ltac2 $(FIND_SKIP_DIRS) '(' -name $(1) ')' -print | sed 's|^\./||') -endef - -define findindir - $(shell find $(1) $(FIND_SKIP_DIRS) '(' -name $(2) ')' -print | sed 's|^\./||') -endef - -## Files in the source tree - -# instead of using "export FOO" do "COQ_EXPORTED += FOO" -# this makes it possible to clean up the environment in the subcall -COQ_EXPORTED := COQ_EXPORTED - -LEXFILES := $(call find, '*.mll') -YACCFILES := $(call find, '*.mly') -MLLIBFILES := $(call find, '*.mllib') -MLPACKFILES := $(call find, '*.mlpack') -MLGFILES := $(call find, '*.mlg') -CFILES := $(call findindir, 'kernel/byterun', '*.c') -COQ_EXPORTED +=MLLIBFILES MLPACKFILES MLGFILES CFILES - -# NB our find wrapper ignores the test suite -MERLININFILES := $(call find, '.merlin.in') test-suite/unit-tests/.merlin.in -MERLINFILES := $(MERLININFILES:.in=) -COQ_EXPORTED += MERLINFILES - -# NB: The lists of currently existing .ml and .mli files will change -# before and after a build or a make clean. Hence we do not export -# these variables, but cleaned-up versions (see below MLFILES and co) - -EXISTINGML := $(call find, '*.ml') -EXISTINGMLI := $(call find, '*.mli') - -## Files that will be generated - -# GRAMFILES must be in linking order -GRAMFILES=$(addprefix gramlib/.pack/gramlib__,Ploc Plexing Gramext Grammar) -GRAMMLFILES := $(addsuffix .ml, $(GRAMFILES)) -GRAMMLIFILES := $(addsuffix .mli, $(GRAMFILES)) -GENGRAMMLFILES := $(GRAMMLFILES) gramlib/.pack/gramlib.ml # why is gramlib.ml not in GRAMMLFILES? - -GENMLGFILES:= $(MLGFILES:.mlg=.ml) -GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) $(GENGRAMMLFILES) ide/coqide_os_specific.ml kernel/copcodes.ml kernel/uint63.ml -GENMLIFILES:=$(GRAMMLIFILES) -GENHFILES:=kernel/byterun/coq_instruct.h kernel/byterun/coq_jumptbl.h -GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) kernel/genOpcodeFiles.exe -COQ_EXPORTED += GRAMFILES GRAMMLFILES GRAMMLIFILES GENMLFILES GENHFILES GENFILES - -## More complex file lists - -MLSTATICFILES := $(filter-out $(GENMLFILES), $(EXISTINGML)) -MLIFILES := $(sort $(GENMLIFILES) $(EXISTINGMLI)) -COQ_EXPORTED += MLSTATICFILES MLIFILES - -export $(COQ_EXPORTED) - -include Makefile.common - -########################################################################### -# Starting rules -########################################################################### - -NOARG: world - -.PHONY: NOARG help noconfig submake camldevfiles - -help: - @echo "Please use either:" - @echo " ./configure" - @echo " make world" - @echo " make install" - @echo " make clean" - @echo "or make archclean" - @echo "For make to be verbose, add VERBOSE=1" - @echo - @echo "Bytecode compilation is now a separate target:" - @echo " make byte" - @echo " make install-byte" - @echo "Please do not mix bytecode and native targets in the same make -j" - -UNSAVED_FILES:=$(shell find . -name '.\#*v' -o -name '.\#*.ml' -o -name '.\#*.ml?') -ifdef UNSAVED_FILES -$(error You have unsaved changes in your editor (emacs?) [$(UNSAVED_FILES)]; \ -cancel them or save before proceeding. Or your editor crashed. \ -Then, you may want to consider whether you want to restore the autosaves) -#If you try to simply remove this explicit test, the compilation may -#fail later. In particular, if a .#*.v file exists, coqdep fails to -#run. -endif - -# Apart from clean and a few misc files, everything will be done in a -# sub-call to make on Makefile.build. This way, we avoid doing here -# the -include of .d : since they trigger some compilations, we do not -# want them for a mere clean. Moreover, we regroup this sub-call in a -# common target named 'submake'. This way, multiple user-given goals -# (cf the MAKECMDGOALS variable) won't trigger multiple (possibly -# parallel) make sub-calls - -ifdef COQ_CONFIGURED -%:: submake ; +# The default build system is make-based one. +ifndef COQ_USE_DUNE +include Makefile.make else -%:: noconfig ; +include Makefile.dune endif - -MAKE_OPTS := --warn-undefined-variable --no-builtin-rules - -bin: - mkdir bin - -submake: alienclean camldevfiles | bin - $(MAKE) $(MAKE_OPTS) -f Makefile.build $(MAKECMDGOALS) - -noconfig: - @echo "Please run ./configure first" >&2; exit 1 - -# To speed-up things a bit, let's dissuade make to attempt rebuilding makefiles - -Makefile $(wildcard Makefile.*) config/Makefile : ; - -########################################################################### -# OCaml dev files -########################################################################### -camldevfiles: $(MERLINFILES) META.coq - -# prevent submake dependency -META.coq.in $(MERLININFILES): ; - -.merlin: .merlin.in - cp -a "$<" "$@" - -%/.merlin: %/.merlin.in - cp -a "$<" "$@" - -META.coq: META.coq.in - cp -a "$<" "$@" - -########################################################################### -# Cleaning -########################################################################### - -.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean plugin-tutorialclean clean-ide mlgclean depclean cleanconfig distclean voclean timingclean alienclean - -clean: objclean cruftclean depclean docclean camldevfilesclean gramlibclean - -cleankeepvo: indepclean clean-ide optclean cruftclean depclean docclean - -objclean: archclean indepclean - -.PHONY: gramlibclean -gramlibclean: - rm -rf gramlib/.pack/ - -cruftclean: mlgclean - find . \( -name '*~' -o -name '*.annot' \) -exec rm -f {} + - rm -f gmon.out core - -camldevfilesclean: - rm -f $(MERLINFILES) META.coq - -indepclean: - rm -f $(GENFILES) - rm -f $(COQTOPBYTE) $(CHICKENBYTE) $(TOPBYTE) - find . \( -name '*~' -o -name '*.cm[ioat]' -o -name '*.cmti' \) -exec rm -f {} + - rm -f */*.pp[iox] plugins/*/*.pp[iox] - rm -rf $(SOURCEDOCDIR) - rm -f toplevel/mltop.byteml toplevel/mltop.optml - rm -f glob.dump - rm -f config/revision.ml revision - rm -f plugins/micromega/.micromega.ml.generated - $(MAKE) -C test-suite clean - -docclean: - rm -f doc/*/*.dvi doc/*/*.aux doc/*/*.log doc/*/*.bbl doc/*/*.blg doc/*/*.toc \ - doc/*/*.idx doc/*/*~ doc/*/*.ilg doc/*/*.ind doc/*/*.dvi.gz doc/*/*.ps.gz doc/*/*.pdf.gz\ - doc/*/*.???idx doc/*/*.???ind doc/*/*.v.tex doc/*/*.atoc doc/*/*.lof\ - doc/*/*.hatoc doc/*/*.haux doc/*/*.hcomind doc/*/*.herrind doc/*/*.hidx doc/*/*.hind \ - doc/*/*.htacind doc/*/*.htoc doc/*/*.v.html - rm -f doc/stdlib/index-list.html doc/stdlib/index-body.html \ - doc/stdlib/*Library.coqdoc.tex doc/stdlib/library.files \ - doc/stdlib/library.files.ls doc/stdlib/FullLibrary.tex - rm -f doc/*/*.ps doc/*/*.pdf doc/*/*.eps doc/*/*.pdf_t doc/*/*.eps_t - rm -rf doc/stdlib/html doc/tutorial/tutorial.v.html - rm -f doc/common/version.tex - rm -f doc/coq.tex - rm -rf doc/sphinx/_build - -archclean: clean-ide optclean voclean plugin-tutorialclean - rm -rf _build - rm -f $(ALLSTDLIB).* - -optclean: - rm -f $(COQTOPEXE) $(CHICKEN) $(TOPBINOPT) - rm -f $(TOOLS) $(PRIVATEBINARIES) $(CSDPCERT) - find . \( -name '*.cmx' -o -name '*.cmx[as]' -o -name '*.[soa]' -o -name '*.so' \) -exec rm -f {} + - -clean-ide: - rm -f $(COQIDECMO) $(COQIDECMX) $(COQIDECMO:.cmo=.cmi) $(COQIDEBYTE) $(COQIDE) - rm -f ide/input_method_lexer.ml - rm -f ide/highlight.ml ide/config_lexer.ml ide/config_parser.mli ide/config_parser.ml - rm -f ide/utf8_convert.ml - rm -f ide/default.bindings ide/default_bindings_src.exe - rm -rf $(COQIDEAPP) - -mlgclean: - rm -f $(GENMLGFILES) - -depclean: - find . $(FIND_SKIP_DIRS) '(' -name '*.d' ')' -exec rm -f {} + - -cacheclean: - find theories plugins test-suite -name '.*.aux' -exec rm -f {} + - -cleanconfig: - rm -f config/Makefile config/coq_config.ml dev/ocamldebug-coq config/Info-*.plist - -distclean: clean cleanconfig cacheclean timingclean - -voclean: - find theories plugins test-suite \( -name '*.vo' -o -name '*.vio' -o -name '*.vos' -o -name '*.vok' -o -name '*.glob' -o -name "*.cmxs" \ - -o -name "*.native" -o -name "*.cmx" -o -name "*.cmi" -o -name "*.o" \) -exec rm -f {} + - find theories plugins test-suite -name .coq-native -empty -exec rm -rf {} + - -timingclean: - find theories plugins test-suite \( -name '*.v.timing' -o -name '*.v.before-timing' \ - -o -name "*.v.after-timing" -o -name "*.v.timing.diff" -o -name "time-of-build.log" \ - -o -name "time-of-build-before.log" -o -name "time-of-build-after.log" \ - -o -name "time-of-build-pretty.log" -o -name "time-of-build-both.log" \) -exec rm -f {} + - -plugin-tutorialclean: - +$(MAKE) -C $(PLUGINTUTO) clean - -# Ensure that every compiled file around has a known source file. -# This should help preventing weird compilation failures caused by leftover -# compiled files after deleting or moving some source files. - -EXISTINGVO:=$(call find, '*.vo') -KNOWNVO:=$(patsubst %.v,%.vo,$(call find, '*.v')) -ALIENVO:=$(filter-out $(KNOWNVO),$(EXISTINGVO)) - -EXISTINGOBJS:=$(call find, '*.cm[oxia]' -o -name '*.cmxa') -KNOWNML:=$(EXISTINGML) $(GENMLFILES) $(MLPACKFILES:.mlpack=.ml) \ - $(patsubst %.mlp,%.ml,$(wildcard grammar/*.mlp)) -KNOWNOBJS:=$(KNOWNML:.ml=.cmo) $(KNOWNML:.ml=.cmx) $(KNOWNML:.ml=.cmi) \ - $(MLIFILES:.mli=.cmi) \ - gramlib/.pack/gramlib.cma gramlib/.pack/gramlib.cmxa $(MLLIBFILES:.mllib=.cma) $(MLLIBFILES:.mllib=.cmxa) grammar/grammar.cma -ALIENOBJS:=$(filter-out $(KNOWNOBJS),$(EXISTINGOBJS)) - -alienclean: - rm -f $(ALIENOBJS) $(ALIENVO) - -########################################################################### -# Continuous Intregration Tests -########################################################################### -include Makefile.ci - -########################################################################### -# Emacs tags -########################################################################### - -.PHONY: tags printenv - -tags: - echo $(filter-out checker/%, $(MLIFILES)) $(filter-out checker/%, $(MLSTATICFILES)) $(MLGFILES) | sort -r | xargs \ - etags --language=none\ - "--regex=/let[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/and[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/type[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/val[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/module[ \t]+\([^ \t]+\)/\1/" - echo $(MLGFILES) | sort -r | xargs \ - etags --append --language=none\ - "--regex=/[ \t]*\([^: \t]+\)[ \t]*:/\1/" - -checker-tags: - echo $(filter-out kernel/%, $(MLIFILES)) $(filter-out kernel/%, $(MLSTATICFILES)) $(MLGFILES) | sort -r | xargs \ - etags --language=none\ - "--regex=/let[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/and[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/type[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/val[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/module[ \t]+\([^ \t]+\)/\1/" - echo $(MLGFILES) | sort -r | xargs \ - etags --append --language=none\ - "--regex=/[ \t]*\([^: \t]+\)[ \t]*:/\1/" - -# Useful to check that the exported variables are within the win32 limits - -printenv: - @env - @echo - @echo -n "Maxsize (win32 limit is 8k) : " - @env | wc -L - @echo -n "Total (win32 limit is 32k) : " - @env | wc -m diff --git a/Makefile.make b/Makefile.make new file mode 100644 index 0000000000..c7d162bc56 --- /dev/null +++ b/Makefile.make @@ -0,0 +1,366 @@ +########################################################################## +## # The Coq Proof Assistant / The Coq Development Team ## +## v # INRIA, CNRS and contributors - Copyright 1999-2019 ## +## <O___,, # (see CREDITS file for the list of authors) ## +## \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) ## +########################################################################## + + +# Makefile for Coq +# +# To be used with GNU Make >= 3.81. +# +# This Makefile is now separated into Makefile.{common,build,doc}. +# You won't find Makefiles in sub-directories and this is done on purpose. +# If you are not yet convinced of the advantages of a single Makefile, please +# read +# http://aegis.sourceforge.net/auug97.pdf +# before complaining. +# +# When you are working in a subdir, you can compile without moving to the +# upper directory using "make -C ..", and the output is still understood +# by Emacs' next-error. +# +# Specific command-line options to this Makefile: +# +# make VERBOSE=1 # restore the raw echoing of commands +# make NO_RECALC_DEPS=1 # avoid recomputing dependencies +# +# Nota: the 1 above can be replaced by any non-empty value +# +# ---------------------------------------------------------------------- +# See dev/doc/build-system*.txt for more details/FAQ about this Makefile +# ---------------------------------------------------------------------- + + +########################################################################### +# File lists +########################################################################### + +# NB: due to limitations in Win32, please refrain using 'export' too much +# to communicate between make sub-calls (in Win32, 8kb max per env variable, +# 32kb total) + +# !! Before using FIND_SKIP_DIRS, please read how you should in the !! +# !! FIND_SKIP_DIRS section of dev/doc/build-system.dev.txt !! +FIND_SKIP_DIRS:='(' \ + -name '{arch}' -o \ + -name '.svn' -o \ + -name '_darcs' -o \ + -name '.git' -o \ + -name '.bzr' -o \ + -name 'debian' -o \ + -name "$${GIT_DIR}" -o \ + -name '_build' -o \ + -name '_build_ci' -o \ + -name '_install_ci' -o \ + -name 'gramlib' -o \ + -name 'user-contrib' -o \ + -name 'test-suite' -o \ + -name '.opamcache' -o \ + -name '.coq-native' -o \ + -name 'plugin_tutorial' \ +')' -prune -o + +define find + $(shell find . user-contrib/Ltac2 $(FIND_SKIP_DIRS) '(' -name $(1) ')' -print | sed 's|^\./||') +endef + +define findindir + $(shell find $(1) $(FIND_SKIP_DIRS) '(' -name $(2) ')' -print | sed 's|^\./||') +endef + +## Files in the source tree + +# instead of using "export FOO" do "COQ_EXPORTED += FOO" +# this makes it possible to clean up the environment in the subcall +COQ_EXPORTED := COQ_EXPORTED + +LEXFILES := $(call find, '*.mll') +YACCFILES := $(call find, '*.mly') +MLLIBFILES := $(call find, '*.mllib') +MLPACKFILES := $(call find, '*.mlpack') +MLGFILES := $(call find, '*.mlg') +CFILES := $(call findindir, 'kernel/byterun', '*.c') +COQ_EXPORTED +=MLLIBFILES MLPACKFILES MLGFILES CFILES + +# NB our find wrapper ignores the test suite +MERLININFILES := $(call find, '.merlin.in') test-suite/unit-tests/.merlin.in +MERLINFILES := $(MERLININFILES:.in=) +COQ_EXPORTED += MERLINFILES + +# NB: The lists of currently existing .ml and .mli files will change +# before and after a build or a make clean. Hence we do not export +# these variables, but cleaned-up versions (see below MLFILES and co) + +EXISTINGML := $(call find, '*.ml') +EXISTINGMLI := $(call find, '*.mli') + +## Files that will be generated + +# GRAMFILES must be in linking order +GRAMFILES=$(addprefix gramlib/.pack/gramlib__,Ploc Plexing Gramext Grammar) +GRAMMLFILES := $(addsuffix .ml, $(GRAMFILES)) +GRAMMLIFILES := $(addsuffix .mli, $(GRAMFILES)) +GENGRAMMLFILES := $(GRAMMLFILES) gramlib/.pack/gramlib.ml # why is gramlib.ml not in GRAMMLFILES? + +GENMLGFILES:= $(MLGFILES:.mlg=.ml) +GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) $(GENGRAMMLFILES) ide/coqide_os_specific.ml kernel/copcodes.ml kernel/uint63.ml +GENMLIFILES:=$(GRAMMLIFILES) +GENHFILES:=kernel/byterun/coq_instruct.h kernel/byterun/coq_jumptbl.h +GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) kernel/genOpcodeFiles.exe +COQ_EXPORTED += GRAMFILES GRAMMLFILES GRAMMLIFILES GENMLFILES GENHFILES GENFILES + +## More complex file lists + +MLSTATICFILES := $(filter-out $(GENMLFILES), $(EXISTINGML)) +MLIFILES := $(sort $(GENMLIFILES) $(EXISTINGMLI)) +COQ_EXPORTED += MLSTATICFILES MLIFILES + +export $(COQ_EXPORTED) + +include Makefile.common + +########################################################################### +# Starting rules +########################################################################### + +NOARG: world + +.PHONY: NOARG help noconfig submake camldevfiles + +help: + @echo "Please use either:" + @echo " ./configure" + @echo " make world" + @echo " make install" + @echo " make clean" + @echo "or make archclean" + @echo "For make to be verbose, add VERBOSE=1" + @echo + @echo "Bytecode compilation is now a separate target:" + @echo " make byte" + @echo " make install-byte" + @echo "Please do not mix bytecode and native targets in the same make -j" + +UNSAVED_FILES:=$(shell find . -name '.\#*v' -o -name '.\#*.ml' -o -name '.\#*.ml?') +ifdef UNSAVED_FILES +$(error You have unsaved changes in your editor (emacs?) [$(UNSAVED_FILES)]; \ +cancel them or save before proceeding. Or your editor crashed. \ +Then, you may want to consider whether you want to restore the autosaves) +#If you try to simply remove this explicit test, the compilation may +#fail later. In particular, if a .#*.v file exists, coqdep fails to +#run. +endif + +# Apart from clean and a few misc files, everything will be done in a +# sub-call to make on Makefile.build. This way, we avoid doing here +# the -include of .d : since they trigger some compilations, we do not +# want them for a mere clean. Moreover, we regroup this sub-call in a +# common target named 'submake'. This way, multiple user-given goals +# (cf the MAKECMDGOALS variable) won't trigger multiple (possibly +# parallel) make sub-calls + +ifdef COQ_CONFIGURED +%:: submake ; +else +%:: noconfig ; +endif + +MAKE_OPTS := --warn-undefined-variable --no-builtin-rules + +bin: + mkdir bin + +submake: alienclean camldevfiles | bin + $(MAKE) $(MAKE_OPTS) -f Makefile.build $(MAKECMDGOALS) + +noconfig: + @echo "Please run ./configure first" >&2; exit 1 + +# To speed-up things a bit, let's dissuade make to attempt rebuilding makefiles + +Makefile $(wildcard Makefile.*) config/Makefile : ; + +########################################################################### +# OCaml dev files +########################################################################### +camldevfiles: $(MERLINFILES) META.coq + +# prevent submake dependency +META.coq.in $(MERLININFILES): ; + +.merlin: .merlin.in + cp -a "$<" "$@" + +%/.merlin: %/.merlin.in + cp -a "$<" "$@" + +META.coq: META.coq.in + cp -a "$<" "$@" + +########################################################################### +# Cleaning +########################################################################### + +.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean plugin-tutorialclean clean-ide mlgclean depclean cleanconfig distclean voclean timingclean alienclean + +clean: objclean cruftclean depclean docclean camldevfilesclean gramlibclean + +cleankeepvo: indepclean clean-ide optclean cruftclean depclean docclean + +objclean: archclean indepclean + +.PHONY: gramlibclean +gramlibclean: + rm -rf gramlib/.pack/ + +cruftclean: mlgclean + find . \( -name '*~' -o -name '*.annot' \) -exec rm -f {} + + rm -f gmon.out core + +camldevfilesclean: + rm -f $(MERLINFILES) META.coq + +indepclean: + rm -f $(GENFILES) + rm -f $(COQTOPBYTE) $(CHICKENBYTE) $(TOPBYTE) + find . \( -name '*~' -o -name '*.cm[ioat]' -o -name '*.cmti' \) -exec rm -f {} + + rm -f */*.pp[iox] plugins/*/*.pp[iox] + rm -rf $(SOURCEDOCDIR) + rm -f toplevel/mltop.byteml toplevel/mltop.optml + rm -f glob.dump + rm -f config/revision.ml revision + rm -f plugins/micromega/.micromega.ml.generated + $(MAKE) -C test-suite clean + +docclean: + rm -f doc/*/*.dvi doc/*/*.aux doc/*/*.log doc/*/*.bbl doc/*/*.blg doc/*/*.toc \ + doc/*/*.idx doc/*/*~ doc/*/*.ilg doc/*/*.ind doc/*/*.dvi.gz doc/*/*.ps.gz doc/*/*.pdf.gz\ + doc/*/*.???idx doc/*/*.???ind doc/*/*.v.tex doc/*/*.atoc doc/*/*.lof\ + doc/*/*.hatoc doc/*/*.haux doc/*/*.hcomind doc/*/*.herrind doc/*/*.hidx doc/*/*.hind \ + doc/*/*.htacind doc/*/*.htoc doc/*/*.v.html + rm -f doc/stdlib/index-list.html doc/stdlib/index-body.html \ + doc/stdlib/*Library.coqdoc.tex doc/stdlib/library.files \ + doc/stdlib/library.files.ls doc/stdlib/FullLibrary.tex + rm -f doc/*/*.ps doc/*/*.pdf doc/*/*.eps doc/*/*.pdf_t doc/*/*.eps_t + rm -rf doc/stdlib/html doc/tutorial/tutorial.v.html + rm -f doc/common/version.tex + rm -f doc/coq.tex + rm -rf doc/sphinx/_build + +archclean: clean-ide optclean voclean plugin-tutorialclean + rm -rf _build + rm -f $(ALLSTDLIB).* + +optclean: + rm -f $(COQTOPEXE) $(CHICKEN) $(TOPBINOPT) + rm -f $(TOOLS) $(PRIVATEBINARIES) $(CSDPCERT) + find . \( -name '*.cmx' -o -name '*.cmx[as]' -o -name '*.[soa]' -o -name '*.so' \) -exec rm -f {} + + +clean-ide: + rm -f $(COQIDECMO) $(COQIDECMX) $(COQIDECMO:.cmo=.cmi) $(COQIDEBYTE) $(COQIDE) + rm -f ide/input_method_lexer.ml + rm -f ide/highlight.ml ide/config_lexer.ml ide/config_parser.mli ide/config_parser.ml + rm -f ide/utf8_convert.ml + rm -f ide/default.bindings ide/default_bindings_src.exe + rm -rf $(COQIDEAPP) + +mlgclean: + rm -f $(GENMLGFILES) + +depclean: + find . $(FIND_SKIP_DIRS) '(' -name '*.d' ')' -exec rm -f {} + + +cacheclean: + find theories plugins test-suite -name '.*.aux' -exec rm -f {} + + +cleanconfig: + rm -f config/Makefile config/coq_config.ml dev/ocamldebug-coq config/Info-*.plist + +distclean: clean cleanconfig cacheclean timingclean + +voclean: + find theories plugins test-suite \( -name '*.vo' -o -name '*.vio' -o -name '*.vos' -o -name '*.vok' -o -name '*.glob' -o -name "*.cmxs" \ + -o -name "*.native" -o -name "*.cmx" -o -name "*.cmi" -o -name "*.o" \) -exec rm -f {} + + find theories plugins test-suite -name .coq-native -empty -exec rm -rf {} + + +timingclean: + find theories plugins test-suite \( -name '*.v.timing' -o -name '*.v.before-timing' \ + -o -name "*.v.after-timing" -o -name "*.v.timing.diff" -o -name "time-of-build.log" \ + -o -name "time-of-build-before.log" -o -name "time-of-build-after.log" \ + -o -name "time-of-build-pretty.log" -o -name "time-of-build-both.log" \) -exec rm -f {} + + +plugin-tutorialclean: + +$(MAKE) -C $(PLUGINTUTO) clean + +# Ensure that every compiled file around has a known source file. +# This should help preventing weird compilation failures caused by leftover +# compiled files after deleting or moving some source files. + +EXISTINGVO:=$(call find, '*.vo') +KNOWNVO:=$(patsubst %.v,%.vo,$(call find, '*.v')) +ALIENVO:=$(filter-out $(KNOWNVO),$(EXISTINGVO)) + +EXISTINGOBJS:=$(call find, '*.cm[oxia]' -o -name '*.cmxa') +KNOWNML:=$(EXISTINGML) $(GENMLFILES) $(MLPACKFILES:.mlpack=.ml) \ + $(patsubst %.mlp,%.ml,$(wildcard grammar/*.mlp)) +KNOWNOBJS:=$(KNOWNML:.ml=.cmo) $(KNOWNML:.ml=.cmx) $(KNOWNML:.ml=.cmi) \ + $(MLIFILES:.mli=.cmi) \ + gramlib/.pack/gramlib.cma gramlib/.pack/gramlib.cmxa $(MLLIBFILES:.mllib=.cma) $(MLLIBFILES:.mllib=.cmxa) grammar/grammar.cma +ALIENOBJS:=$(filter-out $(KNOWNOBJS),$(EXISTINGOBJS)) + +alienclean: + rm -f $(ALIENOBJS) $(ALIENVO) + +########################################################################### +# Continuous Intregration Tests +########################################################################### +include Makefile.ci + +########################################################################### +# Emacs tags +########################################################################### + +.PHONY: tags printenv + +tags: + echo $(filter-out checker/%, $(MLIFILES)) $(filter-out checker/%, $(MLSTATICFILES)) $(MLGFILES) | sort -r | xargs \ + etags --language=none\ + "--regex=/let[ \t]+\([^ \t]+\)/\1/" \ + "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \ + "--regex=/and[ \t]+\([^ \t]+\)/\1/" \ + "--regex=/type[ \t]+\([^ \t]+\)/\1/" \ + "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \ + "--regex=/val[ \t]+\([^ \t]+\)/\1/" \ + "--regex=/module[ \t]+\([^ \t]+\)/\1/" + echo $(MLGFILES) | sort -r | xargs \ + etags --append --language=none\ + "--regex=/[ \t]*\([^: \t]+\)[ \t]*:/\1/" + +checker-tags: + echo $(filter-out kernel/%, $(MLIFILES)) $(filter-out kernel/%, $(MLSTATICFILES)) $(MLGFILES) | sort -r | xargs \ + etags --language=none\ + "--regex=/let[ \t]+\([^ \t]+\)/\1/" \ + "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \ + "--regex=/and[ \t]+\([^ \t]+\)/\1/" \ + "--regex=/type[ \t]+\([^ \t]+\)/\1/" \ + "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \ + "--regex=/val[ \t]+\([^ \t]+\)/\1/" \ + "--regex=/module[ \t]+\([^ \t]+\)/\1/" + echo $(MLGFILES) | sort -r | xargs \ + etags --append --language=none\ + "--regex=/[ \t]*\([^: \t]+\)[ \t]*:/\1/" + +# Useful to check that the exported variables are within the win32 limits + +printenv: + @env + @echo + @echo -n "Maxsize (win32 limit is 8k) : " + @env | wc -L + @echo -n "Total (win32 limit is 32k) : " + @env | wc -m @@ -54,7 +54,7 @@ environment for semi-interactive development of machine-checked proofs. Download the pre-built packages of the [latest release][] for Windows and macOS; read the [help page][opam-using] on how to install Coq with OPAM; -or refer to the [`INSTALL`](INSTALL) file for the procedure to install from source. +or refer to the [`INSTALL.md`](INSTALL.md) file for the procedure to install from source. [latest release]: https://github.com/coq/coq/releases/latest [opam-using]: https://coq.inria.fr/opam/www/using.html diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 82cc7a7117..b1c752ba60 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1385,7 +1385,7 @@ function copy_coq_license { # FIXME: this is not the micromega license # It only applies to code that was copied into one single file! install -D README.md "$PREFIXCOQ/license_readme/coq/ReadMe.md" - install -D INSTALL "$PREFIXCOQ/license_readme/coq/Install.txt" + install -D INSTALL.md "$PREFIXCOQ/license_readme/coq/Install.txt" install -D doc/README.md "$PREFIXCOQ/license_readme/coq/ReadMeDoc.md" || true fi } diff --git a/dev/doc/INSTALL.make.md b/dev/doc/INSTALL.make.md new file mode 100644 index 0000000000..3db5d0b14f --- /dev/null +++ b/dev/doc/INSTALL.make.md @@ -0,0 +1,258 @@ +Quick Installation Procedure using Make. +---------------------------------------- + + $ ./configure + $ make + $ make install (you may need superuser rights) + +Detailed Installation Procedure. +-------------------------------- + +1. Check that you have the OCaml compiler installed on your + computer and that `ocamlc` (or, better, its native code version + `ocamlc.opt`) is in a directory which is present in your $PATH + environment variable. At the time of writing this document, all + versions of Objective Caml later or equal to 4.05.0 are + supported. + + To get Coq in native-code, (which runs 4 to 10 times faster than + bytecode, but it takes more time to get compiled and the binary is + bigger), you will also need the `ocamlopt` (or its native code version + `ocamlopt.opt`) command. + +2. The uncompression and un-tarring of the distribution file gave birth + to a directory named "coq-8.xx". You can rename this directory and put + it wherever you want. Just keep in mind that you will need some spare + space during the compilation (reckon on about 300 Mb of disk space + for the whole system in native-code compilation). Once installed, the + binaries take about 30 Mb, and the library about 200 Mb. + +3. First you need to configure the system. It is done automatically with + the command: + + ./configure <options> + + The `configure` script will ask you for directories where to put + the Coq binaries, standard library, man pages, etc. It will propose + default values. + + For a list of options accepted by the `configure` script, run + `./configure -help`. The main options accepted are: + + * `-prefix <dir>` + Binaries, library, and man pages will be respectively + installed in `<dir>/bin`, `<dir>/lib/coq`, and `<dir>/man` + + * `-bindir <dir>` (default: `/usr/local/bin`) + Directory where the binaries will be installed + + * `-libdir <dir>` (default: `/usr/local/lib/coq`) + Directory where the Coq standard library will be installed + + * `-mandir <dir>` (default: `/usr/local/share/man`) + Directory where the Coq manual pages will be installed + + * `-arch <value>` (default is the result of the command `arch`) + An arbitrary architecture name for your machine (useful when + compiling Coq on two different architectures for which the + result of "arch" is the same, e.g. Sun OS and Solaris) + + * `-local` + Compile Coq to run in its source directory. The installation (step 6) + is not necessary in that case. + + * `-browser <command>` + Use <command> to open an URL in a browser. %s must appear in <command>, + and will be replaced by the URL. + + * `-flambda-opts <flags>` + This experimental option will pass specific user flags to the + OCaml optimizing compiler. In most cases, this option is used + to tweak the flambda backend; for maximum performance we + recommend using: + + -flambda-opts `-O3 -unbox-closures` + + but of course you are free to try with a different combination + of flags. You can read more at + https://caml.inria.fr/pub/docs/manual-ocaml/flambda.html + + There is a known problem with certain OCaml versions and + `native_compute`, that will make compilation to require + a large amount of RAM (>= 10GiB) in some particular files. + + We recommend disabling native compilation (`-native-compiler no`) + with flambda unless you use OCaml >= 4.07.0. + + c.f. https://caml.inria.fr/mantis/view.php?id=7630 + + If you want your build to be reproducible, ensure that the + SOURCE_DATE_EPOCH environment variable is set as documented in + https://reproducible-builds.org/specs/source-date-epoch/ + +4. Still in the root directory, do + + make + + to compile Coq in the best OCaml mode available (native-code if supported, + bytecode otherwise). + + This will compile the entire system. This phase can take more or less time, + depending on your architecture and is fairly verbose. On a multi-core machine, + it is recommended to compile in parallel, via make -jN where N is your number + of cores. + +5. You can now install the Coq system. Executables, libraries, and + manual pages are copied in some standard places of your system, + defined at configuration time (step 3). Just do + + umask 022 + make install + + Of course, you may need superuser rights to do that. + +6. Optionally, you could build the bytecode version of Coq via: + + make byte + + and install it via + + make install-byte + + This version is much slower than the native code version of Coq, but could + be helpful for debugging purposes. In particular, coqtop.byte embeds an OCaml + toplevel accessible via the Drop command. + +7. You can now clean all the sources. (You can even erase them.) + + make clean + +Installation Procedure For Plugin Developers. +--------------------------------------------- + +If you wish to write plugins you *must* keep the Coq sources, without +cleaning them. Therefore, to avoid a duplication of binaries and library, +it is not necessary to do the installation step (6- above). You just have +to tell it at configuration step (4- above) with the option -local : + + ./configure -local <other options> + +Then compile the sources as described in step 5 above. The resulting +binaries will reside in the subdirectory bin/. + +Unless you pass the -nodebug option to ./configure, the -g option of the +OCaml compiler will be used during compilation to allow debugging. +See the debugging file in dev/doc and the chapter 15 of the Coq Reference +Manual for details about how to use the OCaml debugger with Coq. + + +The Available Commands. +----------------------- + +There are two Coq commands: + + coqtop The Coq toplevel + coqc The Coq compiler + +Under architecture where ocamlopt is available, coqtop is the native code +version of Coq. On such architecture, you could additionally request +the build of the bytecode version of Coq via 'make byte' and install it via +'make install-byte'. This will create an extra binary named coqtop.byte, +that could be used for debugging purpose. If native code isn't available, +coqtop.byte is directly built by 'make', and coqtop is a link to coqtop.byte. +coqc also invokes the fastest version of Coq. Options -opt and -byte to coqtop +and coqc selects a particular binary. + +* `coqtop` launches Coq in the interactive mode. By default it loads + basic logical definitions and tactics from the Init directory. + +* `coqc` allows compilation of Coq files directly from the command line. + To compile a file foo.v, do: + + coqc foo.v + + It will produce a file `foo.vo`, that you can now load through the Coq + command `Require`. + + A detailed description of these commands and of their options is given + in the Reference Manual (which you can get in the doc/ + directory, or read online on http://coq.inria.fr/doc/) + and in the corresponding manual pages. + +Compiling For Different Architectures. +-------------------------------------- + +This section explains how to compile Coq for several architecture, sharing +the same sources. The important fact is that some files are architecture +dependent (`.cmx`, `.o` and executable files for instance) but others are not +(`.cmo` and `.vo`). Consequently, you can : + +- save some time during compilation by not cleaning the architecture + independent files; + +- save some space during installation by sharing the Coq standard + library (which is fully architecture independent). + +So, in order to compile Coq for a new architecture, proceed as follows: + +* Omit step 7 above and clean only the architecture dependent files: + it is done automatically with the command + + make archclean + +* Configure the system for the new architecture: + + ./configure <options> + + You can specify the same directory for the standard library but you + MUST specify a different directory for the binaries (of course). + +* Compile and install the system as described in steps 5 and 6 above. + +Moving Binaries Or Library. +--------------------------- + +If you move both the binaries and the library in a consistent way, +Coq should be able to still run. Otherwise, Coq may be "lost", +running "coqtop" would then return an error message of the kind: + + Error during initialization : + Error: cannot guess a path for Coq libraries; please use -coqlib option + +You can then indicate the new places to Coq, using the options -coqlib : + + coqtop -coqlib <new directory> + +See also next section. + +Dynamically Loaded Libraries For Bytecode Executables. +------------------------------------------------------ + +Some bytecode executables of Coq use the OCaml runtime, which dynamically +loads a shared library (.so or .dll). When it is not installed properly, you +can get an error message of this kind: + + Fatal error: cannot load shared library dllcoqrun + Reason: dllcoqrun.so: cannot open shared object file: No such file or directory + +In this case, you need either: + +- to set the `CAML_LD_LIBRARY_PATH` environment variable to point to the + directory where dllcoqrun.so is; this is suitable when you want to run + the command a limited number of times in a controlled environment (e.g. + during compilation of binary packages); +- install dllcoqrun.so in a location listed in the file ld.conf that is in + the directory of the standard library of OCaml; +- recompile your bytecode executables after reconfiguring the location + of the shared library: + + ./configure -vmbyteflags "-dllib,-lcoqrun,-dllpath,<path>" ... + + where `<path>` is the directory where the dllcoqrun.so is installed; +- (not recommended) compile bytecode executables with a custom OCaml + runtime by using: + + ./configure -custom ... + + be aware that stripping executables generated this way, or performing + other executable-specific operations, will make them useless. diff --git a/doc/README.md b/doc/README.md index b784fe92f6..ef3ccc2105 100644 --- a/doc/README.md +++ b/doc/README.md @@ -27,7 +27,7 @@ Dependencies ### HTML documentation To produce the complete documentation in HTML, you will need Coq dependencies -listed in [`INSTALL`](../INSTALL). Additionally, the Sphinx-based +listed in [`INSTALL.md`](../INSTALL.md). Additionally, the Sphinx-based reference manual requires Python 3, and the following Python packages: - sphinx >= 1.7.8 |