Use standard library

test/Makefile

@@ -7,7 +7,7 @@
 ##         #     GNU Lesser General Public License Version 2.1          ##
 ##         #     (see LICENSE file for the text of the license)         ##
 ##########################################################################
-## GNUMakefile for Coq 8.15.1
+## GNUMakefile for Coq 8.17.0
 
 # For debugging purposes (must stay here, don't move below)
 INITIAL_VARS := $(.VARIABLES)
@@ -26,6 +26,7 @@ MLFILES           := $(COQMF_MLFILES)
 MLGFILES          := $(COQMF_MLGFILES)
 MLPACKFILES       := $(COQMF_MLPACKFILES)
 MLLIBFILES        := $(COQMF_MLLIBFILES)
+METAFILE          := $(COQMF_METAFILE)
 CMDLINE_VFILES    := $(COQMF_CMDLINE_VFILES)
 INSTALLCOQDOCROOT := $(COQMF_INSTALLCOQDOCROOT)
 OTHERFLAGS        := $(COQMF_OTHERFLAGS)
@@ -59,12 +60,12 @@ Makefile.conf: _CoqProject
 # practice is discouraged since _CoqProject better not contain make specific
 # code (be nice to user interfaces).
 
-# set KEEP_ERROR to prevent make from deleting files produced by failing rules.
-# For instance if coqc creates a .vo but then fails to native compile,
-# the .vo will be deleted unless KEEP_ERROR is nonempty.
+# Set KEEP_ERROR to have make keep files produced by failing rules.
+# By default, KEEP_ERROR is empty. So for instance if coqc creates a .vo but
+# then fails to native compile, the .vo will be deleted.
 # May confuse make so use only for debugging.
 KEEP_ERROR?=
-ifneq (,$(KEEP_ERROR))
+ifeq (,$(KEEP_ERROR))
 .DELETE_ON_ERROR:
 endif
 
@@ -75,7 +76,7 @@ VERBOSE ?=
 TIMED?=
 TIMECMD?=
 # Use command time on linux, gtime on Mac OS
-TIMEFMT?="$@ (real: %e, user: %U, sys: %S, mem: %M ko)"
+TIMEFMT?="$(if $(findstring undefined, $(flavor 1)),$@,$(1)) (real: %e, user: %U, sys: %S, mem: %M ko)"
 ifneq (,$(TIMED))
 ifeq (0,$(shell command time -f "" true >/dev/null 2>/dev/null; echo $$?))
 STDTIME?=command time -f $(TIMEFMT)
@@ -114,14 +115,11 @@ COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQCORELIB)/tools/make-both-single-timing
 BEFORE ?=
 AFTER ?=
 
-# FIXME this should be generated by Coq (modules already linked by Coq)
-CAMLDONTLINK=str,unix,dynlink,threads,zarith
-
 # OCaml binaries
 CAMLC       ?= "$(OCAMLFIND)" ocamlc   -c
 CAMLOPTC    ?= "$(OCAMLFIND)" opt      -c
-CAMLLINK    ?= "$(OCAMLFIND)" ocamlc   -linkpkg -dontlink $(CAMLDONTLINK)
-CAMLOPTLINK ?= "$(OCAMLFIND)" opt      -linkpkg -dontlink $(CAMLDONTLINK)
+CAMLLINK    ?= "$(OCAMLFIND)" ocamlc   -linkall
+CAMLOPTLINK ?= "$(OCAMLFIND)" opt      -linkall
 CAMLDOC     ?= "$(OCAMLFIND)" ocamldoc
 CAMLDEP     ?= "$(OCAMLFIND)" ocamldep -slash -ml-synonym .mlpack
 
@@ -134,6 +132,7 @@ COQDEBUG ?=
 
 # Extra packages to be linked in (as in findlib -package)
 CAMLPKGS ?=
+FINDLIBPKGS = -package coq-core.plugins.ltac $(CAMLPKGS)
 
 # Option for making timing files
 TIMING?=
@@ -170,8 +169,30 @@ destination_path = $(if $(DESTDIR),$(DESTDIR)/$(call windrive_path,$(1)),$(1))
 # Installation paths of libraries and documentation.
 COQLIBINSTALL ?= $(call destination_path,$(COQLIB)/user-contrib)
 COQDOCINSTALL ?= $(call destination_path,$(DOCDIR)/coq/user-contrib)
+COQPLUGININSTALL ?= $(call destination_path,$(COQCORELIB)/..)
 COQTOPINSTALL ?= $(call destination_path,$(COQLIB)/toploop) # FIXME: Unused variable?
 
+# findlib files installation
+FINDLIBPREINST= mkdir -p "$(COQPLUGININSTALL)/"
+FINDLIBDESTDIR= -destdir "$(COQPLUGININSTALL)/"
+
+# we need to move out of sight $(METAFILE) otherwise findlib thinks the
+# package is already installed
+findlib_install = \
+	$(HIDE)if [ "$(METAFILE)" ]; then \
+	  $(FINDLIBPREINST) && \
+	  mv "$(METAFILE)" "$(METAFILE).skip" ; \
+	  "$(OCAMLFIND)" install $(2) $(FINDLIBDESTDIR) $(FINDLIBPACKAGE) $(1); \
+	  rc=$$?; \
+	  mv "$(METAFILE).skip" "$(METAFILE)"; \
+	  exit $$rc; \
+	fi
+findlib_remove = \
+	$(HIDE)if [ ! -z "$(METAFILE)" ]; then\
+	  "$(OCAMLFIND)" remove $(FINDLIBDESTDIR) $(FINDLIBPACKAGE); \
+	fi
+
+
 ########## End of parameters ##################################################
 # What follows may be relevant to you only if you need to
 # extend this Makefile.  If so, look for 'Extension point' here and
@@ -257,14 +278,14 @@ COQDOCLIBS?=$(COQLIBS_NOML)
 # The version of Coq being run and the version of coq_makefile that
 # generated this makefile
 COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1)
-COQMAKEFILE_VERSION:=8.15.1
+COQMAKEFILE_VERSION:=8.17.0
 
 # COQ_SRC_SUBDIRS is for user-overriding, usually to add
 # `user-contrib/Foo` to the includes, we keep COQCORE_SRC_SUBDIRS for
 # Coq's own core libraries, which should be replaced by ocamlfind
 # options at some point.
 COQ_SRC_SUBDIRS?=
-COQSRCLIBS?= $(foreach d,$(COQCORE_SRC_SUBDIRS), -I "$(COQCORELIB)/$(d)") $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)/$(d)")
+COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)/$(d)")
 
 CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS)
 # ocamldoc fails with unknown argument otherwise
@@ -358,6 +379,8 @@ ALLNATIVEFILES = \
 	$(OBJFILES:.o=.cmi) \
 	$(OBJFILES:.o=.cmx) \
 	$(OBJFILES:.o=.cmxs)
+FINDLIBPACKAGE=$(patsubst .%,%,$(suffix $(METAFILE)))
+
 # trick: wildcard filters out non-existing files, so that `install` doesn't show
 # warnings and `clean` doesn't pass to rm a list of files that is too long for
 # the shell.
@@ -367,13 +390,12 @@ FILESTOINSTALL = \
 	$(VFILES) \
 	$(GLOBFILES) \
 	$(NATIVEFILES) \
+	$(CMXSFILES)		# to be removed when we remove legacy loading
+FINDLIBFILESTOINSTALL = \
 	$(CMIFILESTOINSTALL)
-BYTEFILESTOINSTALL = \
-	$(CMOFILESTOINSTALL) \
-	$(CMAFILES)
 ifeq '$(HASNATDYNLINK)' 'true'
 DO_NATDYNLINK = yes
-FILESTOINSTALL += $(CMXSFILES) $(CMXAFILES) $(CMOFILESTOINSTALL:.cmo=.cmx)
+FINDLIBFILESTOINSTALL += $(CMXSFILES) $(CMXAFILES) $(CMOFILESTOINSTALL:.cmo=.cmx)
 else
 DO_NATDYNLINK =
 endif
@@ -529,12 +551,12 @@ mlihtml: $(MLIFILES:.mli=.cmi)
 	$(SHOW)'CAMLDOC -d $@'
 	$(HIDE)mkdir $@ || rm -rf $@/*
 	$(HIDE)$(CAMLDOC) -html \
-		-d $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES)
+		-d $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES) $(FINDLIBPKGS)
 
 all-mli.tex: $(MLIFILES:.mli=.cmi)
 	$(SHOW)'CAMLDOC -latex $@'
 	$(HIDE)$(CAMLDOC) -latex \
-		-o $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES)
+		-o $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES) $(FINDLIBPKGS)
 
 all.ps: $(VFILES)
 	$(SHOW)'COQDOC -ps $(GAL)'
@@ -570,7 +592,9 @@ beautify: $(BEAUTYFILES)
 # There rules can be extended in Makefile.local
 # Extensions can't assume when they run.
 
-install:
+# findlib needs the package to not be installed, so we remove it before
+# installing it (see the call to findlib_remove)
+install: META
 	$(HIDE)code=0; for f in $(FILESTOINSTALL); do\
 	 if ! [ -f "$$f" ]; then >&2 echo $$f does not exist; code=1; fi \
 	done; exit $$code
@@ -584,22 +608,20 @@ install:
 	   echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\
 	 fi;\
 	done
+	$(call findlib_remove)
+	$(call findlib_install, META $(FINDLIBFILESTOINSTALL))
 	$(HIDE)$(MAKE) install-extra -f "$(SELF)"
 install-extra::
 	@# Extension point
 .PHONY: install install-extra
 
+META: $(METAFILE)
+	$(HIDE)if [ "$(METAFILE)" ]; then \
+		cat "$(METAFILE)" | grep -v 'directory.*=.*' > META; \
+	fi
+
 install-byte:
-	$(HIDE)for f in $(BYTEFILESTOINSTALL); do\
-	 df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\
-	 if [ "$$?" != "0" -o -z "$$df" ]; then\
-	   echo SKIP "$$f" since it has no logical path;\
-	 else\
-	   install -d "$(COQLIBINSTALL)/$$df" &&\
-	   install -m 0644 "$$f" "$(COQLIBINSTALL)/$$df" &&\
-	   echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\
-	 fi;\
-	done
+	$(call findlib_install, $(CMAFILES) $(CMOFILESTOINSTALL), -add)
 
 install-doc:: html mlihtml
 	@# Extension point
@@ -620,13 +642,19 @@ install-doc:: html mlihtml
 
 uninstall::
 	@# Extension point
+	$(call findlib_remove)
 	$(HIDE)for f in $(FILESTOINSTALL); do \
 	 df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\
 	 instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\
 	 rm -f "$$instf" &&\
-	 echo RM "$$instf" &&\
+	 echo RM "$$instf" ;\
+	done
+	$(HIDE)for f in $(FILESTOINSTALL); do \
+	 df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\
+	 echo RMDIR "$(COQLIBINSTALL)/$$df/" &&\
 	 (rmdir "$(COQLIBINSTALL)/$$df/" 2>/dev/null || true); \
 	done
+
 .PHONY: uninstall
 
 uninstall-doc::
@@ -649,12 +677,14 @@ clean::
 	$(HIDE)rm -f $(CMOFILES)
 	$(HIDE)rm -f $(CMIFILES)
 	$(HIDE)rm -f $(CMAFILES)
-	$(HIDE)rm -f $(CMOFILES:.cmo=.cmx)
+	$(HIDE)rm -f $(CMXFILES)
 	$(HIDE)rm -f $(CMXAFILES)
 	$(HIDE)rm -f $(CMXSFILES)
-	$(HIDE)rm -f $(CMOFILES:.cmo=.o)
+	$(HIDE)rm -f $(OFILES)
 	$(HIDE)rm -f $(CMXAFILES:.cmxa=.a)
 	$(HIDE)rm -f $(MLGFILES:.mlg=.ml)
+	$(HIDE)rm -f $(CMXFILES:.cmx=.cmt)
+	$(HIDE)rm -f $(MLIFILES:.mli=.cmti)
 	$(HIDE)rm -f $(ALLDFILES)
 	$(HIDE)rm -f $(NATIVEFILES)
 	$(HIDE)find . -name .coq-native -type d -empty -delete
@@ -668,6 +698,7 @@ clean::
 	$(HIDE)rm -f $(VFILES:.v=.tex)
 	$(HIDE)rm -f $(VFILES:.v=.g.tex)
 	$(HIDE)rm -f pretty-timed-success.ok
+	$(HIDE)rm -f META
 	$(HIDE)rm -rf html mlihtml
 .PHONY: clean
 
@@ -695,7 +726,7 @@ archclean::
 
 $(MLIFILES:.mli=.cmi): %.cmi: %.mli
 	$(SHOW)'CAMLC -c $<'
-	$(HIDE)$(TIMER) $(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $<
+	$(HIDE)$(TIMER) $(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) $<
 
 $(MLGFILES:.mlg=.ml): %.ml: %.mlg
 	$(SHOW)'COQPP $<'
@@ -704,53 +735,53 @@ $(MLGFILES:.mlg=.ml): %.ml: %.mlg
 # Stupid hack around a deficient syntax: we cannot concatenate two expansions
 $(filter %.cmo, $(MLFILES:.ml=.cmo) $(MLGFILES:.mlg=.cmo)): %.cmo: %.ml
 	$(SHOW)'CAMLC -c $<'
-	$(HIDE)$(TIMER) $(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $<
+	$(HIDE)$(TIMER) $(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) $<
 
 # Same hack
 $(filter %.cmx, $(MLFILES:.ml=.cmx) $(MLGFILES:.mlg=.cmx)): %.cmx: %.ml
 	$(SHOW)'CAMLOPT -c $(FOR_PACK) $<'
-	$(HIDE)$(TIMER) $(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(FOR_PACK) $<
+	$(HIDE)$(TIMER) $(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) $(FOR_PACK) $<
 
 
 $(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa
 	$(SHOW)'CAMLOPT -shared -o $@'
-	$(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
-		-linkall -shared -o $@ $<
+	$(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) \
+		-shared -o $@ $<
 
 $(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib
 	$(SHOW)'CAMLC -a -o $@'
-	$(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^
+	$(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $^
 
 $(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib
 	$(SHOW)'CAMLOPT -a -o $@'
-	$(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $^
+	$(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $^
 
 
 $(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmxa
 	$(SHOW)'CAMLOPT -shared -o $@'
-	$(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
-		-shared -linkall -o $@ $<
+	$(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) \
+		-shared -o $@ $<
 
-$(MLPACKFILES:.mlpack=.cmxa): %.cmxa: %.cmx
+$(MLPACKFILES:.mlpack=.cmxa): %.cmxa: %.cmx | %.mlpack
 	$(SHOW)'CAMLOPT -a -o $@'
-	$(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $<
+	$(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $<
 
 $(MLPACKFILES:.mlpack=.cma): %.cma: %.cmo | %.mlpack
 	$(SHOW)'CAMLC -a -o $@'
-	$(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^
+	$(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $^
 
 $(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack
 	$(SHOW)'CAMLC -pack -o $@'
-	$(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^
+	$(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -pack -o $@ $^
 
 $(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack
 	$(SHOW)'CAMLOPT -pack -o $@'
-	$(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^
+	$(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -pack -o $@ $^
 
 # This rule is for _CoqProject with no .mllib nor .mlpack
 $(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(MLGFILES:.mlg=.cmxs)): %.cmxs: %.cmx
 	$(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@'
-	$(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
+	$(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) \
 		-shared -o $@ $<
 
 ifneq (,$(TIMING))
@@ -759,17 +790,43 @@ else
 TIMING_EXTRA =
 endif
 
+# can't make
+# https://www.gnu.org/software/make/manual/make.html#Static-Pattern
+# work with multiple target rules
+# so use eval in a loop instead
+# with grouped targets https://www.gnu.org/software/make/manual/make.html#Multiple-Targets
+# if available (GNU Make >= 4.3)
+ifneq (,$(filter grouped-target,$(.FEATURES)))
+define globvorule=
+
+# take care to $$ variables using $< etc
+  $(1).vo $(1).glob &: $(1).v | $(VDFILE)
+	$(SHOW)COQC $(1).v
+	$(HIDE)$$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $(1).v $$(TIMING_EXTRA)
+ifeq ($(COQDONATIVE), "yes")
+	$(SHOW)COQNATIVE $(1).vo
+	$(HIDE)$(call TIMER,$(1).vo.native) $(COQNATIVE) $(COQLIBS) $(1).vo
+endif
+
+endef
+else
+
 $(VOFILES): %.vo: %.v | $(VDFILE)
 	$(SHOW)COQC $<
 	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $< $(TIMING_EXTRA)
 ifeq ($(COQDONATIVE), "yes")
 	$(SHOW)COQNATIVE $@
-	$(HIDE)$(COQNATIVE) $(COQLIBS) $@
+	$(HIDE)$(call TIMER,[email protected]) $(COQNATIVE) $(COQLIBS) $@
 endif
 
-# FIXME ?merge with .vo / .vio ?
+# this is broken :( todo fix if we ever find a solution that doesn't need grouped targets
 $(GLOBFILES): %.glob: %.v
-	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
+	$(SHOW)'COQC $< (for .glob)'
+	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
+
+endif
+
+$(foreach vfile,$(VFILES:.v=),$(eval $(call globvorule,$(vfile))))
 
 $(VFILES:.v=.vio): %.vio: %.v
 	$(SHOW)COQC -vio $<
@@ -851,7 +908,7 @@ VDFILE_FLAGS:=$(if _CoqProject,-f _CoqProject,) $(CMDLINE_COQLIBS) $(CMDLINE_VFI
 
 $(VDFILE): _CoqProject $(VFILES)
 	$(SHOW)'COQDEP VFILES'
-	$(HIDE)$(COQDEP) -vos -dyndep var $(VDFILE_FLAGS) $(redir_if_ok)
+	$(HIDE)$(COQDEP) $(if $(strip $(METAFILE)),-m "$(METAFILE)") -vos -dyndep var $(VDFILE_FLAGS) $(redir_if_ok)
 
 # Misc ########################################################################
 

theories/Number.v

@@ -14,15 +14,6 @@ From Parsec Require Export
 Export FunctorNotation.
 Open Scope lazy_bool_scope.
 
-Definition ltb (a b : ascii) : bool :=
-  (N_of_ascii a <?  N_of_ascii b)%N.
-
-Definition leb (a b : ascii) : bool :=
-  (N_of_ascii a <=? N_of_ascii b)%N.
-
-Infix "<?"  := ltb : char_scope.
-Infix "<=?" := leb : char_scope.
-
 Definition isupper (a : ascii) : bool :=
   (("A" <=? a) &&& (a <=? "Z"))%char.