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
Tej Chajed
iris
Commits
d543c264
Commit
d543c264
authored
Jan 21, 2016
by
Ralf Jung
Browse files
remove the generated Makefile, add a configure script generating it instead
parent
594afc25
Changes
2
Hide whitespace changes
Inline
Side-by-side
Makefile
deleted
100644 → 0
View file @
594afc25
#############################################################################
## v # The Coq Proof Assistant ##
## <O___,, # INRIA - CNRS - LIX - LRI - PPS ##
## \VV/ # ##
## // # Makefile automagically generated by coq_makefile V8.5rc1 ##
#############################################################################
# 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 -o Makefile
#
.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
"."
""
COQDOCLIBS
?=
-Q
"."
""
##########################
# #
# 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
:=
barrier/heap_lang.v
\
iris/parameter.v
\
iris/hoare.v
\
iris/resources.v
\
iris/pviewshifts.v
\
iris/language.v
\
iris/weakestpre.v
\
iris/ownership.v
\
iris/wsat.v
\
iris/viewshifts.v
\
iris/namespace.v
\
iris/lifting.v
\
iris/hoare_lifting.v
\
iris/adequacy.v
\
iris/model.v
\
modures/excl.v
\
modures/ra.v
\
modures/agree.v
\
modures/cofe_solver.v
\
modures/dra.v
\
modures/base.v
\
modures/cofe.v
\
modures/logic.v
\
modures/fin_maps.v
\
modures/auth.v
\
modures/sts.v
\
modures/cmra.v
\
modures/option.v
\
prelude/error.v
\
prelude/list.v
\
prelude/decidable.v
\
prelude/sets.v
\
prelude/lexico.v
\
prelude/co_pset.v
\
prelude/zmap.v
\
prelude/nmap.v
\
prelude/numbers.v
\
prelude/finite.v
\
prelude/listset_nodup.v
\
prelude/prelude.v
\
prelude/tactics.v
\
prelude/base.v
\
prelude/gmap.v
\
prelude/streams.v
\
prelude/listset.v
\
prelude/collections.v
\
prelude/relations.v
\
prelude/strings.v
\
prelude/natmap.v
\
prelude/orders.v
\
prelude/countable.v
\
prelude/pretty.v
\
prelude/hashset.v
\
prelude/proof_irrel.v
\
prelude/mapset.v
\
prelude/fin_collections.v
\
prelude/stringmap.v
\
prelude/pmap.v
\
prelude/vector.v
\
prelude/fin_maps.v
\
prelude/bsets.v
\
prelude/fin_map_dom.v
\
prelude/option.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)
$(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 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)
//
$$
i
`
"
;
\
install
-m
0644
$$
i
"
$(DSTROOT)
"
$(COQLIBINSTALL)
//
$$
i
;
\
done
install-doc
:
install
-d
"
$(DSTROOT)
"
$(COQDOCINSTALL)
/
$(INSTALLDEFAULTROOT)
/html
for
i
in
html/
*
;
do
\
install
-m
0644
$$
i
"
$(DSTROOT)
"
$(COQDOCINSTALL)
/
$(INSTALLDEFAULTROOT)
/
$$
i
;
\
done
uninstall_me.sh
:
Makefile
echo
'#!/bin/sh'
>
$@
printf
'cd "$
${DSTROOT}
"
$(COQLIBINSTALL)
/ && rm -f
$(VOFILES)
$(VFILES)
$(GLOBFILES)
$(NATIVEFILES)
$(CMOFILES)
$(CMIFILES)
$(CMAFILES)
&& find . -type d -and -empty -delete\ncd "$
${DSTROOT}
"
$(COQLIBINSTALL)
&& find "" -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n'
>>
"
$@
"
printf
'cd "$
${DSTROOT}
"
$(COQDOCINSTALL)
/
$(INSTALLDEFAULTROOT)
\\\n'
>>
"
$@
"
printf
'&& rm -f
$(
shell
find "html" -maxdepth 1 -and -type f -print
)
\n'
>>
"
$@
"
printf
'cd "$
${DSTROOT}
"
$(COQDOCINSTALL)
&& find
$(INSTALLDEFAULTROOT)
/html -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n'
>>
"
$@
"
chmod
+x
$@
uninstall
:
uninstall_me.sh
sh
$<
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
$*
# WARNING
#
# This Makefile has been automagically generated
# Edit at your own risks !
#
# END OF WARNING
configure
0 → 100755
View file @
d543c264
#!/bin/sh
coq_makefile
-f
_CoqProject
-o
Makefile
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