Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Rodolphe Lepigre
Iris
Commits
688d3287
Commit
688d3287
authored
Jul 06, 2014
by
Ralf Jung
Browse files
add makefile to coq-ho
parent
02a753f4
Changes
1
Hide whitespace changes
Inline
Side-by-side
Makefile
0 → 100644
View file @
688d3287
#############################################################################
## v # The Coq Proof Assistant ##
## <O___,, # INRIA - CNRS - LIX - LRI - PPS ##
## \VV/ # ##
## // # Makefile automagically generated by coq_makefile V8.4pl3 ##
#############################################################################
# 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 lib/recdom/ core_lang.v iris.v lang.v masks.v world_prop.v -R lib/recdom/ RecDom
#
.DEFAULT_GOAL
:=
all
#
# This Makefile may take arguments passed as environment variables:
# COQBIN to specify the directory where Coq binaries resides;
# 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)
##########################
# #
# Libraries definitions. #
# #
##########################
COQLIBS
?=
-I
.
-R
lib/recdom/ RecDom
COQDOCLIBS
?=
-R
lib/recdom/ RecDom
##########################
# #
# Variables definitions. #
# #
##########################
OPT
?=
COQDEP
?=
$(COQBIN)
coqdep
-c
COQFLAGS
?=
-q
$(OPT)
$(COQLIBS)
$(OTHERFLAGS)
$(COQ_XML)
COQCHKFLAGS
?=
-silent
-o
COQDOCFLAGS
?=
-interpolate
-utf8
COQC
?=
$(COQBIN)
coqc
GALLINA
?=
$(COQBIN)
gallina
COQDOC
?=
$(COQBIN)
coqdoc
COQCHK
?=
$(COQBIN)
coqchk
##################
# #
# 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
endif
######################
# #
# Files dispatching. #
# #
######################
VFILES
:=
core_lang.v
\
iris.v
\
lang.v
\
masks.v
\
world_prop.v
-include
$(addsuffix .d,$(VFILES))
.SECONDARY
:
$(addsuffix .d
,
$(VFILES))
VOFILES
:=
$(VFILES:.v=.vo)
VOFILESINC
=
$(
filter
$(
wildcard
./
*
)
,
$(VOFILES)
)
GLOBFILES
:=
$(VFILES:.v=.glob)
VIFILES
:=
$(VFILES:.v=.vi)
GFILES
:=
$(VFILES:.v=.g)
HTMLFILES
:=
$(VFILES:.v=.html)
GHTMLFILES
:=
$(VFILES:.v=.g.html)
ifeq
'$(HASNATDYNLINK)' 'true'
HASNATDYNLINK_OR_EMPTY
:=
yes
else
HASNATDYNLINK_OR_EMPTY
:=
endif
#######################################
# #
# Definition of the toplevel targets. #
# #
#######################################
all
:
./lib/recdom/ $(VOFILES)
spec
:
$(VIFILES)
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)
$(COQLIBS)
$(
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 opt byte archclean clean install userinstall depend html validate ./lib/recdom/
###################
# #
# Subdirectories. #
# #
###################
./lib/recdom/
:
cd
./lib/recdom/
;
$(MAKE)
all
####################
# #
# Special targets. #
# #
####################
byte
:
$(MAKE)
all
"OPT:=-byte"
opt
:
$(MAKE)
all
"OPT:=-opt"
userinstall
:
+
$(MAKE)
USERINSTALL
=
true install
install
:
install
-d
$(DSTROOT)$(COQLIBINSTALL)
/RecDom
;
\
for
i
in
$(VOFILESINC)
;
do
\
install
-m
0644
$$
i
$(DSTROOT)$(COQLIBINSTALL)
/RecDom/
`
basename
$$
i
`
;
\
done
(
cd
./lib/recdom/
;
$(MAKE)
DSTROOT
=
$(DSTROOT)
INSTALLDEFAULTROOT
=
$(INSTALLDEFAULTROOT)
/./lib/recdom/
install
)
install-doc
:
install
-d
$(DSTROOT)$(COQDOCINSTALL)
/RecDom/html
for
i
in
html/
*
;
do
\
install
-m
0644
$$
i
$(DSTROOT)$(COQDOCINSTALL)
/RecDom/
$$
i
;
\
done
clean
:
rm
-f
$(VOFILES)
$(VIFILES)
$(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
(
cd
./lib/recdom/
;
$(MAKE)
clean
)
archclean
:
rm
-f
*
.cmx
*
.o
(
cd
./lib/recdom/
;
$(MAKE)
archclean
)
printenv
:
@
$(COQBIN)
coqtop
-config
@
echo
CAMLC
=
$(CAMLC)
@
echo
CAMLOPTC
=
$(CAMLOPTC)
@
echo
PP
=
$(PP)
@
echo
COQFLAGS
=
$(COQFLAGS)
@
echo
COQLIBINSTALL
=
$(COQLIBINSTALL)
@
echo
COQDOCINSTALL
=
$(COQDOCINSTALL)
###################
# #
# Implicit rules. #
# #
###################
%.vo %.glob
:
%.v
$(COQC)
$(COQDEBUG)
$(COQFLAGS)
$*
%.vi
:
%.v
$(COQC)
-i
$(COQDEBUG)
$(COQFLAGS)
$*
%.g
:
%.v
$(GALLINA)
$<
%.tex
:
%.v
$(COQDOC)
$(COQDOCFLAGS)
-latex
$<
-o
$@
%.html
:
%.v %.glob
$(COQDOC)
$(COQDOCFLAGS)
-html
$<
-o
$@
%.g.tex
:
%.v
$(COQDOC)
$(COQDOCFLAGS)
-latex
-g
$<
-o
$@
%.g.html
:
%.v %.glob
$(COQDOC)$(COQDOCFLAGS)
-html
-g
$<
-o
$@
%.v.d
:
%.v
$(COQDEP)
-slash
$(COQLIBS)
"
$<
"
>
"
$@
"
||
(
RV
=
$$
?
;
rm
-f
"
$@
"
;
exit
$
${RV}
)
%.v.beautified
:
$(COQC)
$(COQDEBUG)
$(COQFLAGS)
-beautify
$*
# WARNING
#
# This Makefile has been automagically generated
# Edit at your own risks !
#
# END OF WARNING
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment