Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Dan Frumin
ReLoC-v1
Commits
918a5591
Commit
918a5591
authored
May 06, 2017
by
Dan Frumin
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Remove the Makefile from Git
parent
4dd1bc31
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
with
1 addition
and
354 deletions
+1
-354
.gitignore
.gitignore
+1
-0
Makefile
Makefile
+0
-354
No files found.
.gitignore
View file @
918a5591
...
...
@@ -8,4 +8,5 @@
*~
*.bak
.coq-native/
Makefile
Makefile.coq
\ No newline at end of file
Makefile
deleted
100644 → 0
View file @
4dd1bc31
#############################################################################
## v # The Coq Proof Assistant ##
## <O___,, # INRIA - CNRS - LIX - LRI - PPS ##
## \VV/ # ##
## // # Makefile automagically generated by coq_makefile V8.6 ##
#############################################################################
# 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.
# VERBOSE to disable the short display of compilation rules.
VERBOSE
?=
SHOW
:=
$(
if
$(VERBOSE)
,@true
""
,@echo
""
)
HIDE
:=
$(
if
$(VERBOSE)
,,@
)
# 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
"."
iris_logrel
\
-Q
"../autosubst/theories"
Autosubst
COQCHKLIBS
?=
\
-R
"."
iris_logrel
\
-R
"../autosubst/theories"
Autosubst
COQDOCLIBS
?=
\
-R
"."
iris_logrel
\
-R
"../autosubst/theories"
Autosubst
##########################
# #
# Variables definitions. #
# #
##########################
OPT
?=
OTHERFLAGS
=
-w
-notation-overridden
,-redundant-canonical-projection,-several-object-files
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
:=
prelude/base.v
\
stlc/lang.v
\
stlc/typing.v
\
stlc/rules.v
\
stlc/logrel.v
\
stlc/fundamental.v
\
stlc/soundness.v
\
F_mu/lang.v
\
F_mu/typing.v
\
F_mu/rules.v
\
F_mu/logrel.v
\
F_mu/fundamental.v
\
F_mu/soundness.v
\
F_mu_ref/lang.v
\
F_mu_ref/typing.v
\
F_mu_ref/rules.v
\
F_mu_ref/rules_binary.v
\
F_mu_ref/logrel.v
\
F_mu_ref/logrel_binary.v
\
F_mu_ref/fundamental.v
\
F_mu_ref/fundamental_binary.v
\
F_mu_ref/soundness.v
\
F_mu_ref/context_refinement.v
\
F_mu_ref/soundness_binary.v
\
F_mu_ref_conc/lang.v
\
F_mu_ref_conc/rules.v
\
F_mu_ref_conc/typing.v
\
F_mu_ref_conc/logrel_unary.v
\
F_mu_ref_conc/fundamental_unary.v
\
F_mu_ref_conc/relational_properties.v
\
F_mu_ref_conc/rules_binary.v
\
F_mu_ref_conc/logrel_binary.v
\
F_mu_ref_conc/weakestpre.v
\
F_mu_ref_conc/fundamental_binary.v
\
F_mu_ref_conc/soundness_unary.v
\
F_mu_ref_conc/context_refinement.v
\
F_mu_ref_conc/soundness_binary.v
\
F_mu_ref_conc/tactics.v
\
F_mu_ref_conc/notation.v
\
F_mu_ref_conc/examples/lock.v
\
F_mu_ref_conc/examples/counter.v
\
F_mu_ref_conc/examples/stack/stack_rules.v
\
F_mu_ref_conc/examples/stack/CG_stack.v
\
F_mu_ref_conc/examples/stack/FG_stack.v
\
F_mu_ref_conc/examples/stack/refinement.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)
/iris_logrel/
$$
i
`
"
;
\
install
-m
0644
$$
i
"
$(DSTROOT)
"
$(COQLIBINSTALL)
/iris_logrel/
$$
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)
/iris_logrel && rm -f
$(VOFILES)
$(VFILES)
$(GLOBFILES)
$(NATIVEFILES)
$(CMOFILES)
$(CMIFILES)
$(CMAFILES)
&& find . -type d -and -empty -delete\ncd "$
${DSTROOT}
"
$(COQLIBINSTALL)
&& find "iris_logrel" -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
$<
.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)
ltacprof"
>>
.merlin
@
echo
"B
$(COQLIB)
toplevel"
>>
.merlin
@
echo
"B
$(COQLIB)
stm"
>>
.merlin
@
echo
"B
$(COQLIB)
grammar"
>>
.merlin
@
echo
"B
$(COQLIB)
config"
>>
.merlin
@
echo
"B
$(COQLIB)
ltac"
>>
.merlin
@
echo
"B
$(COQLIB)
engine"
>>
.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
'OCAMLFIND =
$(OCAMLFIND)
'
@
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
$(SHOW)
COQC
$<
$(HIDE)$(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
$(SHOW)
'COQDEP $<'
$(HIDE)$(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
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a 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