diff options
| -rw-r--r-- | .gitignore | 1 | ||||
| -rw-r--r-- | INSTALL.doc | 24 | ||||
| -rwxr-xr-x | dev/ci/ci-vst.sh | 10 | ||||
| -rw-r--r-- | tools/CoqMakefile.in | 2 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 20 |
5 files changed, 42 insertions, 15 deletions
diff --git a/.gitignore b/.gitignore index 25c0996cb2..e2a97b3a12 100644 --- a/.gitignore +++ b/.gitignore @@ -61,6 +61,7 @@ plugins/micromega/csdpcert plugins/micromega/.micromega.ml.generated kernel/byterun/dllcoqrun.so coqdoc.sty +coqdoc.css time-of-build.log time-of-build-pretty.log time-of-build-before.log diff --git a/INSTALL.doc b/INSTALL.doc index 8c578fbd61..f8a0852805 100644 --- a/INSTALL.doc +++ b/INSTALL.doc @@ -31,16 +31,26 @@ To produce all the documents, the following tools are needed: - Antlr4 runtime for Python 3 -Under Debian based operating systems (Debian, Ubuntu, ...) a -working set of packages for compiling the documentation for Coq is: +Under recent Debian based operating systems (Debian 10 "Buster", +Ubuntu 18.04, ...) a working set of packages for compiling the +documentation for Coq is: - texlive texlive-latex-extra texlive-math-extra texlive-fonts-extra - texlive-humanities texlive-pictures latex-xcolor hevea python3 - python-pip3 + texlive-latex-extra texlive-fonts-recommended hevea python3-sphinx + python3-pexpect python3-sphinx-rtd-theme python3-bs4 + python3-sphinxcontrib.bibtex python3-pip -To install the Python packages required to build the user manual, run: - pip3 install sphinx sphinx_rtd_theme beautifulsoup4 antlr4-python3-runtime pexpect sphinxcontrib-bibtex +Then, install the Python3 Antlr4 package: + + pip3 install antlr4-python3-runtime + +Nix users should get the correct development environment to build the +Sphinx documentation from Coq's `default.nix`. [Note Nix setup doesn't +include the LaTeX packages needed to build the full documentation.] +If you are in an older/different distribution you can install the +Python packages required to build the user manual using python3-pip: + + pip3 install sphinx sphinx_rtd_theme beautifulsoup4 antlr4-python3-runtime pexpect sphinxcontrib-bibtex Compilation ----------- diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh index 3c0044bfe9..3817edf0c4 100755 --- a/dev/ci/ci-vst.sh +++ b/dev/ci/ci-vst.sh @@ -8,6 +8,10 @@ VST_CI_DIR="${CI_BUILD_DIR}/VST" # opam install -j ${NJOBS} -y menhir git_checkout "${VST_CI_BRANCH}" "${VST_CI_GITURL}" "${VST_CI_DIR}" -# Targets are: msl veric floyd progs , we remove progs to save time -# Patch to avoid the upper version limit -( cd "${VST_CI_DIR}" && make IGNORECOQVERSION=true .loadpath version.vo msl veric floyd ) +# HACK: from the upstream makefile: +# +# default_target: _CoqProject version.vo msl veric floyd progs +# +# We have to omit progs as otherwise we timeout on Travis; once we +# move to Gitlab we will able to just use `make` +( cd "${VST_CI_DIR}" && make IGNORECOQVERSION=true _CoqProject version.vo msl veric floyd ) diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index f6539d80be..e5f22f25e1 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -382,7 +382,7 @@ real-all: $(VOFILES) $(if $(USEBYTE),bytefiles,optfiles) .PHONY: real-all real-all.timing.diff: $(VOFILES:.vo=.v.timing.diff) -.PHONE: real-all.timing.diff +.PHONY: real-all.timing.diff bytefiles: $(CMOFILES) $(CMAFILES) .PHONY: bytefiles diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 668f9b8935..e60382f2ce 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -435,10 +435,22 @@ let init_toplevel arglist = * early since the master waits us to connect back *) Spawned.init_channels (); Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg)); - if opts.print_where then (print_endline(Envars.coqlib ()); exit(exitcode opts)); - if opts.print_config then (Envars.print_config stdout Coq_config.all_src_dirs; exit (exitcode opts)); - if opts.print_tags then (print_style_tags opts; exit (exitcode opts)); - if opts.filter_opts then (print_string (String.concat "\n" extras); exit 0); + if opts.print_where then begin + print_endline (Envars.coqlib ()); + exit (exitcode opts) + end; + if opts.print_config then begin + Envars.print_config stdout Coq_config.all_src_dirs; + exit (exitcode opts) + end; + if opts.print_tags then begin + print_style_tags opts; + exit (exitcode opts) + end; + if opts.filter_opts then begin + print_string (String.concat "\n" extras); + exit 0; + end; let top_lp = Coqinit.toplevel_init_load_path () in List.iter Mltop.add_coq_path top_lp; Option.iter Mltop.load_ml_object_raw opts.toploop; |