From fc4cfc59b6645f52cdca4aed534276161c82e3ca Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 2 Feb 2013 00:44:07 +0000 Subject: [PATCH] Makefile to extract to ocaml code. --- matita/matita/lib/Makefile | 24 ++++++++++++++++++++---- 1 file changed, 20 insertions(+), 4 deletions(-) diff --git a/matita/matita/lib/Makefile b/matita/matita/lib/Makefile index b7d95a5fc..8c12efbd1 100644 --- a/matita/matita/lib/Makefile +++ b/matita/matita/lib/Makefile @@ -1,9 +1,25 @@ +#TARGET= extraction2.ma +#TARGET= extraction3.ma +#TARGET= basics/logic.ma +#TARGET= basics/types.ma +#TARGET= basics/deqsets.ma +#TARGET= basics/lists/list.ma +#TARGET= arithmetics/nat.ma +TARGET= turing/multi_universal/universal.ma + all: - touch extraction.ma - EXTRACT_HASKELL=1 ../matitac extraction.ma 2> /tmp/foo.hs - cat preamble.hs /tmp/foo.hs > extraction.hs + touch $(TARGET) + #EXTRACT_HASKELL=1 ../matitac $(TARGET) 2> /tmp/foo.hs + #cat preamble.hs /tmp/foo.hs > extraction.hs + EXTRACT_OCAML=1 ../matitac $(TARGET) + +opt: + touch $(TARGET) + #EXTRACT_HASKELL=1 ../matitac.opt $(TARGET) 2> /tmp/foo.hs + #cat preamble.hs /tmp/foo.hs > extraction.hs + EXTRACT_OCAML=1 ../matitac.opt $(TARGET) -.PHONY: all +.PHONY: all opt # ghci extraction.hs # Syntax for datatypes: data Foo = Zero | Succ Foo Foo -- 2.39.2