From accc9fa1f5689d1bf57d3024c4ad293fd10f3617 Mon Sep 17 00:00:00 2001
From: Jason Gross <jagro@google.com>
Date: Wed, 22 Jun 2016 11:47:16 -0700
Subject: Make Coq 8.5 the default target for Fiat-Crypto

Instructions for 8.4 build in the README
---
 coqprime/Makefile | 160 ++++++++++++++++++++++++++++++++++++++----------------
 1 file changed, 113 insertions(+), 47 deletions(-)

(limited to 'coqprime/Makefile')

diff --git a/coqprime/Makefile b/coqprime/Makefile
index 8fa838a1e..c8e44a658 100644
--- a/coqprime/Makefile
+++ b/coqprime/Makefile
@@ -2,7 +2,7 @@
 ##  v      #                   The Coq Proof Assistant                     ##
 ## <O___,, #                INRIA - CNRS - LIX - LRI - PPS                 ##
 ##   \VV/  #                                                               ##
-##    //   #  Makefile automagically generated by coq_makefile V8.4pl6     ##
+##    //   #  Makefile automagically generated by coq_makefile V8.5pl1     ##
 #############################################################################
 
 # WARNING
@@ -19,9 +19,10 @@
 
 .DEFAULT_GOAL := all
 
-# 
 # This Makefile may take arguments passed as environment variables:
 # COQBIN to specify the directory where Coq binaries resides;
+# TIMECMD set a command to log .v compilation time;
+# TIMED if non empty, use the default time command as TIMECMD;
 # ZDEBUG/COQDEBUG to specify debug flags for ocamlc&ocamlopt/coqc;
 # DSTROOT to specify a prefix to install path.
 
@@ -33,14 +34,25 @@ endef
 includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr -d '\r' | tr '\n' '@'; })))
 $(call includecmdwithout@,$(COQBIN)coqtop -config)
 
+TIMED=
+TIMECMD=
+STDTIME?=/usr/bin/time -f "$* (user: %U mem: %M ko)"
+TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
+
+vo_to_obj = $(addsuffix .o,\
+  $(filter-out Warning: Error:,\
+  $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(1))))
+
 ##########################
 #                        #
 # Libraries definitions. #
 #                        #
 ##########################
 
-COQLIBS?= -R Coqprime Coqprime
-COQDOCLIBS?=-R Coqprime Coqprime
+COQLIBS?=\
+  -R "Coqprime" Coqprime
+COQDOCLIBS?=\
+  -R "Coqprime" Coqprime
 
 ##########################
 #                        #
@@ -54,10 +66,11 @@ COQDEP?="$(COQBIN)coqdep" -c
 COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
 COQCHKFLAGS?=-silent -o
 COQDOCFLAGS?=-interpolate -utf8
-COQC?="$(COQBIN)coqc"
+COQC?=$(TIMER) "$(COQBIN)coqc"
 GALLINA?="$(COQBIN)gallina"
 COQDOC?="$(COQBIN)coqdoc"
 COQCHK?="$(COQBIN)coqchk"
+COQMKTOP?="$(COQBIN)coqmktop"
 
 ##################
 #                #
@@ -72,6 +85,7 @@ COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq
 else
 COQLIBINSTALL="${COQLIB}user-contrib"
 COQDOCINSTALL="${DOCDIR}user-contrib"
+COQTOPINSTALL="${COQLIB}toploop"
 endif
 
 ######################
@@ -80,40 +94,51 @@ endif
 #                    #
 ######################
 
-VFILES:=Coqprime/Zp.v\
-  Coqprime/ZSum.v\
-  Coqprime/ZProgression.v\
-  Coqprime/ZCmisc.v\
-  Coqprime/ZCAux.v\
-  Coqprime/UList.v\
-  Coqprime/Tactic.v\
-  Coqprime/Root.v\
-  Coqprime/PocklingtonCertificat.v\
-  Coqprime/Pocklington.v\
-  Coqprime/Pmod.v\
-  Coqprime/Permutation.v\
-  Coqprime/PGroup.v\
-  Coqprime/NatAux.v\
-  Coqprime/LucasLehmer.v\
-  Coqprime/ListAux.v\
-  Coqprime/Lagrange.v\
-  Coqprime/Iterator.v\
-  Coqprime/IGroup.v\
-  Coqprime/FGroup.v\
-  Coqprime/Euler.v\
+VFILES:=Coqprime/Cyclic.v\
   Coqprime/EGroup.v\
-  Coqprime/Cyclic.v
+  Coqprime/Euler.v\
+  Coqprime/FGroup.v\
+  Coqprime/IGroup.v\
+  Coqprime/Iterator.v\
+  Coqprime/Lagrange.v\
+  Coqprime/ListAux.v\
+  Coqprime/LucasLehmer.v\
+  Coqprime/NatAux.v\
+  Coqprime/PGroup.v\
+  Coqprime/Permutation.v\
+  Coqprime/Pmod.v\
+  Coqprime/Pocklington.v\
+  Coqprime/PocklingtonCertificat.v\
+  Coqprime/Root.v\
+  Coqprime/Tactic.v\
+  Coqprime/UList.v\
+  Coqprime/ZCAux.v\
+  Coqprime/ZCmisc.v\
+  Coqprime/ZProgression.v\
+  Coqprime/ZSum.v\
+  Coqprime/Zp.v
 
+ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),)
+-include $(addsuffix .d,$(VFILES))
+else
+ifeq ($(MAKECMDGOALS),)
 -include $(addsuffix .d,$(VFILES))
+endif
+endif
+
 .SECONDARY: $(addsuffix .d,$(VFILES))
 
-VOFILES:=$(VFILES:.v=.vo)
+VO=vo
+VOFILES:=$(VFILES:.v=.$(VO))
 VOFILES1=$(patsubst Coqprime/%,%,$(filter Coqprime/%,$(VOFILES)))
 GLOBFILES:=$(VFILES:.v=.glob)
-VIFILES:=$(VFILES:.v=.vi)
 GFILES:=$(VFILES:.v=.g)
 HTMLFILES:=$(VFILES:.v=.html)
 GHTMLFILES:=$(VFILES:.v=.g.html)
+OBJFILES=$(call vo_to_obj,$(VOFILES))
+ALLNATIVEFILES=$(OBJFILES:.o=.cmi) $(OBJFILES:.o=.cmo) $(OBJFILES:.o=.cmx) $(OBJFILES:.o=.cmxs)
+NATIVEFILES=$(foreach f, $(ALLNATIVEFILES), $(wildcard $f))
+NATIVEFILES1=$(patsubst Coqprime/%,%,$(filter Coqprime/%,$(NATIVEFILES)))
 ifeq '$(HASNATDYNLINK)' 'true'
 HASNATDYNLINK_OR_EMPTY := yes
 else
@@ -128,8 +153,12 @@ endif
 
 all: $(VOFILES) 
 
-spec: $(VIFILES)
+quick: $(VOFILES:.vo=.vio)
 
+vio2vo:
+	$(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio)
+checkproofs:
+	$(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio)
 gallina: $(GFILES)
 
 html: $(GLOBFILES) $(VFILES)
@@ -160,7 +189,7 @@ beautify: $(VFILES:=.beautified)
 	@echo 'Do not do "make clean" until you are sure that everything went well!'
 	@echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/'
 
-.PHONY: all opt byte archclean clean install userinstall depend html validate
+.PHONY: all archclean beautify byte clean cleanall gallina gallinahtml html install install-doc install-natdynlink install-toploop opt printenv quick uninstall userinstall validate vio2vo
 
 ####################
 #                  #
@@ -178,7 +207,7 @@ userinstall:
 	+$(MAKE) USERINSTALL=true install
 
 install:
-	cd "Coqprime"; for i in $(VOFILES1); do \
+	cd "Coqprime" && for i in $(NATIVEFILES1) $(GLOBFILES1) $(VFILES1) $(VOFILES1); do \
 	 install -d "`dirname "$(DSTROOT)"$(COQLIBINSTALL)/Coqprime/$$i`"; \
 	 install -m 0644 $$i "$(DSTROOT)"$(COQLIBINSTALL)/Coqprime/$$i; \
 	done
@@ -189,12 +218,46 @@ install-doc:
 	 install -m 0644 $$i "$(DSTROOT)"$(COQDOCINSTALL)/Coqprime/$$i;\
 	done
 
-clean:
-	rm -f $(VOFILES) $(VIFILES) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)
+uninstall_me.sh: Makefile
+	echo '#!/bin/sh' > $@
+	printf 'cd "$${DSTROOT}"$(COQLIBINSTALL)/Coqprime && rm -f $(NATIVEFILES1) $(GLOBFILES1) $(VFILES1) $(VOFILES1) && find . -type d -and -empty -delete\ncd "$${DSTROOT}"$(COQLIBINSTALL) && find "Coqprime" -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n' >> "$@"
+	printf 'cd "$${DSTROOT}"$(COQDOCINSTALL)/Coqprime \\\n' >> "$@"
+	printf '&& rm -f $(shell find "html" -maxdepth 1 -and -type f -print)\n' >> "$@"
+	printf 'cd "$${DSTROOT}"$(COQDOCINSTALL) && find Coqprime/html -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n' >> "$@"
+	chmod +x $@
+
+uninstall: uninstall_me.sh
+	sh $<
+
+.merlin:
+	@echo 'FLG -rectypes' > .merlin
+	@echo "B $(COQLIB) kernel" >> .merlin
+	@echo "B $(COQLIB) lib" >> .merlin
+	@echo "B $(COQLIB) library" >> .merlin
+	@echo "B $(COQLIB) parsing" >> .merlin
+	@echo "B $(COQLIB) pretyping" >> .merlin
+	@echo "B $(COQLIB) interp" >> .merlin
+	@echo "B $(COQLIB) printing" >> .merlin
+	@echo "B $(COQLIB) intf" >> .merlin
+	@echo "B $(COQLIB) proofs" >> .merlin
+	@echo "B $(COQLIB) tactics" >> .merlin
+	@echo "B $(COQLIB) tools" >> .merlin
+	@echo "B $(COQLIB) toplevel" >> .merlin
+	@echo "B $(COQLIB) stm" >> .merlin
+	@echo "B $(COQLIB) grammar" >> .merlin
+	@echo "B $(COQLIB) config" >> .merlin
+
+clean::
+	rm -f $(OBJFILES) $(OBJFILES:.o=.native) $(NATIVEFILES)
+	find . -name .coq-native -type d -empty -delete
+	rm -f $(VOFILES) $(VOFILES:.vo=.vio) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)
 	rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex
-	- rm -rf html mlihtml
+	- rm -rf html mlihtml uninstall_me.sh
 
-archclean:
+cleanall:: clean
+	rm -f $(patsubst %.v,.%.aux,$(VFILES))
+
+archclean::
 	rm -f *.cmx *.o
 
 printenv:
@@ -217,31 +280,34 @@ Makefile: _CoqProject
 #                 #
 ###################
 
-%.vo %.glob: %.v
+$(VOFILES): %.vo: %.v
+	$(COQC) $(COQDEBUG) $(COQFLAGS) $*
+
+$(GLOBFILES): %.glob: %.v
 	$(COQC) $(COQDEBUG) $(COQFLAGS) $*
 
-%.vi: %.v
-	$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*
+$(VFILES:.v=.vio): %.vio: %.v
+	$(COQC) -quick $(COQDEBUG) $(COQFLAGS) $*
 
-%.g: %.v
+$(GFILES): %.g: %.v
 	$(GALLINA) $<
 
-%.tex: %.v
+$(VFILES:.v=.tex): %.tex: %.v
 	$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@
 
-%.html: %.v %.glob
+$(HTMLFILES): %.html: %.v %.glob
 	$(COQDOC) $(COQDOCFLAGS) -html $< -o $@
 
-%.g.tex: %.v
+$(VFILES:.v=.g.tex): %.g.tex: %.v
 	$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@
 
-%.g.html: %.v %.glob
+$(GHTMLFILES): %.g.html: %.v %.glob
 	$(COQDOC) $(COQDOCFLAGS)  -html -g $< -o $@
 
-%.v.d: %.v
-	$(COQDEP) -slash $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
+$(addsuffix .d,$(VFILES)): %.v.d: %.v
+	$(COQDEP) $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
 
-%.v.beautified:
+$(addsuffix .beautified,$(VFILES)): %.v.beautified:
 	$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*
 
 # WARNING
-- 
cgit v1.2.3