Mercurial > cpdt > repo

comparison src/Large.v @ 369:4550dedad73a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Change make invocations to work properly with -j
author Adam Chlipala <adam@chlipala.net>
date Fri, 16 Dec 2011 13:28:11 -0500
parents e0c5b91e2968
children d1276004eec9
comparison
equal deleted inserted replaced
368:e0c5b91e2968 369:4550dedad73a
754 VS := $(MODULES:%=%.v) 754 VS := $(MODULES:%=%.v)
755 755
756 .PHONY: coq clean 756 .PHONY: coq clean
757 757
758 coq: Makefile.coq 758 coq: Makefile.coq
759 make -f Makefile.coq 759 $(MAKE) -f Makefile.coq
760 760
761 Makefile.coq: Makefile $(VS) 761 Makefile.coq: Makefile $(VS)
762 coq_makefile -R . Lib $(VS) -o Makefile.coq 762 coq_makefile -R . Lib $(VS) -o Makefile.coq
763 763
764 clean:: Makefile.coq 764 clean:: Makefile.coq
765 make -f Makefile.coq clean 765 $(MAKE) -f Makefile.coq clean
766 rm -f Makefile.coq 766 rm -f Makefile.coq
767 >> 767 >>
768 768
769 The Makefile begins by defining a variable %\texttt{%#<tt>#VS#</tt>#%}% holding the list of filenames to be included in the project. The primary target is %\texttt{%#<tt>#coq#</tt>#%}%, which depends on the construction of an auxiliary Makefile called %\texttt{%#<tt>#Makefile.coq#</tt>#%}%. Another rule explains how to build that file. We call %\texttt{%#<tt>#coq_makefile#</tt>#%}%, using the %\texttt{%#<tt>#-R#</tt>#%}% flag to specify that files in the current directory should be considered to belong to the library [Lib]. This Makefile will build a compiled version of each module, such that %\texttt{%#<tt>#X.v#</tt>#%}% is compiled into %\texttt{%#<tt>#X.vo#</tt>#%}%. 769 The Makefile begins by defining a variable %\texttt{%#<tt>#VS#</tt>#%}% holding the list of filenames to be included in the project. The primary target is %\texttt{%#<tt>#coq#</tt>#%}%, which depends on the construction of an auxiliary Makefile called %\texttt{%#<tt>#Makefile.coq#</tt>#%}%. Another rule explains how to build that file. We call %\texttt{%#<tt>#coq_makefile#</tt>#%}%, using the %\texttt{%#<tt>#-R#</tt>#%}% flag to specify that files in the current directory should be considered to belong to the library [Lib]. This Makefile will build a compiled version of each module, such that %\texttt{%#<tt>#X.v#</tt>#%}% is compiled into %\texttt{%#<tt>#X.vo#</tt>#%}%.
770 770
783 VS := $(MODULES:%=%.v) 783 VS := $(MODULES:%=%.v)
784 784
785 .PHONY: coq clean 785 .PHONY: coq clean
786 786
787 coq: Makefile.coq 787 coq: Makefile.coq
788 make -f Makefile.coq 788 $(MAKE) -f Makefile.coq
789 789
790 Makefile.coq: Makefile $(VS) 790 Makefile.coq: Makefile $(VS)
791 coq_makefile -R LIB Lib -R . Client $(VS) -o Makefile.coq 791 coq_makefile -R LIB Lib -R . Client $(VS) -o Makefile.coq
792 792
793 clean:: Makefile.coq 793 clean:: Makefile.coq
794 make -f Makefile.coq clean 794 $(MAKE) -f Makefile.coq clean
795 rm -f Makefile.coq 795 rm -f Makefile.coq
796 >> 796 >>
797 797
798 We change the %\texttt{%#<tt>#coq_makefile#</tt>#%}% call to indicate where the library [Lib] is found. Now %\texttt{%#<tt>#D.v#</tt>#%}% and %\texttt{%#<tt>#E.v#</tt>#%}% can refer to definitions from [Lib] module [A] after running 798 We change the %\texttt{%#<tt>#coq_makefile#</tt>#%}% call to indicate where the library [Lib] is found. Now %\texttt{%#<tt>#D.v#</tt>#%}% and %\texttt{%#<tt>#E.v#</tt>#%}% can refer to definitions from [Lib] module [A] after running
799 [[ 799 [[