Commit f97d446b authored by kleing's avatar kleing
Browse files

removed old IsaMakefiles and ROOT.ML files

parent 76d382703874
## configurables
SESSION-NAME = AVL-Trees
BASE-IMAGE = HOL
## targets
default: $(SESSION-NAME)
test: $(SESSION-NAME)
# usually empty:
images:
all: images test
## global settings
SRC = $(ISABELLE_HOME)/src
OUT = $(ISABELLE_OUTPUT)
LOG = $(OUT)/log
# turn image into absolute path according to ISABELLE_IMAGE_PATH or OUT
ifeq ($(ISABELLE_IMAGE_PATH),)
IMAGE=$(OUT)/$(BASE-IMAGE)
else
IMAGE=$(ISABELLE_IMAGE_PATH)$(BASE-IMAGE)
endif
USEDIR = $(ISABELLE_TOOL) usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/" # -D generated
# time limit (in sec)
MAXTIME = 3600
## dependencies
$(SESSION-NAME): $(LOG)/$(BASE-IMAGE)-$(SESSION-NAME).gz
$(LOG)/$(BASE-IMAGE)-$(SESSION-NAME).gz: $(IMAGE) ROOT.ML *.thy document/*.tex
cd ..; ulimit -t $(MAXTIME); $(USEDIR) $(IMAGE) $(SESSION-NAME)
## clean
clean:
@rm -f $(LOG)/$(BASE-IMAGE)-$(SESSION-NAME).gz
use_thys ["AVL", "AVL2"];
## configurables
SESSION-NAME = Abortable_Linearizable_Modules
BASE-IMAGE = HOLCF
## targets
default: $(SESSION-NAME)
test: $(SESSION-NAME)
# usually empty:
images:
all: images test
## global settings
SRC = $(ISABELLE_HOME)/src
OUT = $(ISABELLE_OUTPUT)
LOG = $(OUT)/log
# not a release image, so only $(OUT)
IMAGE=$(OUT)/$(BASE-IMAGE)
USEDIR = $(ISABELLE_TOOL) usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/" # -D generated
# time limit (in sec)
MAXTIME = 600
## dependencies
$(SESSION-NAME): $(BASE-IMAGE) $(LOG)/$(BASE-IMAGE)-$(SESSION-NAME).gz
$(BASE-IMAGE):
cd $(ISABELLE_HOME)/src/HOL && $(ISABELLE_TOOL) make $(BASE-IMAGE)
$(LOG)/$(BASE-IMAGE)-$(SESSION-NAME).gz: $(IMAGE) ROOT.ML *.thy document/*.tex document/*.bib
cd ..; ulimit -t $(MAXTIME); $(USEDIR) $(IMAGE) $(SESSION-NAME)
## clean
clean:
@rm -f $(LOG)/$(BASE-IMAGE)-$(SESSION-NAME).gz
no_document use_thys
["~~/src/HOL/Library/Sublist", "~~/src/HOL/HOLCF/IOA/meta_theory/IOA"];
use_thys ["CompositionCorrectness"];
## configurables
SESSION-NAME = Abstract-Hoare-Logics
BASE-IMAGE = HOL
## targets
default: $(SESSION-NAME)
test: $(SESSION-NAME)
# usually empty:
images:
all: images test
## global settings
SRC = $(ISABELLE_HOME)/src
OUT = $(ISABELLE_OUTPUT)
LOG = $(OUT)/log
# turn image into absolute path according to ISABELLE_IMAGE_PATH or OUT
ifeq ($(ISABELLE_IMAGE_PATH),)
IMAGE=$(OUT)/$(BASE-IMAGE)
else
IMAGE=$(ISABELLE_IMAGE_PATH)$(BASE-IMAGE)
endif
USEDIR = $(ISABELLE_TOOL) usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/" # -D generated
# time limit (in sec)
MAXTIME = 3600
## dependencies
$(SESSION-NAME): $(LOG)/$(BASE-IMAGE)-$(SESSION-NAME).gz
$(LOG)/$(BASE-IMAGE)-$(SESSION-NAME).gz: $(IMAGE) ROOT.ML While/*.thy Proc/*.thy Procs/*.thy document/*.tex document/*.bib
cd ..; ulimit -t $(MAXTIME); $(USEDIR) $(IMAGE) $(SESSION-NAME)
## clean
clean:
@rm -f $(LOG)/$(BASE-IMAGE)-$(SESSION-NAME).gz
use_thys ["While/HoareTotal", "Proc/PHoareTotal", "Procs/PsHoareTotal"];
## configurables
SESSION-NAME = Abstract-Rewriting
BASE-IMAGE = HOL
## targets
default: $(SESSION-NAME)
test: $(SESSION-NAME)
# usually empty:
images:
all: images test
## global settings
SRC = $(ISABELLE_HOME)/src
OUT = $(ISABELLE_OUTPUT)
LOG = $(OUT)/log
# turn image into absolute path according to ISABELLE_IMAGE_PATH or OUT
ifeq ($(ISABELLE_IMAGE_PATH),)
IMAGE=$(OUT)/$(BASE-IMAGE)
else
IMAGE=$(ISABELLE_IMAGE_PATH)$(BASE-IMAGE)
endif
USEDIR = $(ISABELLE_TOOL) usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/" # -D generated
# time limit (in sec)
MAXTIME = 200
## dependencies
$(SESSION-NAME): $(LOG)/$(BASE-IMAGE)-$(SESSION-NAME).gz
$(LOG)/$(BASE-IMAGE)-$(SESSION-NAME).gz: $(IMAGE) ROOT.ML *.thy document/*.tex document/*.bib
cd ..; ulimit -t $(MAXTIME); $(USEDIR) $(IMAGE) $(SESSION-NAME)
## clean
clean:
@rm -f $(LOG)/$(BASE-IMAGE)-$(SESSION-NAME).gz
no_document use_thys [
"../Transitive-Closure/Transitive_Closure_Impl",
"../Regular-Sets/Regexp_Method"
];
use_thys [
"Seq",
"Abstract_Rewriting",
"Relative_Rewriting",
"SN_Orders",
"SN_Order_Carrier"];
## configurables
SESSION-NAME = ArrowImpossibilityGS
BASE-IMAGE = HOL
## targets
default: $(SESSION-NAME)
test: images
images: $(SESSION-NAME)
all: test
## global settings
SRC = $(ISABELLE_HOME)/src
OUT = $(ISABELLE_OUTPUT)
LOG = $(OUT)/log
# turn image into absolute path according to ISABELLE_IMAGE_PATH or OUT
ifeq ($(ISABELLE_IMAGE_PATH),)
IMAGE=$(OUT)/$(BASE-IMAGE)
else
IMAGE=$(ISABELLE_IMAGE_PATH)$(BASE-IMAGE)
endif
USEDIR = $(ISABELLE_TOOL) usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"
# time limit (in sec)
MAXTIME = 600
## dependencies
$(SESSION-NAME): $(OUT)/$(SESSION-NAME)
$(OUT)/$(SESSION-NAME): $(IMAGE) ROOT.ML Thys/*.thy document/*.tex document/*.bib
ulimit -t $(MAXTIME); $(USEDIR) -b $(IMAGE) $(SESSION-NAME)
## clean
clean:
@rm -f $(LOG)/$(BASE-IMAGE)-$(SESSION-NAME).gz $(LOG)/$(BASE-IMAGE)-$(SESSION-NAME)-build.gz
no_document use_thys ["~~/src/HOL/Library/FuncSet", "~~/src/HOL/Library/Zorn"];
use_thys ["Thys/Arrow_Utility", "Thys/GS"];
## configurables
SESSION-NAME = AutoFocus-Stream
BASE-IMAGE = Nat-Interval-Logic
## targets
default: $(SESSION-NAME)
test: $(SESSION-NAME)-test
# usually empty:
images: $(SESSION-NAME)
all: $(SESSION-NAME)
## global settings
SRC = $(ISABELLE_HOME)/src
OUT = $(ISABELLE_OUTPUT)
LOG = $(OUT)/log
# base image is not an Isabelle release image, so always source from $(OUT)
IMAGE=$(OUT)/$(BASE-IMAGE)
DOCFLAGS = -v true -i true -V outline=/proof,/ML -g true -d pdf
USEDIR = $(ISABELLE_TOOL) usedir $(DOCFLAGS)
BUILD = $(ISABELLE_TOOL) usedir -b $(DOCFLAGS)
BUILD_PART = $(ISABELLE_TOOL) usedir -b -v true -i false -g false -d false
# time limit (in sec)
MAXTIME = 600
# Make sure that the base image is present
$(BASE-IMAGE):
cd ../$(BASE-IMAGE); $(ISABELLE_TOOL) make $(BASE-IMAGE)
# test run and proof document
$(SESSION-NAME)-test: $(BASE-IMAGE) $(LOG)/$(BASE-IMAGE)-$(SESSION-NAME).gz
$(LOG)/$(BASE-IMAGE)-$(SESSION-NAME).gz: $(IMAGE) ROOT.ML \
document/root.tex
cd ..; ulimit -t $(MAXTIME); $(USEDIR) $(IMAGE) $(SESSION-NAME)
# build image
$(SESSION-NAME): $(BASE-IMAGE) $(OUT)/$(SESSION-NAME)
$(OUT)/$(SESSION-NAME): $(IMAGE) ROOT.ML \
document/root.tex
ulimit -t $(MAXTIME); $(BUILD) $(IMAGE) $(SESSION-NAME)
## clean
clean:
@rm -f $(LOG)/$(BASE-IMAGE)-$(SESSION-NAME).gz
@rm -f $(OUT)/$(SESSION-NAME)
\ No newline at end of file
use_thys ["ListSlice", "AF_Stream", "AF_Stream_Exec", "IL_AF_Stream", "IL_AF_Stream_Exec"];
## configurables
SESSION-NAME = BDD
BASE-IMAGE = Simpl
## targets
default: $(SESSION-NAME)
test: $(SESSION-NAME)
# usually empty:
images:
all: images test
## global settings
SRC = $(ISABELLE_HOME)/src
OUT = $(ISABELLE_OUTPUT)
LOG = $(OUT)/log
# base image built by AFP, always in $(OUT)
IMAGE=$(OUT)/$(BASE-IMAGE)
USEDIR = $(ISABELLE_TOOL) usedir -v true -g true -i true -V outline=/proof,/ML -d pdf # -D generated
# time limit (in sec)
MAXTIME = 3600
## dependencies
$(SESSION-NAME): Simpl $(LOG)/$(BASE-IMAGE)-$(SESSION-NAME).gz
Simpl:
cd ../Simpl; $(ISABELLE_TOOL) make Simpl
$(LOG)/$(BASE-IMAGE)-$(SESSION-NAME).gz: $(IMAGE) ROOT.ML *.thy document/*.tex document/*.bib
cd ..; ulimit -t $(MAXTIME); $(USEDIR) $(IMAGE) $(SESSION-NAME)
## clean
clean:
@rm -f $(LOG)/$(BASE-IMAGE)-$(SESSION-NAME).gz
use_thys ["EvalProof", "NormalizeTotalProof"];
## configurables
SESSION-NAME = BinarySearchTree
BASE-IMAGE = HOL
## targets
default: $(SESSION-NAME)
test: $(SESSION-NAME)
# usually empty:
images:
all: images test
## global settings
SRC = $(ISABELLE_HOME)/src
OUT = $(ISABELLE_OUTPUT)
LOG = $(OUT)/log
# turn image into absolute path according to ISABELLE_IMAGE_PATH or OUT
ifeq ($(ISABELLE_IMAGE_PATH),)
IMAGE=$(OUT)/$(BASE-IMAGE)
else
IMAGE=$(ISABELLE_IMAGE_PATH)$(BASE-IMAGE)
endif
USEDIR = $(ISABELLE_TOOL) usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/" # -D generated
# time limit (in sec)
MAXTIME = 3600
## dependencies
$(SESSION-NAME): $(LOG)/$(BASE-IMAGE)-$(SESSION-NAME).gz
$(LOG)/$(BASE-IMAGE)-$(SESSION-NAME).gz: $(IMAGE) ROOT.ML *.thy document/*.tex
cd ..; ulimit -t $(MAXTIME); $(USEDIR) $(IMAGE) $(SESSION-NAME)
## clean
clean:
@rm -f $(LOG)/$(BASE-IMAGE)-$(SESSION-NAME).gz
use_thys ["BinaryTree", "BinaryTree_Map", "BinaryTree_TacticStyle"];
## configurables
SESSION-NAME = Binomial-Heaps
BASE-IMAGE = HOL
## targets
default: $(SESSION-NAME)
test: $(SESSION-NAME)
# usually empty:
images:
all: images test
## global settings
SRC = $(ISABELLE_HOME)/src
OUT = $(ISABELLE_OUTPUT)
LOG = $(OUT)/log
# turn image into absolute path according to ISABELLE_IMAGE_PATH or OUT
ifeq ($(ISABELLE_IMAGE_PATH),)
IMAGE=$(OUT)/$(BASE-IMAGE)
else
IMAGE=$(ISABELLE_IMAGE_PATH)$(BASE-IMAGE)
endif
USEDIR = $(ISABELLE_TOOL) usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/" # -D generated
# time limit (in sec)
MAXTIME = 300
## dependencies
$(SESSION-NAME): $(LOG)/$(BASE-IMAGE)-$(SESSION-NAME).gz
$(LOG)/$(BASE-IMAGE)-$(SESSION-NAME).gz: $(IMAGE) ROOT.ML *.thy document/*.tex document/*.bib
cd ..; ulimit -t $(MAXTIME); $(USEDIR) $(IMAGE) $(SESSION-NAME)
## clean
clean:
@rm -f $(LOG)/$(BASE-IMAGE)-$(SESSION-NAME).gz
no_document use_thys ["~~/src/HOL/Library/Multiset"];
use_thys ["BinomialHeap", "SkewBinomialHeap"];
(* Keep these in, they are to early detect problems with the code generator *)
no_document use_thys ["~~/src/HOL/Library/Efficient_Nat"];
no_document use_thys ["Test"];
## configurables
SESSION-NAME = Binomial-Queues
BASE-IMAGE = HOL
## targets
default: $(SESSION-NAME)
test: $(SESSION-NAME)
# usually empty:
images:
all: images test
## global settings
SRC = $(ISABELLE_HOME)/src
OUT = $(ISABELLE_OUTPUT)
LOG = $(OUT)/log
# turn image into absolute path according to ISABELLE_IMAGE_PATH or OUT
ifeq ($(ISABELLE_IMAGE_PATH),)
IMAGE=$(OUT)/$(BASE-IMAGE)
else
IMAGE=$(ISABELLE_IMAGE_PATH)$(BASE-IMAGE)
endif
USEDIR = $(ISABELLE_TOOL) usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/" # -D generated
# time limit (in sec)
MAXTIME = 300
## dependencies
$(SESSION-NAME): $(LOG)/$(BASE-IMAGE)-$(SESSION-NAME).gz
$(LOG)/$(BASE-IMAGE)-$(SESSION-NAME).gz: $(IMAGE) ROOT.ML *.thy document/*.tex
cd ..; ulimit -t $(MAXTIME); $(USEDIR) $(IMAGE) $(SESSION-NAME)
## clean
clean:
@rm -f $(LOG)/$(BASE-IMAGE)-$(SESSION-NAME).gz
use_thy "PQ_Implementation";
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment