From 27a6a3c21869e3816a96b91bddaa85717d966419 Mon Sep 17 00:00:00 2001
From: Zhen Zhang <izgzhen@gmail.com>
Date: Sun, 11 Sep 2016 14:41:58 +0200
Subject: [PATCH] Add makefiles
---
.gitignore | 2 +-
Makefile | 20 ++++
Makefile.coq | 305 +++++++++++++++++++++++++++++++++++++++++++++++++++
3 files changed, 326 insertions(+), 1 deletion(-)
create mode 100644 Makefile
create mode 100644 Makefile.coq
diff --git a/.gitignore b/.gitignore
index 51e5e61..7d84ea0 100644
--- a/.gitignore
+++ b/.gitignore
@@ -9,4 +9,4 @@
*~
*.bak
.coq-native/
-Makefile*
+
diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..6c554b2
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,20 @@
+# Makefile originally taken from coq-club
+
+%: Makefile.coq
+ +make -f Makefile.coq $@
+
+all: Makefile.coq
+ +make -f Makefile.coq all
+
+clean: Makefile.coq
+ +make -f Makefile.coq clean
+ rm -f Makefile.coq
+
+Makefile.coq: _CoqProject Makefile
+ coq_makefile -f _CoqProject | sed 's/$$(COQCHK) $$(COQCHKFLAGS) $$(COQLIBS)/$$(COQCHK) $$(COQCHKFLAGS) $$(subst -Q,-R,$$(COQLIBS))/' > Makefile.coq
+
+_CoqProject: ;
+
+Makefile: ;
+
+.PHONY: all clean
diff --git a/Makefile.coq b/Makefile.coq
new file mode 100644
index 0000000..f4d7a39
--- /dev/null
+++ b/Makefile.coq
@@ -0,0 +1,305 @@
+#############################################################################
+## v # The Coq Proof Assistant ##
+## <O___,, # INRIA - CNRS - LIX - LRI - PPS ##
+## \VV/ # ##
+## // # Makefile automagically generated by coq_makefile V8.5pl2 ##
+#############################################################################
+
+# WARNING
+#
+# This Makefile has been automagically generated
+# Edit at your own risks !
+#
+# END OF WARNING
+
+#
+# This Makefile was generated by the command line :
+# coq_makefile -f _CoqProject
+#
+
+.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.
+
+# Here is a hack to make $(eval $(shell works:
+define donewline
+
+
+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?=\
+ -Q "." flatcomb
+COQCHKLIBS?=\
+ -R "." flatcomb
+COQDOCLIBS?=\
+ -R "." flatcomb
+
+##########################
+# #
+# Variables definitions. #
+# #
+##########################
+
+
+OPT?=
+COQDEP?="$(COQBIN)coqdep" -c
+COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
+COQCHKFLAGS?=-silent -o
+COQDOCFLAGS?=-interpolate -utf8
+COQC?=$(TIMER) "$(COQBIN)coqc"
+GALLINA?="$(COQBIN)gallina"
+COQDOC?="$(COQBIN)coqdoc"
+COQCHK?="$(COQBIN)coqchk"
+COQMKTOP?="$(COQBIN)coqmktop"
+
+##################
+# #
+# Install Paths. #
+# #
+##################
+
+ifdef USERINSTALL
+XDG_DATA_HOME?="$(HOME)/.local/share"
+COQLIBINSTALL=$(XDG_DATA_HOME)/coq
+COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq
+else
+COQLIBINSTALL="${COQLIB}user-contrib"
+COQDOCINSTALL="${DOCDIR}user-contrib"
+COQTOPINSTALL="${COQLIB}toploop"
+endif
+
+######################
+# #
+# Files dispatching. #
+# #
+######################
+
+VFILES:=incr.v\
+ sync.v\
+ pair_cas.v\
+ flat.v\
+ sync_stack.v\
+ treiber_stack.v\
+ protocol.v\
+ misc.v\
+ atomic_pair.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))
+
+VO=vo
+VOFILES:=$(VFILES:.v=.$(VO))
+GLOBFILES:=$(VFILES:.v=.glob)
+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))
+ifeq '$(HASNATDYNLINK)' 'true'
+HASNATDYNLINK_OR_EMPTY := yes
+else
+HASNATDYNLINK_OR_EMPTY :=
+endif
+
+#######################################
+# #
+# Definition of the toplevel targets. #
+# #
+#######################################
+
+all: $(VOFILES)
+
+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)
+ - mkdir -p html
+ $(COQDOC) -toc $(COQDOCFLAGS) -html $(COQDOCLIBS) -d html $(VFILES)
+
+gallinahtml: $(GLOBFILES) $(VFILES)
+ - mkdir -p html
+ $(COQDOC) -toc $(COQDOCFLAGS) -html -g $(COQDOCLIBS) -d html $(VFILES)
+
+all.ps: $(VFILES)
+ $(COQDOC) -toc $(COQDOCFLAGS) -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
+
+all-gal.ps: $(VFILES)
+ $(COQDOC) -toc $(COQDOCFLAGS) -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
+
+all.pdf: $(VFILES)
+ $(COQDOC) -toc $(COQDOCFLAGS) -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
+
+all-gal.pdf: $(VFILES)
+ $(COQDOC) -toc $(COQDOCFLAGS) -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
+
+validate: $(VOFILES)
+ $(COQCHK) $(COQCHKFLAGS) $(COQCHKLIBS) $(notdir $(^:.vo=))
+
+beautify: $(VFILES:=.beautified)
+ for file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done
+ @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 archclean beautify byte clean cleanall gallina gallinahtml html install install-doc install-natdynlink install-toploop opt printenv quick uninstall userinstall validate vio2vo
+
+####################
+# #
+# Special targets. #
+# #
+####################
+
+byte:
+ $(MAKE) all "OPT:=-byte"
+
+opt:
+ $(MAKE) all "OPT:=-opt"
+
+userinstall:
+ +$(MAKE) USERINSTALL=true install
+
+install:
+ cd "." && for i in $(VOFILES) $(VFILES) $(GLOBFILES) $(NATIVEFILES) $(CMOFILES) $(CMIFILES) $(CMAFILES); do \
+ install -d "`dirname "$(DSTROOT)"$(COQLIBINSTALL)/flatcomb/$$i`"; \
+ install -m 0644 $$i "$(DSTROOT)"$(COQLIBINSTALL)/flatcomb/$$i; \
+ done
+
+install-doc:
+ install -d "$(DSTROOT)"$(COQDOCINSTALL)/flatcomb/html
+ for i in html/*; do \
+ install -m 0644 $$i "$(DSTROOT)"$(COQDOCINSTALL)/flatcomb/$$i;\
+ done
+
+uninstall_me.sh: Makefile
+ echo '#!/bin/sh' > $@
+ printf 'cd "$${DSTROOT}"$(COQLIBINSTALL)/flatcomb && rm -f $(VOFILES) $(VFILES) $(GLOBFILES) $(NATIVEFILES) $(CMOFILES) $(CMIFILES) $(CMAFILES) && find . -type d -and -empty -delete\ncd "$${DSTROOT}"$(COQLIBINSTALL) && find "flatcomb" -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n' >> "$@"
+ printf 'cd "$${DSTROOT}"$(COQDOCINSTALL)/flatcomb \\\n' >> "$@"
+ printf '&& rm -f $(shell find "html" -maxdepth 1 -and -type f -print)\n' >> "$@"
+ printf 'cd "$${DSTROOT}"$(COQDOCINSTALL) && find flatcomb/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 uninstall_me.sh
+
+cleanall:: clean
+ rm -f $(patsubst %.v,.%.aux,$(VFILES))
+
+archclean::
+ rm -f *.cmx *.o
+
+printenv:
+ @"$(COQBIN)coqtop" -config
+ @echo 'CAMLC = $(CAMLC)'
+ @echo 'CAMLOPTC = $(CAMLOPTC)'
+ @echo 'PP = $(PP)'
+ @echo 'COQFLAGS = $(COQFLAGS)'
+ @echo 'COQLIBINSTALL = $(COQLIBINSTALL)'
+ @echo 'COQDOCINSTALL = $(COQDOCINSTALL)'
+
+Makefile: _CoqProject
+ mv -f $@ $@.bak
+ "$(COQBIN)coq_makefile" -f $< -o $@
+
+
+###################
+# #
+# Implicit rules. #
+# #
+###################
+
+$(VOFILES): %.vo: %.v
+ $(COQC) $(COQDEBUG) $(COQFLAGS) $<
+
+$(GLOBFILES): %.glob: %.v
+ $(COQC) $(COQDEBUG) $(COQFLAGS) $<
+
+$(VFILES:.v=.vio): %.vio: %.v
+ $(COQC) -quick $(COQDEBUG) $(COQFLAGS) $<
+
+$(GFILES): %.g: %.v
+ $(GALLINA) $<
+
+$(VFILES:.v=.tex): %.tex: %.v
+ $(COQDOC) $(COQDOCFLAGS) -latex $< -o $@
+
+$(HTMLFILES): %.html: %.v %.glob
+ $(COQDOC) $(COQDOCFLAGS) -html $< -o $@
+
+$(VFILES:.v=.g.tex): %.g.tex: %.v
+ $(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@
+
+$(GHTMLFILES): %.g.html: %.v %.glob
+ $(COQDOC) $(COQDOCFLAGS) -html -g $< -o $@
+
+$(addsuffix .d,$(VFILES)): %.v.d: %.v
+ $(COQDEP) $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
+
+$(addsuffix .beautified,$(VFILES)): %.v.beautified:
+ $(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*.v
+
+# WARNING
+#
+# This Makefile has been automagically generated
+# Edit at your own risks !
+#
+# END OF WARNING
+
--
GitLab