10 files changed, 44 insertions, 201 deletions
diff --git a/Makefile.dune b/Makefile.dune
index 1e401a57b9..ac5f584b90 100644
--- a/Makefile.dune
+++ b/Makefile.dune
@@ -1,7 +1,7 @@
 # -*- mode: makefile -*-
 # Dune Makefile for Coq
 
-.PHONY: help voboot states world apidoc
+.PHONY: help voboot states world watch release apidoc clean
 
 # use DUNEOPT=--display=short for a more verbose build
 # DUNEOPT=--display=short
@@ -15,6 +15,7 @@ help:
 	@echo "  - watch:   build all binaries and libraries [continuous build]"
 	@echo "  - release: build Coq in release mode"
 	@echo "  - apidoc:  build ML API documentation"
+	@echo "  - ocheck:  build for all supported OCaml versions [requires OPAM]"
 	@echo "  - clean:   remove build directory and autogenerated files"
 	@echo "  - help:    show this message"
 
@@ -28,6 +29,9 @@ states: voboot
 world: voboot
 	dune build $(DUNEOPT) @install
 
+ocheck: voboot
+	dune build $(DUNEOPT) @install --workspace=dev/dune-workspace.all
+
 watch: voboot
 	dune build $(DUNEOPT) @install -w
 
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 23eb6fbc63..74dd4d41c1 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -159,19 +159,19 @@ if [ "${COQREGTESTING:-N}" == "Y" ] ; then
   # Log command output - take log target name from command name (like log1 make => log target is "<module>-make")
   log1() {
     { local -; set +x; } 2> /dev/null
-    "$@" >"$LOGS/$LOGTARGET-$1.log"  2>"$LOGS/$LOGTARGET-$1.err"
+    "$@" >"$LOGS/$LOGTARGET-$1_log.txt"  2>"$LOGS/$LOGTARGET-$1_err.txt"
   }
 
   # Log command output - take log target name from command name and first argument (like log2 make install => log target is "<module>-make-install")
   log2() {
     { local -; set +x; } 2> /dev/null
-    "$@" >"$LOGS/$LOGTARGET-$1-$2.log" 2>"$LOGS/$LOGTARGET-$1-$2.err"
+    "$@" >"$LOGS/$LOGTARGET-$1-$2_log.txt" 2>"$LOGS/$LOGTARGET-$1-$2_err.txt"
   }
 
   # Log command output - take log target name from command name and second argument (like log_1_3 ocaml setup.ml -configure => log target is "<module>-ocaml--configure")
   log_1_3() {
     { local -; set +x; } 2> /dev/null
-    "$@" >"$LOGS/$LOGTARGET-$1-$3.log" 2>"$LOGS/$LOGTARGET-$1-$3.err"
+    "$@" >"$LOGS/$LOGTARGET-$1-$3_log.txt" 2>"$LOGS/$LOGTARGET-$1-$3_err.txt"
   }
 
   # Log command output - log target name is first argument (like logn untar tar xvaf ... => log target is "<module>-untar")
@@ -179,26 +179,26 @@ if [ "${COQREGTESTING:-N}" == "Y" ] ; then
     { local -; set +x; } 2> /dev/null
     LOGTARGETEX=$1
     shift
-    "$@" >"$LOGS/$LOGTARGET-$LOGTARGETEX.log" 2>"$LOGS/$LOGTARGET-$LOGTARGETEX.err"
+    "$@" >"$LOGS/$LOGTARGET-${LOGTARGETEX}_log.txt" 2>"$LOGS/$LOGTARGET-${LOGTARGETEX}_err.txt"
   }
 else
   # If COQREGTESTING, log to log files and console
   # Log command output - take log target name from command name (like log1 make => log target is "<module>-make")
   log1() {
     { local -; set +x; } 2> /dev/null
-    "$@" > >(tee "$LOGS/$LOGTARGET-$1.log" | sed -e "s/^/$LOGTARGET-$1.log: /") 2> >(tee "$LOGS/$LOGTARGET-$1.err" | sed -e "s/^/$LOGTARGET-$1.err: /" 1>&2)
+    "$@" > >(tee "$LOGS/$LOGTARGET-$1_log.txt" | sed -e "s/^/$LOGTARGET-$1_log.txt: /") 2> >(tee "$LOGS/$LOGTARGET-$1_err.txt" | sed -e "s/^/$LOGTARGET-$1_err.txt: /" 1>&2)
   }
 
   # Log command output - take log target name from command name and first argument (like log2 make install => log target is "<module>-make-install")
   log2() {
     { local -; set +x; } 2> /dev/null
-    "$@" > >(tee "$LOGS/$LOGTARGET-$1-$2.log" | sed -e "s/^/$LOGTARGET-$1-$2.log: /") 2> >(tee "$LOGS/$LOGTARGET-$1-$2.err" | sed -e "s/^/$LOGTARGET-$1-$2.err: /" 1>&2)
+    "$@" > >(tee "$LOGS/$LOGTARGET-$1-$2_log.txt" | sed -e "s/^/$LOGTARGET-$1-$2_log.txt: /") 2> >(tee "$LOGS/$LOGTARGET-$1-$2_err.txt" | sed -e "s/^/$LOGTARGET-$1-$2_err.txt: /" 1>&2)
   }
 
   # Log command output - take log target name from command name and second argument (like log_1_3 ocaml setup.ml -configure => log target is "<module>-ocaml--configure")
   log_1_3() {
     { local -; set +x; } 2> /dev/null
-    "$@" > >(tee "$LOGS/$LOGTARGET-$1-$3.log" | sed -e "s/^/$LOGTARGET-$1-$3.log: /") 2> >(tee "$LOGS/$LOGTARGET-$1-$3.err" | sed -e "s/^/$LOGTARGET-$1-$3.err: /" 1>&2)
+    "$@" > >(tee "$LOGS/$LOGTARGET-$1-$3_log.txt" | sed -e "s/^/$LOGTARGET-$1-$3_log.txt: /") 2> >(tee "$LOGS/$LOGTARGET-$1-$3_err.txt" | sed -e "s/^/$LOGTARGET-$1-$3_err.txt: /" 1>&2)
   }
 
   # Log command output - log target name is first argument (like logn untar tar xvaf ... => log target is "<module>-untar")
@@ -206,7 +206,7 @@ else
     { local -; set +x; } 2> /dev/null
     LOGTARGETEX=$1
     shift
-    "$@" > >(tee "$LOGS/$LOGTARGET-$LOGTARGETEX.log" | sed -e "s/^/$LOGTARGET-$LOGTARGETEX.log: /") 2> >(tee "$LOGS/$LOGTARGET-$LOGTARGETEX.err" | sed -e "s/^/$LOGTARGET-$LOGTARGETEX.err: /" 1>&2)
+    "$@" > >(tee "$LOGS/$LOGTARGET-${LOGTARGETEX}_log.txt" | sed -e "s/^/$LOGTARGET-${LOGTARGETEX}_log.txt: /") 2> >(tee "$LOGS/$LOGTARGET-${LOGTARGETEX}_err.txt" | sed -e "s/^/$LOGTARGET-${LOGTARGETEX}_err.txt: /" 1>&2)
   }
 fi
 
diff --git a/dev/dune-workspace.all b/dev/dune-workspace.all
new file mode 100644
index 0000000000..44857ed050
--- /dev/null
+++ b/dev/dune-workspace.all
@@ -0,0 +1,11 @@
+(lang dune 1.2)
+
+; Add custom flags here. Default developer profile is `dev`
+(env
+ (dev     (flags :standard -rectypes -w -9-27-50))
+ (release (flags :standard -rectypes)))
+
+(context (opam (switch 4.05.0)))
+(context (opam (switch 4.05.0+32bit)))
+(context (opam (switch 4.07.0)))
+(context (opam (switch 4.07.0+flambda)))
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 636144e0c8..9dae7fd102 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -606,7 +606,7 @@ for several ways of defining a function *and other useful related
 objects*, namely: an induction principle that reflects the recursive
 structure of the function (see :tacn:`function induction`) and its fixpoint equality.
 The meaning of this declaration is to define a function ident,
-similarly to ``Fixpoint`. Like in ``Fixpoint``, the decreasing argument must
+similarly to ``Fixpoint``. Like in ``Fixpoint``, the decreasing argument must
 be given (unless the function is not recursive), but it might not
 necessarily be *structurally* decreasing. The point of the {} annotation
 is to name the decreasing argument *and* to describe which kind of
diff --git a/tools/README.emacs b/tools/README.emacs
deleted file mode 100644
index 4d8e3697a0..0000000000
--- a/tools/README.emacs
+++ /dev/null
@@ -1,31 +0,0 @@
-
-DESCRIPTION:
-
-An emacs mode to help editing Coq vernacular files.
-
-AUTHOR:
-
-Jean-Christophe Filliatre (jcfillia@lri.fr),
-	from the Caml mode of Xavier Leroy.
-
-CONTENTS:
-
-    gallina.el     A major mode for editing Coq files in Gnu Emacs
-
-USAGE:
-
-Add the following lines to your .emacs file:
-
-(setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist))
-(autoload 'coq-mode "gallina" "Major mode for editing Coq vernacular." t)
-
-The Coq major mode is triggered by visiting a file with extension .v,
-or manually by M-x coq-mode. It gives you the correct syntax table for
-the Coq language, and also a rudimentary indentation facility:
-
-- pressing TAB at the beginning of a line indents the line like the line above
-
-- extra TABs increase the indentation level (by 2 spaces by default)
-
-- M-TAB decreases the indentation level.
-
diff --git a/tools/check-translate b/tools/check-translate
deleted file mode 100755
index acb6f45903..0000000000
--- a/tools/check-translate
+++ /dev/null
@@ -1,23 +0,0 @@
-#!/bin/sh
-
-echo -------------- Producing translated files ---------------------
-rm */*/*.v8 >& /dev/null
-make COQOPTS=-translate theories || { echo ---- Failed to translate; exit 1; }
-if [ -e translated ]; then rm -r translated; fi
-if [ -e successful-translation ]; then rm -r successful-translation; fi
-if [ -e failed-translation ]; then rm -r failed-translation; fi
-mv theories translated
-mkdir theories
-echo -------------------- Upgrading files --------------------------
-cd translated
-for i in */*.v
-do
-  mkdir ../theories/`dirname $i` >& /dev/null
-  mv "$i"8 ../theories/$i
-done
-cd ..
-echo --------------- Recompiling translated files ------------------
-make theories || { echo ---- Failed to recompile; mv theories failed-translation; mv translated theories; exit 1; }
-echo ----------------- Recompilation successful --------------------
-if [ -e successful-translation ]; then rm -r successful-translation; fi
-mv theories successful-translation; mv translated theories
diff --git a/tools/coq-sl.sty b/tools/coq-sl.sty
deleted file mode 100644
index 9f6e5480c9..0000000000
--- a/tools/coq-sl.sty
+++ /dev/null
@@ -1,37 +0,0 @@
-% COQ style option, for use with the coq-latex filter.
-
-\typeout{Document Style option `coq-sl' <7 Apr 92>.}
-
-\ifcase\@ptsize
-    \font\sltt = cmsltt10
-\or \font\sltt = cmsltt10 \@halfmag
-\or \font\sltt = cmsltt10 \@magscale1
-\fi
-
-{\catcode`\^^M=\active %
- \gdef\@coqinputline#1^^M{\tt Coq < #1\par} %
- \gdef\@coqoutputline#1^^M{\sltt#1\par} } %
-\def\@coqblankline{\medskip}
-\chardef\@coqbackslash="5C
-
-\def\coq{
-  \bgroup
-  \flushleft
-  \parindent 0pt
-  \parskip 0pt
-  \let\do\@makeother\dospecials
-  \catcode`\^^M=\active
-  \catcode`\\=0
-  \catcode`\ \active
-  \frenchspacing
-  \@vobeyspaces
-  \let\?\@coqinputline
-  \let\:\@coqoutputline
-  \let\;\@coqblankline
-  \let\\\@coqbackslash
-}
-
-\def\endcoq{
-  \endflushleft
-  \egroup\noindent
-}
diff --git a/tools/coqdoc/dune b/tools/coqdoc/dune
index 8e05c7d97e..b20d9f9b2e 100644
--- a/tools/coqdoc/dune
+++ b/tools/coqdoc/dune
@@ -1,3 +1,9 @@
+(install
+ (section lib)
+ (files
+  (coqdoc.css as tools/coqdoc/coqdoc.css)
+  (coqdoc.sty as tools/coqdoc/coqdoc.sty)))
+
 (executable
  (name main)
  (public_name coqdoc)
diff --git a/tools/dune b/tools/dune
index 05a620fb07..20048fde52 100644
--- a/tools/dune
+++ b/tools/dune
@@ -1,8 +1,11 @@
-(executable
- (name coqc)
- (public_name coqc)
- (modules coqc)
- (libraries coq.toplevel))
+(install
+ (section lib)
+ (files
+  (CoqMakefile.in as tools/CoqMakefile.in)
+  (TimeFileMaker.py as tools/TimeFileMaker.py)
+  (make-one-time-file.py as tools/make-one-time-file.py)
+  (make-both-time-files.py as tools/make-both-time-files.py)
+  (make-both-single-timing-files.py as tools/make-both-single-timing-files.py)))
 
 (executable
  (name coq_makefile)
@@ -10,9 +13,11 @@
  (modules coq_makefile)
  (libraries coq.lib))
 
-(install
- (section lib)
- (files (CoqMakefile.in as tools/CoqMakefile.in)))
+(executable
+ (name coqc)
+ (public_name coqc)
+ (modules coqc)
+ (libraries coq.toplevel))
 
 (executable
  (name coqdep)
diff --git a/tools/mkwinapp.ml b/tools/mkwinapp.ml
deleted file mode 100644
index 226302fb2d..0000000000
--- a/tools/mkwinapp.ml
+++ /dev/null
@@ -1,92 +0,0 @@
-(* OCaml-Win32
- * mkwinapp.ml
- * Copyright (c) 2002-2004 by Harry Chomsky
- *
- * This library is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Library General Public
- * License as published by the Free Software Foundation; either
- * version 2 of the License, or (at your option) any later version.
- *
- * This library is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
- * Library General Public License for more details.
- *
- * You should have received a copy of the GNU Library General Public
- * License along with this library; if not, write to the Free
- * Software Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
- *)
-
-(*********************************************************************
- * This program alters an .exe file to make it use the "windows subsystem"
- * instead of the "console subsystem".  In other words, when Windows runs
- * the program, it will not create a console for it.
- *)
-
-(* Pierre Letouzey 23/12/2010 : modification to allow selecting the
-   subsystem to use instead of just setting the windows subsystem *)
-
-(* This tool can be run directly via :
-   ocaml unix.cma mkwinapp.ml [-set|-unset] <filename>
-*)
-
-exception Invalid_file_format
-
-let input_word ic =
-    let lo = input_byte ic in
-    let hi = input_byte ic in
-    (hi lsl 8) + lo
-
-let find_pe_header ic =
-    seek_in ic 0x3C;
-    let peheader = input_word ic in
-    seek_in ic peheader;
-    if input_char ic <> 'P' then
-        raise Invalid_file_format;
-    if input_char ic <> 'E' then
-        raise Invalid_file_format;
-    peheader
-
-let find_optional_header ic =
-    let peheader = find_pe_header ic in
-    let coffheader = peheader + 4 in
-    seek_in ic (coffheader + 16);
-    let optsize = input_word ic in
-    if optsize < 96 then
-        raise Invalid_file_format;
-    let optheader = coffheader + 20 in
-    seek_in ic optheader;
-    let magic = input_word ic in
-    if magic <> 0x010B && magic <> 0x020B then
-        raise Invalid_file_format;
-    optheader
-
-let change flag ic oc =
-    let optheader = find_optional_header ic in
-    seek_out oc (optheader + 64);
-    for i = 1 to 4 do
-        output_byte oc 0
-    done;
-    output_byte oc (if flag then 2 else 3)
-
-let usage () =
-  print_endline "Alters a Win32 executable file to use the Windows subsystem or not.";
-  print_endline "Usage: mkwinapp [-set|-unset] <filename>";
-  print_endline "Giving no option is equivalent to -set";
-  exit 1
-
-let main () =
-  let n = Array.length Sys.argv - 1 in
-  if not (n = 1 || n = 2) then usage ();
-  let flag =
-    if n = 1 then true
-    else if Sys.argv.(1) = "-set" then true
-    else if Sys.argv.(1) = "-unset" then false
-    else usage ()
-  in
-  let filename = Sys.argv.(n) in
-  let f = Unix.openfile filename [Unix.O_RDWR] 0 in
-  let ic = Unix.in_channel_of_descr f and oc = Unix.out_channel_of_descr f in
-  change flag ic oc
-
-let _ = main ()