.gitlab-ci.yml

@@ -4,6 +4,7 @@ stages:
   - docker
   - build
   - test
+  - deploy
 
 # some default values
 variables:
@@ -218,16 +219,15 @@ windows32:
     - /^pr-.*$/
 
 
-pkg:nix:
+.nix-template: &nix-template
   image: nixorg/nix:latest # Minimal NixOS image which doesn't even contain git
   stage: test
   variables:
     # By default we use coq.cachix.org as an extra substituter but this can be overridden
     EXTRA_SUBSTITUTERS: https://coq.cachix.org
-    EXTRA_PUBLIC_KEYS: coq.cachix.org-1:Jgt0DwGAUo+wpxCM52k2V+E0hLoOzFPzvg94F65agtI=
+    EXTRA_PUBLIC_KEYS: coq.cachix.org-1:5QW/wwEnD+l2jvN6QRbRRsa4hBHG3QiQQ26cxu1F5tI=
     # The following variables should not be overridden
     GIT_STRATEGY: none
-    CACHIX_PUBLIC_KEY: cachix.cachix.org-1:eWNHQldwUO7G2VkjpnjDbWwy4KQ/HNxht7H4SSoMckM=
     NIXOS_PUBLIC_KEY: cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY=
 
   dependencies: [] # We don't need to download build artifacts
@@ -235,8 +235,6 @@ pkg:nix:
   script:
     # Use current worktree as tmpdir to allow exporting artifacts in case of failure
     - export TMPDIR=$PWD
-    # Install Cachix as documented at https://github.com/cachix/cachix
-    - nix-env -if https://github.com/cachix/cachix/tarball/master --substituters https://cachix.cachix.org --trusted-public-keys "$CACHIX_PUBLIC_KEY"
     # We build an expression rather than a direct URL to not be dependent on
     # the URL location; we are forced to put the public key of cache.nixos.org
     # because there is no --extra-trusted-public-key option.
@@ -261,11 +259,30 @@ build:macOS:
   script:
     - dev/build/osx/make-macos-dmg.sh
   variables:
+    MACOSX_DEPLOYMENT_TARGET: '10.11'
     NJOBS: "2"
   only:
     variables:
       - $MACOS == "enabled"
 
+pkg:nix:deploy:
+  <<: *nix-template
+  environment:
+    name: cachix
+    url: https://coq.cachix.org
+  before_script:
+    # Install Cachix as documented at https://github.com/cachix/cachix
+    - nix-env -iA cachix -f https://cachix.org/api/v1/install
+  only:
+    - master
+    - /^v.*\..*$/
+
+pkg:nix:
+  <<: *nix-template
+  except:
+    - master
+    - /^v.*\..*$/
+
 doc:refman:
   <<: *doc-template
   dependencies:
@@ -283,6 +300,37 @@ doc:ml-api:
     paths:
       - dev/ocamldoc
 
+doc:refman:deploy:
+  stage: deploy
+  environment:
+    name: deployment
+    url: https://coq.github.io/
+  only:
+    variables:
+      - $DOCUMENTATION_DEPLOY_KEY
+  dependencies:
+    - doc:refman
+  before_script:
+    - which ssh-agent || ( apt-get update -y && apt-get install openssh-client -y )
+    - eval $(ssh-agent -s)
+    - echo "$DOCUMENTATION_DEPLOY_KEY" | tr -d '\r' | ssh-add - > /dev/null
+    - mkdir -p ~/.ssh
+    - chmod 700 ~/.ssh
+    - ssh-keyscan -t rsa github.com >> ~/.ssh/known_hosts
+    - git config --global user.name "coqbot"
+    - git config --global user.email "coqbot@users.noreply.github.com"
+  script:
+    - git clone git@github.com:coq/doc.git _deploy
+    - rm -rf _deploy/$CI_COMMIT_REF_NAME/refman
+    - rm -rf _deploy/$CI_COMMIT_REF_NAME/stdlib
+    - mkdir -p _deploy/$CI_COMMIT_REF_NAME
+    - cp -rv _install_ci/share/doc/coq/sphinx/html _deploy/$CI_COMMIT_REF_NAME/refman
+    - cp -rv _install_ci/share/doc/coq/html/stdlib _deploy/$CI_COMMIT_REF_NAME/stdlib
+    - cd _deploy/$CI_COMMIT_REF_NAME/
+    - git add refman stdlib
+    - git commit -m "Documentation of branch “$CI_COMMIT_REF_NAME” at $CI_COMMIT_SHORT_SHA"
+    - git push # TODO: rebase and retry on failure
+
 test-suite:base:
   <<: *test-suite-template
   dependencies:

CHANGES.md

+Changes from 8.9.0 to 8.9.1
+===========================
+
+- Some quality-of-life fixes.
+- Numerous improvements to the documentation.
+- Fix a critical bug related to primitive projections and `native_compute`.
+- Ship several additional Coq libraries with the Windows installer.
+
 Changes from 8.9+beta1 to 8.9.0
 ===============================
 
@@ -97,8 +105,9 @@ Standard Library
 
 - Syntax notations for `string`, `ascii`, `Z`, `positive`, `N`, `R`,
   and `int31` are no longer available merely by `Require`ing the files
-  that define the inductives.  You must `Import` `Coq.Strings.String`,
-  `Coq.Strings.Ascii`, `Coq.ZArith.BinIntDef`, `Coq.PArith.BinPosDef`,
+  that define the inductives.  You must `Import` `Coq.Strings.String.StringSyntax`
+  (after `Require` `Coq.Strings.String`), `Coq.Strings.Ascii.AsciiSyntax` (after
+  `Require` `Coq.Strings.Ascii`), `Coq.ZArith.BinIntDef`, `Coq.PArith.BinPosDef`,
   `Coq.NArith.BinNatDef`, `Coq.Reals.Rdefinitions`, and
   `Coq.Numbers.Cyclic.Int31.Int31`, respectively, to be able to use
   these notations.  Note that passing `-compat 8.8` or issuing

INSTALL

@@ -121,9 +121,8 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
    "./configure -help". The main options accepted are:
 
 -prefix <dir>
-	Binaries, library, man pages and Emacs mode will be respectively
-	installed in <dir>/bin, <dir>/lib/coq, <dir>/man and
-	<dir>/lib/emacs/site-lisp
+	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
@@ -134,9 +133,6 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
 -mandir <dir>                   (default: /usr/local/share/man)
         Directory where the Coq manual pages will be installed
 
--emacslib <dir>			(default: /usr/local/lib/emacs/site-lisp)
-	Directory where the Coq Emacs mode 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
@@ -183,9 +179,9 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
    it is recommended to compile in parallel, via make -jN where N is your number
    of cores.
 
-6- You can now install the Coq system. Executables, libraries, manual pages
-   and emacs mode are copied in some standard places of your system, defined at
-   configuration time (step 3). Just do
+6- 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

Makefile.build

@@ -237,6 +237,10 @@ OPT:=
 BESTOBJ:=.cmo
 BESTLIB:=.cma
 BESTDYN:=.cma
+
+# needed while booting if non -local
+CAML_LD_LIBRARY_PATH := $(PWD)/kernel/byterun:$(CAML_LD_LIBRARY_PATH)
+export CAML_LD_LIBRARY_PATH
 endif
 
 define bestobj
@@ -408,12 +412,12 @@ grammar/%.cmi: grammar/%.mli
 
 .PHONY: coqbinaries coqbyte
 
-coqbinaries: $(TOPBINOPT) $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE)
-coqbyte: $(TOPBYTE) $(CHICKENBYTE)
+coqbinaries: $(TOPBIN) $(COQC) $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE)
+coqbyte: $(TOPBYTE) $(COQCBYTE) $(CHICKENBYTE)
 
 # Special rule for coqtop, we imitate `ocamlopt` can delete the target
 # to avoid #7666
-$(COQTOPEXE): $(TOPBINOPT:.opt=.$(BEST))
+$(COQTOPEXE): $(TOPBIN)
 	rm -f $@ && cp $< $@
 
 bin/%.opt$(EXE): topbin/%_bin.ml $(LINKCMX) $(LIBCOQRUN)
@@ -435,12 +439,12 @@ COQTOP_BYTE=topbin/coqtop_byte_bin.ml
 
 # Special rule for coqtop.byte
 # VMBYTEFLAGS will either contain -custom of the right -dllpath for the VM
-$(COQTOPBYTE): $(LINKCMO) $(LIBCOQRUN) $(COQTOP_BYTE)
+$(COQTOPBYTE): $(COQTOP_BYTE) $(LINKCMO) $(LIBCOQRUN)
 	$(SHOW)'COQMKTOP -o $@'
 	$(HIDE)$(OCAMLC) -linkall -linkpkg -I lib -I vernac -I toplevel \
 	                 -I kernel/byterun/ -cclib -lcoqrun $(VMBYTEFLAGS) \
 			 $(SYSMOD) -package camlp5.gramlib,compiler-libs.toplevel \
-			 $(LINKCMO) $(BYTEFLAGS) $(COQTOP_BYTE) -o $@
+			 $(LINKCMO) $(BYTEFLAGS) $< -o $@
 
 # For coqc
 COQCCMO:=clib/clib.cma lib/lib.cma toplevel/usage.cmo tools/coqc.cmo
@@ -567,7 +571,7 @@ $(COQWORKMGRBYTE): $(COQWORKMGRCMO)
 
 FAKEIDECMO:=clib/clib.cma lib/lib.cma ide/protocol/ideprotocol.cma ide/document.cmo tools/fake_ide.cmo
 
-$(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOP)
+$(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOPEXE)
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml, -I ide -I ide/protocol -package str -package dynlink)
 

Makefile.checker

@@ -37,16 +37,12 @@ CHECKERDEPS := $(addsuffix .d, $(CHECKMLDFILE) $(CHECKMLLIBFILE))
 # Copied files
 checker/esubst.mli: kernel/esubst.mli
 	cp -a $< $@
-	sed -i.bak '1i(* AUTOGENERATED FILE: DO NOT EDIT *)\n\n\n\n\n\n\n\n' $@ && rm $@.bak
 checker/esubst.ml: kernel/esubst.ml
 	cp -a $< $@
-	sed -i.bak '1i(* AUTOGENERATED FILE: DO NOT EDIT *)\n\n\n\n\n\n\n\n' $@ && rm $@.bak
 checker/names.mli: kernel/names.mli
 	cp -a $< $@
-	sed -i.bak '1i(* AUTOGENERATED FILE: DO NOT EDIT *)\n\n\n\n\n\n\n\n' $@ && rm $@.bak
 checker/names.ml: kernel/names.ml
 	cp -a $< $@
-	sed -i.bak '1i(* AUTOGENERATED FILE: DO NOT EDIT *)\n\n\n\n\n\n\n\n' $@ && rm $@.bak
 
 ifeq ($(BEST),opt)
 $(CHICKEN): checker/check.cmxa checker/main.mli checker/main.ml

Makefile.ci

@@ -55,6 +55,8 @@ ci-math-classes: ci-bignums
 
 ci-corn: ci-math-classes
 
+ci-simple-io: ci-ext-lib
+
 ci-quickchick: ci-ext-lib ci-simple-io
 
 ci-formal-topology: ci-corn

Makefile.common

@@ -74,10 +74,12 @@ endif
 # for Declare ML Module files.
 
 ifeq ($(BEST),opt)
+TOPBIN:=$(TOPBINOPT)
 COQTOPBEST:=$(COQTOPEXE)
 DYNOBJ:=.cmxs
 DYNLIB:=.cmxs
 else
+TOPBIN:=$(TOPBYTE)
 COQTOPBEST:=$(COQTOPBYTE)
 DYNOBJ:=.cmo
 DYNLIB:=.cma

Makefile.doc

@@ -54,6 +54,7 @@ DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex
 
 doc: refman stdlib
 
+SPHINX_DEPS ?=
 ifndef QUICK
 SPHINX_DEPS := coq
 endif

Makefile.install

@@ -68,7 +68,7 @@ endif
 
 install-binaries: install-tools
 	$(MKDIR) $(FULLBINDIR)
-	$(INSTALLBIN) $(COQC) $(CHICKEN) $(COQTOPEXE) $(TOPBINOPT) $(FULLBINDIR)
+	$(INSTALLBIN) $(COQC) $(CHICKEN) $(COQTOPEXE) $(TOPBIN) $(FULLBINDIR)
 
 install-byte: install-coqide-byte
 	$(MKDIR) $(FULLBINDIR)
@@ -104,11 +104,11 @@ install-devfiles:
 	$(MKDIR) $(FULLCOQLIB)
 	$(INSTALLSH)  $(FULLCOQLIB) $(GRAMMARCMA)
 	$(INSTALLSH)  $(FULLCOQLIB) $(INSTALLCMI)           # Regular CMI files
+	$(INSTALLSH)  $(FULLCOQLIB) $(TOOLS_HELPERS)
+ifeq ($(BEST),opt)
 	$(INSTALLSH)  $(FULLCOQLIB) $(INSTALLCMX)           # To avoid warning 58 "-opaque"
 	$(INSTALLSH)  $(FULLCOQLIB) $(PLUGINSCMO:.cmo=.cmx) # For static linking of plugins
 	$(INSTALLSH)  $(FULLCOQLIB) $(PLUGINSCMO:.cmo=.o)   # For static linking of plugins
-	$(INSTALLSH)  $(FULLCOQLIB) $(TOOLS_HELPERS)
-ifeq ($(BEST),opt)
 	$(INSTALLSH)  $(FULLCOQLIB) $(LINKCMX) $(CORECMA:.cma=.a) $(STATICPLUGINS:.cma=.a)
 endif
 

Makefile.vofiles

@@ -31,7 +31,10 @@ vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst the
 
 GLOBFILES:=$(ALLVO:.vo=.glob)
 ifdef NATIVECOMPUTE
-NATIVEFILES := $(call vo_to_cm,$(ALLVO)) $(call vo_to_obj,$(ALLVO))
+NATIVEFILES := $(call vo_to_cm,$(ALLVO))
+ifeq ($(BEST),opt)
+NATIVEFILES += $(call vo_to_obj,$(ALLVO))
+endif
 else
 NATIVEFILES :=
 endif
@@ -39,5 +42,5 @@ LIBFILES:=$(ALLVO) $(NATIVEFILES) $(VFILES) $(GLOBFILES)
 
 # For emacs:
 # Local Variables:
-# mode: makefile
+# mode: makefile-gmake
 # End:

clib/cList.ml

@@ -796,7 +796,7 @@ let share_tails l1 l2 =
 
 (** {6 Association lists} *)
 
-let map_assoc f = List.map (fun (x,a) -> (x,f a))
+let map_assoc f = map (fun (x,a) -> (x,f a))
 
 let rec assoc_f f a = function
   | (x, e) :: xs -> if f a x then e else assoc_f f a xs
@@ -997,7 +997,7 @@ let rec duplicates cmp = function
    and so on if there are more elements in the lists. *)
 
 let cartesian op l1 l2 =
-  map_append (fun x -> List.map (op x) l2) l1
+  map_append (fun x -> map (op x) l2) l1
 
 (* [cartesians] is an n-ary cartesian product: it iterates
    [cartesian] over a list of lists.  *)
@@ -1024,7 +1024,7 @@ let cartesians_filter op init ll =
 let rec factorize_left cmp = function
   | (a,b) :: l ->
       let al,l' = partition (fun (a',_) -> cmp a a') l in
-      (a,(b :: List.map snd al)) :: factorize_left cmp l'
+      (a,(b :: map snd al)) :: factorize_left cmp l'
   | [] -> []
 
 module Smart =

configure.ml

@@ -11,8 +11,8 @@
 #load "str.cma"
 open Printf
 
-let coq_version = "8.9.0"
-let coq_macos_version = "8.9.0" (** "[...] should be a string comprised of
+let coq_version = "8.9.1"
+let coq_macos_version = "8.9.1" (** "[...] should be a string comprised of
 three non-negative, period-separated integers [...]" *)
 let vo_magic = 8900
 let state_magic = 58900

debian/README.source

@@ -16,7 +16,7 @@ Only coqdoc-generated documentation of the standard library is shipped
 in main. The full documentation is shipped in non-free (as coq-doc
 package).
 
-The git-import-orig tool automatically filters out problematic files,
+The `gbp import-orig` tool automatically filters out problematic files,
 thanks to the configuration in debian/gbp.conf. It is suggested to
 append the "dfsg" suffix to the upstream version to make repackaging
 explicit.
@@ -25,19 +25,15 @@ explicit.
 Patch system
 ------------
 
-This source package is in format 3.0 (quilt).
-
-The quilt series, if any, is generated from the Git repository, using
-dom-{apply,save}-patches, from the dh-ocaml (>= 0.5) package. Please
-refer to the appendix about Git in the Debian OCaml Packaging Policy
-(from the same package).
+This source package is in format 3.0 (quilt). The quilt series, if
+any, is generated from the Git repository, using `gbp pq`.
 
 
 Version Control System
 ----------------------
 
-Packaging is versioned with git, using git-import-orig (with
---pristine-tar option) and git-buildpackage (with --git-pristine-tar
+Packaging is versioned with git, using `gbp import-orig` (with
+--pristine-tar option) and `gbp buildpackage` (with --git-pristine-tar
 option). Debian changelog can be updated based on git changelog using
 git-dch. Please consider reading the documentation of these tools.
 
@@ -53,4 +49,4 @@ to ../coq.cache, and debian/rules will detect its presence and rsync
 from there instead of really compiling Coq...
 
 
- -- Stéphane Glondu <glondu@debian.org>, Mon, 20 Aug 2012 18:20:18 +0200
+ -- Stéphane Glondu <glondu@debian.org>, Tue, 20 Aug 2019 03:55:22 +0200

debian/changelog

-coq (8.9.0-2) UNRELEASED; urgency=medium
+coq (8.9.1-1) unstable; urgency=medium
 
+  * New upstream release
   * Fix FTBFS with OCaml 4.08.0
     - add libnum-ocaml-dev to Build-Depends
     - apply a patch to fix double loading of pr_dump.cmo (camlp5)
     - remove a failing test
   * Remove Samuel from Uploaders
+  * Bump Standards-Version to 4.4.0
 
- -- Stéphane Glondu <glondu@debian.org>  Fri, 09 Aug 2019 17:55:00 +0200
+ -- Stéphane Glondu <glondu@debian.org>  Tue, 20 Aug 2019 05:09:34 +0200
 
 coq (8.9.0-1) unstable; urgency=high
 

debian/control

@@ -7,7 +7,7 @@ Uploaders:
  Ralf Treinen <treinen@debian.org>,
  Stéphane Glondu <glondu@debian.org>,
  Enrico Tassi <gareuselesinge@debian.org>
-Standards-Version: 4.3.0
+Standards-Version: 4.4.0
 Build-Depends:
  debhelper (>= 10),
  dh-exec,

debian/patches/fix-bytecode-build.patch

-From: =?utf-8?q?Ga=C3=ABtan_Gilbert?= <gaetan.gilbert@skyskimmer.net>
-Date: Sun, 11 Aug 2019 18:33:24 +0200
-Subject: Makefiles: Fixes for byte compilation
-
-Bug: https://github.com/coq/coq/issues/9464
-Origin: other, https://github.com/SkySkimmer/coq/commit/f29aa6720eba884533972530b4283bf19d8410aa
-Reviewed-by: Benjamin Barenblat <bbaren@debian.org>
-
-- default targets don't depend on ocamlopt when it's unavailable
-- coqc.byte is built by byte target and coqc by coqbinaries target
-- unit tests use best ocaml
-- poly-capture-global-univs tests ml compilation with ocamlc
-- don't try to install .cmx and native-compute .o files
-
-Benjamin Barenblat modified this patch to apply cleanly on top of 8.9.0.
----
- Makefile.build                               | 16 ++++++++++------
- Makefile.common                              |  2 ++
- Makefile.install                             |  6 +++---
- Makefile.vofiles                             |  5 ++++-
- test-suite/misc/poly-capture-global-univs.sh |  2 +-
- 5 files changed, 20 insertions(+), 11 deletions(-)
-
-diff --git a/Makefile.build b/Makefile.build
-index 46ae09c..8d1f3f4 100644
---- a/Makefile.build
-+++ b/Makefile.build
-@@ -237,6 +237,10 @@ OPT:=
- BESTOBJ:=.cmo
- BESTLIB:=.cma
- BESTDYN:=.cma
-+
-+# needed while booting if non -local
-+CAML_LD_LIBRARY_PATH := $(PWD)/kernel/byterun:$(CAML_LD_LIBRARY_PATH)
-+export CAML_LD_LIBRARY_PATH
- endif
- 
- define bestobj
-@@ -408,12 +412,12 @@ grammar/%.cmi: grammar/%.mli
- 
- .PHONY: coqbinaries coqbyte
- 
--coqbinaries: $(TOPBINOPT) $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE)
--coqbyte: $(TOPBYTE) $(CHICKENBYTE)
-+coqbinaries: $(TOPBIN) $(COQC) $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE)
-+coqbyte: $(TOPBYTE) $(COQCBYTE) $(CHICKENBYTE)
- 
- # Special rule for coqtop, we imitate `ocamlopt` can delete the target
- # to avoid #7666
--$(COQTOPEXE): $(TOPBINOPT:.opt=.$(BEST))
-+$(COQTOPEXE): $(TOPBIN)
- 	rm -f $@ && cp $< $@
- 
- bin/%.opt$(EXE): topbin/%_bin.ml $(LINKCMX) $(LIBCOQRUN)
-@@ -435,12 +439,12 @@ COQTOP_BYTE=topbin/coqtop_byte_bin.ml
- 
- # Special rule for coqtop.byte
- # VMBYTEFLAGS will either contain -custom of the right -dllpath for the VM
--$(COQTOPBYTE): $(LINKCMO) $(LIBCOQRUN) $(COQTOP_BYTE)
-+$(COQTOPBYTE): $(COQTOP_BYTE) $(LINKCMO) $(LIBCOQRUN)
- 	$(SHOW)'COQMKTOP -o $@'
- 	$(HIDE)$(OCAMLC) -linkall -linkpkg -I lib -I vernac -I toplevel \
- 	                 -I kernel/byterun/ -cclib -lcoqrun $(VMBYTEFLAGS) \
- 			 $(SYSMOD) -package camlp5.gramlib,compiler-libs.toplevel \
--			 $(LINKCMO) $(BYTEFLAGS) $(COQTOP_BYTE) -o $@
-+			 $(LINKCMO) $(BYTEFLAGS) $< -o $@
- 
- # For coqc
- COQCCMO:=clib/clib.cma lib/lib.cma toplevel/usage.cmo tools/coqc.cmo
-@@ -567,7 +571,7 @@ $(COQWORKMGRBYTE): $(COQWORKMGRCMO)
- 
- FAKEIDECMO:=clib/clib.cma lib/lib.cma ide/protocol/ideprotocol.cma ide/document.cmo tools/fake_ide.cmo
- 
--$(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOP)
-+$(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOPEXE)
- 	$(SHOW)'OCAMLBEST -o $@'
- 	$(HIDE)$(call bestocaml, -I ide -I ide/protocol -package str -package dynlink)
- 
-diff --git a/Makefile.common b/Makefile.common
-index 09457ce..ca331e0 100644
---- a/Makefile.common
-+++ b/Makefile.common
-@@ -74,10 +74,12 @@ endif
- # for Declare ML Module files.
- 
- ifeq ($(BEST),opt)
-+TOPBIN:=$(TOPBINOPT)
- COQTOPBEST:=$(COQTOPEXE)
- DYNOBJ:=.cmxs
- DYNLIB:=.cmxs
- else
-+TOPBIN:=$(TOPBYTE)
- COQTOPBEST:=$(COQTOPBYTE)
- DYNOBJ:=.cmo
- DYNLIB:=.cma
-diff --git a/Makefile.install b/Makefile.install
-index be6fe54..038d507 100644
---- a/Makefile.install
-+++ b/Makefile.install
-@@ -68,7 +68,7 @@ endif
- 
- install-binaries: install-tools
- 	$(MKDIR) $(FULLBINDIR)
--	$(INSTALLBIN) $(COQC) $(CHICKEN) $(COQTOPEXE) $(TOPBINOPT) $(FULLBINDIR)
-+	$(INSTALLBIN) $(COQC) $(CHICKEN) $(COQTOPEXE) $(TOPBIN) $(FULLBINDIR)
- 
- install-byte: install-coqide-byte
- 	$(MKDIR) $(FULLBINDIR)
-@@ -104,11 +104,11 @@ install-devfiles:
- 	$(MKDIR) $(FULLCOQLIB)
- 	$(INSTALLSH)  $(FULLCOQLIB) $(GRAMMARCMA)
- 	$(INSTALLSH)  $(FULLCOQLIB) $(INSTALLCMI)           # Regular CMI files
-+	$(INSTALLSH)  $(FULLCOQLIB) $(TOOLS_HELPERS)
-+ifeq ($(BEST),opt)
- 	$(INSTALLSH)  $(FULLCOQLIB) $(INSTALLCMX)           # To avoid warning 58 "-opaque"
- 	$(INSTALLSH)  $(FULLCOQLIB) $(PLUGINSCMO:.cmo=.cmx) # For static linking of plugins
- 	$(INSTALLSH)  $(FULLCOQLIB) $(PLUGINSCMO:.cmo=.o)   # For static linking of plugins
--	$(INSTALLSH)  $(FULLCOQLIB) $(TOOLS_HELPERS)
--ifeq ($(BEST),opt)
- 	$(INSTALLSH)  $(FULLCOQLIB) $(LINKCMX) $(CORECMA:.cma=.a) $(STATICPLUGINS:.cma=.a)
- endif
- 
-diff --git a/Makefile.vofiles b/Makefile.vofiles
-index d0ae317..4d6b15b 100644
---- a/Makefile.vofiles
-+++ b/Makefile.vofiles
-@@ -31,7 +31,10 @@ vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst the
- 
- GLOBFILES:=$(ALLVO:.vo=.glob)
- ifdef NATIVECOMPUTE
--NATIVEFILES := $(call vo_to_cm,$(ALLVO)) $(call vo_to_obj,$(ALLVO))
-+NATIVEFILES := $(call vo_to_cm,$(ALLVO))
-+ifeq ($(BEST),opt)
-+NATIVEFILES += $(call vo_to_obj,$(ALLVO))
-+endif
- else
- NATIVEFILES :=
- endif
-diff --git a/test-suite/misc/poly-capture-global-univs.sh b/test-suite/misc/poly-capture-global-univs.sh
-index e066ac0..39d20fd 100755
---- a/test-suite/misc/poly-capture-global-univs.sh
-+++ b/test-suite/misc/poly-capture-global-univs.sh
-@@ -11,7 +11,7 @@ coq_makefile -f _CoqProject -o Makefile
- 
- make clean
- 
--make src/evil_plugin.cmxs
-+make src/evil_plugin.cma
- 
- if make; then
-     >&2 echo 'Should have failed!'

debian/patches/remove-bytecode-failing-tests.patch

@@ -18,7 +18,7 @@ of https://github.com/coq/coq/issues/9141.
  1 file changed, 1 insertion(+), 1 deletion(-)
 
 diff --git a/test-suite/Makefile b/test-suite/Makefile
-index 598d6db..c160c64 100644
+index ad73585..8005217 100644
 --- a/test-suite/Makefile
 +++ b/test-suite/Makefile
 @@ -102,7 +102,7 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \

debian/patches/series

@@ -4,9 +4,7 @@ remove-tests-that-need-coqlib.patch
 avoid-usr-bin-env.patch
 python-scripts-libraries.patch
 skip-dot-pc.patch
-spelling.patch
 verbose-build.patch
-fix-bytecode-build.patch
 remove-bytecode-failing-tests.patch
 ssrmatching-license.patch
 0012-ocaml-4.08-does-not-allow-dynamic-loading-of-already.patch

debian/patches/spelling.patch

-From: Benjamin Barenblat <bbaren@debian.org>
-Date: Sun, 11 Aug 2019 18:33:23 +0200
-Subject: Correct spelling errors
-
-Forwarded: no
----
- printing/proof_diffs.ml | 12 ++++++------
- 1 file changed, 6 insertions(+), 6 deletions(-)
-
-diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
-index 0b630b3..bfe7916 100644
---- a/printing/proof_diffs.ml
-+++ b/printing/proof_diffs.ml
-@@ -409,7 +409,7 @@ let match_goals ot nt =
-       match exp, exp2 with
-       | Some expa, Some expb -> constr_expr ogname expa expb
-       | None, None -> ()
--      | _, _ -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (1)")
-+      | _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (1)")
-     in
-     let local_binder_expr ogname exp exp2 =
-       match exp, exp2 with
-@@ -421,7 +421,7 @@ let match_goals ot nt =
-       | CLocalPattern p, CLocalPattern p2 ->
-         let (p,ty), (p2,ty2) = p.v,p2.v in
-         constr_expr_opt ogname ty ty2
--      | _, _ -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (2)")
-+      | _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (2)")
-     in
-     let recursion_order_expr ogname exp exp2 =
-       match exp, exp2 with
-@@ -431,7 +431,7 @@ let match_goals ot nt =
-       | CMeasureRec (m,r), CMeasureRec (m2,r2) ->
-         constr_expr ogname m m2;
-         constr_expr_opt ogname r r2
--      | _, _ -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (3)")
-+      | _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (3)")
-     in
-     let fix_expr ogname exp exp2 =
-       let (l,(lo,ro),lb,ce1,ce2), (l2,(lo2,ro2),lb2,ce12,ce22) = exp,exp2 in
-@@ -515,7 +515,7 @@ let match_goals ot nt =
-       | CastNative a, CastNative a2 ->
-         constr_expr ogname a a2
-       | CastCoerce, CastCoerce -> ()
--      | _, _ -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (4)"))
-+      | _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (4)"))
-     | CNotation (ntn,args), CNotation (ntn2,args2) ->
-       constr_notation_substitution ogname args args2
-     | CGeneralization (b,a,c), CGeneralization (b2,a2,c2) ->
-@@ -523,7 +523,7 @@ let match_goals ot nt =
-     | CPrim p, CPrim p2 -> ()
-     | CDelimiters (key,e), CDelimiters (key2,e2) ->
-       constr_expr ogname e e2
--    | _, _ -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (5)")
-+    | _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (5)")
-     end
-   in
- 
-@@ -626,7 +626,7 @@ let make_goal_map_i op np =
-         in
-         Goal.Set.iter (fun ng -> ng_to_og := GoalMap.add ng (get_og ng) !ng_to_og) add_gs;
-         !ng_to_og
--      with Not_found -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (6)")
-+      with Not_found -> raise (Diff_Failure "Unable to match goals between old and new proof states (6)")
-     end
- 
- let make_goal_map op np =

debian/patches/verbose-build.patch

@@ -8,10 +8,10 @@ Forwarded: no
  1 file changed, 1 insertion(+), 1 deletion(-)
 
 diff --git a/Makefile.build b/Makefile.build
-index c100eda..46ae09c 100644
+index ed29e21..8d1f3f4 100644
 --- a/Makefile.build
 +++ b/Makefile.build
-@@ -619,7 +619,7 @@ $(ALLSTDLIB).v:
+@@ -623,7 +623,7 @@ $(ALLSTDLIB).v:
  	$(SHOW)'MAKE $(notdir $@)'
  	$(HIDE)echo "Require $(ALLMODS)." > $@