Skip to content

Commit 2fe9aea

Browse files
updated the holmake file and commented out the old translation
1 parent 148c5f1 commit 2fe9aea

File tree

3 files changed

+18
-7
lines changed

3 files changed

+18
-7
lines changed

hol/policy_to_table/bdd_cake_trans/Holmakefile

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,12 @@ all: $(TARGETS) $(if $(NEWHOLHEAP),$(NEWHOLHEAP),)
4646

4747
INCLUDES = $(DEPENDENCIES) $(if $(HOLHEAP),$(shell dirname $(HOLHEAP)),)
4848

49-
EXTRA_CLEANS = $(if $(NEWHOLHEAP),$(NEWHOLHEAP) $(NEWHOLHEAP).o,) $(wildcard *.exe)
49+
EXTRA_CLEANS = $(if $(NEWHOLHEAP),$(NEWHOLHEAP) $(NEWHOLHEAP).o,) \
50+
$(wildcard *.exe) \
51+
$(wildcard *.sexp) \
52+
$(wildcard *.S) \
53+
$(wildcard *.o) \
54+
$(wildcard *~)
5055

5156
OPTIONS = QUIT_ON_FAILURE
5257

hol/policy_to_table/bdd_cake_trans/bdd_trans_ProgScript.sml

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,11 +5,11 @@ open preamble basis ml_translatorLib ;
55
open miscTheory ml_translatorTheory ListProgTheory ;
66
open fromSexpTheory;
77

8-
(*
8+
99

1010
val _ = new_theory "bdd_trans_Prog";
11-
*)
1211

12+
(*
1313
1414
val _ = translation_extends "basisProg"
1515
val _ = intLib.deprecate_int();
@@ -805,3 +805,8 @@ val prog =
805805
806806
807807
val _ = astToSexprLib.write_ast_to_file "test_bdd.sexp" prog;
808+
*)
809+
810+
811+
812+
val _ = export_theory ();

hol/policy_to_table/bdd_cake_trans/bdd_trans_new_ProgScript.sml

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -7,11 +7,11 @@ open fromSexpTheory;
77

88

99

10-
(*
10+
1111
val _ = new_theory "bdd_trans_new_Prog";
12-
*)
1312

14-
13+
14+
(*
1515
val _ = translation_extends "basisProg"
1616
1717
val _ = intLib.deprecate_int();
@@ -608,10 +608,11 @@ val _ = astToSexprLib.write_ast_to_file "test_bdd.sexp" prog;
608608
609609
610610
611+
*)
611612

612613

614+
val _ = export_theory ();
613615

614-
stringSyntax.fromMLstring
615616

616617

617618

0 commit comments

Comments
 (0)