diff options
Diffstat (limited to 'language/Makefile')
| -rw-r--r-- | language/Makefile | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/language/Makefile b/language/Makefile index 4ac35b65..4747dc49 100644 --- a/language/Makefile +++ b/language/Makefile @@ -11,9 +11,9 @@ l2_parse.pdf: l2_parse.tex l2Theory.uo: l2Script.sml Holmake --qof -I $(OTTLIB) l2Theory.uo -l2.tex ../src/ast.ml ../src/ast.lem l2Script.sml: l2.ott - ott -sort false -generate_aux_rules false -o l2.tex -picky_multiple_parses true l2.ott - ott -sort false -generate_aux_rules false -o ../src/ast.lem -o l2Script.sml -picky_multiple_parses true l2.ott +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. |