Commit 606a013e authored by Benoit Viguier's avatar Benoit Viguier
Browse files

generate Makefile automatically

parent 069a1965
......@@ -34,6 +34,9 @@ ipch
Doc
*.sublime-project
usenix*
.coqdeps.d
Makefile.conf
Makefile
# Created by https://www.gitignore.io/api/latex,c++,coq,c,ocaml,sublimetext,vim,emacs
......
......@@ -345,7 +345,6 @@ Proof.
2: omega.
rewrite Z.log2_pow2.
2: omega.
Search Z.max.
apply Z.max_case ; assumption.
}
omega.
......
default_target: .loadpath Libs ListsOp Mid Low
all: default_target High
#Note3: for SSReflect, one solution is to install MathComp 1.6
# somewhere add this line to a CONFIGURE file
# MATHCOMP=/my/path/to/mathcomp
VERBOSE?=
SHOW := $(if $(VERBOSE),@true "",@echo "")
HIDE := $(if $(VERBOSE),,@)
DIRS= Libs ListsOp Mid Low High
INCLUDE= $(foreach a,$(DIRS),$(if $(wildcard $(a)), -Q $(a) $(a)))
COQFLAGS=$(foreach d, $(DIRS), $(if $(wildcard $(d)), -Q $(d) $(d))) $(EXTFLAGS)
LIBPREFIX=Tweetnacl
ifdef LIBPREFIX
COQFLAGS=$(foreach d, $(DIRS), $(if $(wildcard $(d)), -Q $(d) $(LIBPREFIX).$(d))) $(EXTFLAGS)
endif
DEPFLAGS:=$(COQFLAGS)
COQC=$(COQBIN)coqc
COQTOP=$(COQBIN)coqtop
COQDEP=$(COQBIN)coqdep $(DEPFLAGS)
COQDOC=$(COQBIN)coqdoc -d doc -g -utf8 $(DEPFLAGS)
COQVERSION= 8.7.0 or-else 8.7.1 or-else 8.7.2 or-else 8.8.0 or-else 8.8+alpha
COQV=$(shell $(COQC) -v)
ifeq ("$(filter $(COQVERSION),$(COQV))","")
$(error FAILURE: You need Coq $(COQVERSION) but you have this version: $(COQV))
endif
LIBS_FILES = $(wildcard Libs/*.v)
LISTSOP_FILES = $(wildcard ListsOp/*.v)
MID_FILES = $(wildcard Mid/*.v)
LOW_FILES = $(wildcard Low/*.v)
HIGH_FILES = $(wildcard High/*.v)
FIELD_FILES = $(wildcard Field/*.v)
COUNTFILES = $(LIBS_FILES) $(LISTSOP_FILES) $(MID_FILES) $(LOW_FILES) \
$(UNPACK_FILES)
FILES = $(COUNTFILES) $(HIGH_FILES)
ifneq ($(filter-out archclean clean cleanall printenv count,$(MAKECMDGOALS)),)
-include $(addsuffix .d,$(FILES))
else
ifeq ($(MAKECMDGOALS),)
-include $(addsuffix .d,$(FILES))
endif
endif
%_stripped.v: %.v
# e.g., 'make progs/verif_reverse_stripped.v will remove the tutorial comments
# from progs/verif_reverse.v
grep -v '^.[*][*][ )]' $*.v >$@
%.vo: %.v
@echo COQC $*.v
ifeq ($(TIMINGS), true)
# bash -c "wc $*.v >>timings; date +'%s.%N before' >> timings; $(COQC) $(COQFLAGS) $*.v; date +'%s.%N after' >>timings" 2>>timings
@bash -c "/bin/time --output=TIMINGS -a -f '%e real, %U user, %S sys, '\"$(shell wc $*.v)\" $(COQC) $(COQFLAGS) $*.v"
# echo -n $*.v " " >>TIMINGS; bash -c "/usr/bin/time -o TIMINGS -a $(COQC) $(COQFLAGS) $*.v"
else
@$(COQC) $(COQFLAGS) $*.v
endif
%.vio: %.v
@echo COQC $*.v
ifeq ($(TIMINGS), true)
# bash -c "wc $*.v >>timings; date +'%s.%N before' >> timings; $(COQC) $(COQFLAGS) $*.v; date +'%s.%N after' >>timings" 2>>timings
@bash -c "/bin/time --output=TIMINGS -a -f '%e real, %U user, %S sys, '\"$(shell wc $*.v)\" $(COQC) $(COQFLAGS) $*.v"
# echo -n $*.v " " >>TIMINGS; bash -c "/usr/bin/time -o TIMINGS -a $(COQC) $(COQFLAGS) $*.v"
else
@$(COQC) -quick $(COQFLAGS) $*.v
endif
all: .loadpath $(FILES:.v=.vo)
quick: .loadpath $(FILES:.v=.vio)
Libs: .loadpath $(LIBS_FILES:%.v=%.vo)
ListsOp: .loadpath $(LISTSOP_FILES:%.v=%.vo)
Mid: .loadpath $(MID_FILES:%.v=%.vo)
Low: .loadpath $(LOW_FILES:%.v=%.vo)
High: .loadpath $(HIGH_FILES:%.v=%.vo)
Field: .loadpath $(FIELD_FILES:%.v=%.vo)
_CoqProject: Makefile
$(SHOW)Generate _CoqProject
$(HIDE)echo $(COQFLAGS) >_CoqProject
.loadpath: _CoqProject
$(SHOW)Generate .loadpath
$(HIDE)echo $(COQFLAGS) > .loadpath
doc:
mkdir -p doc
$(COQDOC) $(FILES)
$(addsuffix .d,$(FILES)): %.v.d: %.v
$(SHOW)'COQDEP $<'
$(HIDE)$(COQDEP) $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
clean:
$(SHOW)cleaning files...
$(HIDE)rm -f $(wildcard */*.d) $(wildcard */*.vo) $(wildcard */*.glob) $(wildcard */.*.aux) .loadpath _CoqProject .depend .nia.cache .lia.cache
# check: quick
# coqtop -schedule-vio2vo
vio2vo: quick
$(COQC) $(COQFLAGS) -schedule-vio2vo $(J) $(FILES:%.v=%.vio)
checkproofs:
$(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio-checking $(J) $(FILES:%.v=%.vio)
count:
wc -l $(COUNTFILES)
printenv:
@"$(COQTOP)" -config
@echo 'CAMLC = $(CAMLC)'
@echo 'CAMLOPTC = $(CAMLOPTC)'
@echo 'PP = $(PP)'
@echo 'COQFLAGS = $(COQFLAGS)'
@echo 'COQLIBINSTALL = $(COQLIBINSTALL)'
@echo 'COQDOCINSTALL = $(COQDOCINSTALL)'
# The .depend file is divided into two parts, .depend and .depend-concur,
# in order to work around a limitation in Cygwin about how long one
# command line can be. (Or at least, it seems to be a solution to some
# such problem, not sure exactly. -- Andrew)
-include .depend
-include .depend-concur
#!/bin/sh
# remove _CoqProject if it alreqdy exists
[ -e _CoqProject ] && rm _CoqProject
# generate the path for coqide and voqv
for D in $(find * -maxdepth 1 -type d | egrep -v '^C|^slides|^readings'); do
echo "-Q $D Tweetnacl.$D" >> _CoqProject
done
echo "" >> _CoqProject
# generate the list of files for coq_makefile
ls */*.v | egrep -v '^C/' >> _CoqProject
coq_makefile INSTALLDEFAULTROOT = Tweetnacl -f _CoqProject -o Makefile
# coq_makefile -f _CoqProject -o Makefile
......@@ -5,7 +5,10 @@ maintainer: "benoit@cs.ru.nl"
homepage: "https://gitlab.science.ru.nl/benoit/tweetnacl/"
bug-reports: "none"
License: "MIT"
build: [make "-j%{jobs}%"]
build: [
["./configure.sh"]
[make "-j%{jobs}%"]
]
install: [
["mkdir" "-p" "%{lib}%/coq/user-contrib/Tweetnacl"]
["cp" "-r" "Libs" "%{lib}%/coq/user-contrib/Tweetnacl/"]
......
FILES := $(wildcard *.tex) $(wildcard tikz/*.tex) $(wildcard *.sty)
curve25519.pdf: $(FILES) collection.bib
latexmk -pdf curve25519.tex
curve25519.pdf: FORCE $(FILES) collection.bib
./latexrun.py curve25519.tex
depend:
@echo $(FILES)
.PHONY: clean
.PHONY: clean FORCE
clean:
@echo cleaning...
......
This diff is collapsed.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment