From 65583684a163786d5bf56a3e14c9d41b089d25bd Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Tue, 2 Aug 2016 13:44:10 +0100 Subject: [PATCH] Makefile for generating theory files. --- examples/Makefile | 40 ++-------------------------------------- 1 file changed, 2 insertions(+), 38 deletions(-) diff --git a/examples/Makefile b/examples/Makefile index 7713f8f..ad82240 100644 --- a/examples/Makefile +++ b/examples/Makefile @@ -29,46 +29,10 @@ # OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE # OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -default: ofmc-anb -images: -test: ofmc-anb - -all: images test - -## global settings - -SRC = $(ISABELLE_HOME)/src -OUT = $(ISABELLE_OUTPUT) -LOG = $(OUT)/log -HEAP = ofmc-anb - -MV = mv -CP = cp - -USEDIR = $(ISATOOL) usedir -b -g true -v true -i true -d pdf ## -D generated -USEDIR = $(ISATOOL) usedir -b - -HOSTNAME = $(shell,$(ISATOOL) getenv HOSTNAME) -export HOSTNAME - -## ofmc-isabelle - -$(HEAP): $(LOG)/HOL-$(HEAP).gz - -$(LOG)/HOL-$(HEAP).gz: ROOT.ML document/root.tex *.thy - @$(RM) -rf $(ISABELLE_BROWSER_INFO)/HOL/$(HEAP)/document - @$(USEDIR) ofmc $(HEAP) - @$(CP) $(ISABELLE_BROWSER_INFO)/HOL/ofmc/$(HEAP)/document.pdf $(HEAP).pdf - thygen: - for i in AnB/*.AnB; do echo -e $$i; anb2thy $$i > `basename $$i .AnB`.thy; done + for i in AnB/*.AnB; do echo -e $$i; ../bin/anb2thy $$i > `basename $$i .AnB`.thy; done thygen-noproof: - for i in AnB/*.AnB; do echo -e $$i; anb2thy --noproof $$i > `basename $$i .AnB`.thy; done + for i in AnB/*.AnB; do echo -e $$i; ../bin/anb2thy --noproof $$i > `basename $$i .AnB`.thy; done fpgen: for i in AnB/*.AnB; do echo -e $$i; ofmc $$i -ot Isa > AnB/`basename $$i .AnB`.fp; done - -## clean - -clean: - @$(RM) -f $(LOG)/HOL-$(HEAP).gz