Mercurial > cpdt > repo
comparison src/Large.v @ 243:b2c72c77ad47
Build Processes
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Wed, 09 Dec 2009 13:59:01 -0500 |
| parents | 5a32784e30f3 |
| children | 4662b6f099b0 |
comparison
equal
deleted
inserted
replaced
| 242:5a32784e30f3 | 243:b2c72c77ad47 |
|---|---|
| 727 Theorem unique_ident : forall e', (forall a, e' + a = a) -> e' = 0. | 727 Theorem unique_ident : forall e', (forall a, e' + a = a) -> e' = 0. |
| 728 exact IntTheorems.unique_ident. | 728 exact IntTheorems.unique_ident. |
| 729 Qed. | 729 Qed. |
| 730 | 730 |
| 731 (** As in ML, the module system provides an effective way to structure large developments. Unlike in ML, Coq modules add no expressiveness; we can implement any module as an inhabitant of a dependent record type. It is the second-class nature of modules that makes them easier to use than dependent records in many case. Because modules may only be used in quite restricted ways, it is easier to support convenient module coding through special commands and editing modes, as the above example demonstrates. An isomorphic implementation with records would have suffered from lack of such conveniences as module subtyping and importation of the fields of a module. *) | 731 (** As in ML, the module system provides an effective way to structure large developments. Unlike in ML, Coq modules add no expressiveness; we can implement any module as an inhabitant of a dependent record type. It is the second-class nature of modules that makes them easier to use than dependent records in many case. Because modules may only be used in quite restricted ways, it is easier to support convenient module coding through special commands and editing modes, as the above example demonstrates. An isomorphic implementation with records would have suffered from lack of such conveniences as module subtyping and importation of the fields of a module. *) |
| 732 | |
| 733 | |
| 734 (** * Build Processes *) | |
| 735 | |
| 736 (** 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. | |
| 737 | |
| 738 Consider a library that we will name [Lib], housed in directory %\texttt{%#<tt>#LIB#</tt>#%}% and split between files %\texttt{%#<tt>#A.v#</tt>#%}%, %\texttt{%#<tt>#B.v#</tt>#%}%, and %\texttt{%#<tt>#C.v#</tt>#%}%. A simple Makefile will compile the library, relying on the standard Coq tool %\texttt{%#<tt>#coq_makefile#</tt>#%}% to do the hard work. | |
| 739 | |
| 740 << | |
| 741 MODULES := A B C | |
| 742 VS := $(MODULES:%=%.v) | |
| 743 | |
| 744 .PHONY: coq clean | |
| 745 | |
| 746 coq: Makefile.coq | |
| 747 make -f Makefile.coq | |
| 748 | |
| 749 Makefile.coq: Makefile $(VS) | |
| 750 coq_makefile -R . Lib $(VS) -o Makefile.coq | |
| 751 | |
| 752 clean:: Makefile.coq | |
| 753 make -f Makefile.coq clean | |
| 754 rm -f Makefile.coq | |
| 755 >> | |
| 756 | |
| 757 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>#%}%. | |
| 758 | |
| 759 Now code in %\texttt{%#<tt>#B.v#</tt>#%}% may refer to definitions in %\texttt{%#<tt>#A.v#</tt>#%}% after running | |
| 760 | |
| 761 [[ | |
| 762 Require Import Lib.A. | |
| 763 | |
| 764 ]] | |
| 765 | |
| 766 Library [Lib] is presented as a module, containing a submodule [A], which contains the definitions from %\texttt{%#<tt>#A.v#</tt>#%}%. These are genuine modules in the sense of Coq's module system, and they may be passed to functors and so on. | |
| 767 | |
| 768 [Require Import] is a convenient combination of two more primitive commands. [Require] finds the %\texttt{%#<tt>#.vo#</tt>#%}% file containing the named module, ensuring that the module is loaded into memory. [Import] loads all top-level definitions of the named module into the current namespace, and it may be used with local modules that do not have corresponding %\texttt{%#<tt>#.vo#</tt>#%}% files. Another command, [Load], is for inserting the contents of a named file verbatim. It is generally better to use the module-based commands, since they avoid rerunning proof scripts, and they facilitate reorganization of directory structure without the need to change code. | |
| 769 | |
| 770 Now we would like to use our library from a different development, called [Client] and found in directory %\texttt{%#<tt>#CLIENT#</tt>#%}%, which has its own Makefile. | |
| 771 | |
| 772 << | |
| 773 MODULES := D E | |
| 774 VS := $(MODULES:%=%.v) | |
| 775 | |
| 776 .PHONY: coq clean | |
| 777 | |
| 778 coq: Makefile.coq | |
| 779 make -f Makefile.coq | |
| 780 | |
| 781 Makefile.coq: Makefile $(VS) | |
| 782 coq_makefile -R LIB Lib -R . Client $(VS) -o Makefile.coq | |
| 783 | |
| 784 clean:: Makefile.coq | |
| 785 make -f Makefile.coq clean | |
| 786 rm -f Makefile.coq | |
| 787 >> | |
| 788 | |
| 789 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 | |
| 790 | |
| 791 [[ | |
| 792 Require Import Lib.A. | |
| 793 | |
| 794 ]] | |
| 795 | |
| 796 and %\texttt{%#<tt>#E.v#</tt>#%}% can refer to definitions from %\texttt{%#<tt>#D.v#</tt>#%}% by running | |
| 797 | |
| 798 [[ | |
| 799 Require Import Client.D. | |
| 800 | |
| 801 ]] | |
| 802 | |
| 803 It can be useful to split a library into several files, but it is also inconvenient for client code to import library modules individually. We can get the best of both worlds by, for example, adding an extra source file %\texttt{%#<tt>#Lib.v#</tt>#%}% to [Lib]'s directory and Makefile. | |
| 804 | |
| 805 [[ | |
| 806 Require Export Lib.A Lib.B Lib.C. | |
| 807 | |
| 808 ]] | |
| 809 | |
| 810 Now client code can import all definitions from all of [Lib]'s modules simply by running | |
| 811 | |
| 812 [[ | |
| 813 Require Import Lib. | |
| 814 | |
| 815 ]] | |
| 816 | |
| 817 The two Makefiles above share a lot of code, so, in practice, it is useful to define a common Makefile that is included by multiple library-specific Makefiles. | |
| 818 | |
| 819 %\medskip% | |
| 820 | |
| 821 The remaining ingredient is the proper way of editing library code files in Proof General. Recall this snippet of %\texttt{%#<tt>#.emacs#</tt>#%}% code from Chapter 2, which tells Proof General where to find the library associated with this book. | |
| 822 | |
| 823 << | |
| 824 (custom-set-variables | |
| 825 ... | |
| 826 '(coq-prog-args '("-I" "/path/to/cpdt/src")) | |
| 827 ... | |
| 828 ) | |
| 829 >> | |
| 830 | |
| 831 To do interactive editing of our current example, we just need to change the flags to point to the right places. | |
| 832 | |
| 833 << | |
| 834 (custom-set-variables | |
| 835 ... | |
| 836 ; '(coq-prog-args '("-I" "/path/to/cpdt/src")) | |
| 837 '(coq-prog-args '("-R" "LIB" "Lib" "-R" "CLIENT" "Client")) | |
| 838 ... | |
| 839 ) | |
| 840 >> | |
| 841 | |
| 842 When working on multiple projects, it is useful to leave multiple versions of this setting in your %\texttt{%#<tt>#.emacs#</tt>#%}% file, commenting out all but one of them at any moment in time. To switch between projects, change the commenting structure and restart Emacs. *) |