From 728216337e2541b37135d86c1b0206706cf4ed1a Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 19 Feb 2019 18:23:42 +0100 Subject: [coq_makefile] Enforce warn_error for plugins. The amount of dangerous warnings in plugins is out of hand, including some very serious ones. As Coq developers are maintaining plugins these days it makes sense to require the contributions to follow the same coding discipline as in the main tree, thus we require the set of warnings fatal warnings to be the same in Coq and in plugins. We don't mark deprecation as fatal as to allow time for migration. Fixes #6974 --- .gitlab-ci.yml | 2 +- Makefile.ci | 2 +- dev/ci/README-users.md | 20 ++++++++++++++++++++ dev/ci/ci-basic-overlay.sh | 2 +- dev/ci/ci-relation-algebra.sh | 8 -------- dev/ci/ci-relation_algebra.sh | 8 ++++++++ dev/doc/changes.md | 9 +++++++++ doc/sphinx/practical-tools/utilities.rst | 4 ++++ lib/envars.ml | 1 + tools/CoqMakefile.in | 5 +++-- 10 files changed, 48 insertions(+), 13 deletions(-) delete mode 100755 dev/ci/ci-relation-algebra.sh create mode 100755 dev/ci/ci-relation_algebra.sh diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 3c427793e2..b074427892 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -662,5 +662,5 @@ plugin:plugin-tutorial: plugin:ci-quickchick: extends: .ci-template-flambda -plugin:ci-relation-algebra: +plugin:ci-relation_algebra: extends: .ci-template diff --git a/Makefile.ci b/Makefile.ci index 000725b6b1..a244c17ef3 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -38,7 +38,7 @@ CI_TARGETS= \ ci-mtac2 \ ci-paramcoq \ ci-quickchick \ - ci-relation-algebra \ + ci-relation_algebra \ ci-sf \ ci-simple-io \ ci-stdlib2 \ diff --git a/dev/ci/README-users.md b/dev/ci/README-users.md index 01769aeddb..06b617d4c1 100644 --- a/dev/ci/README-users.md +++ b/dev/ci/README-users.md @@ -45,6 +45,26 @@ using [coqbot](https://github.com/coq/bot); meanwhile, a workaround is to give merge permissions to someone from the Coq team as to help with these kind of merges. +### OCaml and plugin-specific considerations + +Developments that link against Coq's OCaml API [most of them are known +as "plugins"] do have some special requirements: + +- Coq's OCaml API is not stable. We hope to improve this in the future + but as of today you should expect to have to merge a fair amount of + "overlays", usually in the form of Pull Requests from Coq developers + in order to keep your plugin compatible with Coq master. + + In order to alleviate the load, you can delegate the merging of such + compatibility pull requests to Coq developers themselves, by + granting access to the plugin repository or by using `bots` such as + [Bors](https://github.com/apps/bors) that allow for automatic + management of Pull Requests. + +- Plugins in the CI should compile with the OCaml flags that Coq + uses. In particular, warnings that are considered fatal by the Coq + developers _must_ be also fatal for plugin CI code. + ### Add your development by submitting a pull request Add a new `ci-mydev.sh` script to [`dev/ci`](.); set the corresponding diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 0c89809ee9..4f5988c59c 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -254,7 +254,7 @@ : "${paramcoq_CI_ARCHIVEURL:=${paramcoq_CI_GITURL}/archive}" ######################################################################## -# relation-algebra +# relation_algebra ######################################################################## : "${relation_algebra_CI_REF:=master}" : "${relation_algebra_CI_GITURL:=https://github.com/damien-pous/relation-algebra}" diff --git a/dev/ci/ci-relation-algebra.sh b/dev/ci/ci-relation-algebra.sh deleted file mode 100755 index 84bed5bdfe..0000000000 --- a/dev/ci/ci-relation-algebra.sh +++ /dev/null @@ -1,8 +0,0 @@ -#!/usr/bin/env bash - -ci_dir="$(dirname "$0")" -. "${ci_dir}/ci-common.sh" - -git_download relation_algebra - -( cd "${CI_BUILD_DIR}/relation_algebra" && make && make install ) diff --git a/dev/ci/ci-relation_algebra.sh b/dev/ci/ci-relation_algebra.sh new file mode 100755 index 0000000000..84bed5bdfe --- /dev/null +++ b/dev/ci/ci-relation_algebra.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download relation_algebra + +( cd "${CI_BUILD_DIR}/relation_algebra" && make && make install ) diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 40c3c32e4f..4533a4dc01 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -20,6 +20,15 @@ General deprecation removed. Please, make sure your plugin is warning-free in 8.8 before trying to port it over 8.9. +Warnings + +- Coq now builds plugins with `-warn-error` enabled by default. The + amount of dangerous warnings in plugin code was very high, so we now + require plugins in the CI to adhere to the Coq warning policy. We + _strongly_ recommend against disabling the default set of warnings. + If you have special needs, see the documentation of your build + system and/or OCaml for further help. + Names - Kernel names no longer contain a section path. They now have only two diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 8346b72cb9..35231610fe 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -144,6 +144,10 @@ Here we describe only few of them. :CAMLFLAGS: can be used to specify additional flags to the |OCaml| compiler, like ``-bin-annot`` or ``-w``.... +:OCAMLWARN: + it contains a default of ``-warn-error +a-3``, useful to modify + this setting; beware this is not recommended for projects in + Coq's CI. :COQC, COQDEP, COQDOC: can be set in order to use alternative binaries (e.g. wrappers) diff --git a/lib/envars.ml b/lib/envars.ml index 0f4670688b..af8e45b137 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -178,6 +178,7 @@ let print_config ?(prefix_var_name="") f coq_src_subdirs = fprintf f "%sDOCDIR=%s/\n" prefix_var_name (docdir ()); fprintf f "%sOCAMLFIND=%s\n" prefix_var_name (ocamlfind ()); fprintf f "%sCAMLFLAGS=%s\n" prefix_var_name Coq_config.caml_flags; + fprintf f "%sWARN=%s\n" prefix_var_name "-warn-error +a-3"; fprintf f "%sHASNATDYNLINK=%s\n" prefix_var_name (if Coq_config.has_natdynlink then "true" else "false"); fprintf f "%sCOQ_SRC_SUBDIRS=%s\n" prefix_var_name (String.concat " " coq_src_subdirs) diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 0236c549d5..48b797a3cd 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -38,6 +38,7 @@ DOCDIR := $(COQMF_DOCDIR) OCAMLFIND := $(COQMF_OCAMLFIND) CAMLFLAGS := $(COQMF_CAMLFLAGS) HASNATDYNLINK := $(COQMF_HASNATDYNLINK) +OCAMLWARN := $(COQMF_WARN) @CONF_FILE@: @PROJECT_FILE@ @COQ_MAKEFILE_INVOCATION@ @@ -190,9 +191,9 @@ COQMAKEFILE_VERSION:=@COQ_VERSION@ COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)/$(d)") CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) - # ocamldoc fails with unknown argument otherwise -CAMLDOCFLAGS=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS))) +CAMLDOCFLAGS:=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS))) +CAMLFLAGS+=$(OCAMLWARN) ifneq (,$(TIMING)) TIMING_ARG=-time -- cgit v1.2.3