src/FOLP/IsaMakefile
author wenzelm
Sun Mar 01 23:36:12 2009 +0100 (2009-03-01)
changeset 30190 479806475f3c
parent 28500 4b79e5d3d0aa
child 36862 952b2b102a0a
permissions -rw-r--r--
use long names for old-style fold combinators;
wenzelm@2490
     1
#
wenzelm@2490
     2
# $Id$
wenzelm@2490
     3
#
wenzelm@2490
     4
# IsaMakefile for FOLP
wenzelm@2490
     5
#
wenzelm@2490
     6
wenzelm@4518
     7
## targets
wenzelm@4518
     8
wenzelm@4518
     9
default: FOLP
wenzelm@4518
    10
images: FOLP
wenzelm@4518
    11
test: FOLP-ex
wenzelm@4518
    12
all: images test
wenzelm@4518
    13
wenzelm@4518
    14
wenzelm@4518
    15
## global settings
wenzelm@4518
    16
wenzelm@4518
    17
SRC = $(ISABELLE_HOME)/src
wenzelm@3118
    18
OUT = $(ISABELLE_OUTPUT)
wenzelm@4447
    19
LOG = $(OUT)/log
wenzelm@2490
    20
wenzelm@4518
    21
wenzelm@4518
    22
## FOLP
wenzelm@4518
    23
wenzelm@4518
    24
FOLP: Pure $(OUT)/FOLP
wenzelm@2490
    25
wenzelm@4518
    26
Pure:
wenzelm@28500
    27
	@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
wenzelm@2490
    28
wenzelm@26408
    29
$(OUT)/FOLP: $(OUT)/Pure FOLP.thy IFOLP.thy ROOT.ML classical.ML	\
wenzelm@26408
    30
  hypsubst.ML intprover.ML simp.ML simpdata.ML
wenzelm@28500
    31
	@$(ISABELLE_TOOL) usedir -b $(OUT)/Pure FOLP
wenzelm@2490
    32
wenzelm@4518
    33
wenzelm@4518
    34
## FOLP-ex
wenzelm@2490
    35
wenzelm@4518
    36
FOLP-ex: FOLP $(LOG)/FOLP-ex.gz
wenzelm@4518
    37
wenzelm@26408
    38
$(LOG)/FOLP-ex.gz: $(OUT)/FOLP ex/ROOT.ML ex/Foundation.thy ex/If.thy	\
wenzelm@26408
    39
  ex/Intro.thy ex/Nat.thy ex/Intuitionistic.thy ex/Classical.thy	\
wenzelm@26408
    40
  ex/Prolog.ML ex/Prolog.thy ex/Propositional_Int.thy			\
wenzelm@26408
    41
  ex/Propositional_Cla.thy ex/Quantifiers_Int.thy			\
wenzelm@26408
    42
  ex/Quantifiers_Cla.thy
wenzelm@28500
    43
	@$(ISABELLE_TOOL) usedir $(OUT)/FOLP ex
wenzelm@2490
    44
wenzelm@4518
    45
wenzelm@4518
    46
## clean
wenzelm@4447
    47
wenzelm@4447
    48
clean:
wenzelm@4518
    49
	@rm -f $(OUT)/FOLP $(LOG)/FOLP.gz $(LOG)/FOLP-ex.gz