Mercurial > cpdt > repo

comparison src/Large.v @ 435:a54a4a2ea6e4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Changes while hacking on coqdoc
author Adam Chlipala <adam@chlipala.net>
date Thu, 26 Jul 2012 19:05:12 -0400
parents 5eebaaa9f952
children 8077352044b2
comparison
equal deleted inserted replaced
434:92f386c33e94 435:a54a4a2ea6e4
771 End Client. 771 End Client.
772 (* end hide *) 772 (* end hide *)
773 773
774 (** As in software development, large Coq projects are much more manageable when split across multiple files and when decomposed into libraries. Coq and Proof General provide very good support for these activities. 774 (** As in software development, large Coq projects are much more manageable when split across multiple files and when decomposed into libraries. Coq and Proof General provide very good support for these activities.
775 775
776 Consider a library that we will name [Lib], housed in directory <<LIB>> and split between files <<A.v>>, <<B.v>>, and <<C.v>>. A simple %\index{Makefile}%Makefile will compile the library, relying on the standard Coq tool %\index{coq\_makefile}\texttt{%#<tt>#coq_makefile#</tt>#%}% to do the hard work. 776 Consider a library that we will name [Lib], housed in directory <<LIB>> and split between files <<A.v>>, <<B.v>>, and <<C.v>>. A simple %\index{Makefile}%Makefile will compile the library, relying on the standard Coq tool %\index{coq\_makefile}%<<coq_makefile>> to do the hard work.
777 777
778 << 778 <<
779 MODULES := A B C 779 MODULES := A B C
780 VS := $(MODULES:%=%.v) 780 VS := $(MODULES:%=%.v)
781 781
790 clean:: Makefile.coq 790 clean:: Makefile.coq
791 $(MAKE) -f Makefile.coq clean 791 $(MAKE) -f Makefile.coq clean
792 rm -f Makefile.coq 792 rm -f Makefile.coq
793 >> 793 >>
794 794
795 The Makefile begins by defining a variable <<VS>> holding the list of filenames to be included in the project. The primary target is <<coq>>, which depends on the construction of an auxiliary Makefile called <<Makefile.coq>>. Another rule explains how to build that file. We call %\texttt{%#<tt>#coq_makefile#</tt>#%}%, using the <<-R>> 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 <<X.v>> is compiled into <<X.vo>>. 795 The Makefile begins by defining a variable <<VS>> holding the list of filenames to be included in the project. The primary target is <<coq>>, which depends on the construction of an auxiliary Makefile called <<Makefile.coq>>. Another rule explains how to build that file. We call <<coq_makefile>>, using the <<-R>> 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 <<X.v>> is compiled into <<X.vo>>.
796 796
797 Now code in <<B.v>> may refer to definitions in <<A.v>> after running 797 Now code in <<B.v>> may refer to definitions in <<A.v>> after running
798 [[ 798 [[
799 Require Import Lib.A. 799 Require Import Lib.A.
800 ]] 800 ]]
819 clean:: Makefile.coq 819 clean:: Makefile.coq
820 $(MAKE) -f Makefile.coq clean 820 $(MAKE) -f Makefile.coq clean
821 rm -f Makefile.coq 821 rm -f Makefile.coq
822 >> 822 >>
823 823
824 We change the %\texttt{%#<tt>#coq_makefile#</tt>#%}% call to indicate where the library [Lib] is found. Now <<D.v>> and <<E.v>> can refer to definitions from [Lib] module [A] after running 824 We change the <<coq_makefile>> call to indicate where the library [Lib] is found. Now <<D.v>> and <<E.v>> can refer to definitions from [Lib] module [A] after running
825 [[ 825 [[
826 Require Import Lib.A. 826 Require Import Lib.A.
827 ]] 827 ]]
828 %\vspace{-.15in}\noindent{}%and <<E.v>> can refer to definitions from <<D.v>> by running 828 %\vspace{-.15in}\noindent{}%and <<E.v>> can refer to definitions from <<D.v>> by running
829 [[ 829 [[