diff options
Diffstat (limited to 'language/Makefile')
| -rw-r--r-- | language/Makefile | 46 |
1 files changed, 22 insertions, 24 deletions
diff --git a/language/Makefile b/language/Makefile index 4747dc49..d650f957 100644 --- a/language/Makefile +++ b/language/Makefile @@ -1,36 +1,34 @@ OTTLIB=$(dir $(shell which ott))../hol -all: l2.pdf l2_parse.pdf parse_ast.ml +.PHONY: all +all: l2.pdf l2_parse.pdf l2.ml l2_parse.ml l2.lem -l2.pdf: l2.tex - pdflatex l2.tex +%.pdf: %.tex + pdflatex $< -l2_parse.pdf: l2_parse.tex - pdflatex l2_parse.tex +%Theory.uo: %Script.sml + Holmake --qof -I $(OTTLIB) $@ -l2Theory.uo: l2Script.sml - Holmake --qof -I $(OTTLIB) l2Theory.uo +l2.tex: l2.ott l2_rules.ott + ott -sort false -generate_aux_rules false -o $@ -picky_multiple_parses true $^ -l2.tex ../src/ast.ml ../src/ast.lem l2Script.sml: l2.ott l2_rules.ott - ott -sort false -generate_aux_rules false -o l2.tex -picky_multiple_parses true l2.ott l2_rules.ott - ott -sort false -generate_aux_rules false -o ../src/lem_interp/ast.lem -o l2Script.sml -picky_multiple_parses true l2.ott - ott -sort false -generate_aux_rules true -o ../src/ast.ml -picky_multiple_parses true l2.ott -# the above is working around what is probably a bug in -generate_aux_rules true: when we try to generate Lem code with that turned on, we get some surprising-looking parse failures in a few rules. Likely we're not doing the proper transform for rules generated from inductive relation syntax. +%.tex: %.ott + ott -sort false -generate_aux_rules false -o $@ -picky_multiple_parses true $^ -l2_parse.tex parse_ast.ml ../src/parse_ast.ml: l2_parse.ott - ott -sort false -generate_aux_rules false -o l2_parse.tex -picky_multiple_parses true l2_parse.ott - ott -sort false -generate_aux_rules true -o ../src/parse_ast.ml -picky_multiple_parses true l2_parse.ott - +%.ml: %.ott + ott -sort false -generate_aux_rules true -o $@ -picky_multiple_parses true $^ -# rm -f ../src/ast.ml -# chmod a-w ../src/ast.ml - -l2.lem: l2.ott - ott -o l2.lem -picky_multiple_parses true l2.ott +%Script.sml: %.ott + ott -sort false -generate_aux_rules true -o $@ -picky_multiple_parses true $^ +%.lem: %.ott + # work around what is probably a bug in -generate_aux_rules true: when we try to generate Lem code with + # that turned on, we get some surprising-looking parse failures in a + # few rules. Likely we're not doing the proper transform for rules + # generated from inductive relation syntax. + ott -sort false -generate_aux_rules false -o $@ -picky_multiple_parses true $^ clean: rm -rf *~ - -rm -rf *.uo *.ui l2Theory.sig l2Theory.sml l2.tex l2Script.sml l2.aux l2.log l2.dvi l2.ps l2_unwrapped.tex .HOLMK l2.ml -#l2.sys l2 library/lib_cache - + -rm -rf *.uo *.ui *.sig *.sml .HOLMK + -rm -f *.tex *.aux *.log *.dvi *.ps *.pdf |