Merge PR #13007: [build] Don't link `num` anymore in Coq

Reviewed-by: Zimmi48
Reviewed-by: vbgl
Ack-by: Zimmi48
Ack-by: vbgl

14 files changed, 35 insertions, 46 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 4a57c6bc68..16f82a19ee 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -19,7 +19,7 @@ stages:
 variables:
   # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here
   # for reference]
-  CACHEKEY: "bionic_coq-V2020-09-16-V38"
+  CACHEKEY: "bionic_coq-V2020-09-17-V88"
   IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
   # By default, jobs run in the base switch; override to select another switch
   OPAM_SWITCH: "base"
@@ -605,7 +605,7 @@ test-suite:edge:dune:dev:
     - opam repo add ocaml-beta https://github.com/ocaml/ocaml-beta-repository.git
     - opam update
     - opam install ocaml-variants=$OCAMLVER
-    - opam install dune num zarith
+    - opam install dune zarith
     - eval $(opam env)
     - export COQ_UNIT_TEST=noop
     - make -f Makefile.dune test-suite
diff --git a/INSTALL.md b/INSTALL.md
index adc0f557ac..51d59e1638 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -15,9 +15,6 @@ 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.11.1)
 
-- The [num](https://github.com/ocaml/num) library; note that it is
-  included in the OCaml distribution for OCaml versions < 4.06.0
-
 - The [ZArith library](https://github.com/ocaml/Zarith) >= 1.10
 
 - The [findlib](http://projects.camlcity.org/projects/findlib.html) library (version >= 1.8.0)
@@ -35,15 +32,15 @@ To compile Coq yourself, you need:
   (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.
+Primitive floating-point numbers require IEEE-754 compliance
+(`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 proving `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.
+Note that OCaml dependencies (`zarith` and `lablgtk3-sourceview3` at
+this moment) must be properly registered with `findlib/ocamlfind`
+since Coq's build system uses `findlib` to locate them.
 
 Debian / Ubuntu users can get the necessary system packages for
 CoqIDE with:
@@ -55,7 +52,7 @@ the corresponding packages.
 
     $ opam switch create coq 4.11.1+flambda
     $ eval $(opam env)
-    $ opam install num ocamlfind lablgtk3-sourceview3
+    $ opam install ocamlfind zarith lablgtk3-sourceview3
 
 should get you a reasonable OCaml environment to compile Coq. See the
 OPAM documentation for more help.
diff --git a/META.coq.in b/META.coq.in
index 5aaa8cc8a6..a6747c614b 100644
--- a/META.coq.in
+++ b/META.coq.in
@@ -223,7 +223,7 @@ package "toplevel" (
   description = "Coq Toplevel"
   version     = "8.13"
 
-  requires    = "num, coq.stm"
+  requires    = "coq.stm"
   directory   = "toplevel"
 
   archive(byte)    = "toplevel.cma"
@@ -327,7 +327,7 @@ package "plugins" (
     description = "Coq micromega plugin"
     version     = "8.13"
 
-    requires    = "num, coq.plugins.ltac"
+    requires    = "coq.plugins.ltac"
     directory   = "micromega"
 
     archive(byte)    = "micromega_plugin.cmo"
diff --git a/Makefile.build b/Makefile.build
index 061489f47f..eed3c2813a 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -302,7 +302,7 @@ $(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(CUSTOM) -o $@ -linkpkg $(1) $^
 endef
 
 # Main packages linked by Coq.
-SYSMOD:=-package str,unix,dynlink,threads,num,zarith
+SYSMOD:=-package str,unix,dynlink,threads,zarith
 
 ###########################################################################
 # Infrastructure for the rest of the Makefile
@@ -587,11 +587,11 @@ CSDPCERTCMO:=clib/clib.cma $(addprefix plugins/micromega/, \
 
 $(CSDPCERT): $(call bestobj, $(CSDPCERTCMO))
 	$(SHOW)'OCAMLBEST -o $@'
-	$(HIDE)$(call bestocaml, -package num,unix)
+	$(HIDE)$(call bestocaml, -package unix)
 
 $(CSDPCERTBYTE): $(CSDPCERTCMO)
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(call ocamlbyte, -package num,unix)
+	$(HIDE)$(call ocamlbyte, -package unix)
 
 ###########################################################################
 # tests
@@ -707,7 +707,7 @@ COND_OPTFLAGS= \
 
 plugins/micromega/%.cmi: plugins/micromega/%.mli
 	$(SHOW)'OCAMLC    $<'
-	$(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix,num -c $<
+	$(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix -c $<
 
 %.cmi: %.mli
 	$(SHOW)'OCAMLC    $<'
@@ -715,7 +715,7 @@ plugins/micromega/%.cmi: plugins/micromega/%.mli
 
 plugins/micromega/%.cmo: plugins/micromega/%.ml
 	$(SHOW)'OCAMLC    $<'
-	$(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix,num -c $<
+	$(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix -c $<
 
 %.cmo: %.ml
 	$(SHOW)'OCAMLC    $<'
@@ -752,7 +752,7 @@ plugins/micromega/csdpcert_FORPACK:=
 
 plugins/micromega/%.cmx: plugins/micromega/%.ml
 	$(SHOW)'OCAMLOPT  $<'
-	$(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) $($(@:.cmx=_FORPACK)) -package unix,num -c $<
+	$(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) $($(@:.cmx=_FORPACK)) -package unix -c $<
 
 plugins/%.cmx: plugins/%.ml
 	$(SHOW)'OCAMLOPT  $<'
diff --git a/azure-pipelines.yml b/azure-pipelines.yml
index be9e774381..41b5210f45 100644
--- a/azure-pipelines.yml
+++ b/azure-pipelines.yml
@@ -80,7 +80,7 @@ jobs:
       opam switch set ocaml-base-compiler.$COMPILER
       eval $(opam env)
       opam update
-      opam install -j "$NJOBS" num ocamlfind${FINDLIB_VER} ounit lablgtk3-sourceview3 zarith.1.10
+      opam install -j "$NJOBS" ocamlfind${FINDLIB_VER} ounit lablgtk3-sourceview3 zarith.1.10
       opam list
     displayName: 'Install OCaml dependencies'
     env:
diff --git a/configure.ml b/configure.ml
index 2dbc01651e..43c55af495 100644
--- a/configure.ml
+++ b/configure.ml
@@ -688,23 +688,16 @@ let operating_system =
   else
     (try Sys.getenv "OS" with Not_found -> "")
 
-(** Zarith and num libraries *)
-
-let check_for_numlib () =
-  (if caml_version_nums >= [4;6;0] then
-    let numlib,_ = tryrun camlexec.find ["query";"num"] in
-    match numlib with
-    | ""  ->
-      die "Num library not installed, required for OCaml 4.06 or later"
-    | _   -> cprintf "You have the Num library installed. Good!");
+(** Zarith library *)
+
+let check_for_zarith () =
   let zarith,_ = tryrun camlexec.find ["query";"zarith"] in
   match zarith with
   | ""  ->
     die "Zarith library not installed, required"
   | _   -> cprintf "You have the Zarith library installed. Good!"
 
-let numlib =
-  check_for_numlib ()
+let numlib = check_for_zarith ()
 
 (** * lablgtk3 and CoqIDE *)
 
diff --git a/coq.opam b/coq.opam
index 342adee1f4..77fdf14834 100644
--- a/coq.opam
+++ b/coq.opam
@@ -24,7 +24,6 @@ depends: [
   "ocaml"     { >= "4.05.0" }
   "dune"      { >= "2.5.0"  }
   "ocamlfind" { build }
-  "num"
   "zarith"    { >= "1.10" }
 ]
 
diff --git a/coq.opam.docker b/coq.opam.docker
index 09065fdffd..74ca68ac0b 100644
--- a/coq.opam.docker
+++ b/coq.opam.docker
@@ -23,7 +23,6 @@ version: "dev"
 depends: [
   "ocaml"     { >= "4.05.0" }
   "ocamlfind" { build }
-  "num"
   "zarith"    { >= "1.10" }
   "conf-findutils" {build}
 ]
diff --git a/default.nix b/default.nix
index e383d214e0..ffee77f1f7 100644
--- a/default.nix
+++ b/default.nix
@@ -72,7 +72,7 @@ stdenv.mkDerivation rec {
   # Since #12604, ocamlfind looks for num when building plugins
   # This follows a similar change in the nixpkgs repo (cf. NixOS/nixpkgs#94230)
   # Same for zarith which is needed since its introduction as a dependency of Coq
-  propagatedBuildInputs = with ocamlPackages; [ num zarith ];
+  propagatedBuildInputs = with ocamlPackages; [ zarith ];
 
   src =
     if shell then null
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 2fcd69e130..f672ead807 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2020-09-16-V38"
+# CACHEKEY: "bionic_coq-V2020-09-17-V88"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -40,10 +40,8 @@ ENV NJOBS="2" \
 # Base opam is the set of base packages required by Coq
 ENV COMPILER="4.05.0"
 
-# Common OPAM packages, num to be removed once the migration to
-# micromega is complete, `num` also does not have a version number as
-# the right version to install varies with the compiler version.
-ENV BASE_OPAM="num zarith.1.10 ocamlfind.1.8.1 ounit2.2.2.3 odoc.1.5.1" \
+# Common OPAM packages
+ENV BASE_OPAM="zarith.1.10 ocamlfind.1.8.1 ounit2.2.2.3 odoc.1.5.1" \
     CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \
     BASE_ONLY_OPAM="elpi.1.11.0"
 
diff --git a/doc/changelog/11-infrastructure-and-dependencies/13007-zarith+goodbye_num.rst b/doc/changelog/11-infrastructure-and-dependencies/13007-zarith+goodbye_num.rst
new file mode 100644
index 0000000000..c142eec561
--- /dev/null
+++ b/doc/changelog/11-infrastructure-and-dependencies/13007-zarith+goodbye_num.rst
@@ -0,0 +1,4 @@
+- **Removed:**
+  The `num` library is not linked to Coq anymore
+  (`#13007 <https://github.com/coq/coq/pull/13007>`_,
+  by Emilio Jesus Gallego Arias).
diff --git a/plugins/micromega/dune b/plugins/micromega/dune
index 33ad3a0138..204125ab56 100644
--- a/plugins/micromega/dune
+++ b/plugins/micromega/dune
@@ -4,7 +4,7 @@
  ; be careful not to link the executable to the plugin!
  (modules (:standard \ csdpcert g_zify zify))
  (synopsis "Coq's micromega plugin")
- (libraries num coq.plugins.ltac))
+ (libraries coq.plugins.ltac))
 
 (executable
  (name csdpcert)
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 02ababd928..0ebb97d0bf 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -104,7 +104,7 @@ BEFORE ?=
 AFTER ?=
 
 # FIXME this should be generated by Coq (modules already linked by Coq)
-CAMLDONTLINK=str,unix,dynlink,threads,num,zarith
+CAMLDONTLINK=str,unix,dynlink,threads,zarith
 
 # OCaml binaries
 CAMLC       ?= "$(OCAMLFIND)" ocamlc   -c
diff --git a/toplevel/dune b/toplevel/dune
index 5f10346ac4..98f4ba2edf 100644
--- a/toplevel/dune
+++ b/toplevel/dune
@@ -3,8 +3,7 @@
  (public_name coq.toplevel)
  (synopsis "Coq's Interactive Shell [terminal-based]")
  (wrapped false)
- ; num still here due to some plugins using it
- (libraries num coq.stm))
+ (libraries coq.stm))
 ; Interp provides the `zarith` library to plugins, we could also use
 ; -linkall in the plugins file, to be discussed.