|
13739
|
1 |
#
|
|
|
2 |
# $Id$
|
|
|
3 |
#
|
|
|
4 |
# IsaMakefile for PSV2002
|
|
|
5 |
#
|
|
|
6 |
|
|
|
7 |
SESSIONS = a1 a2 a3 a5 a6
|
|
|
8 |
|
|
|
9 |
## targets
|
|
|
10 |
|
|
|
11 |
default: clean sessions
|
|
|
12 |
sessions: $(SESSIONS)
|
|
|
13 |
# all: sessions
|
|
|
14 |
|
|
|
15 |
|
|
|
16 |
## global settings
|
|
|
17 |
|
|
|
18 |
|
|
|
19 |
SRC = $(ISABELLE_HOME)/src
|
|
|
20 |
OUT = $(ISABELLE_OUTPUT)
|
|
|
21 |
LOG = $(OUT)/log
|
|
|
22 |
INFO = $(ISABELLE_BROWSER_INFO)
|
|
|
23 |
USEDIR = $(ISATOOL) usedir -v true -i false -d false -D generated
|
|
|
24 |
RSYNC = rsync --rsh ssh --rsync-path /usr/local/dist/bin/rsync
|
|
|
25 |
WWW = www4.in.tum.de:/home/html/wbroy/html-data/lehre/praktika/psv
|
|
|
26 |
|
|
|
27 |
|
|
|
28 |
# reomve old log files
|
|
|
29 |
clean:
|
|
|
30 |
rm -f $(LOG)/HOL-a?.gz $(LOG)/HOL-l?.gz
|
|
|
31 |
|
|
|
32 |
## provide style.tex
|
|
|
33 |
|
|
|
34 |
style:
|
|
|
35 |
@for D in $(SESSIONS); do test -d $$D/document && { test -r $$D/document/style.tex || ln -s ../../style.tex $$D/document/style.tex; } done;
|
|
|
36 |
|
|
|
37 |
|
|
|
38 |
## a1
|
|
|
39 |
|
|
|
40 |
a1: a1/generated/session.tex
|
|
|
41 |
|
|
|
42 |
a1/generated/session.tex: a1/ROOT.ML \
|
|
|
43 |
a1/*.thy
|
|
|
44 |
@$(USEDIR) HOL a1
|
|
|
45 |
|
|
|
46 |
## a2
|
|
|
47 |
|
|
|
48 |
a2: a2/generated/session.tex
|
|
|
49 |
|
|
|
50 |
a2/generated/session.tex: a2/ROOT.ML \
|
|
|
51 |
a2/*.thy
|
|
|
52 |
@$(USEDIR) HOL a2
|
|
|
53 |
|
|
|
54 |
## a3
|
|
|
55 |
|
|
|
56 |
a3: a3/generated/session.tex
|
|
|
57 |
|
|
|
58 |
a3/generated/session.tex: a3/ROOT.ML \
|
|
|
59 |
a3/*.thy
|
|
|
60 |
@$(USEDIR) HOL a3
|
|
|
61 |
|
|
|
62 |
## a5
|
|
|
63 |
|
|
|
64 |
a5: a5/generated/session.tex
|
|
|
65 |
|
|
|
66 |
a5/generated/session.tex: a5/ROOT.ML \
|
|
|
67 |
a5/*.thy
|
|
|
68 |
@$(USEDIR) HOL a5
|
|
|
69 |
|
|
|
70 |
## a6
|
|
|
71 |
|
|
|
72 |
a6: a6/generated/session.tex
|
|
|
73 |
|
|
|
74 |
a6/generated/session.tex: a6/ROOT.ML \
|
|
|
75 |
a6/*.thy
|
|
|
76 |
@$(USEDIR) HOL a6
|